cmp_sub_zero_right
plain-language theorem explainer
Right-subtraction by zero is invisible to signed-orbit comparison: cmp(b, a−0) equals cmp(b, a). Anyone building the internal PRC integer order cites this when normalizing differences. The proof is a two-line congruence: b is balanced with itself and a−0 is balanced with a, so cmp is unchanged.
Claim. For signed orbits $a,b$, the internal comparison satisfies $\mathrm{cmp}(b,\, a-0)=\mathrm{cmp}(b,\, a)$. Equivalently, subtracting the zero orbit on the right does not change how $b$ orders against $a$.
background
In Primitive Recognition Calculus, integers are carried by signed orbits: pairs of nonnegative $\delta$-orbit lengths (pos, neg). Two orbits are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$; by K4.9 this is equivalent to equal verifier displays $a.\mathrm{toInt}=b.\mathrm{toInt}$.
Internal order is not defined by reading $\mathbb{Z}$. The selector $\mathrm{cmp}(a,b)$ returns equality when $a$ and $b$ are balanced, otherwise uses the nonnegativity flag of $b-a$. Congruence of cmp under balanced replacements is already proved: if $a\sim a'$ and $b\sim b'$ then $\mathrm{cmp}(a,b)=\mathrm{cmp}(a',b')$. Separately, $a-0$ is balanced with $a$ (via the toInt bridge and $\omega$).
This module assembles a closed internal order surface on signed orbits, independent of the external integer display except through the balanced bridge.
proof idea
Reflexivity of balance on $b$ is immediate from the characterization $\mathrm{balanced}\leftrightarrow\mathrm{toInt}$ equality (both sides $b.\mathrm{toInt}$). The prior lemma $\mathrm{sub_zero_balanced}$ supplies $\mathrm{balanced}(a-0,, a)$. Feed those two balanced hypotheses into $\mathrm{cmp_congr_of_balanced}$ with the left pair $(b,b)$ and the right pair $(a-0,, a)$. The resulting equality is exactly the claim.
why it matters
The parent consumer is $\mathrm{integer_order_certificate}$, which packages the closed internal signed-orbit order surface (truncated subtraction, $\le$ display, abs-diff, nonneg flags). Right-invariance of cmp under $-0$ is a normalization step that certificate needs so difference-based comparisons do not depend on a trivial zero summand.
In the Recognition stack this sits in foundation ledger/PRC integer structure, beneath the forcing chain rather than inside T5–T8 themselves. It keeps order native to $\delta$-orbit balance instead of smuggling classical $\mathbb{Z}$ comparison into the calculus. No open scaffold remains: the claim is fully proved and only feeds the certificate assembly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.