balanced_product_factors_iff_of_balanced
plain-language theorem explainer
If two pairs of signed orbits are balanced (same integer display), their products stay interchangeable when testing balance against a third orbit: mul(a,b) balances c exactly when mul(a',b') does. Order and certificate authors in the primitive recognition calculus cite this to treat multiplication as well-defined on the balanced quotient. The proof rewrites both sides through the toInt bridge and multiplies equal integers.
Claim. Let $a,a',b,b',c$ be signed orbits. If $a$ is balanced with $a'$ and $b$ is balanced with $b'$ (equivalently $a.toInt = a'.toInt$ and $b.toInt = b'.toInt$), then $\mathrm{mul}(a,b)$ is balanced with $c$ if and only if $\mathrm{mul}(a',b')$ is balanced with $c$.
background
In the primitive recognition calculus, a signed orbit is a pair of distinction naturals (pos, neg) read as the formal difference pos - neg. Two signed orbits are balanced when a.pos + b.neg = b.pos + a.neg; this is the internal integer relation on δ-orbit positions (K4.9), defined without leaving the PRC layer.
The bridge theorem balanced_iff_toInt_eq identifies that relation with equality of the conservative integer displays: balanced pairs are exactly those with equal toInt. Multiplication of signed orbits is compatible with that display: (mul a b).toInt = a.toInt * b.toInt.
The local module builds the order surface on these signed orbits (reflexivity, totality, trichotomy, sign flags). Balance is the equality relation underlying that order, so product well-definedness on balanced classes is a prerequisite for treating the integer display as a ring-like quotient.
proof idea
Term-mode rewrite proof. Unfold both sides of the target iff via balanced_iff_toInt_eq, then replace each product display by the product of displays via mul_toInt. The hypotheses ha and hb are likewise rewritten to a.toInt = a'.toInt and b.toInt = b'.toInt. Substituting those equalities makes the two integer products identical, so the iff collapses.
why it matters
Feeds the downstream integer_order_certificate, whose doc states that the internal signed-orbit order surface is closed. That certificate packages display lemmas for truncated subtraction, leq, absolute difference, and signed nonnegativity; product stability under balance is part of keeping the integer view coherent when orbits are multiplied.
In the Recognition foundation stack this sits inside the primitive recognition calculus that underwrites ledger integers before forcing-chain landmarks (T5 J-uniqueness, T6 φ, T7 eight-tick, T8 D=3). It does not itself force a physical constant; it closes an algebraic hygiene step so later order and mass-ladder constructions can treat balanced orbits as interchangeable factors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.