absDiff
plain-language theorem explainer
Absolute difference on finite δ-orbit positions: |a−b| built as truncated subtraction both ways and summed. Anyone constructing signed-orbit absolute value or the integer-order certificate cites it. The body is a two-term definition, not a proof.
Claim. For finite $\delta$-orbit positions $a,b$, the absolute difference is $\mathrm{truncSub}(a,b)+\mathrm{truncSub}(b,a)$, where truncated subtraction is the structural predecessor recursion that returns zero when the minuend is exhausted.
background
In the primitive recognition calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction: an inductive type with zero and successor, standing in for natural numbers without importing $\mathbb{N}$ as primitive. Arithmetic on these orbits is built by structural recursion so that later verifier displays can match ordinary integer arithmetic.
Truncated subtraction is the one-sided difference: it peels matching successors and yields zero when the second argument outruns the first. Absolute difference is the symmetric combination of the two truncated differences, so exactly one summand is nonzero whenever the positions differ.
The surrounding module develops integer and rational structure from these orbit positions (signed orbits, order, absolute value) before any external integer library is treated as authoritative.
proof idea
Definition only: unfold to the sum of the two truncated subtractions. No tactics or lemmas. Downstream theorems such as the verifier display identity for absolute difference expand this definition, rewrite with the addition and truncated-subtraction display lemmas, and case-split on which orbit is larger in toNat.
why it matters
This is the internal absolute-value kernel for signed orbits: absolute value of a signed orbit is absolute difference of its positive and negative parts. It feeds the step-1 integer-order certificate, which packages display equalities for truncated subtraction, order, and absolute value so that orbit arithmetic matches ordinary $\mathbb{Z}$ displays. In the Recognition foundation stack this sits under primitive recognition calculus, before forcing-chain landmarks (J-uniqueness, $\varphi$, eight-tick, $D=3$); it supplies the discrete magnitude needed for later cost and ladder constructions rather than those physics claims themselves.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.