balanced_iff_toInt_eq
plain-language theorem explainer
Two signed orbits are balanced (cross-sums of positive and negative orbit lengths agree) exactly when their integer displays coincide in ℤ. Anyone working the Primitive Recognition Calculus integer layer cites this to pass between the internal δ-orbit relation and ordinary integer equality. The proof rewrites to the Nat-level balance characterization, unfolds the difference display, and finishes each implication by linear arithmetic.
Claim. For signed orbits $a=(a_+,a_-)$ and $b=(b_+,b_-)$, the internal balance relation $a_++b_-=b_++a_-$ holds if and only if the verifier displays agree: $a_+^{\mathbb{N}}-a_-^{\mathbb{N}}=b_+^{\mathbb{N}}-b_-^{\mathbb{N}}$ as elements of $\mathbb{Z}$.
background
In the Primitive Recognition Calculus, integers are recovered rather than assumed. A signed orbit is a pair $(pos,neg)$ of distinction-orbit lengths, with intended meaning $pos-neg$. Two signed orbits are internally equivalent when they balance: $a.pos+b.neg=b.pos+a.neg$. That relation is stated entirely on δ-orbit positions, with no reference to $\mathbb{Z}$.
The verifier display sends a signed orbit to an ordinary integer by subtracting the underlying natural numbers: $\mathrm{toInt}(z)=z.pos.\mathrm{toNat}-z.neg.\mathrm{toNat}$. An upstream lemma already characterizes balance at Nat level: balance holds exactly when the corresponding four-term Nat sums agree. The present result lifts that characterization to the integer display.
The local setting is K4.6–K4.9 of the foundation layer that builds integer arithmetic from recognition structure before later forcing steps introduce physical constants.
proof idea
Rewrite the goal with the Nat-level characterization, so the left-hand side becomes equality of the four-term Nat sums. Unfold the integer display to differences of those Nats. Split the biconditional into two implications and discharge each by linear arithmetic (omega) on the relation between the Nat sums and the two integer differences. The split is intentional: omega on a bare iff goal would introduce classical choice, while the per-direction form stays choice-free.
why it matters
Doc-comment K4.9 calls this the bridge from the internal PRC balance relation to the conservative $\mathbb{Z}$ view. Downstream, IntegerOrder routes absolute-value transport through it: absolute values agree under balance, vanish exactly on orbits balanced with zero, and are preserved by multiplication when factors are replaced by balanced partners. Comparison and zero-tests in that module are defined from balance and signed-orbit order, not from the display; this lemma is what lets those internal facts talk to ordinary integer arithmetic when needed.
In the broader Recognition foundation it sits among the results that recover $\mathbb{Z}$ from logic and recognition structure, prior to the T0–T8 forcing chain that fixes $J$, $\varphi$, the eight-tick octave, and $D=3$. It does not itself force physics constants; it closes the integer-display bridge those later steps rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.