lt_congr_left_of_balanced
plain-language theorem explainer
If two signed orbits represent the same integer (they balance), left-swapping either into a strict comparison leaves the truth value unchanged. Order and arithmetic lemmas that treat balance as congruence cite this. The proof rewrites both sides to integer comparison and substitutes equal displays.
Claim. Let $a$, $a'$, and $b$ be signed orbits. If $a$ and $a'$ are balanced (equivalently $a$ and $a'$ display the same integer), then $a < b$ if and only if $a' < b$.
background
In the Primitive Recognition Calculus, integers are carried by signed orbits: pairs of nonnegative orbit positions (positive and negative limbs). Two signed orbits are balanced when $a.pos + b.neg = b.pos + a.neg$. That internal relation is exactly equality of the conservative integer displays: balanced iff $a.toInt = b.toInt$.
Strict order on signed orbits is defined internally as nonnegative difference with nonzero (non-balanced) difference. The bridge lemma states this matches ordinary integer order: $a < b$ iff $a.toInt < b.toInt$. The present result is the left half of congruence of that order under balance.
The module builds the closed integer-order surface used by the recognition ledger stack: order, comparison, and arithmetic must respect the balance equivalence before certificates can treat signed orbits as $\mathbb{Z}$.
proof idea
Term-mode rewrite proof. Rewrite both sides of the biconditional with the bridge $lt \leftrightarrow toInt,<$. Then rewrite the left display using the forward direction of balanced iff equal integer displays on the balance hypothesis. The two integer inequalities become identical, so the iff is immediate.
why it matters
Balance is the internal integer equality of PRC. Without left-congruence of $<$, later product and difference factor lemmas could not move balanced representatives through comparisons. Downstream, full two-sided congruence composes this with the right-hand twin; comparison congruence and the product/subtraction factor iff lemmas apply it directly. Those feed the integer-order certificate that closes the signed-orbit order surface. In the foundation layer this is bookkeeping for the arithmetic forced from recognition logic, not a physics constant claim, but it is required scaffolding before mass-ladder and forcing-chain material can treat integer order as well-defined on orbit data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.