cmp_sub_left_input_of_balanced
plain-language theorem explainer
If two signed orbits are balanced-equivalent, left-subtracting a fixed orbit and then comparing against a third orbit yields the same Ordering. Order theorists and anyone building the PRC integer-order surface cite this congruence. The proof is a two-line composition of left-subtraction congruence with comparison congruence under balance.
Claim. Let $a,a',b,c$ be signed orbits. If $a$ is balanced with $a'$ (i.e. $a.pos+a'.neg=a'.pos+a.neg$), then $\mathrm{cmp}(a-b,\,c)=\mathrm{cmp}(a'-b,\,c)$, where $\mathrm{cmp}$ is the internal signed-orbit comparison selector.
background
In the Primitive Recognition Calculus, integers are carried by signed orbits: pairs of nonnegative orbit lengths (pos, neg). Two signed orbits are balanced when $a.pos+b.neg=b.pos+a.neg$; this is the internal PRC integer relation (K4.9), defined entirely on $\delta$-orbit positions. The bridge to the verifier display is balanced_iff_toInt_eq: balance holds iff the induced integers agree.
Comparison cmp is not taken from the integer display. It is defined from the signed-orbit order and the balance relation: equal when the arguments are balanced, otherwise decided by the nonnegativity flag of the difference. Subtraction of signed orbits is the corresponding internal difference operation.
This module builds the order surface on those internal primitives. Upstream, left-subtraction already preserves balance (sub_congr_of_balanced_left), and comparison is congruent under balance on both slots (cmp_congr_of_balanced).
proof idea
Short tactic proof. First obtain reflexivity of balance on the right argument $c$ by rewriting with the characterization that balance is equivalent to equal toInt values (so $c$ balances with itself). Then apply comparison-congruence under balance, feeding (i) left-subtraction congruence of the balanced pair $a\sim a'$ against fixed $b$, and (ii) the reflexivity just shown for $c$. The result is equality of the two cmp values.
why it matters
Feeds the closing certificate integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed. That certificate packages display lemmas (truncated subtraction, $\le$, absolute difference, nonnegativity flags) into a single interface object used downstream in the foundation stack.
Without left-input invariance of cmp after subtraction, the order would depend on which balanced representative is chosen for the minuend, breaking the claim that the PRC integer order is well-defined on balance classes. This is bookkeeping inside the foundation layer that underwrites later forcing-chain material (ledger balance, integer displays), not a physics landmark itself; it keeps the integer-order surface choice-free and representative-independent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.