Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Complete singleton mirror and transition kernel receipts

Abstract

Complete singleton mirror and transition kernel receipts

The finite proof blocks form 6 imported interval groups. The complete mirror and transition receipts consume every group by exhaustive interval dispatch.

The interval-dispatched receipts cover every one of the 8689 rows. The transition guard restricts verification to the original unknown coordinates and preserves all 66132 actual value transitions. The cache association theorem applies these receipts only after proving that the actual coordinate is unknown. No external generator check, producer premise, partial sample or native evaluator is an acceptance theorem.

Theorem 1.1 (Every original row has an exact mirror).

Lean statement: D5/S3/Quantum/Entanglement/EJM/EJMSingletonCacheReceipts.mirror_accepted

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

Source. Repository-derived.

Commentary.

All finite chunks of the mirror check are consumed by exhaustive index dispatch. The receipt supplies the whole assignment equality and exact lower equality.

Theorem 1.2 (Every actual unknown-coordinate/value transition is exact).

Lean statement: D5/S3/Quantum/Entanglement/EJM/EJMSingletonCacheReceipts.transitions_accepted

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

Source. Repository-derived.

Commentary.

Exhaustive row dispatch supplies each complete transition checker result. All four values and every unknown coordinate remain quantified in the checked proposition.

Theorem 1.3 (Mirror assignments are the original assignments).

Lean statement: D5/S3/Quantum/Entanglement/EJM/EJMSingletonCacheReceipts.assignment_eq

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

Source. Repository-derived.

Commentary.

This extracts the assignment component of the full mirror receipt at an arbitrary actual row index.

Theorem 1.4 (Literal lower fields equal original scaled bounds).

Lean statement: D5/S3/Quantum/Entanglement/EJM/EJMSingletonCacheReceipts.lower_eq

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

Source. Repository-derived.

Commentary.

This extracts exact integer equality from the mirror receipt, permitting later leaf arithmetic to reuse small literals without changing the bound.

Theorem 1.5 (Earn the generic cache transition on original rows).

Lean statement: D5/S3/Quantum/Entanglement/EJM/EJMSingletonCacheReceipts.transition_accepted

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

Source. Repository-derived.

Commentary.

The actual unknown-coordinate hypothesis and full mirrored transition receipt are rewritten through both assignment equalities. The result is the generic checkTransition theorem for the original row function.

References