abs_toNat
plain-language theorem explainer
For any signed orbit difference z = pos − neg, the natural-number reading of its internal absolute value equals the ordinary integer absolute value of its verifier integer. Order and arithmetic lemmas on signed orbits cite this bridge constantly. The proof unfolds the two displays and applies the absolute-difference identity on distinction naturals.
Claim. Let $z$ be a signed orbit (a pair of distinction naturals interpreted as $\mathrm{pos}-\mathrm{neg}$). Then the natural-number reading of the internal absolute value of $z$ equals $\lvert z\rvert_{\mathbb{Z}}$ under the verifier map to ordinary integers: $\mathrm{toNat}(\lvert z\rvert)=\mathrm{natAbs}(\mathrm{toInt}(z))$.
background
In the primitive recognition calculus, integers are built before classical $\mathbb{Z}$ is assumed. A SignedOrbit is a pair of distinction naturals $(\mathrm{pos},\mathrm{neg})$ with intended meaning $\mathrm{pos}-\mathrm{neg}$. Its internal absolute value is the orbit-level absolute difference of those two components, not a post-hoc absolute value on a classical integer.
Two display maps sit side by side. One reads a distinction natural as an ordinary $\mathbb{N}$ by counting orbit steps (toNat). The other recovers a classical integer from a signed orbit (toInt). The absolute-value operation on signed orbits is defined by absDiff on the positive and negative legs.
The local module develops integer and rational structure from recognition orbits. This lemma is the coherence statement that the internal absolute value, once displayed as a natural, matches Mathlib's Int.natAbs of the verifier integer.
proof idea
Term-mode, three lines. Unfold the definitions of internal absolute value and of the signed-orbit-to-integer display. Both reduce to the absolute difference of the two distinction-natural legs. The goal is then exactly DistinctionNat.toNat_absDiff applied to z.pos and z.neg, which is invoked directly.
why it matters
This is the standard bridge from internal absolute value to classical natAbs. Downstream order and ring lemmas in IntegerOrder rewrite through it constantly: triangle inequality abs_add_le_add_abs reduces to Int.natAbs_add_le; multiplicativity abs_mul reduces to Int.natAbs_mul; balanced-orbit equalities and the characterization abs_le_iff_between all transport via the same identity.
In the Recognition foundation stack, signed orbits are the integer layer beneath cost, forcing, and ladder arithmetic. Without this display coherence, internal comparisons could not be discharged by ordinary integer facts. It is pure bookkeeping relative to T5–T8, but it is the bookkeeping those later layers inherit whenever absolute values appear.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.