Proof step e-b3a5a732652de064

basis_map_theorem → concludes about Triangle of coefficients of Chebyshev's S(n,x-2) = U(n,x/2-1) polynomials (exponents of x in increasing order). JSON

Theorem

Affine-current basis map theorem polytool RealRooted orderTwoConstants_nonneg_iff ?

Operation

Basis map theorem for the node's own rule

{
  "operation": "basis_map_theorem"
}

Premises

None: this step is a direct theorem check.

Claims

• { "claim": "basis_map_preserver", "input_interval": "[-1, 1]", "output_interval": "(-inf, +inf)", "statement": "every real polynomial with all roots in E = [-1, 1] has a real-rooted image" }
• { "claim": "basis_map_preserver", "input_interval": "[-1, 1]", "output_interval": "[0, 4]", "statement": "every real polynomial with all roots in E = [-1, 1] has an image with all roots in I = [0, 4]" }

Verification and certificate

• polytool: replayed (the certificate replayed when the step was written)
• Lean: not attempted
• certificate: basis_map_theorem, SHA-256 2955c263c849c1d530da5654f45217eb2111e20d9e8e7e575584ec4076b8543c, 4,296 bytes (1,290 compressed); download JSON

Cited by

• n-f7e7f08472ec987a (basis_map_preserver)