axisTwistCharacter_ratio_character
plain-language theorem explainer
For every prime distinction orbit p, the axis-twist map on ratio orbits is a genuine PRC ratio character: it fixes the unit, multiplies, inverts, preserves normalization, and never sends nonzero ratios to zero. Downstream uniqueness and orientation-freedom arguments cite it as the per-prime character witness. The proof reduces each character axiom through the toRat display and applies the corresponding rational axis-twist identities.
Claim. Let $p$ be a prime distinction orbit. Then the axis-twist map $\chi_p$ on ratio orbits is a PRC ratio character: $\chi_p(1)\sim 1$, $\chi_p(xy)\sim\chi_p(x)\chi_p(y)$, $\chi_p(x^{-1})\sim\chi_p(x)^{-1}$, $\chi_p$ is invariant under ratio normalization, and $\chi_p(q)\neq 0$ whenever $q\neq 0$ (all equalities up to cross-equivalence of ratio orbits).
background
In the Primitive Recognition Calculus, costs are built from ratio-orbit data rather than bare reals. A PRCRatioCharacter is a map $\chi$ on ratio orbits that behaves like a multiplicative character up to cross-equivalence: it fixes the unit orbit, preserves multiplication and reciprocals, respects normalization of distinction ratios, and keeps nonzero orbits nonzero. Cross-equivalence is the quotient-native equality of ratio orbits; by the IntegerRational bridge it is equivalent to equality of the rational displays toRat.
The axis-twist character attached to a prime orbit $p$ is the candidate that inverts the $p$-axis while fixing other prime axes. The hypothesis primeOrbit p forces the underlying natural display p.toNat to be a genuine Nat prime (natPrime_toNat_of_primeOrbit), so the construction can inherit ordinary prime factorization structure on the readout.
This module sits in the native-cost uniqueness development: one asks which ratio characters can arise from a $\delta$-native cost and whether orientation along each prime axis is forced. The character axioms are the d'Alembert-side input to that classification.
proof idea
Tactic proof that builds the PRCRatioCharacter structure fieldwise. First install Fact (Nat.Prime p.toNat) from natPrime_toNat_of_primeOrbit hp.
For unit, multiplicativity, and reciprocity: rewrite the cross-equivalence goal via crossEq_iff_toRat_eq, unfold axisTwistCharacter_toRat (and mul_toRat / recip_toRat / one_toRat as needed), then apply the rational lemmas axisTwistRat_one, axisTwistRat_mul, and axisTwistRat_inv at p.toNat.
Normalized invariance rewrites similarly and uses DistinctionNat.normalizeRatio_toRat. Nonzero preservation rewrites to the rational display and applies axisTwistRat_ne_zero. No global uniqueness argument appears here; only the five character axioms for this explicit map.
why it matters
This is the reusable per-prime character witness for native-cost orientation freedom. The sole direct consumer is prc_every_prime_axis_orientation_free, the headline $\delta$-native non-forcing theorem: for every prime orbit $p$ there exists a PRC ratio character that fixes every other prime axis yet inverts the $p$-axis. That result replaces earlier one-off witnesses for $p=2$ and $p=3$ with a uniform statement.
In the Recognition forcing picture, cost uniqueness (T5 J-uniqueness and the Recognition Composition Law) constrains the continuous cost shape, but the discrete prime-axis orientations of a native ratio character remain free until further calibration is imposed. Establishing that each axis-twist map is a legitimate character is the algebraic prerequisite for exhibiting that residual freedom. Without it, the orientation-undetermined classification cannot even state its witnesses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.