Whole canonical birth packs
Abstract
Whole canonical birth packs
Theorem 1.1 (All old whole labels are retained).
Lean statement: D5/S3/Topology/InverseLimit/SignedOrdinalHistoryBirth.prepared_old_readback
Proof. Machine-checked in Lean as D5/S3/Topology/InverseLimit/SignedOrdinalHistoryBirth.prepared_old_readback (✓ std3). ∎
Source. Repository-derived.
Commentary.
A BirthPack contains the support enumeration U, natural clopen enumeration B, chosen support family V and complete BornData enumeration nu on every Label. Preparation preserves every older whole pack through oldV and oldNu, including labels that are not yet eligible for J. B is read from the original birth. Literal carrier equality changes neither labels nor enumeration indices; permanent N arrivals are a separate object.