abs_eq_of_balanced
plain-language theorem explainer
Balanced signed orbit differences carry the same absolute value as distinction naturals. Order and congruence lemmas in the PRC integer layer cite this whenever absolute value must be invariant under the internal balance relation. The proof is a short term argument: injectivity of the natural display, the abs-to-natAbs bridge, and the balance/toInt equivalence.
Claim. Let $z,w$ be signed orbit differences (pairs of distinction naturals, read as $\mathrm{pos}-\mathrm{neg}$). If they are balanced, meaning $z_{+}+w_{-}=w_{+}+z_{-}$ (equivalently their integer displays agree), then their absolute values as distinction naturals are equal: $|z|=|w|$.
background
In the Primitive Recognition Calculus integer layer, a signed orbit is a pair of distinction naturals $(\mathrm{pos},\mathrm{neg})$ with intended meaning $\mathrm{pos}-\mathrm{neg}$. Absolute value is the orbit-position absolute difference of those two components, not a classical $\mathbb{Z}$ constructor.
Balance is the internal equivalence of K4.9: two signed orbits $a,b$ satisfy $a_{+}+b_{-}=b_{+}+a_{-}$. The bridge theorem states this is equivalent to equality of the conservative integer displays $a.\mathrm{toInt}=b.\mathrm{toInt}$. A companion display lemma records that the natural value of the internal absolute value is exactly $\mathrm{Int.natAbs}$ of that integer display.
The local module builds the order surface on these signed orbits (reflexivity, totality, trichotomy, sign flags). Absolute-value invariance under balance is the congruence fact needed before subtraction and order certificates can treat balanced representatives interchangeably.
proof idea
Term-mode, three steps. Apply injectivity of the distinction-natural display map so it suffices to equate natural numbers. Rewrite both sides with the absolute-value display lemma, turning each internal abs into $\mathrm{Int.natAbs}$ of the corresponding integer display. Finally rewrite by the forward direction of the balance/toInt equivalence on the hypothesis, so the two integer displays (hence their natAbs values) agree.
why it matters
This is the absolute-value congruence for the internal balance relation. Immediate parents are the three subtraction variants: abs of a difference is unchanged when the left operand, the right operand, or both are replaced by balanced representatives. Those feed the closed integer-order certificate, whose doc-comment states the internal signed-orbit order surface is closed (display lemmas for truncated subtraction, $\leq$, abs-diff, and nonnegativity flags).
In the Recognition foundation this keeps the PRC integer order choice-free and internal: absolute magnitude is a property of the balance class, not of a particular signed representative. It sits under the ledger/forcing stack that later supports the forcing chain, without yet invoking J-cost, $\varphi$, or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.