Proof step e-d9546d61239ca2e3

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

Cited by

• n-6466a8550c08a52f (basis_map_preserver)