PRCReducedSignCanonicalRatioUniqueTarget_proved
plain-language theorem explainer
Two reduced, sign-canonical ratio orbits that agree under cross-multiplication are definitionally equal as raw ratio displays. Number theorists and anyone closing the PRC native-cost uniqueness chain cite this as the last raw-display uniqueness step before canonical normalization. The proof cases both orbits, applies the numerator and denominator equality lemmas under cross-equality, then substitutes.
Claim. For all ratio orbits $q$ and $r$, if both are reduced and sign-canonical and $q$ is cross-multiplication-equivalent to $r$, then $q = r$ as raw ratio orbits.
background
In the Primitive Recognition Calculus, ratio orbits are the raw rational displays used to present cost characters before canonical normalization. A display is reduced and sign-canonical when its numerator and denominator are in a fixed reduced form with a fixed sign convention, so that each rational class has at most one preferred raw representative.
Cross-multiplication equivalence identifies two orbits when their cross products match (the usual $ad = bc$ relation for fractions). The target proposition asserts that this equivalence, restricted to the reduced sign-canonical slice, collapses to definitional equality of the raw orbits.
The module develops native-cost uniqueness for PRC characters. Upstream, separate lemmas already force numerator equality and denominator equality of two reduced sign-canonical orbits once they are cross-equivalent; this declaration packages those two equalities into full orbit identity.
proof idea
Term-mode proof by introduction and structure cases. Fix two ratio orbits $q,r$ with reduced sign-canonical hypotheses and a cross-equality hypothesis. Case both as mk num den records. Apply the upstream numerator lemma to obtain $q_{\mathrm{num}} = r_{\mathrm{num}}$, and the upstream denominator lemma to obtain $q_{\mathrm{den}} = r_{\mathrm{den}}$. Substitute both equalities and close by reflexivity. No further arithmetic is needed beyond those two lemmas.
why it matters
This is the remaining raw-display number-theory blocker for canonical normalization of PRC ratio displays. Downstream, the proved normalize-ratio-canonical target is obtained in one step by feeding this uniqueness into the reduced-sign-canonical-unique bridge. The same uniqueness is reused to prove that prime calibration forces character cross-equality respect, which is part of the product no-mixing story for calibrated characters.
It also appears among the ingredients of the native-cost uniqueness blocker certificate that aggregates factorization and admissibility targets for the uniqueness program. In the broader Recognition framework this sits in the foundation layer that pins the native cost functional before the forcing chain (J-uniqueness, $\varphi$, eight-tick structure) is applied at the physics layer; without unique reduced displays, character-to-cost matching would retain an orbit ambiguity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.