Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Terminal inequalities require the earned original contractions

Abstract

Faithful transport from checked terminal witnesses to original centered-score inequalities.

The theorems keep the complete original contraction receipts and actual terminal checks as explicit premises. They read exact coordinate and outcome transport from each successful terminal check, then use the previously earned original-function contraction invariance to replace its stored contraction integer by the actual contraction at that terminal event. The whole-row consumers additionally use the checked complete-event tags. EJMLocalBoundAcceptance supplies every premise from the full actual numerical receipts in the same final certificate delivery.

Theorem 1.1 (One checked triangle terminal bounds its original centered score).

Lean statement: D5/S3/Quantum/Entanglement/EJM/EJMTerminalBoundSoundness.triangle_terminal_sound

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

Source. Repository-derived.

Commentary.

Assuming every original triangle contraction receipt, acceptance of the selected terminal’s actual transport and integer comparison bounds triangleCentered F1 at its literal complete event. The conclusion is conditional on those exact numerical premises.

Theorem 1.2 (One checked singleton terminal bounds its original centered score).

Lean statement: D5/S3/Quantum/Entanglement/EJM/EJMTerminalBoundSoundness.singleton_terminal_sound

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

Source. Repository-derived.

Commentary.

The analogous conditional transport applies to singletonCentered F2 and retains its separate factor 64. The stored singleton contraction is substituted only using the earned actual contraction equation.

Theorem 1.3 (Every actual complete triangle row has its required score bound).

Lean statement: D5/S3/Quantum/Entanglement/EJM/EJMTerminalBoundSoundness.triangle_all_terminal_bounds

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

Source. Repository-derived.

Commentary.

Acceptance of all actual terminal checks and all row tags, together with every exact contraction receipt, yields the score inequality for any triangle row whose original rule is complete. The checked tag equality identifies the row’s original event with the literal terminal event used in the proof.

Theorem 1.4 (Every actual complete singleton row has its required score bound).

Lean statement: D5/S3/Quantum/Entanglement/EJM/EJMTerminalBoundSoundness.singleton_all_terminal_bounds

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

Source. Repository-derived.

Commentary.

The entire singleton complete-row domain obtains its original centered-score bound under the same three discharged-in-the-consumer premise families. This is the exact terminal premise required by the generic full-row acceptance theorem.

References