PRCNormalizeRatioCanonicalTarget_of_reduced_signCanonical_unique
plain-language theorem explainer
Reduced sign-canonical uniqueness for ratio orbits implies that native GCD normalization is canonical on cross-equivalence classes: cross-equivalent raw displays normalize to the same representative. Anyone closing quotient respect for native cost characters cites this reduction. The proof applies the uniqueness hypothesis to the two normalized displays after chaining cross-equivalence through the normalization lemmas.
Claim. Assume that any two reduced, sign-canonical ratio orbits that are cross-equivalent are equal as raw displays. Then for all ratio orbits $q$ and $r$, if $q$ and $r$ are cross-equivalent, their native GCD normalizations coincide: $\mathrm{normalize}(q)=\mathrm{normalize}(r)$.
background
A ratio orbit is an integer numerator over a nonzero distinction-nat denominator: a raw rational display built from signed orbits and the base-neutral finite orbit of repeated distinction. Cross-equivalence is the balanced cross-multiplication relation on those displays; it is symmetric and transitive by the integer-bridge lemmas in the IntegerRational layer.
Native normalization applies a GCD-style reduction and a signed quotient so that the result is reduced and sign-canonical (literally the nonnegative display of its absolute value, or its negation). The upstream fact normalizeRatio_crossEq records that every raw display is cross-equivalent to its normalization; normalizeRatio_reduced_signCanonical records that the image is always reduced and sign-canonical.
The local setting is the Primitive Recognition Calculus native-cost uniqueness development: turning normalized invariance of cost characters into full quotient respect requires exactly that normalization be a canonical section of cross-equivalence classes.
proof idea
Short tactic proof. Fix cross-equivalent $q,r$. Apply the reduced sign-canonical uniqueness hypothesis to $\mathrm{normalize}(q)$ and $\mathrm{normalize}(r)$. The two side conditions are the upstream lemma that every normalization is reduced and sign-canonical. The cross-equivalence hypothesis is assembled by symmetry and transitivity: $q$ is cross-equivalent to its normalization, $q$ is cross-equivalent to $r$, and $r$ is cross-equivalent to its normalization, so the two normalizations are cross-equivalent. Uniqueness then forces the normalizations equal.
why it matters
This is the exact bridge from the remaining raw-display number-theory blocker (reduced sign-canonical uniqueness) to the canonical-normalization target needed for quotient respect of native cost characters. Downstream, the proved form of reduced uniqueness is plugged in to discharge the normalization target outright, and the same reduction feeds the prime-calibration argument that forces character respect for cross-equivalence. Both sit on the path to the native-cost uniqueness blocker certificate in this module.
In the broader Recognition stack, native cost uniqueness is the PRC-side route toward the unique $J$-cost of the forcing chain (T5: $J(x)=(x+x^{-1})/2-1$). Without canonical normalization, cross-equivalent ratio displays could present different raw representatives and break character invariance under the Recognition Composition Law. Closing this reduction removes one structural obstruction between orbit arithmetic and a unique native cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.