costFromCharacter_normalized_congr
plain-language theorem explainer
For any PRC ratio-character χ, the cost generated from χ is invariant under GCD-normalization of its ratio-orbit argument, up to cross-equivalence. Anyone checking that character-generated native costs satisfy the native-cost hypotheses cites this. The proof unfolds the cost constructor and applies orbit congruence to the character's built-in normalized invariance.
Claim. Let $\chi$ be a map on ratio orbits satisfying the PRC ratio-character axioms (unit, multiplicativity, reciprocity, and normalized invariance under cross-equivalence). For every ratio orbit $q$, the cost generated by $\chi$ at $q$ is cross-equivalent to the cost generated by $\chi$ at the native-GCD normalization of $q$.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero distinction-nat denominator: the internal display of a rational. Two ratio orbits are related by cross-equivalence when cross-multiplication of numerators and denominators balances as signed orbits; this is the quotient-native equality used throughout PRC rather than definitional equality of representatives.
Normalization divides numerator magnitude and denominator by their native orbit GCD (restoring sign via the nonneg flag). A PRC ratio-character is a map $\chi$ on ratio orbits that is a unit-preserving multiplicative reciprocal character at the orbit level, stated with cross-equivalence so it stays quotient-native. Cost from a character is the ordinary PRC cost functional applied after $\chi$: the identity character recovers the canonical cost.
Upstream, the ordinary cost already satisfies normalized invariance (normalizing a representative preserves cost under cross-equivalence). The character package carries an analogous normalized-invariance field so generated costs inherit the same representative independence.
proof idea
Term proof in two steps. Unfold the definition of cost-from-character, which is ordinary cost on the image $\chi(q)$. The goal becomes cross-equivalence of ordinary cost at $\chi(q)$ and at $\chi$ of the normalized $q$. Apply the orbit-level congruence lemma for ordinary cost to the character's normalized-invariance hypothesis at $q$, which supplies cross-equivalence of $\chi(q)$ with $\chi$ of the normalized representative. No further arithmetic is needed.
why it matters
Native-cost uniqueness in PRC requires that candidate costs built from characters (absolute-value generated, two-adic generated, and the identity case) satisfy the native-cost hypothesis package, including well-definedness on ratio representatives. This lemma is the normalization half of that package for arbitrary characters.
It is used directly by the theorems that discharge native-cost hypotheses for the absolute-value-generated and two-adic-generated native costs. Those feed the uniqueness chain that pins the PRC cost to the J-cost shape forced at T5 in the unified forcing chain ($J(x)=(x+x^{-1})/2-1$), via d'Alembert factorization at the ratio-orbit level. Without representative independence under normalize, character-generated costs would not be legitimate native costs on the quotient.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.