Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Stored contraction proposals require the original-function equality receipts

Abstract

Candidate exact EJM tail representatives and stored contraction integers.

Private literal dictionaries store 95 triangle-tail representatives with proposed contraction integers and 332 singleton-tail representatives with their proposed integers. The public functions decode those same dictionaries. This data module contains no theorem asserting that a stored integer is an original coefficient contraction. EJMContractionCertificates must kernel-check the original weighted head sum at every actual representative. Earned contraction symmetries then permit the terminal-bound consumer to transport those equalities; neither external calculation nor a data definition discharges an equality premise.

Definition 1.1 (The actual 95 seven-coordinate triangle-tail proposals).

Lean statement: D5/S3/Quantum/Entanglement/EJM/EJMContractionData.triangleTail

Formalization. D5/S3/Quantum/Entanglement/EJM/EJMContractionData.triangleTail (✓ std3).

Source. Repository-derived.

Commentary.

Each index queries the literal tail-code dictionary and decodes seven base-five digits, reduced modulo four. These are the actual representative inputs to the original F1 head-sum checker.

Definition 1.2 (The actual proposed triangle contraction integer).

Lean statement: D5/S3/Quantum/Entanglement/EJM/EJMContractionData.triangleValue

Formalization. D5/S3/Quantum/Entanglement/EJM/EJMContractionData.triangleValue (✓ std3).

Source. Repository-derived.

Commentary.

The original integer dictionary lookup supplies the proposed value at each triangle representative. Its equality to the weighted sum of 64 original F1 head assignments is a separate kernel receipt.

Definition 1.3 (The actual 332 eight-coordinate singleton-tail proposals).

Lean statement: D5/S3/Quantum/Entanglement/EJM/EJMContractionData.singletonTail

Formalization. D5/S3/Quantum/Entanglement/EJM/EJMContractionData.singletonTail (✓ std3).

Source. Repository-derived.

Commentary.

The singleton tail dictionary is decoded into eight actual Fin 4 outcomes for the original F2 head-sum check.

Definition 1.4 (The actual proposed singleton contraction integer).

Lean statement: D5/S3/Quantum/Entanglement/EJM/EJMContractionData.singletonValue

Formalization. D5/S3/Quantum/Entanglement/EJM/EJMContractionData.singletonValue (✓ std3).

Source. Repository-derived.

Commentary.

The stored integer is a proposal for the sum of four original F2 head values. The additional factor 64 belongs to the separate centered score and is not part of this stored contraction function.

References