Proof step e-23f2fa3b69d7e23d

basis_map_theorem → concludes about Triangle of coefficients of Gaussian polynomials [2n+1,1]_q represented as finite sum of terms (1+q^2)^k*q^(g-k), where k = 0,1,...,g with g=n. 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": "[-2, 2]", "statement": "every real polynomial with all roots in E = [-1, 1] has an image with all roots in I = [-2, 2]" }

Verification and certificate

• polytool: replayed (the certificate replayed when the step was written)
• Lean: not attempted
• certificate: basis_map_theorem, SHA-256 fedb9ea9643994cde62b5b3d0a14e6fd4b28a1fe1d298be074f0823e04705381, 4,332 bytes (1,310 compressed); download JSON

Cited by

• n-0b318b4ec2091cb2 (basis_map_preserver)