PRCReducedSignCanonical_den_dvd_of_crossEq
plain-language theorem explainer
When two reduced, sign-canonical ratio orbits are cross-equivalent, the natural-number display of the first denominator divides that of the second. Used inside the native-cost uniqueness blocker certificate. One-line transport of a native divisibility lemma through the DistinctionNat-to-Nat bridge.
Claim. Let $q$ and $r$ be ratio orbits that are reduced and sign-canonical (numerator absolute value coprime to the positive denominator, signed numerator in canonical raw form). If $q$ and $r$ are equivalent under cross-multiplication, then the natural number of $q$'s denominator divides that of $r$'s denominator.
background
In the Primitive Recognition Calculus, rationals are displayed as RatioOrbit: a signed-orbit numerator over a nonzero DistinctionNat denominator (the base-neutral finite orbit of repeated distinction). Two such displays are cross-equivalent when the scaled products of numerator and opposite denominator balance as signed orbits; that is the internal PRC stand-in for rational equality.
A display is reduced and sign-canonical when the absolute numerator is coprime to the positive denominator and the signed numerator sits in the canonical raw signed-orbit form. Native divisibility on distinction orbits is related to ordinary Nat divisibility by the bridge lemma: divides $a$ $b$ if and only if $a.\mathrm{toNat}$ divides $b.\mathrm{toNat}$.
This module develops uniqueness of the native cost character on those reduced displays; the present statement is a Nat-level corollary of the corresponding native divisibility fact for reduced sign-canonical pairs.
proof idea
One-line term proof. Apply the forward direction of divides_iff_toNat_dvd on the two denominators, feeding the native divisibility already established by PRCReducedSignCanonical_den_divides_of_crossEq for the same reduced sign-canonical cross-equivalent pair. No new arithmetic is done here; the work is pure transport from DistinctionNat divisibility to Nat divisibility.
why it matters
Native cost uniqueness in PRC needs control of denominators of reduced ratio displays that represent the same rational. This lemma supplies the Nat-level divisibility form used by the uniqueness blocker certificate (prc_native_cost_uniqueness_blocker_certificate), which packages zero-calibrated factorization targets for the native cost character.
In the broader Recognition chain, unique native cost on ratio orbits underwrites the J-cost identification (T5: $J(x)=(x+x^{-1})/2-1$) and the Recognition Composition Law on the phi-ladder. Without denominator control under cross-equivalence, distinct reduced displays of one rational could host distinct cost characters, blocking uniqueness of the native cost functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.