PRCReducedSignCanonical_den_eq_of_crossEq
plain-language theorem explainer
Two reduced, sign-canonical rational orbit displays that agree under cross-multiplication have identical denominators. Anyone proving uniqueness of reduced ratio representatives in the primitive recognition calculus cites this. The proof is a one-line antisymmetry argument: each denominator divides the other, so they coincide.
Claim. Let $q$ and $r$ be rational orbit displays (signed-orbit numerator over nonzero distinction-nat denominator). If both are reduced and sign-canonical (numerator absolute value coprime to the denominator, and the signed numerator in canonical raw signed-orbit form) and $q$ is cross-equivalent to $r$ (cross-multiplication balances as signed orbits), then the denominators agree: $q.\mathrm{den}=r.\mathrm{den}$.
background
In the primitive recognition calculus, rationals are not bare $\mathbb{Q}$ values. A RatioOrbit is a signed-orbit numerator over a nonzero DistinctionNat denominator (the base-neutral finite orbit of repeated distinction). Equality of displays is internal: crossEq says the two cross-products balance as signed orbits, i.e. $a.num\cdot b.den$ matches $b.num\cdot a.den$ on $\delta$-orbit positions (K4.10).
Reduced sign-canonical form means the absolute numerator is coprime to the positive denominator and the signed numerator itself sits in the canonical raw signed-orbit shape. That is the uniqueness normal form for ratio displays used throughout native-cost uniqueness.
Divisibility on DistinctionNat is antisymmetric: mutual division forces equality via the underlying natural-number dvd relation. The sibling one-sided lemma already shows that, under cross-equivalence of two reduced sign-canonical displays, each denominator divides the other.
proof idea
Term-mode one-liner. Apply DistinctionNat.divides_antisymm to the pair of one-sided divisibility facts from PRCReducedSignCanonical_den_divides_of_crossEq: once with $(q,r)$ and the given cross-equivalence, once with $(r,q)$ after crossEq_symm. Mutual division yields $q.den=r.den$.
why it matters
Denominator equality is half of reduced-ratio uniqueness. The sibling PRCReducedSignCanonical_num_eq_of_crossEq gets the numerators; together they feed PRCReducedSignCanonicalRatioUniqueTarget_proved, which states that cross-equivalent reduced sign-canonical ratio orbits are identical as structures.
That uniqueness target is part of the native-cost uniqueness stack: distinct reduced ratio characters cannot represent the same cross-class, so cost-from-character assignments cannot split on equivalent displays. Downstream, the blocker certificate prc_native_cost_uniqueness_blocker_certificate packages the factorization and admissibility closures that rely on this normal-form rigidity.
In the broader Recognition forcing picture this is bookkeeping inside the J-cost / native-cost uniqueness lane (toward T5-style uniqueness of the cost functional), not a direct citation of RCL or the eight-tick octave, but it keeps rational orbit displays unique before cost is read off.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.