balanced_iff_toNat_eq
plain-language theorem explainer
Two signed orbits are balanced exactly when the natural numbers on their opposite legs satisfy the cross-sum equality that encodes equal integer values. Grow-layer order, divisibility, and ratio-orbit lemmas cite this as the Nat rewrite of the internal balanced relation. The proof is a short bidirectional transport through additivity and injectivity of the iteration-count map.
Claim. For signed orbits $a=(a_+,a_-)$ and $b=(b_+,b_-)$ (pairs of distinction naturals, intended as $a_+-a_-$), the balanced relation holds if and only if $a_+^{\mathbb{N}}+b_-^{\mathbb{N}}=b_+^{\mathbb{N}}+a_-^{\mathbb{N}}$, where $(\cdot)^{\mathbb{N}}$ is the forward iteration-count map from distinction naturals into $\mathbb{N}$.
background
In the Primitive Recognition Calculus, a signed orbit is a pair of distinction naturals (pos, neg) with intended meaning pos - neg. Distinction naturals carry addition recovered from logic-level step iteration; the map that reads off the iteration count is a monoid homomorphism into ordinary Nat (the recovery theorem for addition).
Balanced on two signed orbits is the internal equality saying their difference legs match after cross-addition at the distinction-natural level. The module builds integer and rational displays on these orbits so later growth and order arguments can drop into conservative ℤ and ℚ reasoning.
Upstream, the addition-recovery theorem states that distinction-natural addition agrees with Nat addition under the iteration-count map, and injectivity of that map lets equalities travel both ways. Logic-integer negation swaps pair components, the same bookkeeping signed orbits use.
proof idea
Unfold the definition of balanced. Forward direction: from a distinction-level equality of sums, apply the iteration-count map via congruence and rewrite both summands by the addition-recovery theorem. Converse: apply injectivity of the iteration-count map, rewrite both sides again by addition recovery, and feed in the assumed Nat equality. Pure term-mode bidirectional constructor; no induction.
why it matters
K4.9 is the bridge from the internal PRC balanced relation to the conservative integer display. Downstream, the two IntegerDivisibility lemmas convert between balanced pairs and equal integer displays by rewriting through this characterization plus a short linear-arithmetic step. Order lemmas in the Grow layer (left and right congruence under a balanced twin, product and nonneg-flag variants) use it to replace one side of a comparison without changing truth value.
Ratio-orbit density and positivity arguments likewise reduce cross-equality and strict order to Nat arithmetic via this rewrite. Within the Recognition foundation this sits in the arithmetic-from-logic layer that underwrites ledger balance and integer displays, not a T0–T8 landmark itself; it closes the Nat-level characterization needed before signed-orbit order is choice-free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.