scaleByNat_balanced_zero_iff
plain-language theorem explainer
Scaling a signed orbit by a distinction-count yields the zero orbit exactly when the original orbit is already zero or the scale factor is zero. Order and certificate authors cite it to control when scaled integers remain nonzero. The proof rewrites balance to integer equality, then applies the no-zero-divisors law on LogicInt.
Claim. For any signed orbit $z$ and distinction count $d$, the scaled orbit $z\cdot d$ is balanced with zero if and only if either $z$ is balanced with zero or $d=0$.
background
In the Primitive Recognition Calculus, integers are carried by signed orbits: pairs of distinction-orbit lengths (pos, neg). Two orbits are balanced when a.pos + b.neg = b.pos + a.neg; that internal relation is the PRC stand-in for integer equality. The bridge theorem balanced_iff_toInt_eq states that balance holds exactly when the conservative toInt displays agree.
scaleByNat multiplies both legs of an orbit by a positive-only distinction count d, so on the integer display it is ordinary multiplication by toNat d. Zero is the orbit with equal legs (display 0). The ambient arithmetic layer already knows that LogicInt has no zero divisors: a * b = 0 forces a = 0 or b = 0, forced by the ring isomorphism with ℤ.
This module builds the order surface on those signed orbits (reflexivity, totality, trichotomy, sign flags). The present lemma is the zero-divisor form specialized to scaling against zero.
proof idea
Term-mode proof. Rewrite the balanced predicate on both sides via balanced_iff_toInt_eq, push scaleByNat through scaleByNat_toInt, and replace zero by zero_toInt. The goal becomes toInt(z) * toNat(d) = 0 ↔ toInt(z) = 0 ∨ d = 0.
Forward: apply mul_eq_zero from IntegersFromLogic; the left disjunct rewrites back to balance of z with zero, the right uses toNat_inj and toNat_zero to recover d = zero.
Backward: case-split the disjunction; each arm substitutes and closes by ring.
why it matters
Feeds the companion scaleByNat_not_balanced_zero_iff (the negated form used when proving strict inequalities survive scaling) and sits inside the closed integer_order_certificate, whose doc states that the internal signed-orbit order surface is closed.
In the Recognition foundation stack, integers and their order are not postulated: they are forced from ledger balance and δ-orbit arithmetic. This lemma is the exact zero-divisor gate that keeps scaled nonzero orbits nonzero, which is required before one can lift nonnegativity flags, trichotomy, and the display bridges that the certificate packages. It is pure foundation arithmetic, not yet a physics forcing step (T5–T8), but it underwrites every later comparison that multiplies by a distinction count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.