reciprocal_ratio_character
plain-language theorem explainer
The reciprocal map on ratio orbits is itself a PRC ratio character. Cost-uniqueness and d'Alembert factorization arguments cite it as the first explicit non-identity witness: multiplicative character laws alone do not fix orientation. The proof discharges the structure fields by reducing cross-equivalence to rational equality and ordinary field arithmetic.
Claim. The global reciprocal map $\chi(q)=q^{-1}$ on ratio orbits is a ratio character: $\chi(1)\sim 1$, $\chi(xy)\sim\chi(x)\chi(y)$, $\chi(q^{-1})\sim\chi(q)^{-1}$ (all up to cross-equivalence), $\chi$ is invariant under normalization of the orbit, and $\chi$ sends nonzero orbits to nonzero orbits.
background
In the Primitive Recognition Calculus, costs are analyzed at the level of ratio orbits rather than raw reals. A RatioOrbit packages a signed numerator/denominator pair; two orbits are cross-equivalent when their verifier rationals agree (crossEq iff toRat equality). Multiplication, reciprocal, and unit are the orbit-level group operations, compatible with toRat.
A ratio character is a map $\chi$ on orbits that is a candidate factor in a d'Alembert factorization of a PRC cost. It must fix the unit up to cross-equivalence, be multiplicative, intertwine reciprocal, respect normalization, and preserve the nonzero locus. The structure is quotient-native: obligations use cross-equivalence, not definitional equality.
Upstream, the same reciprocal idea appears as the reciprocal $J$-automorphism in CostAlgebra and as the reciprocal recognition event in LedgerForcing (swap source/target, invert ratio). Here the map is the pure orbit reciprocal, before cost or ledger decoration.
proof idea
Tactic proof that builds the ratio-character structure field by field. Unit: rewrite cross-equivalence to toRat, apply recip_toRat and one_toRat, finish with norm_num ($1^{-1}=1$). Multiplicativity: reduce both sides to rationals via recip_toRat and mul_toRat; case-split on zero factors and field_simp on the nonzero branch. Reciprocal field: both sides become recip(recip x), so crossEq_refl closes it. Normalized invariance: normalizeRatio is cross-equivalent to the input, so their rationals agree; invert both sides. Nonzero preservation: recip_toRat plus inv_ne_zero.
why it matters
Doc-comment states the point directly: this is the first explicit witness that multiplicative character laws alone do not choose the identity orientation. Downstream, it is the ratio_character field of reciprocal_admissible_ratio_character, which packages reciprocal as an admissible character (prime-calibrated, with prime-pair product cost). That admissible witness is fed into the refutation PRCPrimeCalibrationForcesOrbitSuccessorAdditiveCompatibilityTarget_refuted: assuming prime calibration forced successor-additive compatibility, one would obtain it for reciprocal, contradicting a separate non-compatibility lemma. The same package appears in the native-cost uniqueness blocker certificate. In the broader RS forcing chain this sits under native-cost uniqueness for the PRC $J$-cost (T5 landmark: $J(x)=(x+x^{-1})/2-1$), showing the character side of the factorization is at least two-valued before further calibration kills the reciprocal branch.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.