costFromCharacter_reciprocal_congr
plain-language theorem explainer
A PRC ratio character induces a cost that is invariant under reciprocal of the input ratio orbit, up to cross-equivalence. Anyone discharging the reciprocal clause of native-cost hypotheses cites this. The proof is a short crossEq chain: unfold the cost constructor, apply reciprocal symmetry of the character value, then the character's reciprocal axiom.
Claim. Let $\chi$ be a map on ratio orbits that is a PRC ratio character (preserves the unit, is multiplicative, and intertwines reciprocal, all up to cross-equivalence). Then for every ratio orbit $q$, the cost built from $\chi$ at $q$ is cross-equivalent to the cost built from $\chi$ at the reciprocal orbit $q^{-1}$.
background
In the Primitive Recognition Calculus, ratios live as RatioOrbit displays: a signed-orbit numerator over a nonzero distinction-orbit denominator. Equality of such displays is not definitional; it is the internal relation crossEq, which asserts that the two cross-multiplied signed orbits balance (K4.10). That relation is symmetric and transitive by choice-free integer-bridge lemmas.
A PRCRatioCharacter is a quotient-native candidate for the d'Alembert factor of a PRC cost: a map $\chi$ on ratio orbits that fixes the unit, is multiplicative, and sends reciprocal to reciprocal, each identity stated as crossEq rather than = so it stays orbit-native.
The cost constructor costFromCharacter turns such a character into a cost display on ratio orbits. Reciprocal symmetry of ordinary J-style costs (from the PRCJCost layer) supplies the algebraic half of the argument; the character's own reciprocal axiom supplies the other half.
proof idea
Term proof after unfolding costFromCharacter. The goal becomes a crossEq between two cost displays. Apply crossEq_trans to a two-step path: first reciprocal_symmetric at the character value $\chi(q)$, which equates the cost built from $\chi(q)$ with the cost built from its reciprocal; second, the symmetric of onRatioOrbit_congr applied to the character axiom hχ.reciprocal q, which identifies $\chi(q^{-1})$ with the reciprocal of $\chi(q)$ up to crossEq. The composite is exactly cost-at-$q$ cross-equivalent to cost-at-$q^{-1}$.
why it matters
Native cost uniqueness in this module requires every candidate cost to satisfy PRCNativeCostHypotheses, whose reciprocal clause demands cost$(q)$ ~ cost$(q^{-1})$. This lemma discharges that clause whenever the cost is generated from a PRC ratio character.
Downstream, absValueGeneratedNativeCost_native_hypotheses and twoAdicGeneratedNativeCost_hypotheses both route their reciprocal fields through the same crossEq-trans pattern; this result is the character-level engine those generators rely on.
In the broader forcing chain the move is the PRC-native shadow of T5 J-uniqueness and the Recognition Composition Law: costs built from multiplicative reciprocal characters automatically inherit the $x\leftrightarrow x^{-1}$ symmetry that singles out $J(x)=(x+x^{-1})/2-1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.