Successor extension of one actual past
Abstract
Successor extension of one actual past
Theorem 1.1 (Exact adjacent coherence).
Lean statement: D5/S3/Topology/InverseLimit/SignedOrdinalHistorySuccessor.next_coherent
Proof. Machine-checked in Lean as D5/S3/Topology/InverseLimit/SignedOrdinalHistorySuccessor.next_coherent (✓ std3). ∎
Source. Repository-derived.
Commentary.
The actual selected Result is the next literal Prefix and its nextP is the next predecessor. The next clopen table is read from the same current whole birth pack. All older U, V and nu fields agree by literal carrier transport. The permanent arrival uses the same Result.N at its outgoing maximum stage. Its oldI and oldJ give the required refinement.
Theorem 1.2 (Preservation of every earlier state).
Lean statement: D5/S3/Topology/InverseLimit/SignedOrdinalHistorySuccessor.next_coherent_earlier
Proof. Machine-checked in Lean as D5/S3/Topology/InverseLimit/SignedOrdinalHistorySuccessor.next_coherent_earlier (✓ std3). ∎
Source. Repository-derived.
Commentary.
If the current state is coherent with an earlier state, advancing its actual selected Result preserves that coherence. Whole birth equality composes through the current old pack; older arrival entries are retained exactly. The one-sided almost inclusions of I and J compose. No replacement history or extension witness is supplied as a premise.