Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

FiveRowP1Algebra

Abstract

Polynomial coordinates for the five-row scalar inequalities.

Definition 1.1 (Scalar necessary inequalities).

Lean statement: D5/S3/Quantum/Entanglement/AbsolutePPT/FiveRowP1Algebra.Hyp

Formalization. D5/S3/Quantum/Entanglement/AbsolutePPT/FiveRowP1Algebra.Hyp (✓ std3).

Source. Repository-derived.

Commentary.

Fifteen rational coefficients encode the quadratic expressions in r, H, D and q. The scalar hypotheses include all budget, cap and tail inequalities. Exact evaluation identities connect the endpoint and vertex polynomials to the energy gap for every real j.

Theorem 1.2 (Necessary polynomial projection).

Lean statement: D5/S3/Quantum/Entanglement/AbsolutePPT/FiveRowP1Algebra.necessary_sound

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

Source. Repository-derived.

Commentary.

Fifteen rational coefficients encode the quadratic expressions in r, H, D and q. The scalar hypotheses include all budget, cap and tail inequalities. Exact evaluation identities connect the endpoint and vertex polynomials to the energy gap for every real j.

Theorem 1.3 (Eight necessary upper envelopes).

Lean statement: D5/S3/Quantum/Entanglement/AbsolutePPT/FiveRowP1Algebra.fixed_sound

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

Source. Repository-derived.

Commentary.

Fifteen rational coefficients encode the quadratic expressions in r, H, D and q. The scalar hypotheses include all budget, cap and tail inequalities. Exact evaluation identities connect the endpoint and vertex polynomials to the energy gap for every real j.

Theorem 1.4 (Continuous left endpoint reduction).

Lean statement: D5/S3/Quantum/Entanglement/AbsolutePPT/FiveRowP1Algebra.target_left

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

Source. Repository-derived.

Commentary.

Fifteen rational coefficients encode the quadratic expressions in r, H, D and q. The scalar hypotheses include all budget, cap and tail inequalities. Exact evaluation identities connect the endpoint and vertex polynomials to the energy gap for every real j.

Theorem 1.5 (Continuous right endpoint reduction).

Lean statement: D5/S3/Quantum/Entanglement/AbsolutePPT/FiveRowP1Algebra.target_right

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

Source. Repository-derived.

Commentary.

Fifteen rational coefficients encode the quadratic expressions in r, H, D and q. The scalar hypotheses include all budget, cap and tail inequalities. Exact evaluation identities connect the endpoint and vertex polynomials to the energy gap for every real j.

Theorem 1.6 (Square completion reduction).

Lean statement: D5/S3/Quantum/Entanglement/AbsolutePPT/FiveRowP1Algebra.vertex_value

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

Source. Repository-derived.

Commentary.

Fifteen rational coefficients encode the quadratic expressions in r, H, D and q. The scalar hypotheses include all budget, cap and tail inequalities. Exact evaluation identities connect the endpoint and vertex polynomials to the energy gap for every real j.

References