trace_closure_certificate
plain-language theorem explainer
The K4.13 trace-closure certificate is inhabited: a completed infinite distinction-act ledger and a completed orbit ledger both exist, the canonical orbit verifier is faithful on naturals, and the strength tag is honestly traceClosure. Kernel and PRC stratification authors cite it as the completion boundary. The proof is a term that packages the canonical constructions and a simp identity.
Claim. There exists a first trace-closure certificate: the type of completed traces (infinite ledgers of distinction acts) is nonempty, as is the type of completed orbit ledgers (infinite sequences of finite $\delta$-orbit positions); the canonical orbit ledger satisfies $(\mathrm{positionAt}\, n).\mathrm{toNat}=n$ for every $n\in\mathbb{N}$; and the associated claim is tagged $\mathrm{traceClosure}$.
background
In the Primitive Recognition Calculus, a completed trace is an infinite ledger of distinction acts, not a finite $\delta$-only prefix. The module supplies a canonical completed trace that repeats the primitive distinction act at every index. Separately, a completed orbit ledger is the natural-number side of the same closure: an infinite sequence of finite $\delta$-orbit positions, with a canonical ledger sending verifier index $n$ to the $n$th position.
The certificate structure packages nonemptiness of both objects, faithfulness of the canonical orbit verifier (its position at $n$ converts back to $n$), and an honest strength tag equal to $\mathrm{traceClosure}$. Upstream, the faithfulness fact is the simp theorem that the canonical ledger's $\mathrm{toNat}$ recovers the index; the canonical completed trace is the constant-delta construction.
proof idea
Term-mode structure inhabitant. Nonemptiness of completed traces is witnessed twice by the canonical completed trace (constant primitive distinction act). Nonemptiness of completed orbit ledgers is witnessed by the canonical orbit ledger. Faithfulness is exactly the upstream identity that the canonical ledger's position at $n$ converts to $n$ via $\mathrm{toNat}$. The strength tag is discharged by reflexivity against the claim's fixed tag.
why it matters
This is the K4.13 boundary object: it marks that the PRC has closed traces at infinity rather than stopping at finite $\delta$-only syntax. Downstream, prc_full_stratification installs it as the completion boundary field, discharging full stratification field-by-field with no project-local axioms. The kernel first-pass certificate sits on the same stack (delta-only floor below completion). In the broader Recognition forcing picture this is infrastructure for the primitive calculus that later feeds cost uniqueness and stratification, not yet a T5–T8 forcing step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.