balanced_trans
plain-language theorem explainer
Transitivity of the balanced relation on signed orbits: if a balances b and b balances c, then a balances c. Anyone building the integer quotient of δ-orbits cites this as the third Equivalence axiom. The proof rewrites balance to Nat equality of orbit lengths and finishes by linear arithmetic.
Claim. Let $a,b,c$ be signed orbits (pairs of distinction-nats, read as $\mathrm{pos}-\mathrm{neg}$). If $a$ is balanced with $b$ and $b$ is balanced with $c$, then $a$ is balanced with $c$, where balance means $a_{\mathrm{pos}}+b_{\mathrm{neg}}=b_{\mathrm{pos}}+a_{\mathrm{neg}}$.
background
In the Primitive Recognition Calculus, integers are not primitive. A SignedOrbit is a pair of distinction-nats (pos, neg) with intended meaning $\mathrm{pos}-\mathrm{neg}$. Two such pairs represent the same integer when their lengths balance: $a.pos + b.neg = b.pos + a.neg$. That internal relation is the local balanced predicate (K4.9), defined entirely on δ-orbit positions rather than on a pre-existing $\mathbb{Z}$.
The companion lemma balanced_iff_toNat_eq characterises balance by ordinary Nat addition on the underlying toNat values of the four distinction-nats. That characterisation is the bridge from the orbit-level Prop to arithmetic that omega can discharge. The surrounding module builds the rational and order structure on these signed orbits before any continuum or cost functional appears.
proof idea
Term-style tactic proof in two steps. First rewrite the two hypotheses and the goal along balanced_iff_toNat_eq, converting every balanced atom into an equality of Nat sums of toNat projections. The goal is then a pure Nat linear equality; omega closes it. No case splits and no induction.
why it matters
This is the trans field of balanced_equivalence, which packages balanced as an Equivalence on signed orbits. That equivalence is the integer identification relation of the PRC: without transitivity the quotient that plays the role of $\mathbb{Z}$ is not well-defined. Downstream, cmp_congr_of_balanced in IntegerOrder uses balance on both arguments to show the comparison function is invariant, so order descends to the quotient. In the broader Recognition stack this sits in the foundation layer that forces discrete arithmetic before the T0–T8 chain (J-uniqueness, $\varphi$, eight-tick octave, $D=3$) is invoked; it is pure ledger/orbit bookkeeping, not a physics claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.