balanced
plain-language theorem explainer
Two signed orbits represent the same integer precisely when their positive and negative lengths cross-balance: a.pos + b.neg equals b.pos + a.neg. This is the internal equivalence of the PRC integer construction, stated entirely on δ-orbit positions. Anyone building integers or rationals from recognition orbits cites it. The body is a one-line Prop definition, the classical pair-equivalence for differences.
Claim. Two signed orbits $a=(a_+,a_-)$ and $b=(b_+,b_-)$ (each a pair of distinction-natural lengths, intended as $a_+-a_-$) are balanced when $a_+ + b_- = b_+ + a_-$. Balanced pairs are the internal equivalence relation of the primitive recognition calculus integer construction.
background
In the primitive recognition calculus, integers are not postulated. A signed orbit is a pair of distinction-natural lengths (pos, neg), with intended meaning pos - neg (K4.6). Distinction naturals themselves arise as orbit lengths under the δ-dynamics, so the whole construction stays inside recognition data.
The classical construction of ℤ from ℕ uses pairs with (a,b) ~ (c,d) iff a+d = b+c. Here the same relation is written on signed orbits: balance means the two differences agree. The module sits in the Foundation layer that builds integers and rationals from logic and orbit arithmetic, importing orbit structure and orbit arithmetic before defining this relation.
Upstream, the same pattern appears as negation on logic integers (-(a,b)=(b,a)) and as ledger balance on event lists. Those are parallel balance notions; this definition is the PRC-native version on δ-orbit positions only.
proof idea
Definition, not a theorem. The body is the single equality a.pos + b.neg = b.pos + a.neg as a Prop on two SignedOrbit values. No tactics, no lemmas applied. Downstream proofs treat it as the equivalence (or the kernel) of the map that sends a signed orbit to its integer value via toInt.
why it matters
K4.9 in the PRC integer ladder: without this balance relation there is no well-defined integer from orbit differences, and no path to rationals-from-logic. It is heavily reused (dozens of use sites).
Downstream it feeds symplectic cost work: the calibrated trace cost vanishes on the balanced σ = 0 ground state, and jcost_forced_by_symplectic_action closes the bridge from area-preserving ledger action to the unique recognition cost J (T5). Circle-winding and chain ℓ¹ arguments use the same balance language for free-boundary-zero flows. Cosmology side, Sakharov-from-ledger structures that permit multi-axis rotations sit on balanced ledger data.
In the forcing chain this is infrastructure under integers and ledgers, not a T-step itself, but it is what makes the σ = 0 balanced ground state and the RCL-facing cost uniqueness statements speak the same language as PRC orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.