cmp_sub_self_left
plain-language theorem explainer
Subtracting a signed orbit from itself is order-indistinguishable from zero: the internal comparison of a−a against any b equals the comparison of zero against b. Order-surface and certificate authors cite it when normalizing self-differences. The proof is a short congruence application: a−a is balanced with zero, b is balanced with itself, so cmp is invariant.
Claim. For any signed orbits $a$ and $b$, the internal comparison satisfies $\mathrm{cmp}(a-a,\,b)=\mathrm{cmp}(0,\,b)$.
background
In the Primitive Recognition Calculus, integers are carried as signed orbits: pairs of nonnegative orbit lengths (positive and negative legs) rather than as bare ℤ values. Two signed orbits are balanced when $a_{\mathrm{pos}}+b_{\mathrm{neg}}=b_{\mathrm{pos}}+a_{\mathrm{neg}}$; this is the internal equivalence, and balanced_iff_toInt_eq bridges it to equality of the conservative integer display.
The internal comparison cmp is defined from that balanced relation and the nonnegativity flag of the difference, not from the verifier integer display. Congruence under balanced pairs is already available as cmp_congr_of_balanced. Separately, sub_self_balanced_zero records that $a-a$ is balanced with the zero orbit.
This module builds the order surface on those primitives so that later certificates can treat signed-orbit order as closed without leaking display-level choices.
proof idea
Reflexivity of balance on $b$ is obtained by rewriting with balanced_iff_toInt_eq (equal integer displays). The main step applies cmp_congr_of_balanced to the pair of balanced hypotheses sub_self_balanced_zero a (so $a-a\sim 0$) and $b\sim b$, which forces $\mathrm{cmp}(a-a,b)=\mathrm{cmp}(0,b)$.
why it matters
Self-difference collapse is a basic normalization fact on the signed-orbit order surface. It feeds integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed: display bridges for truncated subtraction, $\le$, absolute difference, and nonnegativity flags are packaged there.
In the Recognition foundation stack this sits under ledger and forcing infrastructure (balanced ledgers, PRC integer relations) rather than under the T5–T8 forcing chain itself. It keeps order reasoning internal to $\delta$-orbit positions so certificate assembly does not smuggle classical integer trichotomy through the display layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.