FiveRowP1Analytic
Abstract
The analytic equality neighborhood of the scalar system.
Theorem 1.1 (Full analytic equality neighbourhood).
Lean statement: D5/S3/Quantum/Entanglement/AbsolutePPT/FiveRowP1Analytic.analytic_region
Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/AbsolutePPT/FiveRowP1Analytic.analytic_region (✓ std3). ∎
Source. Repository-derived.
Commentary.
For 25 <= N <= 90, every real 10 <= j <= N-15, r <= 1/10 and D <= 1/4, the scalar hypotheses imply a nonnegative energy gap. Splitting at H=2-r-D/5 combines concavity below that value with the cap and increasing gap above it, including the equality boundary r=D=0.