PRCRatioReducedSignCanonical
plain-language theorem explainer
A ratio-orbit display is reduced and sign-canonical when the absolute value of its numerator is coprime to its positive denominator and the signed numerator is already in raw sign-canonical form. Anyone proving uniqueness of reduced rational displays under cross-equality cites this predicate. It is a two-conjunct Prop definition, not a proved theorem.
Claim. A ratio orbit $q$ (signed numerator over a nonzero distinction-nat denominator) is reduced and sign-canonical when $\mathrm{gcd}(|q_{\mathrm{num}}|, q_{\mathrm{den}})$ is a unit and the signed numerator is either the nonnegative orbit display of its absolute value or the negation of that display.
background
In the Primitive Recognition Calculus, rationals are not bare $\mathbb{Q}$ values. A ratio orbit packages a signed orbit numerator with a nonzero distinction-nat denominator (the base-neutral finite orbit of repeated distinction). Absolute value on a signed orbit is the orbit position given by the absolute difference of its positive and negative parts.
Object-level coprimality means the gcd of two distinction-nats is a unit. Sign-canonicity for a signed orbit is stricter than balanced integer equality: the display must be literally the nonnegative orbit of its absolute value, or literally the negation of that nonnegative display (the raw representative condition coming from signed quotient).
This module develops native cost uniqueness for PRC. The present definition is the standard reduced-form predicate used when comparing ratio displays by cross-multiplication equality.
proof idea
Definitional conjunction only. The body is the meet of two existing predicates: coprimality of the numerator absolute value with the denominator, and sign-canonicity of the signed numerator. No tactics, no lemmas applied.
why it matters
Native cost uniqueness needs a unique reduced representative for each rational orbit class. This predicate is the target shape of ratio normalization: the theorem that normalization yields a reduced sign-canonical display uses it directly. From there, a chain of lemmas shows that two reduced sign-canonical ratios related by cross-equality have equal denominators and equal numerators (first divisibility, then equality).
Those uniqueness facts feed the Pass-25 blocker certificate for native cost uniqueness, which records that uniqueness is not yet closed but is split into exact Lean targets. In the broader RS forcing picture this is bookkeeping on the rational display layer beneath J-cost and character/trace matching, not a T5–T8 landmark itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.