sub_balanced_zero_iff_of_balanced
plain-language theorem explainer
If two pairs of signed orbits are balanced-equivalent, their differences are zero (balanced against the zero orbit) under exactly the same condition. Order and certificate lemmas cite this to transport vanishing of a−b across the PRC integer equivalence. The proof is a one-line specialization of the general balanced-sub-inputs iff at the zero orbit.
Claim. Let $a,a',b,b'$ be signed orbits. If $a$ is balanced-equivalent to $a'$ and $b$ is balanced-equivalent to $b'$, then $a-b$ is balanced-equivalent to the zero orbit if and only if $a'-b'$ is balanced-equivalent to the zero orbit.
background
In the Primitive Recognition Calculus, a signed orbit is a pair of distinction-natural lengths (pos, neg), read as the formal difference pos − neg. Two signed orbits are balanced-equivalent when their lengths satisfy the internal integer relation a.pos + b.neg = b.pos + a.neg (K4.9): the orbit lengths cancel in the same way on both sides.
Subtraction of signed orbits is the corresponding difference operation on those pairs. Balancing against the zero orbit is the internal statement that a difference vanishes as an integer. The surrounding IntegerOrder module builds the order surface (nonnegativity flags, trichotomy, certificates) entirely on these δ-orbit positions, without external ℤ.
The immediate upstream result is the general transport law: if a ∼ a' and b ∼ b', then a − b ∼ c iff a' − b' ∼ c for any third signed orbit c. That lemma reduces via the characterization of balance by equality of the underlying integer values.
proof idea
One-line term wrapper. Instantiate the general theorem balanced_sub_inputs_iff_of_balanced at the third argument c := SignedOrbit.zero, feeding the two balance hypotheses on the input pairs. No extra rewriting is needed at this site.
why it matters
Vanishing of differences is the zero test for the internal signed-orbit order. This specialization packages that test so later lemmas can move “a−b is zero” across balanced representatives without reopening the toInt characterization.
It is used immediately by the negated form sub_not_balanced_zero_iff_of_balanced (rewrite of this iff) and feeds the closed order surface assembled in integer_order_certificate (“The internal signed-orbit order surface is closed”). That certificate is part of the foundation layer that underwrites discrete integer structure before the forcing chain (T0–T8) and the Recognition Composition Law are applied at the continuum level.
No open scaffold: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.