signedOrbit_neg_ofOrbit_abs_self
plain-language theorem explainer
Negating a nonnegative signed orbit built from a distinction count n, then taking absolute value, recovers n. Anyone normalizing signs in the primitive recognition calculus integer layer cites this identity. The proof injects into naturals, rewrites through the integer embedding of absolute value, negation, and the nonnegative embedding, then simplifies.
Claim. For every distinction count $n$, embedding $n$ as a nonnegative signed orbit, negating that orbit (swapping its positive and negative parts), and taking the absolute value recovers $n$.
background
In the primitive recognition calculus, distinction counts index nonnegative orbit positions. Signed orbits are pairs of such counts (positive part, negative part), read as the integer difference positive minus negative, so the foundation can talk about signs without treating classical $\mathbb{Z}$ as primitive data.
The nonnegative embedding of a distinction count $n$ places $n$ in the positive slot and zero in the negative slot. Negation swaps the two slots. Absolute value returns the absolute difference of the slots as a distinction count. Upstream lemmas record that this absolute value matches the natural absolute value of the integer view, that negation flips the sign of the integer view, and that the nonnegative embedding has integer view equal to the underlying natural of $n$.
proof idea
Apply injectivity of the distinction-count-to-natural map so the goal becomes an equality of naturals. Rewrite with the three display lemmas: absolute value becomes natural absolute value of the integer view; negation becomes unary minus on that integer; the nonnegative embedding becomes the underlying natural of $n$. A final simplification closes the arithmetic identity $|-(n)|=n$ on naturals.
why it matters
This is a sign-normalization identity inside the native-cost uniqueness development. It is used when proving that a signed quotient is sign-canonical whenever the divisor divides the absolute value of the signed orbit. That canonicity step contributes to the native-cost uniqueness blocker certificate, which packages zero-calibrated factorization targets and the refutation of signed-admissible alternatives that pin down the unique native cost character.
In the broader Recognition Science stack this lives in the foundation layer that supports the forcing chain toward J-uniqueness (T5) and the self-similar fixed point $\varphi$ (T6). The lemma itself is purely about the signed-orbit model of integers and does not invoke the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.