Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Actual proper-limit advancement

Abstract

Actual proper-limit advancement of one strict past

Definition 1.1 (Canonical strict-past archive).

Lean statement: D5/S3/Topology/InverseLimit/SignedOrdinalHistoryLimit.archive

Formalization. D5/S3/Topology/InverseLimit/SignedOrdinalHistoryLimit.archive (✓ std3).

Source. Repository-derived.

Commentary.

For a proper limit a above omega and one pairwise coherent strict past, Archive reads the full canonical Q at each born row and the actual selected R at max(row,label). The successor arrival of every such R lies strictly before a. Its Data are exactly the already proved strict Data, including the original incoming I/J. The base onto invariant comes from the actual earlier stage omega. There is no supplied complete history or promised future extension.

Definition 1.2 (Retain the same actual limit event).

Lean statement: D5/S3/Topology/InverseLimit/SignedOrdinalHistoryLimit.limitState

Formalization. D5/S3/Topology/InverseLimit/SignedOrdinalHistoryLimit.limitState (✓ std3).

Source. Repository-derived.

Commentary.

The approved proper-limit constructor is called on that strict Archive and its proven Laws. The resulting State retains its actual Extension, exact I/J and carrier readbacks, original births, regular bounded F and DI/DJ. Whole U/B/V/nu are carried together through literal carrier equality. One outgoing Q is then prepared once and one actual ordinary or delayed Result is selected on that same Q.

Theorem 1.3 (Coherence with every actual earlier state).

Lean statement: D5/S3/Topology/InverseLimit/SignedOrdinalHistoryLimit.limit_coherent

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

Source. Repository-derived.

Commentary.

The constructed limit State extends every state of its own strict past: exact carriers and canonical whole births agree, permanent N equals the unique earlier R arrival, and incoming I/J almost refine every eligible old set. Regular bounded F is obtained from that same Extension.F before the weaker predecessor interface can discard its output regularity and bound.

References