canonical_toNat
plain-language theorem explainer
The canonical completed orbit ledger is verifier-faithful: reading the position at step n back as a natural number recovers n. Anyone assembling the K4.13 trace-closure certificate cites this as the orbit-verifier faithfulness field. The proof is a one-line wrapper of the DistinctionNat roundtrip lemma toNat_ofNat.
Claim. For every natural number $n$, if $p_n$ is the position of the canonical completed orbit ledger at step $n$, then converting $p_n$ back to a natural number yields $n$: $\mathrm{toNat}(p_n)=n$.
background
In the Primitive Recognition Calculus, a finite orbit of repeated distinction is the base-neutral inductive type DistinctionNat (constructors zero and succ). The verifier map toNat sends zero to 0 and succ to Nat.succ, so orbits can be compared with ordinary Lean naturals. The inverse ofNat builds an orbit from a Nat; the roundtrip toNat_ofNat states that toNat(ofNat n)=n.
TraceClosure packages completed traces and completed orbit ledgers as the boundary objects of the calculus. The canonical completed orbit ledger exposes a positionAt map that, at each Nat index, returns a DistinctionNat. This theorem asserts that those positions are exactly the standard ofNat embedding, so the ledger is faithful as a Nat-indexed orbit.
Upstream, ArithmeticFromLogic.toNat plays the same role for LogicNat (identity/step), and several other modules expose a canonical object; here the relevant canonical is the TraceClosure ledger, not the measure-forcing or dyadic-protocol canons.
proof idea
One-line wrapper. The goal reduces to the already-proved DistinctionNat roundtrip toNat_ofNat at n, because canonical.positionAt is definitionally the ofNat embedding of DistinctionNat. Discharged by exact DistinctionNat.toNat_ofNat n; marked @[simp] so later certificate assembly can rewrite with it.
why it matters
Feeds directly into trace_closure_certificate (K4.13: "the trace-closure boundary is inhabited and tagged honestly"), which sets canonical_orbit_verifier_faithful := CompletedOrbitLedger.canonical_toNat. Without this equality the certificate cannot claim that the canonical completed orbit ledger is a faithful Nat verifier.
In the broader foundation stack this is bookkeeping, not a forcing step: it closes the orbit side of the trace-closure package so that completed traces, completed orbit ledgers, and strength tags sit in one inhabited certificate. It does not itself force phi, the eight-tick octave, or D=3; those live in the T0–T8 chain. It does guarantee that whatever downstream physics reads off orbit length from the canonical ledger is reading ordinary naturals, not a twisted enumeration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.