balanced_toInt_eq
plain-language theorem explainer
Balanced signed orbits display the same integer: if the cross-sum of positive and negative lengths agrees, the verifier map pos−neg yields equal values in ℤ. Used by anyone building divisibility or arithmetic on the PRC integer layer. Proof applies the Nat-level balance characterization, unfolds the difference display, and closes by linear arithmetic.
Claim. Let $x,y$ be signed orbits (pairs of distinction-naturals read as $\mathrm{pos}-\mathrm{neg}$). If they are balanced, meaning $x_{\mathrm{pos}}+y_{\mathrm{neg}}=y_{\mathrm{pos}}+x_{\mathrm{neg}}$, then their integer displays agree: $\mathrm{toInt}(x)=\mathrm{toInt}(y)$, where $\mathrm{toInt}(z)=z_{\mathrm{pos}}^{\mathbb{N}}-z_{\mathrm{neg}}^{\mathbb{N}}$ as an element of $\mathbb{Z}$.
background
In Primitive Recognition Calculus, integers are recovered as signed orbits: a structure with positive and negative distinction-natural components, intended meaning $\mathrm{pos}-\mathrm{neg}$. The verifier display sends a signed orbit to $\mathbb{Z}$ by subtracting the underlying natural values after toNat.
Two signed orbits are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$. Doc-comment K4.9 calls this the internal PRC integer relation, defined entirely on $\delta$-orbit positions. An upstream characterization equates balance with equality of the corresponding Nat-level cross-sums: $a.\mathrm{pos}.\mathrm{toNat}+b.\mathrm{neg}.\mathrm{toNat}=b.\mathrm{pos}.\mathrm{toNat}+a.\mathrm{neg}.\mathrm{toNat}$.
This module sits in the Grow layer that equips those signed orbits with a divisibility relation, importing the integer-rational and integer-order primitives.
proof idea
One short term-mode argument. Take the forward direction of the characterization that balance is equivalent to equality of the four Nat cross-summands, obtaining a pure Nat identity. Unfold the integer display (difference of the two toNat values coerced to $\mathbb{Z}$). The target equality of differences is then immediate from that Nat identity by omega (linear arithmetic on $\mathbb{Z}$).
why it matters
Supports the divisibility theory on signed orbits. Both dvdZ_trans and dvdZ_add obtain a multiplicative or additive witness, then call this lemma to turn each balanced hypothesis into equal integer displays before rebuilding a balanced conclusion via the converse. Without the display equality, the integer-level divisibility relation cannot be shown transitive or closed under addition of multiples.
The result is pure foundation plumbing: it ties the internal balance relation (K4.9) to the ordinary integer display used when PRC integers interface with Lean's $\mathbb{Z}$. It does not itself touch the forcing chain T0–T8, but it is part of the integer recovery that later arithmetic and ladder constructions rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.