normalizeRatio_num_mul_gcd_toInt
plain-language theorem explainer
For a ratio orbit, the integer display of the gcd-normalized numerator, times the gcd of absolute numerator and denominator, recovers the original numerator as an integer. Cited by anyone showing that orbit-ratio reduction preserves the displayed rational. Proof unfolds the normalizer and applies the signed-quotient recovery lemma under gcd-divides-left and gcd-nonzero.
Claim. For every ratio orbit $q$ (signed-orbit numerator $n$ over nonzero distinction-nat denominator $d$), writing $g=\gcd(|n|,d)$, the integer display of the numerator of the gcd-normalized form of $q$, multiplied by the natural value of $g$ cast to $\mathbb{Z}$, equals the integer display of $n$.
background
In the primitive recognition calculus, rationals are displayed as ratio orbits: a signed orbit numerator over a nonzero distinction-nat denominator (K4.7). The integer display of a signed orbit is the difference of the natural values of its positive and negative legs. Absolute value collapses a signed orbit to a distinction-nat by absolute difference of those legs.
The ambient module develops the Euclidean algorithm on distinction-nats: division-with-remainder, then a fuelled gcd, with the usual divisibility facts (gcd divides each argument; gcd is nonzero when the right argument is). Normalization of a ratio orbit divides numerator and denominator by that gcd, using a signed quotient on the numerator side so the sign of $n$ is preserved.
The companion recovery fact needed here is that if a distinction-nat divisor divides the absolute value of a signed orbit, the signed quotient times the divisor recovers the original signed integer display.
proof idea
Term proof. Unfold the definition of the normalizer so the left-hand numerator becomes the signed quotient of $q$'s numerator by $\gcd(|n|,d)$. Discharge the claim by the upstream recovery lemma signedQuotient_mul_divisor_toInt_of_divides, feeding: the numerator, that gcd, nonzeroness of the gcd (from the denominator nonzero hypothesis via gcd_ne_zero_of_right_ne_zero), and left-divisibility (gcd_divides_left).
why it matters
This is the numerator half of the bookkeeping that makes gcd-reduction of ratio orbits well-defined on displayed rationals. The sole recorded consumer is normalizeRatio_toRat, which combines this identity with the matching denominator identity to conclude that the normalized form has the same rational display as the input.
In the Recognition foundation stack, ratio orbits sit above integers-from-logic and distinction-nats-from-orbits; Euclidean normalization is the bridge from raw ratio displays to reduced representatives. Without this recovery identity, the later claim that reduction does not change the rational value has no numerator step. It is pure arithmetic scaffolding inside the forcing chain's number layer, not a physics landmark (T5–T8), but it is required before mass-ladder or constant displays can sit on a clean rational substrate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.