balanced_equivalence
plain-language theorem explainer
The balance relation on signed orbits is an equivalence relation: reflexive, symmetric, and transitive. Anyone building integers or rationals from δ-orbit data in the Primitive Recognition Calculus cites this. The proof is a three-field record that installs the already-proved refl, symm, and trans lemmas.
Claim. The relation $\sim$ on signed orbits defined by $a \sim b$ iff $a_{+} + b_{-} = b_{+} + a_{-}$ is an equivalence relation on the type of signed orbits.
background
In the Primitive Recognition Calculus, integers are not postulated; they are recovered from signed orbits. A signed orbit packages a positive δ-orbit length and a negative one. Two signed orbits $a$ and $b$ are declared balanced when the cross-sum identity $a_{+} + b_{-} = b_{+} + a_{-}$ holds. That identity is the internal PRC stand-in for equality of integer values, written entirely in orbit positions rather than in $\mathbb{Z}$.
The surrounding module develops truncated subtraction, absolute difference, and the conversion of signed orbits to integers. Balance is the kernel of that conversion: orbits that balance represent the same integer. Upstream, the same name "balanced" appears for ledgers whose event lists cancel, but here the predicate is the orbit-level relation of K4.9.
proof idea
Term-mode construction of Mathlib's Equivalence structure. The three fields are filled by the sibling lemmas already proved in this module: reflexivity (balanced_refl), symmetry (balanced_symm), and transitivity (balanced_trans). No further arithmetic is done at this site; the record simply certifies that those three properties assemble into a full equivalence.
why it matters
This is the gate that turns the balance predicate into a usable equality-like relation. Downstream, signedOrbitEquiv_equivalence is a one-line alias of this theorem, so every later construction that quotients signed orbits by balance (integer arithmetic, order, absolute value in the K4.13 block) rests on it. In the Recognition foundation stack it sits under the Primitive Recognition Calculus path that builds discrete number structure from δ-orbits before the forcing chain (T5–T8) and the Recognition Composition Law are applied at the continuum level. Without equivalence, the integer quotient would not be well-defined.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.