lt_of_product_factors_iff_of_balanced
plain-language theorem explainer
If two pairs of signed orbits are balanced (integer-equivalent), strict inequality against a fixed third orbit is invariant under replacing either factor of a product. Anyone assembling the internal integer order from δ-orbits cites this. The proof is a one-line term composition of multiplicative balanced-congruence with right-congruence of strict order.
Claim. Let $a,a',b,b',c$ be signed orbits. If $a$ is balanced with $a'$ and $b$ is balanced with $b'$ (i.e. $a_{+} + a'_{-} = a'_{+} + a_{-}$ and likewise for $b,b'$), then $c < a\cdot b$ if and only if $c < a'\cdot b'$.
background
In the Primitive Recognition Calculus, integers are carried by signed orbits: pairs of δ-orbit positions (pos, neg). Two signed orbits are balanced when their lengths match crosswise, $a_{+} + b_{-} = b_{+} + a_{-}$; this is the internal integer equality, defined entirely on orbit positions (K4.9).
Strict order on signed orbits is the conjunction of the weak order with failure of balance: $a < b$ means $a \le b$ and $\neg,\mathrm{balanced}(a,b)$. Multiplication of signed orbits is the ring product induced on these pairs; the companion lemma mul_congr_of_balanced shows that balanced factors yield a balanced product.
The local module builds the full order surface (reflexivity, totality, trichotomy, sign flags) needed before the integer-order certificate can close.
proof idea
One-line term proof. First apply multiplicative congruence: balanced factors $a\sim a'$ and $b\sim b'$ imply the products are balanced, $\mathrm{mul}(a,b)\sim\mathrm{mul}(a',b')$. Then feed that witness into right-congruence of strict order: if the right-hand sides are balanced, $c < x$ iff $c < x'$. The composite is exactly the claimed biconditional.
why it matters
This lemma is a congruence step on the path to integer_order_certificate, which asserts that the internal signed-orbit order surface is closed (display lemmas for truncated subtraction, $\le$, absolute difference, and nonnegativity flags all line up). Without product-factor invariance of $<$, the order would not descend cleanly to the balanced quotient that represents $\mathbb{Z}$.
In the broader Recognition stack this sits inside Foundation arithmetic: integers forced from ledger/δ-orbit structure rather than postulated. It does not itself touch the T0–T8 forcing chain, but it is part of the arithmetic substrate those later steps assume when they speak of integer ranks, rungs, and the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.