Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

FiveRowP1Checker

Abstract

Soundness of finite rational covers for the scalar inequalities.

Definition 1.1 (All local checks and complete postorder traversal).

Lean statement: D5/S3/Quantum/Entanglement/AbsolutePPT/FiveRowP1Checker.check

Formalization. D5/S3/Quantum/Entanglement/AbsolutePPT/FiveRowP1Checker.check (✓ std3).

Source. Repository-derived.

Commentary.

Each accepted forest retains both closed halves at every split. Infeasibility uses strict upper bounds, whereas target bounds are nonstrict. Endpoint derivative signs and the quadratic vertex cover the continuous real interval of j; the generic local-step cover theorem assembles the leaves.

Theorem 1.2 (Finite rational covers imply the scalar bound).

Lean statement: D5/S3/Quantum/Entanglement/AbsolutePPT/FiveRowP1Checker.checked_scalar_bound

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/AbsolutePPT/FiveRowP1Checker.checked_scalar_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

Each accepted forest retains both closed halves at every split. Infeasibility uses strict upper bounds, whereas target bounds are nonstrict. Endpoint derivative signs and the quadratic vertex cover the continuous real interval of j; the generic local-step cover theorem assembles the leaves.

References