mul_ne_zero
plain-language theorem explainer
Nonzero orbit positions multiply to a nonzero orbit position: DistinctionNat has no zero divisors. Anyone proving domain-like facts for recognition arithmetic, or discharging nonzero product side-conditions in cost algebra, cites this. The proof is a short contradiction that pushes the claim through the toNat isomorphism onto ordinary Nat multiplication.
Claim. Let $a,b$ be orbit positions (elements of DistinctionNat). If $a \neq 0$ and $b \neq 0$, then $a \cdot b \neq 0$.
background
OrbitArithmetic equips DistinctionNat (orbit positions from PrimitiveRecognitionCalculus.Orbit) with the usual Peano-style operations, recovered from the recognition step. The bridge to classical arithmetic is the forward map toNat, which reads off the iteration count: identity maps to $0$, and each step increments. Upstream recovery theorems state that this map intertwines multiplication and sends zero to $0$ (toNat_mul, toNat_zero), and that it is injective (toNat_inj).
The local goal is the integral-domain fragment for these positions: products of nonzero positions stay nonzero. A parallel fact already exists for LogicInt (mul_eq_zero), forced by the ring isomorphism with Int; here the same no-zero-divisors property is established directly on DistinctionNat via the Nat bridge.
proof idea
Proof by contradiction. Assume $a \cdot b = 0$. Apply toNat and rewrite with toNat_mul and toNat_zero to obtain toNat(a) * toNat(b) = 0 in Nat. Nat.mul_eq_zero splits into toNat(a) = 0 or toNat(b) = 0. In each branch, toNat_inj plus toNat_zero recovers $a = 0$ or $b = 0$, contradicting the hypotheses. No induction is needed; the work is entirely the isomorphism.
why it matters
Catalogued as K4.7 in the primitive recognition calculus. It is a workhorse side-condition lemma: forty downstream uses, including the foundational RCL identity in CostAlgebra (RCL_holds: "J satisfies the RCL. This is the foundational identity — everything else follows"), where nonzero products of positive arguments must be preserved. The same fact appears in constant-derivation pipelines (curvature numerator/denominator uniqueness at $\pi^5$, $\tau_0^2$ identities, K-gate unit invariance, calibrated-tick injectivity). Without no-zero-divisors on orbit positions, those algebraic rewrites cannot discharge denominator and product nonzero goals. It sits under the arithmetic-from-logic layer that feeds T5 J-uniqueness and the Recognition Composition Law, rather than stating a new physical law itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.