Proof step e-28dfe6801aeae3ea

basis_map_theorem → concludes about Triangle T(n,k), 0 <= k <= n, read by rows, given by [0, 2, -1, 0, 0, 0, 0, 0, ...] DELTA [1, 0, 0, 0, 0, 0, 0, 0, ...] where DELTA is the operator defined in … 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 - sqrt(2), -1 + sqrt(2)]", "output_interval": "(-inf, +inf)", "statement": "every real polynomial with all roots in E = [-1 - sqrt(2), -1 + sqrt(2)] has a real-rooted image" }
• { "claim": "basis_map_preserver", "input_interval": "[-1 - sqrt(2), 0]", "output_interval": "(-inf, 0]", "statement": "every PF input with all roots in [-1 - sqrt(2), 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 a95a683a9aaefd41b6e3de4e8df4156456fd717819b3a639e2f9732033601af3, 4,532 bytes (1,429 compressed); download JSON

Cited by

• n-b0fc620949fb5990 (basis_map_preserver)