CompletedOrbitLedger
plain-language theorem explainer
A completed orbit ledger is an infinite sequence of finite δ-orbit positions, one per natural index. It is the natural-number half of K4.13 trace closure, dual to the completed act-trace. Anyone citing the trace-closure certificate or the canonical orbit verifier uses this type. The declaration is a one-field structure; the canonical instance is the standard embedding of Nat into distinction-orbit positions.
Claim. A completed orbit ledger is a map $n \mapsto p_n$ from natural numbers to finite distinction-orbit positions (the base-neutral finite orbit of repeated distinction). This infinite sequence of $\delta$-orbit positions is the natural-number side of trace closure (K4.13).
background
Module TraceClosure sits in the Primitive Recognition Calculus and packages the K4.13 boundary between finite recognition acts and their completed infinite records. A finite distinction-orbit position is the inductive type with constructors zero and succ: the base-neutral finite orbit of repeated distinction (K2.12). That type is the value space of the ledger.
The dual object is a completed trace: an infinite sequence of distinction acts. The canonical completed trace repeats the primitive distinction act $\delta$ at every index. The ledger records, instead, the orbit position reached after $n$ such distinctions. Together they form the two sides of trace closure: acts on one side, natural-number orbit positions on the other.
Local notation treats the ledger as a bare functional field positionAt, so later lemmas can state faithfulness (position $n$ recovers $n$) without committing to a particular encoding beyond the inductive orbit type.
proof idea
No proof: this is a structure definition. It declares a single field, a function from ordinary natural numbers to finite distinction-orbit positions. Inhabitation is supplied separately by the canonical instance, which sets that field to the standard ofNat embedding. Downstream one-liners such as the successor identity are then just rfl on that choice.
why it matters
K4.13 needs both an infinite act record and an infinite orbit-position record. This structure is the latter. It is required by the first trace-closure certificate, whose fields demand a nonempty completed orbit ledger and a faithfulness statement that the canonical ledger's position at $n$ has natural value $n$.
Downstream, the certificate theorem inhabits those fields with the canonical ledger and the corresponding toNat identity; a small successor lemma records that the canonical positions commute with succ. Without this type, the natural-number side of trace closure has nowhere to live, and the certificate cannot close.
In the broader PRC stack this is bookkeeping rather than a forcing step (not T5–T8), but it is the interface that lets later strength tags and verifier claims talk about completed orbits as ordinary Nat-indexed data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.