signedOrbit_ofOrbit_abs_self
plain-language theorem explainer
Embedding a nonnegative distinction orbit as a signed orbit and taking absolute value recovers the original orbit. Anyone working with signed orbit arithmetic or native-cost uniqueness cites this identity. The proof is a short injectivity argument: reduce via toNat, rewrite absolute value and ofOrbit-to-integer, then simplify.
Claim. For every distinction orbit $n$, if one forms the nonnegative signed orbit with positive part $n$ and zero negative part, then the absolute value of that signed orbit equals $n$.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (the native stand-in for natural numbers). A SignedOrbit is a pair of such orbits (pos, neg), intended as the difference pos - neg. The constructor that builds a nonnegative signed orbit from a single orbit sets the negative part to zero.
Absolute value on signed orbits returns a distinction orbit: the absolute difference of the two components. Internally this matches integer absolute value after the signed orbit is interpreted as an integer (toInt). The companion facts used here are that the absolute-value map displays as Int.natAbs on that integer, and that the nonnegative embedding has toInt equal to the underlying natural value.
The local module develops uniqueness of the native cost functional on PRC characters. Signed-orbit arithmetic is the integer layer underneath ratio characters and doubled-trace identities that feed the uniqueness argument.
proof idea
Apply injectivity of the underlying natural embedding toNat on distinction orbits. Rewrite the goal with the display lemma that absolute value on a signed orbit equals Int.natAbs of its integer interpretation, and with the simplification that the nonnegative embedding has integer value equal to n.toNat. The resulting integer identity is then discharged by simp.
why it matters
This is a basic normalization identity for the signed-orbit layer: nonnegative orbits are fixed points of absolute value after embedding. Downstream it is used by signedQuotient_signCanonical_of_divides, which establishes that signed quotients of admissible divisors land in the sign-canonical class needed for character arithmetic.
That quotient fact sits on the path to the native-cost uniqueness blocker certificate in the same module, which packages zero-calibrated factorization targets and refutations of signed-admissible alternatives. In the broader Recognition forcing chain, native cost uniqueness is the PRC-side counterpart of J-uniqueness (T5): only one cost compatible with the Recognition Composition Law and the discrete orbit calculus. The lemma itself is elementary bookkeeping, but without it the sign-canonical quotient step does not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.