Exact P1 forest N80AShape
Abstract
Exact structural traversal and local numerical premises of the same full scalar reduction.
Theorem 1.1 (Exact forest premise checked_walk).
Lean statement: D5/S3/Quantum/Entanglement/AbsolutePPT/P1Data/Traversal/N80AShape.checked_walk
Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/AbsolutePPT/P1Data/Traversal/N80AShape.checked_walk (✓ 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.