Proof step e-e1219184df277b70

basis_map_theorem → concludes about Triangle read by rows: T(k,s) = ((2*k+1)/(2*s+1))*binomial(k+s,2*s), 0 <= s <= k. 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": "[-4, 0]", "statement": "every real polynomial with all roots in E = [-1, 1] has an image with all roots in I = [-4, 0]" }
• { "claim": "basis_map_preserver", "input_interval": "[-1, 0]", "output_interval": "[-4, 0]", "statement": "every PF input with all roots in [-1, 0] has a PF image; no larger [-R, 0] works" }

Verification and certificate

• polytool: replayed (the certificate replayed when the step was written)
• Lean: not attempted
• certificate: basis_map_theorem, SHA-256 91e23b4cbd7484cd6f152a3894585413479ec89e7f2cf0bf3066d08ab705efea, 5,271 bytes (1,359 compressed); download JSON

Cited by

• n-318700a428d7b97b (basis_map_preserver)