abs_negate
plain-language theorem explainer
Absolute value on signed orbits is invariant under pointwise negation: swapping the positive and negative distinction components leaves the absolute difference unchanged. Anyone assembling the internal integer order from orbit differences cites this. The proof reduces equality of DistinctionNat values to equality of their natural displays, then invokes the classical fact that natAbs ignores sign.
Claim. For every signed orbit $z$ (a pair of distinction-orbit positions interpreted as $\mathrm{pos}-\mathrm{neg}$), the absolute value of its pointwise negation equals the absolute value of $z$: $|\mathrm{negate}(z)|=|z|$, where absolute value is the absolute difference of the two components as a distinction-orbit position.
background
Signed orbits are the K4.6 encoding of integer differences inside the primitive recognition calculus: a pair $(\mathrm{pos},\mathrm{neg})$ of distinction-orbit positions, read as $\mathrm{pos}-\mathrm{neg}$. DistinctionNat is the base-neutral finite orbit of repeated distinction (zero and successor), the raw counting type before integers appear.
Pointwise negation swaps the two components. Absolute value is defined as the absolute difference of those components, landing again in DistinctionNat. The bridge to classical integers is the display map $\mathrm{toInt}$, with the verifier lemma that the natural display of absolute value equals $\mathrm{natAbs}$ of $\mathrm{toInt}$. Negation itself displays as ordinary integer negation.
The local module builds the order surface on these signed orbits (reflexivity, totality, trichotomy, sign flags). Absolute-value identities are the metric half of that surface.
proof idea
Apply injectivity of the natural display on DistinctionNat, so it suffices to show the two absolute values have equal $\mathrm{toNat}$. Rewrite both sides by the display lemma for absolute value, turning the goal into equality of $\mathrm{natAbs}$ of the corresponding $\mathrm{toInt}$ values. Rewrite the left $\mathrm{toInt}$ by the negation-display lemma, then finish with the standard library fact $\mathrm{natAbs}(-n)=\mathrm{natAbs}(n)$.
why it matters
This is a basic symmetry of the signed-orbit absolute value, needed before the order certificate can treat magnitude as sign-blind. Downstream, $\mathrm{abs_negate_ofOrbit}$ specializes it to orbits embedded as nonnegative signed orbits, recovering that absolute value of a negated pure orbit is the orbit itself. The same identity is listed among the facts supporting $\mathrm{integer_order_certificate}$, whose doc-comment states that the internal signed-orbit order surface is closed.
In the Recognition foundation stack this sits under PrimitiveRecognitionCalculus: integers and their order are reconstructed from distinction orbits rather than assumed. It does not itself touch the forcing chain T0-T8 or the J-cost, but it is part of the arithmetic substrate those later layers consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.