normalizeRatio_reduced_signCanonical
plain-language theorem explainer
Euclidean normalization of any rational orbit display yields a reduced, sign-canonical representative: absolute numerator coprime to the positive denominator, and signed numerator in canonical signed-orbit form. Used by the normalize-ratio canonical target and the native-cost uniqueness blocker certificate. Proof is a two-goal constructor: coprimality from the normalizer, sign-canonicity from the signed quotient after GCD division.
Claim. For every rational orbit display $q$ (signed numerator over a nonzero orbit denominator), the Euclidean normalization of $q$ is reduced and sign-canonical: the absolute value of its numerator is coprime to its positive denominator, and its signed numerator lies in canonical signed-orbit form.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12). A RatioOrbit is a rational orbit display: a signed numerator over a nonzero orbit denominator (K4.7). Absolute value of a signed orbit is the orbit position given by absolute difference of its positive and negative parts.
Object-level GCD is defined by subtractive Euclidean descent. Normalization of a ratio divides numerator and denominator by that GCD (with a sign-canonical presentation of the signed quotient). The predicate PRCRatioReducedSignCanonical packages the two residual conditions: absolute numerator coprime to the positive denominator, and the signed numerator itself in canonical raw signed-orbit form.
This lemma lives in the native-cost uniqueness module, which builds the discrete arithmetic needed before cost characters and doubled-trace d'Alembert identities can be forced uniquely.
proof idea
Tactic proof by constructor on the conjunction defining reduced sign-canonicity.
First conjunct: apply normalizeRatio_coprime directly to $q$.
Second conjunct: unfold normalizeRatio, then apply signedQuotient_signCanonical_of_divides to the numerator and gcd(|num|, den). The two side conditions are gcd_ne_zero_of_right_ne_zero (using den_ne_zero) and gcd_divides_left. No further casework.
why it matters
Native cost uniqueness is the discrete half of forcing the unique J-cost (T5 in the forcing chain: $J(x)=(x+x^{-1})/2-1$). Before characters can be unique, ratio displays must sit in a single reduced sign-canonical form so that cost-from-character maps do not fork on presentation.
Downstream, PRCNormalizeRatioCanonicalTarget_of_reduced_signCanonical_unique applies this lemma to every $q$ when discharging the normalize-ratio canonical target from a uniqueness hypothesis on reduced sign-canonical ratios. That target feeds the Pass-25 blocker certificate PRCNativeCostUniquenessBlockerCertificate, which records that native cost uniqueness is not yet closed but is split into exact Lean targets (zero-calibrated factorization proved; signed-admissible factorization refuted).
Without this normalization lemma, the uniqueness path cannot even state that two equal rational values share one canonical display.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.