Exact P1 forest N55B
Abstract
Exact numerical premises for the original full continuous P1 scalar reduction.
Definition 1.1 (Ordered literal forest nodes).
Lean statement: D5/S3/Quantum/Entanglement/AbsolutePPT/P1Data/N55B.nodes
Formalization. D5/S3/Quantum/Entanglement/AbsolutePPT/P1Data/N55B.nodes (✓ std3).
Source. Repository-derived.
Commentary.
The ordered records retain every box endpoint, rule, child index and rational coefficient. These data assert no successful check.
Theorem 1.2 (Exact forest premise accepted).
Lean statement: D5/S3/Quantum/Entanglement/AbsolutePPT/P1Data/N55B.accepted
Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/AbsolutePPT/P1Data/N55B.accepted (✓ std3). ∎
Source. Repository-derived.
Commentary.
The exact rational or structural premise is used in the complete forest check, which supplies the continuous real scalar inequality.