canonical_succ
plain-language theorem explainer
On the canonical completed orbit ledger, the position at discrete step n+1 is exactly the DistinctionNat successor of the position at step n. Cite this when checking that the ledger clock is Peano-compatible under finite prefixes or the K1/R9 trace-closure audit. The equality is purely definitional and closes by reflexivity.
Claim. For every natural number $n$, the position of the canonical completed orbit ledger at step $n+1$ equals the successor (in the base-neutral distinction-number type) of its position at step $n$.
background
The ambient module builds completed traces and their orbit ledgers for the primitive recognition calculus. A completed trace supplies an act at every discrete time; the canonical completed trace repeats the primitive distinction act at every step.
DistinctionNat is the inductive, base-neutral finite orbit of repeated distinction (zero and successor only). It is the discrete position type for how many distinctions have been recorded. CompletedOrbitLedger packages a completed orbit with a position clock positionAt : Nat → DistinctionNat. The canonical ledger is the standard instance built from that canonical completed trace.
Upstream, successor on the logic/Peano side is one more application of the generator; here the same successor shape appears on DistinctionNat, so the ledger clock must intertwine ordinary Nat succession with DistinctionNat succession.
proof idea
One-line reflexivity proof. Unfolding canonical.positionAt on the canonical completed orbit ledger and DistinctionNat.succ makes both sides of the equality definitionally identical, so rfl discharges the goal with no lemmas or case splits.
why it matters
This is a small but necessary clock-compatibility fact inside TraceClosure: the canonical ledger advances its distinction count exactly once per Nat tick. It sits beside canonical_toNat, canonical_actAt, and the finite-prefix lemmas, and supports the K1/R9 audit record that completed traces carry a trace-closure tag (traceClosureClaim, TraceClosureCertificate).
In the broader foundation stack it keeps the recognition-side discrete orbit aligned with Peano succession forced from logic, so later forcing-chain and ledger arguments can treat the canonical position as an ordinary inductive counter. No downstream theorems currently depend on it in the graph; it is infrastructure for the closure certificate rather than a physics endpoint (T5–T8, RCL, masses).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.