PRCReducedSignCanonical_num_eq_of_crossEq
plain-language theorem explainer
Two reduced, sign-canonical ratio orbits that lie in the same cross-multiplication class have identical numerators. Number theorists and anyone closing native-cost uniqueness cite this as the numerator half of raw-display uniqueness. The proof cancels a common nonzero denominator after lifting cross-equality to integer products, then invokes signed-orbit canonicity from equal integer values.
Claim. Let $q$ and $r$ be ratio orbits that are reduced and sign-canonical (numerator absolute value coprime to the positive denominator, and the signed numerator in canonical signed-orbit form). If $q$ and $r$ are cross-multiplication equivalent, then their numerators are equal.
background
In the Primitive Recognition Calculus, a ratio orbit is a raw display of a rational as a signed numerator orbit over a positive denominator. Cross-equality RatioOrbit.crossEq is the usual cross-multiplication relation: the two scaled signed numerators are balanced (same integer value after scaling by the opposite denominator).
Reduced sign-canonical form means two constraints at once: the absolute numerator is coprime to the denominator, and the signed numerator itself sits in the canonical raw signed-orbit representative. That package is the normalization target for unique raw ratio displays before costs are read off.
The local module develops native-cost uniqueness from character and doubled-trace data. Upstream integer recovery (toInt) and the balanced-iff-toInt lemma turn display-level balance into ordinary integer arithmetic, which is what the cancellation step needs.
proof idea
First apply the sibling denominator lemma: reduced sign-canonical orbits in the same cross class already share a denominator. Unfold cross-equality and pass through SignedOrbit.balanced_iff_toInt_eq on the two scale-by-opposite-denominator numerators; after rewriting scaleByNat_toInt, this yields $q.\mathrm{num}.\mathrm{toInt}\cdot r.\mathrm{den}.\mathrm{toNat}=r.\mathrm{num}.\mathrm{toInt}\cdot q.\mathrm{den}.\mathrm{toNat}$ in $\mathbb{Z}$. Substitute equal denominators, cancel the nonzero toNat cast of the common denominator by mul_right_cancel₀, and finish with PRCSignedOrbitSignCanonical.eq_of_toInt_eq on the two sign-canonical numerators.
why it matters
This is the numerator half of reduced sign-canonical uniqueness, which the module doc flags as the remaining raw-display number-theory blocker for canonical normalization: two reduced sign-canonical ratio displays in one cross class are the same raw orbit. Downstream, PRCReducedSignCanonicalRatioUniqueTarget_proved packages num and den uniqueness into that target, and the result feeds the native-cost uniqueness blocker certificate that records which factorization and admissibility targets are proved or refuted.
In the broader Recognition stack this sits under PRC native-cost uniqueness (the J-cost side of the forcing chain), not yet at T5 J-uniqueness itself, but as the arithmetic hygiene that lets a unique native cost character attach to a unique reduced display. Without num uniqueness, cross-class collapse would leave an ambiguous numerator before cost extraction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.