FiveRowP1Caps
Abstract
Tail-derived upper caps for the five-row scalar system.
Definition 1.1 (Rational lower chord endpoint guards).
Lean statement: D5/S3/Quantum/Entanglement/AbsolutePPT/FiveRowP1Caps.chordOK
Formalization. D5/S3/Quantum/Entanglement/AbsolutePPT/FiveRowP1Caps.chordOK (✓ std3).
Source. Repository-derived.
Commentary.
The square-tail branch uses a rational chord whose endpoint values are nonnegative and whose squares lie below q. The linear-tail branch uses the upper endpoint of D. The cases H=0 and an upper D endpoint of zero are retained without dividing by zero.
Theorem 1.2 (Ninth cap from the original tail disjunction).
Lean statement: D5/S3/Quantum/Entanglement/AbsolutePPT/FiveRowP1Caps.cap_sound
Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/AbsolutePPT/FiveRowP1Caps.cap_sound (✓ std3). ∎
Source. Repository-derived.
Commentary.
The square-tail branch uses a rational chord whose endpoint values are nonnegative and whose squares lie below q. The linear-tail branch uses the upper endpoint of D. The cases H=0 and an upper D endpoint of zero are retained without dividing by zero.