PRCAdmissibleRatioCharacter
plain-language theorem explainer
An admissible ratio character is a map on rational orbits that obeys the multiplicative ratio-character laws, matches canonical J-cost on every prime direction, and matches J-cost on every product of two prime directions. Anyone proving native-cost uniqueness or character rigidity after the two-adic countermodel cites this interface. It is a pure Prop bundle: three named fields, no proof body.
Claim. A map $\chi$ from ratio orbits to ratio orbits is an admissible ratio character when (i) it is a ratio character: $\chi(1)\sim 1$, $\chi(xy)\sim\chi(x)\chi(y)$, and $\chi(x^{-1})$ obeys the reciprocal law up to cross-equivalence; (ii) the cost generated by $\chi$ agrees with the canonical $J$-cost on every prime direction; (iii) that generated cost also agrees with $J$ on every product of two prime directions.
background
In the Primitive Recognition Calculus, costs live on ratio orbits: pairs (signed numerator orbit, nonzero denominator orbit). A ratio character $\chi$ is a candidate factor for a d'Alembert-style factorization of a PRC cost. It is stated at the orbit level and compared by cross-equivalence rather than definitional equality, so it stays quotient-native.
The generated cost of $\chi$ is compared to the canonical on-orbit $J$-cost (the unique cost forced by the Recognition Composition Law and T5). Prime calibration demands agreement on every native prime direction. Prime-pair product cost consistency demands the same agreement on products of two such directions; that field is character-local, so it can be required of a single $\chi$ as part of admissibility.
This structure is the repaired admissible interface after a two-adic countermodel. The older unsigned package could not force the signed-unit field; the present three-field bundle keeps the two global orientations (identity and reciprocal) while cutting out valuation twists.
proof idea
No proof: the declaration is a structure of type Prop. It packages three existing predicates on a map $\chi$: the ratio-character laws (unit, multiplicativity, reciprocal up to cross-equivalence), prime-direction calibration of the generated cost against canonical $J$, and character-local prime-pair product cost consistency. Inhabitants are built by supplying proofs of those three fields, as in the absolute-value and identity character instances.
why it matters
Native-cost uniqueness needs a tight class of characters whose generated cost is forced to $J$. This repaired interface is that class: it is the hypothesis of the global-orientation target (every admissible $\chi$ should be identity- or reciprocal-oriented pointwise), the prime-orientation coherence target, and the signed-unit calibration target. Downstream theorems show the absolute-value character and the identity map are admissible, and that admissibility implies prime-identity criteria used in factorization arguments.
In the broader RS chain this sits under T5 $J$-uniqueness and the Recognition Composition Law: admissible characters are the discrete multiplicative data that must reproduce $J$ on prime axes and prime-pair products before one can claim the native cost is unique. Pass 279 already shows the unsigned interface cannot force signed-unit calibration; the signed-unit target remains an open rigidity obligation on top of this bundle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.