normalizeRatio_toRat
plain-language theorem explainer
GCD-normalization of a ratio orbit leaves its rational display unchanged: the verifier map to ℚ is invariant under canceling the native orbit gcd of absolute numerator and denominator. Cited wherever PRC costs or gauge-orbit native costs must be independent of representative choice. Proof casts the integer/nat gcd scaling identities to ℚ, clears denominators, and rearranges by a short calc chain.
Claim. Let $q$ be a ratio orbit (signed-orbit numerator over a nonzero distinction-nat denominator). Write $\mathrm{normalize}(q)$ for the representative obtained by dividing numerator and denominator by $\gcd(|\mathrm{num}|,\mathrm{den})$ in the native orbit arithmetic. Then the rational displays agree: $\mathrm{toRat}(\mathrm{normalize}(q)) = \mathrm{toRat}(q)$ in $\mathbb{Q}$.
background
Ratio orbits are the K4.7 rational display in the primitive recognition calculus: a signed orbit numerator paired with a nonzero distinction-nat denominator. The map toRat sends such a pair to an ordinary rational by casting the recovered integer numerator and natural denominator. Absolute value on signed orbits is the distinction-nat absolute difference of the positive and negative legs.
This module develops the Euclidean algorithm on distinction nats (div-mod fuel, gcd) and the induced normalization of ratio orbits. Upstream recovery maps toNat and toInt read iteration counts and signed differences out of the logic-built naturals and integers, so all gcd identities can be stated both natively and after casting.
The local goal is representative hygiene: many later cost identities are stated on ratio orbits, but the cost must depend only on the rational class. Denominator nonvanishing after cast (den_cast_ne_zero) is the standing side condition that makes the rational display well-defined.
proof idea
Unfold the rational display. Invoke the two scaling lemmas: normalized numerator times the gcd recovers the original integer numerator, and normalized denominator times the gcd recovers the original natural denominator. Cast both identities to $\mathbb{Q}$.
Record that both the original and normalized denominators remain nonzero in $\mathbb{Q}$. Apply field_simp to clear the rational division, then a four-step calc: substitute the denominator scaling, reassociate, substitute the numerator scaling, and commute factors. Equality of the cleared products is exactly equality of the two rationals.
why it matters
This is the bridge from native Euclidean normalization to rational equality. Immediately downstream, normalizeRatio_crossEq rewrites it as cross-equality of ratio orbits, the relation used throughout cost certificates.
PRCJCost.normalized_invariant quotes it to prove that the PRC cost is unchanged by GCD normalization of the representative. The same identity appears in the reciprocal legs of slim native-cost hypothesis packs: signed-power, sign-gauge, Liouville-twist, and RCL-spike costs all reduce reciprocal invariance to toRat equalities that rely on normalized representatives agreeing in $\mathbb{Q}$.
In the Recognition stack this is bookkeeping under the J-cost layer (T5 uniqueness of $J(x)=(x+x^{-1})/2-1$), not a new physical claim: it guarantees that cost selection and minimality certificates are well-defined on rational classes rather than on raw orbit pairs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.