normalized_invariant
plain-language theorem explainer
GCD-normalizing a ratio-orbit representative leaves the PRC cost unchanged under cross-equivalence. Anyone assembling native-cost hypothesis packs, the PRC J-cost certificate, or real-character factorization cites this invariance. The proof rewrites cross-equivalence to rational equality and applies the cost and normalization toRat lemmas.
Claim. For every ratio orbit $q$, the PRC cost of $q$ is cross-equivalent (by balanced cross-multiplication of numerator/denominator orbits) to the PRC cost of the GCD-normalized representative of $q$. Equivalently, the two cost values display the same rational.
background
In the Primitive Recognition Calculus (PRC), ratios live as RatioOrbit data: signed numerator and denominator orbits rather than bare rationals. Two orbits are related by cross-equivalence when scaled cross-products balance as signed orbits; that relation is exactly rational equality of the verifier displays (crossEq_iff_toRat_eq).
The map onRatioOrbit is the native PRC cost surface on those orbits. DistinctionNat.normalizeRatio cancels the native GCD of a representative so the same rational class is written in reduced form. The module builds the discrete cost that must match the continuous J-cost $J(x)=(x+x^{-1})/2-1$ forced by the Recognition Composition Law.
Upstream, cross-equivalence is the internal PRC rational relation (K4.10), defined entirely on $\delta$-orbit positions, and is already known to agree with toRat equality.
proof idea
Short rewrite proof. First replace cross-equivalence by rational equality via crossEq_iff_toRat_eq. Then rewrite both sides with onRatioOrbit_toRat and the middle with DistinctionNat.normalizeRatio_toRat, so both cost displays reduce to the same rational and the goal closes.
why it matters
This is the normalization leg of the native-cost hypothesis pack. Downstream, BaseSansTwo records it as a required field (RCL pack without the two-point anchor), and prc_jcost_certificate installs it as normalization so the PRC rational cost surface closes through canonical RCL and bridges to continuous-real J-uniqueness (forcing-chain T5).
It is also consumed by real-character factorization: traceDisplay_eq_of_crossEq uses the normalized-invariant field to move cost traces across equivalent representatives, and gauge-orbit constructions (signedPowerNativeCost_base, signGaugeNativeCost_base_sans_two, structural-to-light hypothesis packs) inherit the same invariance. Without it, cost would depend on unreduced orbit presentation rather than the rational class, breaking uniqueness of the discrete J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.