Proof step e-216cbdf61e3ed56f

basis_map_theorem → concludes about Pascal-(1,7,1) array. 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": "[-7 - sqrt(56), -7 + sqrt(56)]", "output_interval": "(-inf, +inf)", "statement": "every real polynomial with all roots in E = [-7 - sqrt(56), -7 + sqrt(56)] has a real-rooted image" }
• { "claim": "basis_map_preserver", "input_interval": "[-7 - sqrt(56), -7 + sqrt(56)]", "output_interval": "[-15 - 2 sqrt(56), -15 + 2 sqrt(56)]", "statement": "every real polynomial with all roots in E = [-7 - sqrt(56), -7 + sqrt(56)] has an image with all roots in I = [-15 - 2 sqrt(56), -15 + 2 sqrt(56)]" }
• { "claim": "basis_map_preserver", "input_interval": "[-7 - sqrt(56), 0]", "output_interval": "[-15 - 2 sqrt(56), -15 + 2 sqrt(56)]", "statement": "every PF input with all roots in [-7 - sqrt(56), 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 0a6de4c4cd055cfc120b210d9cec81478518f044990b50b6d719f4e0ea460845, 5,817 bytes (1,464 compressed); download JSON

Cited by

• n-1e2f1b7f566b371c (basis_map_preserver)