abs_negate_ofOrbit
plain-language theorem explainer
Negating a nonnegative signed orbit built from a distinction count n, then taking absolute value, recovers n. Order and ratio constructions cite this when they need |−n| = n on the orbit embedding. The proof is a two-step rewrite through absolute-value-of-negation and absolute-value-of-ofOrbit.
Claim. For every distinction count $n$, if one embeds $n$ as the nonnegative signed orbit $\langle n, 0\rangle$, swaps the positive and negative legs, and takes the absolute value (as a distinction count), the result is again $n$: $\bigl|\mathrm{negate}(\mathrm{ofOrbit}(n))\bigr| = n$.
background
In the primitive recognition calculus, integers are represented as signed orbit differences: a SignedOrbit is a pair of distinction counts (pos, neg) with intended meaning $\mathrm{pos}-\mathrm{neg}$. Absolute value returns the orbit position $\lvert\mathrm{pos}-\mathrm{neg}\rvert$ as a DistinctionNat. Negation swaps the two legs. The embedding ofOrbit n builds the nonnegative representative $\langle n, 0\rangle$.
The IntegerOrder module develops the order surface on these signed orbits (reflexivity, totality, trichotomy, sign flags). Two prior facts sit immediately upstream: absolute value is invariant under negation, and absolute value of ofOrbit n is $n$ itself. The present statement composes those two facts on the nonnegative ray.
proof idea
One-line wrapper. Rewrite with the two sibling lemmas: first replace absolute value of a negated signed orbit by absolute value of the original orbit (abs_negate), then replace absolute value of ofOrbit n by $n$ (abs_ofOrbit). No case split or induction.
why it matters
Closes a small but necessary identity on the nonnegative ray of signed orbits: $|-n|=n$ after embedding. Downstream, recipNonzero_num_abs_eq_den uses the absolute-value-of-ofOrbit family when simplifying the numerator of a reciprocal ratio orbit; the integer-order certificate packages the closed order surface that this identity supports. In the Recognition foundation stack this is pure scaffolding for the integer/rational layer beneath the forcing chain (T5–T8), not a physics claim itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.