Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Every actual row and every value branch is structurally checked

Abstract

Complete structural premises of the actual EJM local bound DAGs.

The structural checks use the original partial-row interpreters and actual local actions. Every complete row must equal its stated completed event. Every split must cover every outcome value, point to an earlier row, inherit a valid lower bound and match the entire transported child assignment. These checks supply structural premises only. Exact centered-score inequalities at complete rows are earned separately before the generic complete/split assembly produces full checkRow acceptance.

Theorem 1.1 (All 41294 actual triangle rows pass the structural check).

Lean statement: D5/S3/Quantum/Entanglement/EJM/EJMStructureCertificates.triangle_structure

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/EJM/EJMStructureCertificates.triangle_structure (✓ std3). ∎

Source. Repository-derived.

Commentary.

Private kernel computations cover the entire triangle row domain, and the exported theorem dispatches to the corresponding checked chunk for every index. EJMLocalBoundAcceptance consumes this complete structural premise together with the independently earned terminal inequalities.

Theorem 1.2 (All 8689 actual singleton rows pass the structural check).

Lean statement: D5/S3/Quantum/Entanglement/EJM/EJMStructureCertificates.singleton_structure

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/EJM/EJMStructureCertificates.singleton_structure (✓ std3). ∎

Source. Repository-derived.

Commentary.

The same whole-domain structural check covers every singleton row. Complete-row score inequalities are supplied by the exact terminal and contraction receipts. Full local acceptance then supplies the actual-context cache lower bound.

References