abs_mul_ofOrbit_right_eq_zero_iff
plain-language theorem explainer
Absolute value of a signed orbit times a nonnegative orbit embedding vanishes exactly when the signed orbit is zero or the embedded position is zero. Order and integrality arguments on signed orbits cite this as the right-multiplication zero-divisor law for absolute values. The proof reduces absolute values to integer images, then applies the no-zero-divisors property of the logic integers.
Claim. For every signed orbit $z$ and every distinction-natural $d$, $\lvert z \cdot \iota(d)\rvert = 0$ if and only if $\lvert z\rvert = 0$ or $d = 0$, where $\iota(d)$ is the nonnegative signed orbit with positive part $d$ and negative part $0$.
background
Signed orbits are the internal model of integers in the primitive recognition calculus: each carries a positive and a negative distinction-natural coordinate. Absolute value is the orbit-position distance between those coordinates, absDiff. The embedding ofOrbit builds a nonnegative signed orbit from a single distinction-natural by pairing it with zero on the negative side.
Multiplication of signed orbits is defined so that the integer image is a ring homomorphism: (mul a b).toInt = a.toInt * b.toInt. Absolute value vanishes exactly when that integer image is zero. Upstream, LogicInt (and thus the integer image) has no zero divisors: a * b = 0 forces a = 0 or b = 0, forced by the ring isomorphism with ordinary integers.
The local module develops the order surface on these signed orbits (reflexivity, totality, trichotomy, sign flags). This lemma is the absolute-value form of right-multiplication by a nonnegative embedding having no unexpected zeros.
proof idea
Term-mode rewrite chain, then a two-sided constructor. First rewrite both absolute-value zeros into integer-image zeros via abs_eq_zero_iff_toInt_eq_zero, push multiplication through mul_toInt, and evaluate the embedding with ofOrbit_toInt. The goal becomes z.toInt * (d.toNat : ℤ) = 0 ↔ z.toInt = 0 ∨ d = 0.
Forward direction: apply mul_eq_zero on the logic integers; the left disjunct is immediate, the right is transported back to distinction-naturals by toNat_inj and toNat_zero. Reverse direction: case-split on the disjunction and finish each arm by rewriting the zero factor and ring.
why it matters
Feeds the complementary non-vanishing form abs_mul_ofOrbit_right_ne_zero_iff, which packages the same fact as a conjunction of nonzero hypotheses. That pair is part of the scaffolding that closes integer_order_certificate: "the internal signed-orbit order surface is closed."
In the Recognition foundation stack, integers and their order are not postulated; they are reconstructed from distinction orbits and logic. A clean absolute-value zero law for multiplication by nonnegative embeddings is required before signed comparison, sign flags, and truncated subtraction can be certified as a coherent order. Without it, the certificate's signed-nonnegativity displays would not sit on a domain free of zero-divisor pathologies.
This is pure foundation arithmetic, not a forcing-chain landmark (T5–T8), but it underwrites the integer layer those later physics steps assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.