abs_sub_self_eq_zero
plain-language theorem explainer
The absolute value of a signed orbit subtracted from itself is the zero distinction. Anyone assembling the internal integer order on signed orbits cites this as the zero-difference reflexivity fact. The proof is a short term application of the abs-sub-zero characterization together with the balanced-to-integer bridge.
Claim. For every signed orbit $a$ (a pair of distinction-naturals read as $\mathrm{pos}-\mathrm{neg}$), the absolute value of the signed difference $a-a$ equals the zero distinction: $|a-a|=0$.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (zero and successor). A SignedOrbit is a pair of such orbits, intended as $\mathrm{pos}-\mathrm{neg}$. Its absolute value is the absolute difference of the two legs, returned as a plain distinction-natural.
Two signed orbits are balanced when they represent the same integer. The bridge theorem states that balanced agrees with equality of the conservative $\mathbb{Z}$ display: balanced $a,b$ if and only if $a.\mathrm{toInt}=b.\mathrm{toInt}$. Upstream, absolute value of a difference vanishes exactly on balanced pairs: $|a-b|=0\leftrightarrow$ balanced $a,b$.
This module builds the order surface on that signed-orbit arithmetic without classical choice.
proof idea
One short term proof. Apply the right-to-left direction of abs_sub_eq_zero_iff_balanced at the diagonal pair $(a,a)$, reducing the goal to balanced $a,a$. Rewrite that goal by balanced_iff_toInt_eq, which becomes $a.\mathrm{toInt}=a.\mathrm{toInt}$ and closes by reflexivity. No case split and no omega on the final goal.
why it matters
Feeds integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed. That certificate packages display lemmas for truncated subtraction, $\le$, absolute difference, and nonnegativity flags; the present fact is the diagonal zero-abs identity needed for a coherent absolute-value display on differences.
In the Recognition foundation this sits inside the integer layer of the Primitive Recognition Calculus: signed orbits must behave like $\mathbb{Z}$ before later forcing steps (J-cost uniqueness, $\varphi$, eight-tick octave, $D=3$) can treat integer indices as already ordered. It is a small but load-bearing reflexivity step, not an open scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.