cmp_product_factors_of_balanced
plain-language theorem explainer
If two pairs of signed orbits are balanced (same internal integer value), their products compare identically against any third orbit. Order and arithmetic theorists working the PRC integer surface cite this when products must respect the balanced equivalence. The proof is a short tactic chain: self-balance of the third argument, product congruence, then comparison congruence.
Claim. Let $a,a',b,b',c$ be signed orbits. If $a$ is balanced with $a'$ and $b$ is balanced with $b'$ (equivalently $a.{\rm toInt}=a'.{\rm toInt}$ and $b.{\rm toInt}=b'.{\rm toInt}$), then $\mathrm{cmp}(a\cdot b,\,c)=\mathrm{cmp}(a'\cdot b',\,c)$.
background
In the Primitive Recognition Calculus, integers are carried by signed orbits: pairs of nonnegative orbit lengths (pos, neg). Two orbits are balanced when a.pos + b.neg = b.pos + a.neg. That internal relation is equivalent to equality of the verifier display toInt (K4.9), so balanced is the choice-free integer equality on the PRC side.
Comparison cmp is defined from the signed-orbit order and balanced length, not from the verifier integer display: equal when balanced, otherwise ordered by the nonnegativity flag of the difference. Multiplication of signed orbits multiplies the corresponding integer values.
The local module builds the internal order surface on these orbits. Upstream, mul_congr_of_balanced already shows that balanced factors yield balanced products, and cmp_congr_of_balanced shows that balanced pairs may be substituted in either slot of cmp.
proof idea
Short tactic proof. First obtain reflexivity of balanced at c by rewriting with balanced_iff_toInt_eq (same toInt implies balanced). Then apply mul_congr_of_balanced to the two factor hypotheses to get that mul a b is balanced with mul a' b'. Feed that product congruence together with the self-balance of c into cmp_congr_of_balanced, which substitutes both arguments of cmp and yields the claimed equality of orderings.
why it matters
This lemma closes a substitution law for products under the internal comparison: once factors are identified by the balanced relation, their product may be rewritten inside any comparison against a fixed third orbit. It is consumed by integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed."
In the Recognition foundation stack this sits under the ledger and forcing layer that eventually feeds the T0–T8 chain. Keeping multiplication congruent for cmp is part of showing that the PRC integer order is a genuine ordered ring surface, not merely a display of ℤ. Without product-factor congruence, the certificate could not treat multiplicative structure as well-defined on balanced classes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.