Actual states and strict-past coherence
Abstract
Actual states and strict-past coherence
Definition 1.1 (Incoming stage and outgoing birth).
Lean statement: D5/S3/Topology/InverseLimit/SignedOrdinalHistoryState.State
Formalization. D5/S3/Topology/InverseLimit/SignedOrdinalHistoryState.State (✓ std3).
Source. Repository-derived.
Commentary.
A proper stage state contains its literal Prefix, actual Predecessor, incoming initial, successor or limit evidence, regular bounded F, and one selected outgoing event. A limit incoming record retains the entire actual Extension, not merely its resulting predecessor. Coherence compares exact earlier carriers, whole birth packs, permanent max(row,label) arrivals and eligible almost inclusions of I and J. The initial finite and omega carriers remain the full coordinate cubes. This state type by itself asserts no global existence.