Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Intrinsic delayed semantics of the original birth

Abstract

Intrinsic delayed semantics of the original birth

Theorem 1.1 (Intrinsic semantics under literal equality).

Lean statement: D5/S3/Topology/InverseLimit/SignedOrdinalHistoryTask.intrinsic_cast

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

Source. Repository-derived.

Commentary.

Intrinsic delayed validity is invariant under equality transport of the entire original birth pack. The final realization uses this equivalence to execute a delayed request on the same original Q.

Theorem 1.2 (Local tasks and original whole birth tests).

Lean statement: D5/S3/Topology/InverseLimit/SignedOrdinalHistoryTask.local_semantics

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

Source. Repository-derived.

Commentary.

The natural code uses the fixed mathlib equivalence from naturals to pairs of naturals, indexing the original birth clopen table B. Intrinsic validity means distinct whole measure labels, disjoint source and target clopens, original target Dirac points in V and the target clopen, and original source variation supported on the source clopen. On the old eligible row and label domain this is equivalent to the actual executable DelayedTask predicate on Q. No I, J, F, future carrier or final continuous map is part of intrinsic validity.

Theorem 1.3 (Stability from canonical whole birth coherence).

Lean statement: D5/S3/Topology/InverseLimit/SignedOrdinalHistoryTask.stable_local

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

Source. Repository-derived.

Commentary.

For two actual coherent proper states, an older row and eligible source and target labels, the local delayed predicate at the later Q is equivalent to Intrinsic on the earlier canonical whole birth. Preparation first reads the older predecessor pack, coherence identifies it with the original Q, and literal carrier equality transports that same pack. The global semantic condition is a consequence of these equalities, not an input to the local executor.

References