Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

One actual successor event

Abstract

One actual successor event

Definition 1.1 (Once-prepared local execution).

Lean statement: D5/S3/Topology/InverseLimit/SignedOrdinalHistoryEvent.execute

Formalization. D5/S3/Topology/InverseLimit/SignedOrdinalHistoryEvent.execute (✓ std3).

Source. Repository-derived.

Commentary.

Under CH the actual exists_prepared_step chooses one Prepared Q. The original reservation sum is read before target projection. A locally valid delayed reservation selects a DelayedTask on that same Q and retains its Result and certificate; all other reservations select an ordinary Result. The event stores exactly the selected Q and Result, together with branch and execution equations. Local delayed tests read only already born rows and labels and the clopen enumeration of their original whole birth.

Theorem 1.2 (Incoming regular bounded convergence).

Lean statement: D5/S3/Topology/InverseLimit/SignedOrdinalHistoryEvent.next_regular

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

Source. Repository-derived.

Commentary.

The same selected Result supplies the next predecessor and its regular bounded every-choice F. Literal carrier equality transports the original signed pushforwards and weak-dual convergence. The output retains both Jordan regularity proofs and total variation at most one; this information is not inferred from the weaker Predecessor.F.

References