Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Ordinal successor and arrival births

Abstract

Ordinary ordinal successor with actual legal births and permanent arrival readback

The predecessor consists of one literal Prefix through stage a, where omega is at most a and a is below omega-one. Its actual current carrier maps onto Cube(omega). All old rows have exhaustive support and legal regular signed enumerations; old I and J have their strict born domains. Old N is read from the entry at the unique stage succ(max(row,label)). Only these partial predecessor laws are assumed. No complete history or extension supplier is an input.

Theorem 1.1 (Executed ordinary successor).

Lean statement: D5/S3/Topology/InverseLimit/SignedOrdinalSuccessor.exists_successor

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

Source. Repository-derived.

Commentary.

Under CH, the construction first enumerates all current support families and clopens. Launch(row,supportIndex) then pulls back the chosen support family, using the newly chosen current enumeration when launch.row equals a. A genuine exhaustive enumeration of all legal signed measures on this launched row is chosen before Treatment(row,label). Launch indices and signed sequence labels are separate typed fields. Actual proper ordinal countability constructs an injective row code with code(a)=0 and an auxiliary old-label schedule with infinite fibres at each parity.

The proof applies SignedSplitSuccessor.exists_measured_dynamic_split to the actual K(a), its literal coordinate functions, and literal onto restrictions. The new row projection is the identity. The same executed split supplies final I and J, inherited N on old rows and labels, auxiliary parity reservoirs on the new row for old labels, and final-I residual reservoirs on every row for label a. SignedSuccessorCoordinates.exists_successor_coordinates inserts this split in Cube(succ(a)) and extends the same Prefix without replacing old carriers. A through-a arrival pack is returned together with all-pair readback and exact preservation of every earlier birth entry.

The Result retains A, B, C, exact one-step refinement of old I and J, whole-support fibre E, and regular common every-choice signed F on its certified split presentation. It separately retains quantitative G with the same StrictMono column index. This local result does not construct the ordinal schedule, delayed execution with an exposed increasing target index, well-founded history, same-family proper limits, final omega-one carrier, anti-homeomorphism, Grothendieck property, or entire signed dual ball. The same executed coordinate equivalence also transports common F and whole-support E to the literal cube.

Theorem 1.2 (Permanent birth readback).

Lean statement: D5/S3/Topology/InverseLimit/SignedOrdinalSuccessor.birth_readback

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

Source. Repository-derived.

Commentary.

For every omega<=row<=a, label<=a and parity, readback from the enlarged partial birth history at succ(max(row,label)) equals the reservoir in the executed Result. If both indices are old, the predecessor’s permanent entry is read. If the row is a and the label is old, the executed new-row parity output is read. If the label is a, including the doubly new pair, the executed residual output is read. No value for an unborn row or label is inserted.

Theorem 1.3 (Old entries are unchanged).

Lean statement: D5/S3/Topology/InverseLimit/SignedOrdinalSuccessor.arrival_retains

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

Source. Repository-derived.

Commentary.

The entire entry for every outgoing stage b<a remains equal to the predecessor entry, on exactly its born domain max(row,label)=b. The newly available arrival at a+1 is supplied as additional data; it is never claimed to be already present in a strict prefix ending at a+1.

Theorem 1.4 (Common every-choice F on the literal cube).

Lean statement: D5/S3/Topology/InverseLimit/SignedOrdinalSuccessor.literal_f

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

Source. Repository-derived.

Commentary.

For each original row r and label d, one signed measure mu on the literal successor has total variation at most one and regular positive and negative Jordan parts. This mu is chosen before all sequences of signed norm-one lifts of the unchanged Q.measure(r,d,n). Every such sequence converges weak-star to mu along the original R.J(r,d).

Choose the common split reference from Result.F and push it forward once through Result.coordinates.equiv. The images of its mutually singular Jordan parts form the image signed measure’s Jordan decomposition; the homeomorphism preserves their regularity and total variation. Pull each arbitrary literal lift backward through the inverse of that same equivalence. Its projection and norm remain unchanged. Evaluating a continuous test after transport equals evaluating its composition with the homeomorphism before transport, so the original common convergence yields literal convergence. No measure label, subsequence or reference limit is reselected.

Theorem 1.5 (Whole-support E for every literal coordinate).

Lean statement: D5/S3/Topology/InverseLimit/SignedOrdinalSuccessor.literal_e

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

Source. Repository-derived.

Commentary.

For each row and each coordinate below succ(a), eventually along the original I(row), any two points above the same point of the original support clopen have equal coordinate values. Old coordinates use their clopen truth sets in Result.E and the exact insertion equation. Coordinate a uses the sheet equality from that same E and the exact inverse-sheet equation.

Theorem 1.6 (Quantitative G on the literal cube).

Lean statement: D5/S3/Topology/InverseLimit/SignedOrdinalSuccessor.quantitative_g

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

Source. Repository-derived.

Commentary.

Result.quantitative_transport transfers any predicate of the split-sheet signed value through this same coordinate equivalence, preserving the original whole measure and column index. It is consumed both here and by the strong delayed certificate. The literal successor clopen tests the newly inserted ordinal coordinate a. Pushforward along the inverse homeomorphism preserves total variation and the original projection equation. For every q and every signed norm-one lift of the original treated sequence at the same increasing column index, even q has clopen value strictly greater than one sixth and odd q has value zero. This quantitative certificate is separate from Prefix.Laws and from any nonconvergence assertion.

References