onPRCRat_normalized_representative
plain-language theorem explainer
The native cost on a PRC rational is unchanged when its ratio-orbit display is replaced by the GCD-normalized representative. Field and cost-uniqueness arguments in the primitive recognition calculus cite this invariance. The proof pushes equality through injectivity of the rational display map and the fact that normalization preserves the underlying rational value.
Claim. For every ratio orbit $q$ (integer numerator over a nonzero distinction-orbit denominator), the cost of the PRC-rational class of $q$ equals the cost of the PRC-rational class of the GCD-normalized representative of $q$.
background
In the primitive recognition calculus, a ratio orbit is an integer (signed orbit) numerator over a nonzero distinction-orbit denominator. PRC rationals are the quotient of these displays by cross-multiplication equivalence, so equal cross-products yield the same class. The display map toRat sends a class to its ordinary rational value and is injective on the quotient.
Normalization divides numerator magnitude and denominator by their native orbit GCD, restoring sign via the nonnegativity flag. Upstream, that operation preserves the rational value: the normalized display maps to the same rational as the original. The cost onPRCRat is the native cost (J-type) lifted to PRC rationals; it is determined by the underlying rational display.
This module builds the rational field structure on those classes and packages algebraic identities into a certificate. The local setting is the PRCJCost namespace, where cost is evaluated on quotient classes rather than raw displays.
proof idea
Term-mode proof. Apply injectivity of the PRC-rational display map toRat. Rewrite both sides with the bridge from cost to display (onPRCRat_toRat), the constructor identity toRat (mk q) = q.toRat, and the upstream fact that GCD-normalization preserves the rational value (normalizeRatio_toRat). Equality of displays yields equality of costs.
why it matters
Cost must be well-defined on quotient classes, not on a particular fraction display. Without invariance under normalization, native-cost uniqueness and field packaging would depend on unreduced numerators and denominators. Downstream, rational_field_certificate bundles the field laws on PRC rationals; this lemma keeps cost compatible with that certificate's representatives.
In the Recognition forcing chain, T5 forces the unique cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) from the Recognition Composition Law. Here the same cost is evaluated on the PRC rational field built from distinction orbits, so normalized representatives are the right carriers for later ladder and mass formulas. The result is a small but necessary hygiene step between orbit arithmetic and the rational field certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.