mul_balanced_zero_iff_of_balanced
plain-language theorem explainer
If two pairs of signed orbits are balanced (same integer display), their products are zero in the balanced sense exactly when each other is. Anyone building the internal integer order or zero-product rules on δ-orbits cites this. The proof is a short rewrite chain through the toInt bridge and multiplicativity of toInt.
Claim. Let $a,a',b,b'$ be signed orbits. If $a$ is balanced with $a'$ and $b$ is balanced with $b'$, then the product $a\cdot b$ is balanced with zero if and only if $a'\cdot b'$ is balanced with zero.
background
In the Primitive Recognition Calculus, a signed orbit is a pair of distinction naturals (pos, neg) meant as the difference pos - neg. Two signed orbits are balanced when a.pos + b.neg = b.pos + a.neg; that internal relation is the PRC integer equivalence on δ-orbit positions (K4.9).
The bridge to ordinary integers is balanced_iff_toInt_eq: balanced holds exactly when the conservative toInt displays agree. Multiplication of signed orbits is defined so that toInt is a ring homomorphism: (mul a b).toInt = a.toInt * b.toInt, and the zero orbit has toInt = 0.
This module develops the order surface on those signed orbits (reflexivity, totality, trichotomy, sign flags). The present lemma is the zero-product stability of the balanced relation under replacement by balanced partners.
proof idea
Term-mode rewrite proof. Both sides of the goal are rewritten with balanced_iff_toInt_eq, then mul_toInt on each product and zero_toInt, so the claim becomes (a.toInt * b.toInt = 0) ↔ (a'.toInt * b'.toInt = 0). The hypotheses are rewritten the same way to a.toInt = a'.toInt and b.toInt = b'.toInt, then substituted. No case split or omega is needed once the displays match.
why it matters
Feeds integer_order_certificate, which packages the closed internal signed-orbit order surface (nonneg display, flag display, truncated subtraction, and related leq facts). Without product-zero stability under balanced replacement, the certificate could not treat zero as a well-defined class on the PRC integer quotient.
In the foundation layer this is bookkeeping for the integer model built from distinction orbits before the forcing chain (T5–T8) and the Recognition Composition Law are applied at the continuum level. It does not itself force φ, the eight-tick octave, or D = 3; it keeps the discrete integer order coherent so later recognition calculus can sit on a certified ℤ-like surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.