PRCNormalizeRatioCanonicalTarget
plain-language theorem explainer
Canonical-normalization uniqueness for ratio orbits: cross-equivalent raw ratio displays must share the same GCD-normalized representative. Anyone proving that characters or doubled traces respect the cross-equivalence quotient cites this target. The body is a pure Prop definition packaging that universal statement; a separate theorem discharges it from reduced sign-canonical uniqueness.
Claim. For all ratio orbits $q$ and $r$, if $q$ and $r$ are cross-equivalent, then the native GCD normalization of $q$ equals that of $r$ as raw representatives.
background
In the Primitive Recognition Calculus, ratio orbits are the raw displays of rational ratios used by the native cost and character constructions. Cross-equivalence identifies displays that represent the same ratio class under the ledger's multiplicative structure. Native GCD normalization (normalizeRatio) picks a preferred raw representative of each orbit by clearing common factors.
The surrounding module develops uniqueness of the native cost functional on these orbits. Characters and doubled-trace maps are maps on ratio orbits; for them to descend to the quotient by cross-equivalence, normalization must be invariant on cross-equivalent pairs. The doc-comment states the role cleanly: this is "the exact quotient-normalization uniqueness statement needed to turn normalized_invariant into general quotient respect."
Related scaffolding in the same file includes reduced sign-canonical uniqueness (every reduced sign-canonical display is unique in its class) and the character/doubled-trace respect targets that consume this Prop.
proof idea
No proof: this is a definition of a proposition. The body is the universal statement that cross-equivalence of ratio orbits implies equality of their native GCD-normalized representatives. Discharge is external: PRCNormalizeRatioCanonicalTarget_of_reduced_signCanonical_unique derives it from reduced sign-canonical uniqueness by applying that uniqueness to the already-reduced, sign-canonical outputs of normalizeRatio. The closed form is PRCNormalizeRatioCanonicalTarget_proved.
why it matters
This target is the hinge between orbit-level normalization and quotient-level functoriality of native cost data. Downstream, PRCCharacterRespectsCrossEq_of_normalizeRatio_canonical and PRCDoubledTraceRespectsCrossEq_of_normalizeRatio_canonical turn the Prop into respect theorems for characters and doubled traces. Those feed prime-calibration forcing of character cross-equivalence respect, and the Prop appears among the exact Lean targets listed by the Pass-25 native-cost uniqueness blocker certificate.
In the Recognition Science forcing picture, native cost uniqueness is the analytic side of J-cost uniqueness (T5: $J(x)=(x+x^{-1})/2-1$) on the ratio lattice. Without canonical normalization on cross-equivalent displays, characters cannot be shown to respect the Recognition Composition Law's multiplicative structure on orbits. Closing this target (already done via the reduced sign-canonical route) removes one blocker on the native-cost uniqueness chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.