quotient_ne_zero_of_divides
plain-language theorem explainer
If a nonzero distinction orbit d divides a nonzero orbit n, the native Euclidean quotient n/d is nonzero. Factorization and signed-ratio normalization cite this to keep reduced numerators and factors off the zero orbit. The proof is a short contradiction through the toNat bridge: a zero quotient would force n = 0 in Nat, hence n = zero.
Claim. Let $n,d$ be finite distinction orbits with $d \neq 0$ and $n \neq 0$. If $d$ divides $n$ in the native orbit sense, then the Euclidean quotient of $n$ by $d$ is not the zero orbit.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction: an inductive copy of the naturals with constructors zero and succ. Division and gcd live on this type in the Euclidean layer of Primitive Recognition Calculus, not on Lean Nat directly.
The verifier map toNat reads an orbit as an ordinary natural (iteration count). Sibling lemmas already connect the native quotient to Nat arithmetic: when $d$ divides $n$, toNat(n) = toNat(quotient(n,d)) \cdot toNat(d). The predicate divides d n is the native divisibility relation from the orbit-divisibility module.
Local setting is the Euclidean algorithm on orbits: divMod, quotient, remainder, and later native GCD, used to normalize ratios and extract factors without leaving the recognition calculus.
proof idea
Proof by contradiction. Assume the quotient equals zero. Rewrite with toNat_zero to get toNat(quotient) = 0.
Invoke the sibling identity quotient_mul_divisor_toNat_of_divides: under divisibility, toNat(n) equals the product of the quotient and divisor in Nat. Substitute the zero quotient and Nat.zero_mul to conclude toNat(n) = 0.
Apply toNat_inj (injectivity of the orbit-to-Nat map) together with toNat_zero to obtain $n = zero$, contradicting the hypothesis $n \neq zero$.
why it matters
Keeps native quotients off the zero orbit whenever both arguments are nonzero and divisibility holds. That is the arithmetic hygiene step for reduced forms and nontrivial factors.
Downstream, normalizeRatio divides numerator magnitude and denominator by their native GCD; this lemma (with the GCD nonzero facts) ensures the reduced denominator quotient is nonzero. nontrivialFactorization_of_proper_divisor uses the same guarantee so a proper nonunit divisor yields a genuine nontrivial factorization for period-readout factoring. signedQuotient_signCanonical_of_divides relies on the unsigned quotient being well-behaved when building signed quotients.
In the Recognition stack this sits in the foundation arithmetic layer that underwrites later cost uniqueness and chart transitions, not yet at the T5–T8 forcing landmarks, but as infrastructure those layers consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.