lt_product_factors_iff_of_balanced
plain-language theorem explainer
If two pairs of signed orbits are balanced-equivalent, their products stand in the same strict order relative to any third orbit. Anyone building the internal integer order on Primitive Recognition Calculus cites this when transporting inequalities across product representatives. The proof is a one-line term application of left-order congruence to the balanced product of the factors.
Claim. Let $a,a',b,b',c$ be signed orbits. If $a$ is balanced with $a'$ and $b$ is balanced with $b'$, then $a\cdot b < c$ if and only if $a'\cdot b' < c$, where $<$ is the internal strict order (nonnegative difference and not balanced) and $\cdot$ is signed-orbit multiplication.
background
In Primitive Recognition Calculus, integers are realized as signed orbits: pairs of orbit positions carrying a positive and a negative leg. Two signed orbits are balanced when $a.pos + b.neg = b.pos + a.neg$; this is the internal equivalence relation that identifies representatives of the same integer (K4.9). Strict order is defined internally as $a < b$ when $a \le b$ and the pair is not balanced.
Multiplication of signed orbits is well-defined on these representatives, and the companion lemma mul_congr_of_balanced shows that balanced factors yield a balanced product. Left-order congruence under balanced already exists: if $a$ is balanced with $a'$, then $a < b$ iff $a' < b$. The present statement packages those two facts for the product-on-the-left case against a fixed right-hand side $c$.
The surrounding module builds the full order surface on signed orbits (reflexivity, transitivity, trichotomy, sign flags) needed before the integer-order certificate can close.
proof idea
One-line term proof. First apply mul_congr_of_balanced to the two balanced hypotheses to obtain that $a\cdot b$ is balanced with $a'\cdot b'$. Then feed that balanced product into lt_congr_left_of_balanced, which rewrites the left argument of $<$ under balanced equivalence and yields the biconditional against the fixed $c$. No case analysis or unfolding of lt is required at this site.
why it matters
This lemma is a transport rule for product inequalities under representative change. It feeds the module's integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed." Without product-side congruence, inequalities involving composite signed orbits could not be moved between balanced representatives, leaving a gap in the certificate's signed-order display obligations.
In the broader Recognition foundation stack, signed-orbit arithmetic is the bridge from the logic-native natural numbers (ArithmeticFromLogic) up toward the real and Cauchy layers. Closing order under multiplication is a prerequisite for treating the phi-ladder and mass-rung arithmetic as well-defined on equivalence classes rather than on raw orbit pairs. The result is pure order algebra; it does not itself invoke J-cost, RCL, or the T0–T8 forcing chain, but it sits on the path that makes those later numeric claims well-typed on integers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.