balanced_symm
plain-language theorem explainer
Symmetry of the signed-orbit balance relation: if two signed orbits balance, so do they in reverse order. Anyone building order, multiplication, or equivalence on PRC integers cites this. The proof is a one-line unfold of the additive equality plus symmetry of propositional equality.
Claim. Let $a,b$ be signed orbits (pairs of distinction naturals, read as $\mathrm{pos}-\mathrm{neg}$). If $a$ and $b$ are balanced, meaning $a_{\mathrm{pos}}+b_{\mathrm{neg}}=b_{\mathrm{pos}}+a_{\mathrm{neg}}$, then $b$ and $a$ are balanced.
background
In the Primitive Recognition Calculus, integers are not primitive. A signed orbit is a pair of distinction naturals (pos, neg) with intended meaning pos - neg (K4.6). Equality of integers is replaced by an internal balance relation on these pairs.
Two signed orbits a and b are balanced when their orbit lengths satisfy a.pos + b.neg = b.pos + a.neg (K4.9). That equation is the PRC stand-in for a = b as integers: rearranging gives a.pos - a.neg = b.pos - b.neg once subtraction is available. The relation is defined entirely on δ-orbit positions, with no appeal to classical ℤ.
The surrounding module builds the integer and rational layer of PRC from orbits and orbit arithmetic. Balance is the kernel of the map to integers and the congruence used by later comparison and arithmetic lemmas.
proof idea
Unfold the definition of balance on both the hypothesis and the goal. The goal becomes the swapped additive equality b.pos + a.neg = a.pos + b.neg. Apply symmetry of equality (Eq.symm) to the hypothesis. No further lemmas are required.
why it matters
Balance must be an equivalence relation before signed orbits can stand in for integers. Symmetry is the first half of that story; it is used immediately by balanced_equivalence and crossEq_symm in the same module.
Downstream, IntegerOrder leans on it heavily: cmp_congr_of_balanced needs both directions of balance to transport comparisons; cmp_negate_swap, the left/right negative-flag multiplication comparison lemmas, recipNonzero_num_zero_cmp, and zero_lt_iff_nonnegFlag_and_not_balanced_zero all invoke symmetry when rearranging balance hypotheses. Without it, the order and sign structure on PRC integers does not close.
In the broader Recognition stack this sits under the foundation forcing chain: ledger balance (equal debit and credit, vanishing recognition cost) is the physical ancestor; here the same idea is formalized at the orbit-arithmetic level that feeds later mass and gap constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.