Proof step e-3519459d402fdd95

basis_map_theorem → concludes about Triangular array: row n gives the coefficients of the polynomial p(n,x) defined in Comments. 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/2 - sqrt(3/4), -1/2 + sqrt(3/4)]", "output_interval": "(-inf, +inf)", "statement": "every real polynomial with all roots in E = [-1/2 - sqrt(3/4), -1/2 + sqrt(3/4)] has a real-rooted image" }
• { "claim": "basis_map_preserver", "input_interval": "[-1/2 - sqrt(3/4), -1/2 + sqrt(3/4)]", "output_interval": "[-1 - sqrt(3/4), -1 + sqrt(3/4)]", "statement": "every real polynomial with all roots in E = [-1/2 - sqrt(3/4), -1/2 + sqrt(3/4)] has an image with all roots in I = [-1 - sqrt(3/4), -1 + sqrt(3/4)]" }
• { "claim": "basis_map_preserver", "input_interval": "[-1/2 - sqrt(3/4), 0]", "output_interval": "[-1 - sqrt(3/4), -1 + sqrt(3/4)]", "statement": "every PF input with all roots in [-1/2 - sqrt(3/4), 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 01ebd1ac64ec452416fb7a8a6dd8fadef2ed66101a80c17a816ba7637a341a60, 5,958 bytes (1,457 compressed); download JSON

Cited by

• n-e7331b0d50084c15 (basis_map_preserver)