normalizeRatio_den_mul_gcd_toNat
plain-language theorem explainer
When a rational orbit is reduced by the native GCD of absolute numerator and denominator, the reduced denominator times that GCD recovers the original denominator as ordinary naturals. Anyone proving that ratio normalization preserves the displayed rational value cites this identity. The proof unfolds the normalizer and applies the quotient-times-divisor recovery lemma under the GCD-divides and GCD-nonzero facts.
Claim. For every rational orbit $q$ with signed numerator $n$ and nonzero orbit denominator $d$, let $g=\gcd(|n|,d)$ and let $q'$ be $q$ reduced by dividing both parts by $g$. Then $(\mathrm{den}\,q').\mathrm{toNat}\cdot g.\mathrm{toNat}=d.\mathrm{toNat}$.
background
In the primitive recognition calculus, a RatioOrbit is an integer numerator (signed orbit) over a nonzero orbit denominator: the K4.7 display of a rational. Orbit positions carry a verifier map toNat that reads them as ordinary Lean naturals; signed orbits have an absolute-value map into nonnegative orbit positions.
The module builds an object-level Euclidean algorithm on distinction naturals. The native gcd is defined by subtractive fuelled descent. Upstream, gcd_divides_right states that this GCD divides its right argument, and gcd_ne_zero_of_right_ne_zero keeps the GCD nonzero whenever the denominator is nonzero.
Normalization of a ratio divides numerator and denominator by that GCD. The present identity is the denominator half of the usual cancellation bookkeeping: reduced denominator times GCD equals the original denominator after toNat.
proof idea
Term proof. Unfold the definition of the normalizer so the reduced denominator is the native quotient of $d$ by $g=\gcd(|n|,d)$. Discharge the claim by the already-proved recovery lemma quotient_mul_divisor_toNat_of_divides, instantiated at $n:=d$ and $d:=g$. The two side conditions are exactly gcd_ne_zero_of_right_ne_zero (using q.den_ne_zero) and gcd_divides_right.
why it matters
Feeds the sibling theorem normalizeRatio_toRat, which shows that reducing a rational orbit by its native GCD does not change the displayed rational: the numerator and denominator identities cancel in the fraction. That invariance is the bridge from object-level Euclidean arithmetic on orbits to a well-defined rational value, so later foundation steps can treat reduced ratios as canonical without changing semantics.
Inside Recognition Science this sits in the arithmetic-from-logic layer that underwrites the forcing chain: before J-cost uniqueness (T5), phi, the eight-tick octave, or $D=3$, one needs integers, GCDs, and reduced ratios built only from distinction orbits. The lemma is pure bookkeeping, but it closes the denominator side of that reduction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.