PRCReducedSignCanonicalRatioUniqueTarget
plain-language theorem explainer
Two reduced, sign-canonical ratio orbits that agree under cross-multiplication are equal as raw ratio displays. Number theorists on the PRC native-cost uniqueness chain cite this as the remaining raw-display blocker for canonical normalization. The declaration is a pure Prop target; a sibling theorem discharges it by case analysis on the orbit constructors.
Claim. For all ratio orbits $q$ and $r$, if both are reduced and sign-canonical (numerator absolute value coprime to the positive denominator, and signed numerator in canonical raw form) and $q$ is cross-multiplication equivalent to $r$, then $q=r$.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator (as a signed orbit) over a nonzero distinction-nat denominator. Cross-multiplication equivalence says the scaled signed numerators balance: $a.num$ scaled by $b.den$ matches $b.num$ scaled by $a.den$. That is the internal PRC rational relation, defined entirely on $\delta$-orbit positions rather than on classical $\mathbb{Q}$.
A raw ratio display is reduced and sign-canonical when the absolute value of its numerator is coprime to the positive denominator and the signed numerator itself sits in the canonical raw signed-orbit form. The present target packages uniqueness of such displays inside a single cross-multiplication class.
The module sits in the native-cost uniqueness development: characters, doubled traces, and d'Alembert structure for the PRC cost, with this Prop as the number-theory gate for canonical ratio normalization.
proof idea
Definitional packaging only: the body is the quantified implication that any two reduced sign-canonical ratio orbits related by cross-multiplication are definitionally equal. No tactics or lemmas are applied here. Discharge lives in the sibling theorem that proves the target by destructing both orbits and using the reduced/sign-canonical hypotheses with the cross-balance relation.
why it matters
Doc-comment calls this the exact remaining raw-display number-theory blocker for canonical normalization. Assuming the target yields the normalize-ratio-canonical target (normalized displays that cross-agree are equal), which then feeds the prime-calibration force that characters respect cross-equivalence. Both appear in the Pass-25 native-cost uniqueness blocker certificate, which splits unfinished uniqueness work into exact Lean targets. In the broader Recognition chain this is bookkeeping on rational displays before cost characters can be forced unique; it is not itself a T5--T8 forcing step, but it clears the display layer those steps need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.