gcd_ne_zero_of_right_ne_zero
plain-language theorem explainer
If the second argument of the native orbit GCD is nonzero, the GCD itself is nonzero. Ratio-normalization and reduced-form lemmas cite this to justify dividing by that GCD. The proof reduces to Lean Nat via toNat, applies Nat.gcd_eq_zero_iff, and injects back.
Claim. For base-neutral finite distinction orbits $a,b$, if $b \neq 0$ then $\gcd(a,b) \neq 0$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with zero and successor, the primitive counting object of the Primitive Recognition Calculus. Its verifier display toNat reads the orbit as a Lean natural; that map is injective (toNat_inj), so Nat-level facts transfer back to orbits.
This module builds a Euclidean algorithm on those orbits: native divMod, quotient, remainder, and the recursive gcd (with fuel). The bridge lemma gcd_toNat says the orbit GCD displays as ordinary Nat.gcd of the displays. The present result is the non-vanishing half of that bridge when the right argument is nonzero.
Local setting is the Euclidean layer on orbits, imported from IntegerRational and OrbitDivisibility, feeding ratio normalization rather than classical number theory for its own sake.
proof idea
Contradiction on gcd a b = zero. Rewrite with toNat_zero to get (gcd a b).toNat = 0, then gcd_toNat yields Nat.gcd a.toNat b.toNat = 0. Mathlib's Nat.gcd_eq_zero_iff forces b.toNat = 0. Injectivity toNat_inj plus toNat_zero recovers b = zero, contradicting the hypothesis. Pure transport: no orbit-level induction.
why it matters
Native ratio reduction needs a nonzero divisor. Downstream, normalizeRatio divides numerator magnitude and denominator by gcd q.num.abs q.den and packages the non-vanishing proof obligation with this theorem (have hg : g ≠ zero := gcd_ne_zero_of_right_ne_zero ... q.den_ne_zero). The companion identities normalizeRatio_den_mul_gcd_toNat and normalizeRatio_num_mul_gcd_toInt then recover the original components after scaling.
Further up, normalizeRatio_reduced_signCanonical in PRCNativeCostUniqueness uses the normalized form to assert coprimality plus sign-canonical numerator, the reduced representative needed for uniqueness of native cost on ratios. In the Recognition stack this is scaffolding arithmetic under the forcing chain, not a physics landmark itself: it keeps orbit GCD safe so phi-ladder and J-cost constructions can treat reduced ratios without a zero-denominator hole.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.