PRCReducedSignCanonical_den_divides_of_crossEq
plain-language theorem explainer
If two ratio orbits are cross-equal and the first is reduced and sign-canonical, its denominator divides the second's denominator in the internal natural arithmetic. Ratio-uniqueness and native-cost arguments cite this as the divisibility half of denominator rigidity. The proof lifts cross-equality to an integer cross-product, passes to absolute values, then uses coprimality of numerator absolute value and denominator.
Claim. Let $q,r$ be ratio orbits. Suppose $q$ is reduced and sign-canonical (absolute numerator coprime to the positive denominator, and the signed numerator in canonical signed-orbit form), $r$ is likewise reduced and sign-canonical, and $q$ is cross-equal to $r$. Then the denominator of $q$ divides the denominator of $r$ in the internal natural numbers.
background
In the Primitive Recognition Calculus, ratios are carried as RatioOrbit data: a signed numerator orbit and a positive denominator. Cross-equality is the internal balance relation that says the two displays represent the same rational after clearing denominators (scaled numerators are balanced). The bridge lemma balanced_iff_toInt_eq identifies that internal balance with equality of the recovered integers.
Reduced sign-canonical form means two things at once: the absolute value of the numerator is coprime to the denominator, and the signed numerator itself sits in the canonical raw signed-orbit representative. Absolute value and the maps toInt/toNat are the verifier displays that connect PRC arithmetic to ordinary $\mathbb{Z}$ and $\mathbb{N}$.
This module develops uniqueness of the native cost functional on such reduced ratio characters. Denominator control under cross-equality is the arithmetic step that later forces two reduced displays of the same ratio to share a denominator.
proof idea
Unfold cross-equality and apply balanced_iff_toInt_eq to the scaled numerators to obtain the integer cross-product identity $q_{\mathrm{num}}\cdot r_{\mathrm{den}}=r_{\mathrm{num}}\cdot q_{\mathrm{den}}$ after scaleByNat_toInt.
Apply Int.natAbs and rewrite with abs_toNat to pass to a natural cross-product on absolute numerators. From that identity, $q_{\mathrm{den}}$ divides $q_{\mathrm{num}}^{\mathrm{abs}}\cdot r_{\mathrm{den}}$ in the internal naturals (divides_iff_toNat_dvd, toNat_mul, and ordinary left-factor divisibility).
Finish with coprime_divides_of_divides_mul_left using the coprimality half of the reduced hypothesis on $q$: a denominator coprime to the absolute numerator that divides a product with that absolute numerator must divide the remaining factor $r_{\mathrm{den}}$. The reduced hypothesis on $r$ is unused.
why it matters
This is the internal-divides form of denominator rigidity for reduced sign-canonical ratio orbits. Immediate parents are the Nat-display version PRCReducedSignCanonical_den_dvd_of_crossEq and the equality theorem PRCReducedSignCanonical_den_eq_of_crossEq, which together pin denominators of cross-equal reduced displays.
In the Recognition stack, unique reduced ratio characters feed the native cost uniqueness argument: the cost functional is forced once ratio displays are canonical. That uniqueness sits under the J-cost forcing chain (T5 J-uniqueness via the Recognition Composition Law) by ensuring the discrete ratio data that the cost reads cannot be rewritten by a non-unique denominator choice.
Without this divisibility step, cross-equal reduced forms could still differ by denominator multiples, blocking the later equality of denominators and the uniqueness of the native cost on ratio characters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.