mul_balanced_zero_iff_of_balanced_left
plain-language theorem explainer
If two signed orbits represent the same integer, then either both products with a third orbit vanish or neither does. Order and zero-detection lemmas in the PRC integer layer cite this to transport nullity under left-factor equivalence. The proof is a short rewrite chain through the toInt bridge and multiplicativity of toInt.
Claim. Let $a,a',b$ be signed orbits. If $a$ is balanced with $a'$ (i.e. $a$ and $a'$ display the same integer), then $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-nats (pos, neg) meant as the difference pos - neg. Two signed orbits are balanced when a.pos + b.neg = b.pos + a.neg; this is the internal integer equality relation, defined only on orbit positions.
The bridge theorem balanced_iff_toInt_eq equates that relation with equality of the conservative integer displays toInt. Multiplication of signed orbits is defined so that toInt is a ring homomorphism: (mul a b).toInt = a.toInt * b.toInt. The zero orbit has toInt = 0.
This module builds the order surface on those signed orbits (reflexivity, totality, trichotomy, sign flags). The present lemma is a left-factor transport fact for the predicate "product is balanced with zero".
proof idea
Term-mode rewrite proof. Rewrite both sides of the goal with balanced_iff_toInt_eq, then apply mul_toInt on each product and zero_toInt on the zero orbit, reducing the claim to a.toInt * b.toInt = 0 ↔ a'.toInt * b.toInt = 0. Rewrite the hypothesis with balanced_iff_toInt_eq to obtain a.toInt = a'.toInt, substitute, and the two sides match.
why it matters
Feeds integer_order_certificate, which packages the closed internal signed-orbit order surface (nonneg display, flag display, truncated subtraction, abs-diff). Without left-factor transport of zero-balance under equivalence, the certificate could not treat balanced orbits as interchangeable when testing product nullity.
In the Recognition foundation this sits under the PRC integer layer that underwrites ledger forcing and the later forcing chain (T0–T8). It is pure algebraic hygiene on the signed-orbit model of ℤ, not a physics claim, but the order certificate it supports is part of the discrete substrate from which continuum structure is later forced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.