lt_congr_of_balanced
plain-language theorem explainer
Strict order on signed orbits is invariant under balanced replacement of either argument: if a ~ a' and b ~ b' in the balanced sense, then a < b if and only if a' < b'. Anyone proving that integer comparisons, products, or differences are well-defined on balanced classes will cite this. The proof is a one-line transitivity of the left and right congruence lemmas.
Claim. For signed orbits $a,a',b,b'$, if $a$ is balanced with $a'$ and $b$ is balanced with $b'$, then $a < b$ if and only if $a' < b'$.
background
In the primitive recognition calculus, integers are carried by signed orbits rather than by a bare verifier display. The strict order on those orbits is the internal comparison used throughout the IntegerOrder development; sibling facts already give reflexivity, transitivity, antisymmetry on balanced pairs, totality, and trichotomy.
Balanced is the equivalence that identifies two signed orbits as the same integer (same ledger balance / same displayed value). The module builds order and arithmetic so that they descend to these classes. Upstream, the left- and right-hand congruence lemmas already state that replacing one side of a strict comparison by a balanced partner preserves the comparison; this declaration packages both sides at once.
The surrounding certificate work treats the signed-orbit order surface as closed once nonnegativity flags, truncated subtraction, and absolute difference all match the integer display.
proof idea
Term-mode one-liner. Apply left congruence under the balanced hypothesis on the first pair to rewrite $a < b$ as $a' < b$, then right congruence under the second balanced hypothesis to rewrite that as $a' < b'$. Compose the two iff steps with Iff.trans. No new case analysis.
why it matters
This is the two-sided well-definedness fact for strict order on balanced classes. Downstream it feeds the integer-order certificate ("the internal signed-orbit order surface is closed") and the product and subtraction congruence theorems: lt_products_iff_of_balanced, lt_subtractions_iff_of_balanced, and the nonzero orbit-multiplication monotonicity iff lemmas. Without two-sided order congruence, those arithmetic comparisons could not safely replace representatives. In the Recognition foundation stack this sits under the arithmetic-from-logic and ledger-forcing layer that eventually supports the forcing chain's discrete structure, not a physics constant claim itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.