PRCNormalizeRatioCanonicalTarget_proved
plain-language theorem explainer
Cross-equivalent ratio orbits share one native GCD-normalized raw representative. Anyone showing that character displays, doubled traces, or structural costs respect the ratio quotient cites this uniqueness. The proof is a one-line term application of uniqueness already established on reduced sign-canonical forms.
Claim. For all ratio orbits $q,r$, if $q$ and $r$ are cross-equivalent (same rational display up to the native equivalence), then native GCD normalization returns the same raw representative: $\mathrm{normalize}(q)=\mathrm{normalize}(r)$.
background
In the Primitive Recognition Calculus, ratio orbits are the raw integer-pair displays of positive rationals (numerator, denominator, denominator nonzero). Cross-equivalence identifies orbits that present the same rational value. Native normalization applies a GCD reduction (and a fixed sign convention) so each orbit class has a preferred raw representative.
The target proposition states exactly that this normalization is constant on cross-equivalence classes: if two raw displays are cross-equivalent, their normalized forms are definitionally equal as raw orbits, not merely equal after further quotienting. The module doc framing is native-cost uniqueness: one must pass from invariants stated on already-normalized data to full quotient respect for characters and costs.
Upstream, uniqueness is first proved on the narrower class of reduced sign-canonical representatives (orbits that are already GCD-reduced and literally nonnegative or literally negated-nonnegative). A reduction lemma then lifts that uniqueness to arbitrary orbits by observing that normalization always lands in the reduced sign-canonical class.
proof idea
One-line term proof. Apply the reduction lemma that derives the full canonical-normalization target from uniqueness on reduced sign-canonical ratio orbits, feeding the already-proved uniqueness theorem for that restricted class. The reduction itself (not expanded here) introduces two arbitrary cross-equivalent orbits, notes that each normalize image is reduced and sign-canonical, and invokes the restricted uniqueness hypothesis on those images.
why it matters
This is the exact quotient-normalization uniqueness step that turns normalized-only invariants into general cross-equivalence respect for ratio characters and native costs. Downstream, character display equality on equal rationals applies it via the character-respects-crossEq bridge; structural native-cost uniqueness (round-5 terminal: the structural ledger forces the canonical cost) and calibration of structural characters on positive integers depend on that bridge. Cost-side consumers include equality of trace displays under cross-equivalence and the doubled-trace crossEq-respect certificate inside the native-cost uniqueness blocker path.
In the broader Recognition chain this sits under native J-cost uniqueness (forcing landmark T5: $J(x)=(x+x^{-1})/2-1$), because well-definedness of character and cost on the ratio quotient is a prerequisite before d'Alembert or calibration arguments can pin the cost to $J$. It does not itself name $J$; it clears the representative-normalization obstruction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.