Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Same actual events on the literal realization

Abstract

SignedOrdinalRealizationEvents

Theorem 1.1 (Whole prepared measure readback).

Lean statement: D5/S3/Topology/InverseLimit/SignedOrdinalRealizationEvents.prepared_measure_read

Proof. Machine-checked in Lean as D5/S3/Topology/InverseLimit/SignedOrdinalRealizationEvents.prepared_measure_read (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every old prepared whole measure equals the original whole birth on the final literal carrier, with its label and every natural index preserved. Both delayed source and target measures use this same readback.

Theorem 1.2 (The actual selected projection).

Lean statement: D5/S3/Topology/InverseLimit/SignedOrdinalRealizationEvents.selected_projection

Proof. Machine-checked in Lean as D5/S3/Topology/InverseLimit/SignedOrdinalRealizationEvents.selected_projection (✓ std3). ∎

Source. Repository-derived.

Commentary.

The actual selected R literal projection, after final projection to succ(a), equals final projection to the original row transported only across literal carrier equality. The same split and coordinate restriction are used.

Theorem 1.3 (Same outgoing and incoming J).

Lean statement: D5/S3/Topology/InverseLimit/SignedOrdinalRealizationEvents.successor_J

Proof. Machine-checked in Lean as D5/S3/Topology/InverseLimit/SignedOrdinalRealizationEvents.successor_J (✓ std3). ∎

Source. Repository-derived.

Commentary.

At succ(a), original eligible J is exactly the same selected R.J at a. The outgoing R carrier belongs to succ(a), while its J becomes incoming at that stage.

Theorem 1.4 (Actual ordinary events on the final prefix).

Lean statement: D5/S3/Topology/InverseLimit/SignedOrdinalRealizationEvents.ordinary_cofinal

Proof. Machine-checked in Lean as D5/S3/Topology/InverseLimit/SignedOrdinalRealizationEvents.ordinary_cofinal (✓ std3). ∎

Source. Repository-derived.

Commentary.

Arbitrarily late ordinary execution retains the same Treatment and Result, its exact final carrier at succ(a), and every original whole-birth measure at each natural index. That Result retains its quantitative_g, quantitativeClopen and strictly increasing column indices. No oscillation premise is supplied.

Theorem 1.5 (Actual delayed events on the final prefix).

Lean statement: D5/S3/Topology/InverseLimit/SignedOrdinalRealizationEvents.delayed_cofinal

Proof. Machine-checked in Lean as D5/S3/Topology/InverseLimit/SignedOrdinalRealizationEvents.delayed_cofinal (✓ std3). ∎

Source. Repository-derived.

Commentary.

Intrinsic validity on the final original whole birth yields an actual later delayed event with the identical Task, Result and certificate. Both B supports read back to their original decoded birth pair. The permanent source reservoirs and source J at succ(a) are exactly those of the same R. Its certificate keeps the same M sets and literal clopen; no second split transport is introduced.

These are realization interfaces; final signed and AH endpoint proofs are separate.

References