toNat_absDiff
plain-language theorem explainer
On distinction naturals, the natural readout of the internal absolute difference equals the usual absolute value of the integer difference of the two readouts. Order-certificate and signed-orbit absolute-value lemmas cite it as the display bridge to ℤ. The proof unfolds the sum-of-truncated-subs definition, cases on which side is larger, and injects equality through ℤ via nonnegativity of natAbs.
Claim. For distinction naturals $a$ and $b$, if $\mathrm{absDiff}(a,b)$ is the internal absolute difference (sum of the two truncated subtractions), then its natural readout equals $\lvert n(a)-n(b)\rvert$, where $n$ is the iteration-count map into $\mathbb{N}$ and the right-hand side is $\mathrm{natAbs}$ of the difference in $\mathbb{Z}$.
background
This module sits in the Primitive Recognition Calculus layer that rebuilds arithmetic from recognition orbits rather than assuming bare $\mathbb{N}$. Distinction naturals carry an internal truncated subtraction and an absolute difference built as the sum of the two one-sided truncations, so the structure never goes negative inside the type.
The forward map $n$ (toNat) reads off the iteration count of a logic/orbit natural into ordinary $\mathbb{N}$. Upstream recovery already shows that internal addition is transported correctly: $n(a+b)=n(a)+n(b)$. A sibling lemma does the same for truncated subtraction. Absolute difference is then the sum of the two truncated subs, so its readout is forced once those two transport lemmas are in hand.
The local goal is a verifier display: external $\mathbb{Z}$ absolute value must match the internal construction, so later signed-orbit and order surfaces can quote a single equality rather than re-proving case splits.
proof idea
Unfold absolute difference to the sum of the two truncated subtractions. Rewrite the left-hand side with the addition transport lemma and the truncated-subtraction transport lemma on each summand, obtaining ordinary $\mathbb{N}$ arithmetic $(n(a)-n(b))+(n(b)-n(a))$ in the truncated sense.
Case on $n(b)\le n(a)$. In the true branch, the reverse truncated sub is zero, so the sum collapses to $n(a)-n(b)$; nonnegativity of the $\mathbb{Z}$ difference gives $\mathrm{natAbs}(n(a)-n(b))=n(a)-n(b)$, and injectivity of the cast $\mathbb{N}\to\mathbb{Z}$ finishes after a short omega cleanup.
In the false branch, the forward truncated sub is zero and the $\mathbb{Z}$ difference is nonpositive; reduce $\mathrm{natAbs}$ via $\mathrm{natAbs}(-x)=\mathrm{natAbs}(x)$ and nonnegativity of the negation, then inject through $\mathbb{Z}$ again with omega.
why it matters
The integer-order certificate packages this equality as its absolute-difference display field, closing the internal signed-orbit order surface against ordinary $\mathbb{Z}$ comparison. The sibling absolute-value display for signed orbits is a one-line application: absolute value of a signed orbit is absolute difference of its positive and negative parts, so the present lemma is exactly the transport step.
In the broader Recognition stack this is foundation plumbing, not a forcing-chain landmark: it lets later mass, rung, and certificate layers treat distinction-built integers as interchangeable with Mathlib $\mathbb{Z}$ on absolute value without re-opening truncated-sub cases. It does not itself force $\phi$, the eight-tick octave, or $D=3$; it only keeps the arithmetic substrate honest for those higher theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.