cmp_subtractions_of_balanced
plain-language theorem explainer
Balanced signed-orbit pairs may be replaced inside both arguments of a difference comparison without changing the Ordering result. Anyone building the internal integer order from δ-orbits cites this when showing cmp is well-defined on equivalence classes of differences. The proof is a two-step term: subtract congruence, then compare congruence.
Claim. Let $a,a',b,b',c,c',d,d'$ be signed orbits. If $a$ is balanced with $a'$, $b$ with $b'$, $c$ with $c'$, and $d$ with $d'$ (i.e.\ each pair satisfies the internal length relation $\mathrm{pos}+\mathrm{neg}'=\mathrm{pos}'+\mathrm{neg}$), then $\mathrm{cmp}(a-b,\,c-d)=\mathrm{cmp}(a'-b',\,c'-d')$.
background
In the Primitive Recognition Calculus, integers are not taken as primitives. A SignedOrbit is a pair of distinction-natural lengths (pos, neg), read as the formal difference pos − neg. Two signed orbits are balanced when their lengths match crosswise: $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$. That relation is the internal PRC integer equivalence (K4.9), defined only on δ-orbit positions.
Comparison cmp is an internal Ordering selector built from that balance relation and a nonnegativity flag on the difference, not from any external integer display. Subtraction of signed orbits is defined so that it respects balance: if the summands are pairwise balanced, the differences are balanced (sub_congr_of_balanced). The companion lemma cmp_congr_of_balanced says cmp itself is invariant under replacing either argument by a balanced partner.
This module assembles those pieces into a closed internal order surface on signed orbits, later certified for display against truncated naturals.
proof idea
Pure term proof, no tactics. Apply sub_congr_of_balanced to (ha, hb) to obtain balance of sub a b with sub a' b', and again to (hc, hd) for the second pair of differences. Feed those two balance witnesses into cmp_congr_of_balanced, which yields equality of the two cmp values. Nothing else is unfolded.
why it matters
Well-definedness of difference comparison is required before the internal signed-orbit order can be treated as an integer order. Downstream, integer_order_certificate packages the closed order surface ("The internal signed-orbit order surface is closed") and lists display bridges for truncated subtraction, ≤, absolute difference, and nonnegativity flags. This lemma is one of the congruence steps that make those bridges legitimate: cmp on differences does not depend on which balanced representative is chosen.
In the broader Recognition foundation, integer structure is forced from ledger/orbit combinatorics rather than postulated. Congruence lemmas like this keep the order internal to δ-orbits, consistent with the ledger-forcing and primitive-calculus path that later feeds the forcing chain (T0–T8) and the Recognition Composition Law. No open scaffold remains here; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.