abs_scaleByNat_eq_zero_iff
plain-language theorem explainer
Absolute value of a signed orbit after scaling by a distinction count is zero exactly when the orbit is already zero or the scale factor is zero. Authors of the integer-order surface and its certificate cite this as the no-zero-divisors law for orbit scaling. The proof rewrites both sides through the toInt isomorphism and applies the LogicInt zero-divisor lemma, then splits cases.
Claim. For every signed orbit $z$ and every distinction count $d$, the absolute value of the scaled orbit satisfies $|z\cdot d|=0$ if and only if $|z|=0$ or $d=0$.
background
In the primitive recognition calculus, integers are realized as signed orbits: a pair of distinction counts (pos, neg) whose difference is the integer value. DistinctionNat is the nonnegative orbit position type; its zero is the unique empty distinction. Absolute value of a signed orbit is the absolute difference of its two legs, again a DistinctionNat.
Scaling multiplies both legs by a DistinctionNat factor: $\mathrm{scale}(z,d)$ has legs $z_+\cdot d$ and $z_-\cdot d$. The companion identity $\mathrm{toInt}(\mathrm{scale}(z,d))=\mathrm{toInt}(z)\cdot d$ links this geometric scaling to ordinary integer multiplication. Absolute value vanishes exactly when the underlying integer is zero.
Upstream, LogicInt (and hence the signed-orbit integers) has no zero divisors: $a\cdot b=0$ forces $a=0$ or $b=0$, forced by the ring isomorphism with $\mathbb{Z}$. The present lemma is the orbit-language packaging of that fact for absolute values under scaling.
proof idea
Rewrite both sides with the characterization that absolute value is zero iff toInt is zero, and replace the scaled toInt by the product identity. The goal becomes $z\cdot d=0$ in $\mathbb{Z}$ iff $z=0$ or $d=0$.
Forward direction: apply the LogicInt no-zero-divisors lemma to the product; the $z$ case is immediate, while the $d$ case is transported back to DistinctionNat zero via injectivity of toNat and the simp fact that toNat of zero is $0$. Reverse direction: case-split on the disjunction and cancel by ring after substituting the zero factor.
why it matters
This is the zero-divisor half of the scaling calculus on signed orbits. Its immediate consumer is the negated form (absolute value of a scaled orbit is nonzero iff both factors are nonzero), obtained by classical negation of the biconditional.
Both feed the integer-order certificate, which closes the internal signed-orbit order surface: nonnegativity flags, absolute-difference displays, and truncated subtraction are all required to be coherent with the underlying integer order. Without a clean zero law for scaling, absolute-value comparisons after multiplication by distinction counts would not be trustworthy.
In the broader Recognition stack this sits in the foundation layer that reconstructs arithmetic and order from distinction orbits before the forcing chain (T5 J-uniqueness through T8 dimension) is applied. It is pure arithmetic infrastructure, not a physics claim, but every later magnitude comparison on the phi-ladder inherits the integrity of this zero law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.