DistinctionNat
plain-language theorem explainer
DistinctionNat is the free Peano carrier for finite orbits of repeated distinction: zero together with a successor. It is the base-neutral counting type used throughout the primitive recognition calculus and cost factorization. Anyone citing ratio-orbit normalization, Archimedean magnitude, or native-cost hypotheses on orbits depends on it. The declaration is a bare inductive with DecidableEq and Repr; Peano facts are proved as sibling theorems.
Claim. There is an inductive type of finite distinction counts with constructors $0$ and $n \mapsto n+1$, equipped with decidable equality. It is the base-neutral finite orbit of repeated distinction (K2.12).
background
In the primitive recognition calculus, physical content is carried by orbits under reciprocal and normalization moves on ratios. Before those moves, one needs a pure counting type that records how many times the distinction generator has been applied. DistinctionNat is that type: the free inductive generated by a zero and a unary successor, exactly as Peano naturals, but named for the recognition setting rather than arithmetic.
The module sits under Foundation.PrimitiveRecognitionCalculus.Orbit and imports the basic PRC layer. Upstream, ArithmeticFromLogic already treats successor as "one more application of the generator" on a logic-level Nat; DistinctionNat plays the same structural role for distinction orbits. Sibling lemmas immediately recover the Peano package (zero is not a successor, successor is injective, induction) and the mutually inverse bridges toNat / ofNat to ordinary Nat.
Downstream cost and factorization code treat a DistinctionNat as the discrete magnitude of an orbit position, independent of any preferred radix or calibration constant.
proof idea
No proof body: this is an inductive definition. Two constructors (zero, succ) generate the type; deriving DecidableEq, Repr supplies equality decision and printing. All Peano content is deferred to sibling theorems (zero_ne_succ, succ_injective, induction) and the toNat/ofNat isomorphism lemmas in the same namespace.
why it matters
K2.12 installs the discrete skeleton on which ratio orbits and native cost live. Downstream, Archimedean magnitude is literally n.toNat on a DistinctionNat; chart-transition certificates and factor pairs index by it; BaseSansTwo and the signed-power / sign-gauge native-cost packages quantify normalization and reciprocal invariance over orbits whose discrete part is this type. The physically-real iff delta-forced bridge in DeltaForced also threads through the same orbit layer.
In the broader Recognition chain this is pre-T5 scaffolding: it does not yet force the J-cost, $\varphi$, or the eight-tick octave, but every later orbit-normalized cost identity needs a base-neutral finite counter. With forty use sites already, it is the standard discrete parameter for PRC factorization rather than a local convenience.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.