balanced_refl
plain-language theorem explainer
Every signed orbit balances with itself under the PRC integer relation a.pos + b.neg = b.pos + a.neg. Anyone constructing the integer quotient, cross-equality of ratios, or zero tests on signed orbits cites this reflexivity. The proof unfolds the balance predicate and closes by commutativity of DistinctionNat addition.
Claim. For every signed orbit $a=(a_+,a_-)$ (intended meaning $a_+-a_-$), the balance relation holds of the pair $(a,a)$: $a_+ + a_- = a_+ + a_-$. Equivalently, $a\sim a$ where $a\sim b$ means $a_+ + b_- = b_+ + a_-$.
background
In the Primitive Recognition Calculus, integers are not postulated; they are assembled from finite distinction orbits. DistinctionNat is the base-neutral inductive type of repeated distinction (zero / succ). A SignedOrbit is a pair (pos, neg) of such orbits, read as the formal difference pos − neg (K4.6).
Two signed orbits represent the same integer when their lengths balance: balanced a b is the proposition a.pos + b.neg = b.pos + a.neg (K4.9), stated entirely on δ-orbit positions. This is the internal equivalence used before quotienting to PRC integers.
Addition on DistinctionNat is commutative (inherited from the logic-nat development via OrbitArithmetic). Reflexivity of balance is the first Equivalence law needed to treat signed orbits as integer data.
proof idea
Short tactic proof. Unfold balanced on the diagonal pair (a,a), exposing the equation a.pos + a.neg = a.pos + a.neg. Rewrite with DistinctionNat.add_comm so both sides match under the commutative law for orbit addition; the goal closes.
No induction and no case split: pure definitional expansion plus one commutativity rewrite.
why it matters
This is the refl leg of balanced_equivalence, which packages balance as a full Equivalence on signed orbits and thereby licenses the PRC integer quotient. Downstream, crossEq_refl reduces ratio cross-equality on the diagonal to this fact; isZero_zero, and the well-definedness obligations around add and mul, invoke it when comparing a constructed orbit to itself.
In IntegerOrder it appears inside reciprocal flag lemmas (recip_num_balanced_zero_iff, nonneg/negative flag characterizations), where zero-tests and sign tests are phrased as balance against SignedOrbit.zero. Within the Recognition foundation stack it is bookkeeping for K4 (orbit arithmetic → integers → rationals), not a forcing-chain step (T5–T8), but without it the integer layer cannot be an equivalence relation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.