normalizeRatio_crossEq
plain-language theorem explainer
Any ratio orbit is cross-equivalent to its GCD-normalized form: dividing numerator magnitude and denominator by their native orbit GCD preserves the internal PRC rational relation. Cited wherever reduced representatives must stand in for arbitrary ratio orbits. Proof is a two-line rewrite through the crossEq–toRat bridge and the already-proved equality of rational displays.
Claim. For every ratio orbit $q$ (signed-orbit numerator over a nonzero distinction-nat denominator), the cross-multiplication relation holds between $q$ and its normalized form: if $g=\gcd(|q_{\mathrm{num}}|,q_{\mathrm{den}})$, then $q$ and the orbit with numerator $q_{\mathrm{num}}/g$ and denominator $q_{\mathrm{den}}/g$ satisfy $a_{\mathrm{num}}\cdot b_{\mathrm{den}}=b_{\mathrm{num}}\cdot a_{\mathrm{den}}$ as balanced signed orbits.
background
In the Primitive Recognition Calculus, rationals are not bare ℚ values. A RatioOrbit is a signed-orbit numerator over a nonzero distinction-nat denominator (K4.7). Equality of two such displays is internal: crossEq asserts that the scaled numerators balance as signed orbits (K4.10), i.e. $a.num\cdot b.den$ matches $b.num\cdot a.den$ without leaving the δ-orbit surface.
Normalization runs the Euclidean algorithm on orbit magnitudes. normalizeRatio q takes $g=\gcd(|q.num|,q.den)$, replaces the numerator by the signed quotient and the denominator by the unsigned quotient, and restores orientation via the nonneg flag. The companion lemma normalizeRatio_toRat already shows that the verifier rational is unchanged: $(normalizeRatio,q).toRat=q.toRat$.
The bridge theorem crossEq_iff_toRat_eq equates the internal cross-multiplication relation with ordinary equality of those rational displays. Together these make preservation of crossEq under normalization a one-step consequence.
proof idea
Term-mode, two steps. Rewrite the goal with crossEq_iff_toRat_eq, converting crossEq q (normalizeRatio q) into equality of toRat displays. Discharge by symmetry of normalizeRatio_toRat q, which already proves (normalizeRatio q).toRat = q.toRat. No new arithmetic on orbits is performed here.
why it matters
This is the equivalence half of the Euclidean normalization certificate. Downstream, ratio_normalization_target packages it with the coprimality fact to witness RatioNormalizationTarget: every ratio orbit has a cross-equivalent reduced representative. That bundle feeds the PRC native-cost uniqueness stack.
In PRCNativeCostUniqueness, the lemma is used to show that reduced sign-canonical forms are unique targets under normalization, that identity and reciprocal maps are ratio characters (sanity checks that multiplicative character laws alone do not fix orientation), and that trace-root candidates respect cross-equivalence after normalization. Without crossEq-preservation, reduced representatives could not safely replace arbitrary orbits inside cost and character arguments.
Framework role: this sits in the foundation layer that builds rationals and their Euclidean structure on δ-orbits before cost uniqueness and the forcing chain (T5 J-uniqueness onward) can talk about ratio characters cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.