TraceClosureCertificate
plain-language theorem explainer
Packages the K4.13 trace-closure boundary as a single proposition: completed infinite distinction traces and orbit ledgers exist, the canonical ledger is faithful to verifier naturals, and the claim is tagged as traceClosure strength. Cited by the first-pass PRC kernel certificate and by the full honest stratification as the completion boundary. Pure structure definition; inhabited later by a one-line constructor theorem.
Claim. A trace-closure certificate is the proposition that (i) there exists a completed trace (an infinite ledger of distinction acts), (ii) a canonical such trace exists, (iii) there exists a completed orbit ledger (an infinite sequence of finite $\delta$-orbit positions), (iv) the canonical ledger satisfies $\mathrm{toNat}(\mathrm{positionAt}(n))=n$ for every $n\in\mathbb{N}$, and (v) the associated strength tag equals the trace-closure tag.
background
In the Primitive Recognition Calculus, a finite $\delta$-trace records only finitely many distinction acts. Trace closure steps past that floor: a completed trace is an infinite ledger actAt : Nat → DistinctionAct, and a completed orbit ledger is the natural-number side, positionAt : Nat → DistinctionNat. The module treats these as boundary objects, not as $\delta$-only data.
The orbit side reuses the verifier map toNat on DistinctionNat (zero maps to 0, successor to successor), so faithfulness of the canonical ledger is the statement that the infinite position sequence is just the standard Peano indexing. Upstream arithmetic-from-logic supplies the same iteration-count reading on logic naturals; here the content is the $\delta$-orbit copy.
Locally this structure is the K4.13 certificate shape: inhabitance of the closure objects plus an honest strength tag, before any continuum or cost-uniqueness claims are attached.
proof idea
No proof body: this is a bare structure ... : Prop bundling five fields. Inhabitance is discharged downstream by trace_closure_certificate, which supplies CompletedTrace.canonical and CompletedOrbitLedger.canonical for the nonempty fields, applies CompletedOrbitLedger.canonical_toNat for verifier faithfulness, and closes the tag equation by rfl.
why it matters
Marks the completion boundary in the PRC forcing stratification. PRCFullStratification takes a field completion_boundary : TraceClosureCertificate and pairs it with the $\delta$-only floor (KernelFirstPassCertificate) and a carrier-strictly-below-completion clause (existence of $\sqrt{2}$ in $\mathbb{R}$ but not on ratio orbits). That is the load-bearing "what is forced versus assumed" joint: infinite traces and orbit ledgers are admitted as boundary data, not derived from finite $\delta$ alone.
KernelFirstPassCertificate sits on the floor side of the same chain; continuum non-forcing (prc_continuum_not_forced) uses the countable $\delta$-index story that this boundary deliberately exceeds. In framework terms this is bookkeeping for the passage beyond finite recognition acts toward continuum carriers, not yet T5 J-uniqueness or the mass ladder. It closes K4.13 as an inhabited, honestly tagged certificate rather than a sorry stub.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.