PRCRatioCharacter
plain-language theorem explainer
A ratio-orbit map χ is a PRC ratio character when it preserves the unit, products, and reciprocals up to cross-equivalence, is invariant under ratio normalization, and sends nonzero rational displays to nonzero ones. Anyone proving d'Alembert factorization or character rigidity for native PRC costs cites this interface. It is a Prop structure (no proof body): the five fields are the axioms of the candidate character.
Claim. A map $\chi$ from ratio orbits to ratio orbits is a PRC ratio character if: (i) $\chi(1)\sim 1$; (ii) $\chi(xy)\sim\chi(x)\chi(y)$ for all orbits $x,y$; (iii) $\chi(x^{-1})\sim\chi(x)^{-1}$; (iv) $\chi(q)\sim\chi(\mathrm{normalize}(q))$ for every orbit $q$; (v) if the rational display of $q$ is nonzero then so is that of $\chi(q)$. Here $\sim$ denotes cross-equivalence of ratio orbits (quotient-native equality of displays).
background
Primitive Recognition Calculus (PRC) works with ratio orbits: equivalence classes of rational ratios that appear as ledger distinctions, equipped with multiplication, reciprocal, a unit orbit, and a rational display toRat. Cross-equivalence is the native equality on that quotient: two orbits match when their rational displays agree, without forcing definitional equality of representatives.
The Recognition Composition Law and the forced J-cost $J(x)=(x+x^{-1})/2-1$ admit a d'Alembert-style factorization on the positive reals. At the discrete PRC level one needs an analogous multiplicative character on ratio orbits so that a native cost can be recovered from a doubled-trace construction. Upstream CostAlgebra already packages multiplicativity and the reciprocal map as J-automorphisms on positive reals; this structure is the quotient-native counterpart of that package.
The module sits in the native-cost uniqueness development: characters feed costFromCharacter and the doubled-trace d'Alembert hypotheses that pin the canonical PRC cost to the identity-character case.
proof idea
No proof: this is a structure ... : Prop bundling five fields. Each field is an axiom on $\chi$, stated with RatioOrbit.crossEq rather than =, so the interface stays well-defined on the orbit quotient. Downstream lemmas unpack individual fields (e.g. hχ.unit, hχ.multiplicative) and rewrite via crossEq_iff_toRat_eq when a rational display is needed.
why it matters
This is the character interface for PRC cost uniqueness and continuum rigidity. Downstream CharacterRigidityForcing builds calibration at an orbit (CharacterCalibratedAt: $\chi(q)\sim q$), proves the unit is always calibrated, and closes calibration under products, reciprocals, and squares using the multiplicative and reciprocal fields. Rational-display lemmas (character_mul_toRat, etc.) turn cross-equivalence into ordinary rational arithmetic for forcing arguments.
In the broader framework this is the discrete skeleton behind T5 J-uniqueness and the Recognition Composition Law: only characters compatible with mul/recip (and normalization) can factor a native cost. Calibration at a single generator (classically two) plus these axioms is the route that forces $\chi$ to act as the identity character, hence forces the canonical PRC cost. Sibling constructions (costFromCharacter, PRCCharacterTraceMatchesCost) consume exactly this Prop.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.