cmp_zero_sub_left
plain-language theorem explainer
Comparing zero-minus-a against b equals comparing the negation of a against b, for signed orbits under the internal PRC order. Order-certificate and integer-order proofs cite it when rewriting left subtraction from zero into negation. The proof is a short congruence: zero-sub is balanced with negate, b is balanced with itself, so cmp is invariant.
Claim. For signed orbits $a$ and $b$, $\mathrm{cmp}(0-a,\,b)=\mathrm{cmp}(-a,\,b)$, where $\mathrm{cmp}$ is the internal signed-orbit comparison (equality on the balanced relation, otherwise decided by the nonnegativity flag of the difference).
background
In Primitive Recognition Calculus, integers are carried as signed orbits: pairs of nonnegative orbit lengths (pos, neg) rather than a bare $\mathbb{Z}$ display. Two orbits are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$; that internal relation is equivalent to equal verifier integers via balanced_iff_toInt_eq.
The comparison selector cmp is defined from that balanced relation and the nonnegativity flag of the difference, not from the external integer display. Congruence cmp_congr_of_balanced says balanced replacements on either side leave the Ordering unchanged.
Upstream, zero_sub_balanced_negate already records that subtracting $a$ from zero is balanced with the orbit negation of $a$ (via the toInt bridge: $0-\mathrm{toInt}(a)=-\mathrm{toInt}(a)$). This lemma packages that fact for left-hand sides of cmp.
proof idea
Reflexivity of balance on $b$: rewrite with balanced_iff_toInt_eq so $b$ is balanced with itself. Feed that together with zero_sub_balanced_negate a into cmp_congr_of_balanced. The congruence immediately yields equality of the two cmp values. No case split on Ordering is needed.
why it matters
Feeds integer_order_certificate, which closes the internal signed-orbit order surface (display bridges for truncated subtraction, $\le$, absolute difference, and nonnegativity flags). Without left-zero-sub rewriting to negation, order identities that mix subtraction and sign would stay stuck on the internal representation.
In the foundation stack this is bookkeeping on the PRC integer layer beneath ledger forcing and the T0–T8 chain: it keeps order proofs choice-free and display-independent while still matching the conservative $\mathbb{Z}$ view. It does not itself force $\phi$, eight-tick structure, or $D=3$; it keeps the integer-order certificate honest so later recognition calculus can rely on a closed order API.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.