CompletedTrace
plain-language theorem explainer
A completed trace is an infinite sequence of primitive distinction acts, one at each natural-number step. It is the trace-closure object of K4.13/R9, not a finite δ-only ledger. Anyone building orbit ledgers, finite prefixes, or the trace-closure certificate cites it. As a structure definition it is just a single field: a map Nat → DistinctionAct.
Claim. A completed trace is a structure consisting of a map $\mathrm{actAt}\colon \mathbb{N}\to\{\delta\}$ that assigns a primitive distinction act to every natural-number index. Equivalently, it is an infinite ledger of distinction acts (the trace-closure object), as opposed to a finite $\delta$-only trace.
background
In the Primitive Recognition Calculus, the only object-level act is the primitive distinction $\delta$ (K2.1), packaged as the inductive type DistinctionAct with sole constructor delta. Finite traces are built inductively from the empty trace by successive extension; their length is the obvious Nat-valued recursion.
The TraceClosure module lifts that finite story to an infinite ledger. A completed trace is not a finite list of $\delta$'s; it is a function from every natural index to a distinction act. Finite prefixes are then cut out of that infinite object by recursion on length, recovering ordinary finite traces.
The local setting is K4.13/R9: inhabit the trace-closure boundary honestly, with a named completed object rather than an open-ended finite approximation.
proof idea
No proof body: this is a structure definition. It declares a single field actAt : Nat → DistinctionAct. Downstream definitions (finite prefixes, the canonical constant-δ ledger) inhabit or consume that field by ordinary function application and Nat recursion; the simp lemmas for prefix zero and successor are definitional rfl.
why it matters
CompletedTrace is the carrier for the K4.13/R9 trace-closure story. The canonical inhabitant repeats $\delta$ at every index; its finite prefixes supply the Nonempty Trace witnesses used by canonical_prefix_exists. The same type appears in TraceClosureCertificate and trace_closure_certificate, which assert that the closure boundary is inhabited and tagged with the strength annotation.
Downstream orbit-ledger constructions (CompletedOrbitLedger, canonical_toNat) sit on the same infinite-ledger idea. In the broader Recognition chain this is scaffolding for closing finite δ-traces into a completed object before strength and orbit arguments, not a forcing-chain (T0–T8) step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.