cmp_sub_zero_left
plain-language theorem explainer
Subtracting zero on the left leaves the internal signed-orbit comparison unchanged: cmp(a−0,b)=cmp(a,b). Order lemmas and the closed integer-order certificate on the Primitive Recognition Calculus surface cite this identity. The proof is a short congruence step: a−0 is balanced with a, b is balanced with itself, so the comparison selector is invariant under those replacements.
Claim. For signed orbits $a$ and $b$, the internal comparison satisfies $\mathrm{cmp}(a-0,\,b)=\mathrm{cmp}(a,\,b)$.
background
In the Primitive Recognition Calculus integer layer, integers are carried as signed orbits: pairs of nonnegative orbit lengths (pos, neg) on δ-positions, not as bare verifier ℤ values. Two signed orbits are balanced when a.pos+b.neg=b.pos+a.neg; that internal relation is the PRC equivalence, and it agrees with equality of the conservative toInt display (K4.9).
The internal comparison selector cmp is defined from that balanced relation and the nonnegFlag of the difference, not from the verifier integer display: equal when balanced, otherwise ordered by whether (b−a) is nonnegative. Congruence of cmp under balanced replacements is already available: if a∼a' and b∼b' then cmp(a,b)=cmp(a',b').
A prior lemma records that left subtraction of zero is balanced with the original orbit: sub(a,0)∼a, proved by reducing toInt and a short omega step. The present result is the comparison-level consequence of that balance fact.
proof idea
First obtain reflexivity of balance on the right argument: b is balanced with b, by rewriting through balanced_iff_toInt_eq (toInt equality is reflexive). Then apply cmp_congr_of_balanced to the pair of balance witnesses sub_zero_balanced a (left: a−0 ∼ a) and that reflexivity fact (right: b ∼ b). The congruence lemma rewrites the cmp goal directly; no case split on Ordering is needed at this site.
why it matters
The integer-order surface must treat zero as a true unit for subtraction before the order certificate can close. This identity is one of the elementary cmp-invariance facts collected into integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed (display bridges for truncated sub, leq, absdiff, and nonneg flags).
In the broader Recognition stack, signed-orbit order is the choice-free integer substrate under ledger forcing and the Primitive Recognition Calculus. Keeping cmp stable under a↦a−0 means later order and trichotomy lemmas can normalize differences without leaving the internal δ-orbit language. It does not itself force φ, the eight-tick octave, or D=3; those sit upstream in the T0–T8 chain. It is a local algebraic hygiene step that the certificate packages with the other display bridges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.