balanced_of_toInt_eq
plain-language theorem explainer
Equal integer displays of two signed orbits imply they are balanced in the PRC sense (cross-sum of pos/neg lengths agree). Used throughout the SignedOrbit divisibility layer (dvdZ refl/trans/add/zero/one). Proof rewrites by the Nat characterization of balance, unfolds toInt, and closes by omega on the resulting Nat equation.
Claim. Let $x,y$ be signed orbits (pairs of distinction-nats read as $\mathrm{pos}-\mathrm{neg}$). If their integer displays agree, $(x_{\mathrm{pos}}^{\mathbb{N}}-x_{\mathrm{neg}}^{\mathbb{N}})=(y_{\mathrm{pos}}^{\mathbb{N}}-y_{\mathrm{neg}}^{\mathbb{N}})$ in $\mathbb{Z}$, then $x$ and $y$ are balanced: $x_{\mathrm{pos}}+y_{\mathrm{neg}}=y_{\mathrm{pos}}+x_{\mathrm{neg}}$.
background
In Primitive Recognition Calculus, a SignedOrbit is a pair of distinction-nats (pos, neg) with intended meaning pos minus neg (K4.6). The display map toInt sends such a pair to an ordinary integer by subtracting the underlying Nats: $\mathrm{toInt}(z)=z.pos.toNat-z.neg.toNat$.
Two signed orbits are balanced when their orbit lengths match under cross-addition: $a.pos+b.neg=b.pos+a.neg$ (K4.9). This is the internal PRC integer-equivalence relation, defined only on $\delta$-orbit positions, not on Lean Int. The companion lemma balanced_iff_toNat_eq rewrites that Prop as equality of Nat sums of the four toNat projections.
This module grows integer divisibility on that carrier. The present direction (equal displays imply balance) is the bridge from ordinary integer arithmetic back into the PRC relation.
proof idea
Short tactic proof. Rewrite the goal with balanced_iff_toNat_eq, so it becomes equality of four Nat sums. Unfold SignedOrbit.toInt in the hypothesis, exposing $(x.pos.toNat:ℤ)-(x.neg.toNat:ℤ)=(y.pos.toNat:ℤ)-(y.neg.toNat:ℤ)$. The linear arithmetic tactic omega closes the Nat form of that equality.
why it matters
This is the workhorse that turns integer equalities into PRC balance witnesses inside the dvdZ layer. Every basic divisibility law in the module uses it: dvdZ_refl, dvdZ_trans, dvdZ_add, one_dvdZ, and dvdZ_zero each refine a witness and discharge the balance obligation via balanced_of_toInt_eq after a mul_toInt/add calculation.
Together with the sibling balanced_toInt_eq (balance implies equal displays), it identifies the PRC balance relation with equality of integer displays on signed orbits. That identification is what lets divisibility, and later ring structure, be grown from distinction-orbit data rather than postulated as Lean Int axioms. It sits in the Foundation forcing path that builds integers from logic before the T0–T8 chain is applied to physics constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.