le_antisymm_balanced_cf
plain-language theorem explainer
If two signed orbits satisfy a ≤ b and b ≤ a, they are balanced (equal δ-orbit lengths). This is the choice-free antisymmetry law for the internal SignedOrbit order. Anyone assembling the ratio ordered-field tower without Classical.choice cites it. The proof rewrites both inequalities to ℕ comparisons, then closes by omega on Nat equality.
Claim. Let $a,b$ be signed orbits. If $a \le b$ and $b \le a$ (each meaning the difference is nonnegative), then $a$ and $b$ are balanced: $a_{\mathrm{pos}}+b_{\mathrm{neg}}=b_{\mathrm{pos}}+a_{\mathrm{neg}}$.
background
Signed orbits are the internal PRC stand-in for integers: each carries a positive and a negative δ-orbit position. The order is defined by nonnegativity of the difference: $a \le b$ means $\mathrm{sub},b,a$ is nonnegative. Two orbits are balanced when $a_{\mathrm{pos}}+b_{\mathrm{neg}}=b_{\mathrm{pos}}+a_{\mathrm{neg}}$; that is the internal integer equivalence (K4.9).
The parent IntegerRational module characterizes order via toInt into Mathlib $\mathbb{Z}$, which imports Classical.choice. This module re-grounds every order fact on finite ℕ positions of δ-orbits. The two bridges are balanced_iff_toNat_eq (balanced length is Nat equality) and le_iff_toNat_cf (order is a single Nat inequality on the four toNat coordinates). Forced-floor receipt: axioms stay inside {propext, Quot.sound}.
proof idea
Short tactic proof. Rewrite both hypotheses with le_iff_toNat_cf, so $a \le b$ and $b \le a$ become the pair of Nat inequalities
$b_{\mathrm{neg}}+a_{\mathrm{pos}} \le b_{\mathrm{pos}}+a_{\mathrm{neg}}$ and the swapped form. Rewrite the goal with balanced_iff_toNat_eq, turning balanced into Nat equality of the same four sums. omega discharges the two-sided Nat comparison to equality.
why it matters
Antisymmetry-to-balanced is the last of the four order axioms (refl, trans, total, antisymm) needed before ratios can form an ordered field. The module doc states this choice-free base is exactly what the ratio_* tower requires; without it every downstream rung inherits Classical.choice via toInt.
In the Recognition foundation stack this sits under Primitive Recognition Calculus integer construction: signed orbits are the pre-rational ledger integers, and balanced is the internal equality relation. No downstream consumers are wired yet in the graph (used_by empty), but sibling theorems (le_refl_cf, le_trans_cf, le_total_cf) form the complete choice-free order package. Landmark link is structural rather than T5–T8: clean arithmetic from logic, no choice taint before physics constants are read off.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.