normalizeRatio_coprime
plain-language theorem explainer
After GCD normalization of a ratio orbit, the absolute numerator and the denominator are coprime in the native arithmetic. Cited by anyone packaging reduced ratio representatives for Euclidean orbit certificates or PRC cost uniqueness. The proof transports the claim to ordinary naturals and applies the classical fact that dividing both arguments by their positive gcd yields a coprime pair.
Claim. For every ratio orbit $q$, let $q'$ be the representative obtained by signed division of the numerator and denominator by $\gcd(|q_{\mathrm{num}}|, q_{\mathrm{den}})$. Then $\gcd(|q'_{\mathrm{num}}|, q'_{\mathrm{den}}) = 1$ (equivalently, $|q'_{\mathrm{num}}|$ and $q'_{\mathrm{den}}$ are coprime in the native LogicNat sense).
background
Ratio orbits package a signed numerator with a nonzero denominator in the LogicNat arithmetic of Primitive Recognition Calculus. The Euclidean layer of this module builds gcd and signed quotients on those values, so a ratio can be reduced by dividing both parts by their orbit gcd while staying in the same cross-multiplicative class.
Native coprimality is the module predicate on LogicNat pairs; under the forward map toNat it matches ordinary natural-number coprimality. Because every ratio orbit has nonzero denominator, the gcd is strictly positive on Nat, which is the hypothesis the classical division-by-gcd lemma needs.
The local setting is the closed Euclidean surface on orbits: normalize, prove cross-equality, and prove the reduced pair is coprime, then bundle those facts as a normalization target.
proof idea
Rewrite native coprimality as natural-number coprimality. Unfold the normalizer so the claim is about the absolute numerator and the denominator each divided by the orbit gcd. Transport those quotients across toNat with the signed-quotient absolute-value and quotient lemmas.
Prove the gcd is positive: map to Nat, use positivity of gcd when the right argument is positive, and obtain that positivity from the ratio-orbit denominator invariant (zero denominator would contradict den_ne_zero after toNat injectivity). A second rewrite aligns the gcd with its toNat image. Finish by Mathlib's theorem that $m/\gcd(m,n)$ and $n/\gcd(m,n)$ are coprime whenever the gcd is positive.
why it matters
This is one leg of the ratio-normalization target in the same module: every orbit admits a balanced equivalent representative that is cross-equal and whose absolute numerator is coprime to the denominator. The bundling theorem packages this fact with cross-equality into the Euclidean orbit surface certificate closed in this pass.
Further downstream, PRC native cost uniqueness invokes it to obtain the reduced sign-canonical form of a normalized ratio. That reduced form is the uniqueness surface for recognition cost on rational distinctions, so coprimality after normalization is not cosmetic: without it the cost comparison would still see residual common factors.
In the broader framework this lives in the arithmetic substrate beneath J-cost and the forcing chain, not as a T5–T8 landmark itself. It closes a concrete certificate obligation on the Euclidean orbit calculus that later uniqueness arguments rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.