le_antisymm_balanced
plain-language theorem explainer
Antisymmetry for the internal signed-orbit order: mutual non-strict inequality forces the two orbits to be balanced (same integer display). Anyone building or citing the PRC integer-order surface will use it. The proof rewrites both sides through the toInt bridges and finishes by omega on ℤ.
Claim. Let $a,b$ be signed orbits. If $a \le b$ and $b \le a$ in the internal order (nonnegative difference), then $a$ and $b$ are balanced: $a.pos + b.neg = b.pos + a.neg$, equivalently $a$ and $b$ display the same integer.
background
In Primitive Recognition Calculus, integers are carried by signed orbits: pairs of δ-orbit lengths (pos, neg) rather than bare ℤ. The internal order is defined by le a b := nonneg (sub b a), i.e. the difference is a nonnegative orbit. Two orbits are balanced when a.pos + b.neg = b.pos + a.neg (K4.9): the internal equivalence that plays the role of equality of integers.
Two display bridges connect this language to ordinary integers: le_iff_toInt_le says internal order matches toInt order on ℤ, and balanced_iff_toInt_eq says balance matches equality of toInt. The module builds the order laws (refl, trans, antisymm, total, trichotomy) on that surface so the certificate can close without smuggling classical ℤ structure into the core definitions.
proof idea
Term/tactic hybrid, three steps. Rewrite both hypotheses with SignedOrbit.le_iff_toInt_le, so hab and hba become a.toInt ≤ b.toInt and b.toInt ≤ a.toInt. Rewrite the goal with SignedOrbit.balanced_iff_toInt_eq, turning balance into a.toInt = b.toInt. Close by omega on those two integer inequalities. No case splits and no classical choice; the bridges already did the structural work.
why it matters
Feeds integer_order_certificate, whose doc states the internal signed-orbit order surface is closed. Antisymmetry is the missing partial-order axiom once refl and trans are in place; without it the certificate cannot claim a genuine order. In the Recognition stack this sits under Foundation / Primitive Recognition Calculus: integers and their order are forced from δ-orbit bookkeeping before arithmetic and ledger forcing are used higher up. It does not itself touch T5–T8 or the J-cost, but it is part of the integer substrate those later forcing steps assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.