Original head sums at every stored tail representative
Abstract
Exact contraction premises for the actual EJM locality refutation.
The numerical receipts evaluate the original coefficient functions at every head assignment of each explicit tail representative. Finite chunks cover the entire representative domains; the public interval dispatch consumes every chunk. These values become useful through the earned contraction symmetries and terminal-bound soundness, then full local acceptance and the actual-context cache lower bound. External contraction calculations supply the proposed integers but supply no proof premise. The numerical receipts are consumed helpers in the same local cache soundness delivery.
Theorem 1.1 (All 95 exact triangle-tail contractions).
Lean statement: D5/S3/Quantum/Entanglement/EJM/EJMContractionCertificates.triangle_contractions
Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/EJM/EJMContractionCertificates.triangle_contractions (✓ std3). ∎
Source. Repository-derived.
Commentary.
For every one of the 95 literal seven-tail representatives, the sum of all 64 original F1 head values weighted by the actual integer EJM numerator equals its stored contraction value. This is the complete numerical premise used by triangle terminal-bound soundness.
Theorem 1.2 (All 332 exact singleton-tail contractions).
Lean statement: D5/S3/Quantum/Entanglement/EJM/EJMContractionCertificates.singleton_contractions
Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/EJM/EJMContractionCertificates.singleton_contractions (✓ std3). ∎
Source. Repository-derived.
Commentary.
For every one of the 332 literal eight-tail representatives, the sum of the four original F2 head values equals its stored contraction value. The factor 64 belongs to the separate singleton centered score and remains present in its terminal inequality.