toNat_truncatedSub
plain-language theorem explainer
Truncated subtraction on finite δ-orbit positions displays as ordinary natural subtraction under the verifier map toNat. Anyone building order, absolute difference, or Euclidean algorithms on DistinctionNat cites this bridge. The proof is structural induction on both arguments, matching the recursive clauses of truncatedSub to Nat.sub.
Claim. For finite $\delta$-orbit positions $a,b$, the verifier reading of their truncated difference equals ordinary natural subtraction: $\mathrm{toNat}(a \dot{-} b) = \mathrm{toNat}(a) - \mathrm{toNat}(b)$.
background
DistinctionNat is the finite $\delta$-orbit type used in the primitive recognition calculus: positions reached by iterating the distinction generator a finite number of times. The map toNat reads off that iteration count as an ordinary natural number (the same forward map as on LogicNat: identity maps to 0, successor adds one).
Truncated subtraction on these positions is defined by structural recursion only: $a \dot{-} 0 = a$, $0 \dot{-} S(b) = 0$, and $S(a) \dot{-} S(b) = a \dot{-} b$. It never goes negative; excess minuend is clamped at zero. This module builds integer and rational structure from those orbit positions without importing classical arithmetic axioms as primitives.
The theorem is the display lemma: the internal operation, once projected by toNat, agrees with Lean's Nat subtraction. Downstream absolute difference and order certificates rely on that agreement.
proof idea
Double structural induction. Induct on $a$, generalizing $b$. In the zero case, case-split on $b$: both zero is rfl; $b$ a successor simplifies by the truncatedSub clause that returns zero. In the successor case for $a$, case-split on $b$ again: $b = 0$ is rfl (truncatedSub returns $a$); both successors apply simp with the inductive hypothesis and the recursive clause of truncatedSub. No external lemmas beyond the definitional equations of truncatedSub and toNat.
why it matters
This is a verifier-display bridge in the integer/rational layer of PrimitiveRecognitionCalculus. It is registered as truncated_sub_display inside integer_order_certificate, which closes the internal signed-orbit order surface. Sibling toNat_absDiff rewrites absolute difference through two applications of this lemma plus addition. The Euclidean layer uses it in the fuelled div/mod and gcd correctness proofs (divModFuel_toNat_aux, gcdFuel_toNat_aux), so quotient/remainder and gcd on orbit positions match Nat arithmetic under toNat.
In the broader Recognition stack, arithmetic is derived from the inductive orbit rather than posited; display lemmas like this keep the internal calculus aligned with the verifier Nat used in certificates. It does not itself touch T5–T8 or the J-cost equation, but it is infrastructure those later layers assume when they count ticks and rungs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.