abs_ofOrbit
plain-language theorem explainer
The absolute value of a nonnegative signed orbit recovers the underlying distinction count: embedding n as ⟨n,0⟩ and taking abs yields n again. Order and ratio constructions cite this when they need |+n| = n on the signed-orbit surface. The proof is a short injectivity argument on the Nat display, rewriting through abs_toNat and ofOrbit_toInt.
Claim. For every distinction-orbit position $n$, if one forms the nonnegative signed orbit $\langle n, 0\rangle$, then its absolute value (as a distinction-orbit position) equals $n$.
background
In the primitive recognition calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction: zero and successor, the internal stand-in for natural numbers. A SignedOrbit is a pair of such positions (pos, neg), intended as the difference pos − neg (K4.6).
The embedding ofOrbit n builds the nonnegative signed orbit ⟨n, 0⟩. Absolute value on signed orbits is defined by abs z := absDiff z.pos z.neg, returning a plain distinction position. The display lemmas abs_toNat and ofOrbit_toInt connect this internal surface to ordinary integers: z.abs.toNat = Int.natAbs z.toInt and (ofOrbit n).toInt = n.toNat.
This module develops the order theory of that signed-orbit surface (reflexivity, totality, sign flags, certificates). The present identity is the nonnegative special case of absolute value.
proof idea
Apply injectivity of DistinctionNat.toNat so it suffices to check equality after the Nat display. Rewrite with SignedOrbit.abs_toNat and SignedOrbit.ofOrbit_toInt: the left side becomes Int.natAbs (n.toNat) and the right side is n.toNat. A final simp closes the integer identity.
why it matters
Absolute value must fix the nonnegative ray before signed order and reciprocal constructions can be trusted. Downstream, abs_negate_ofOrbit reuses it to get |−n| = n, and recipNonzero_num_abs_eq_den uses it in the nonnegative branch of ratio inversion so the reciprocal numerator's abs equals the original denominator.
It also feeds the closed order surface packaged by integer_order_certificate ("The internal signed-orbit order surface is closed"). In the Recognition foundation stack this is bookkeeping on the integer layer beneath the forcing chain, not a T5–T8 landmark itself, but it keeps the signed-orbit model of ℤ coherent for later calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.