normalizeRatio
plain-language theorem explainer
Normalizes a rational orbit display to lowest terms: divide numerator magnitude and denominator by their native GCD, then restore the numerator sign. Anyone working with ratio-orbit cost maps or RCL invariance cites it as the canonical reduction. The body is a direct structure construction from the object-level Euclidean GCD and signed quotient.
Claim. Given a rational orbit $q$ with signed numerator $n$ and nonzero orbit denominator $d$, let $g = \gcd(|n|, d)$. The normalized orbit has numerator $\mathrm{sgn}(n)\cdot(|n|/g)$ and denominator $d/g$ (still nonzero).
background
A ratio orbit is the primitive rational display used in the foundation layer: a signed orbit numerator over a nonzero distinction-nat denominator (K4.7). Absolute value of a signed orbit is the orbit position obtained by absolute difference of its positive and negative legs.
The ambient module builds an object-level Euclidean algorithm on distinction nats: subtractive GCD fuel, quotient, and remainder, with divisibility lemmas that mirror ordinary $\mathbb{N}$. In particular the native GCD divides its right argument, and is nonzero whenever the right argument is nonzero. Signed quotient restores orientation after dividing the absolute magnitude.
Local setting is pre-real arithmetic on orbits: no classical rationals yet, only cross-equality and later toRat bridges. Normalization is the orbit analogue of reducing a fraction.
proof idea
Definitional construction, not a tactic proof. Compute $g = \gcd(|n|, d)$; nonzeroness of $g$ follows from the right-input nonzeroness lemma and $d \neq 0$. Pack a new ratio orbit whose numerator is the signed quotient of $n$ by $g$ and whose denominator is the ordinary quotient of $d$ by $g$. Denominator nonzeroness is discharged by the quotient-nonzero-of-divides lemma using that $g$ divides $d$.
why it matters
Canonical reduction for ratio orbits. Downstream, normalizeRatio_crossEq shows the normalized form is cross-equal to the input (same rational value), and normalizeRatio_coprime shows the result is coprime in numerator magnitude and denominator. Multiplicative reconstruction lemmas recover the original num/den after multiplying back by the GCD.
In cost theory, BaseSansTwo requires normalized invariance: a candidate RCL pack $F$ must satisfy cross-equality of $F(q)$ with $F$ of the normalized $q$. Trace-display congruence then descends along cross-equality using that invariance. This is the orbit-level lowest-terms map that lets Recognition Composition Law factorizations ignore redundant common factors before real character work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.