threeAdicAxisTwistCharacter_ratio_character
plain-language theorem explainer
The three-adic axis twist map on ratio orbits (multiply by 3 to the power of minus twice the 3-adic valuation) is a PRC ratio character: it preserves the unit, multiplies, takes reciprocals, is normalization-invariant, and keeps nonzero orbits nonzero. Downstream uniqueness arguments cite it as the witness that a cost can match J on the 2-axis while flipping the 3-axis. The proof reduces each structure field through the toRat display to the corresponding rational twist lemmas.
Claim. The map $\chi$ on ratio orbits given by the three-adic axis twist $x \mapsto x \cdot 3^{-2\,v_3(x)}$ is a PRC ratio character: $\chi(1)\sim 1$, $\chi(xy)\sim\chi(x)\chi(y)$, $\chi(x^{-1})\sim\chi(x)^{-1}$, $\chi$ is invariant under ratio normalization, and $\chi$ sends nonzero orbits to nonzero orbits (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 ratio orbit packages a signed integer numerator and a positive natural denominator; two orbits are cross-equivalent when their rational displays agree. The structure PRCRatioCharacter packages the algebraic axioms a candidate character $\chi:\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$ must satisfy for d'Alembert factorization of a PRC cost: unit, multiplicativity, reciprocity, invariance under normalization, and nonzero-preservation, all stated with cross-equivalence so the statement stays quotient-native.
The three-adic axis twist is the orbit-level lift of the rational map that multiplies by $3^{-2v_3(\cdot)}$. Upstream, crossEq_iff_toRat_eq identifies cross-equivalence with equality of rational displays, and the orbit arithmetic lemmas one_toRat, mul_toRat, recip_toRat transport the monoid operations to $\mathbb{Q}$. CostAlgebra and LedgerForcing supply the ambient multiplicative/reciprocal language that the character axioms mirror at the orbit level.
proof idea
Tactic proof that fills the five fields of the ratio-character structure one by one. Each field rewrites cross-equivalence to rational equality via crossEq_iff_toRat_eq, unfolds the character through threeAdicAxisTwistCharacter_toRat, and applies the matching orbit-to-rational transport (one_toRat, mul_toRat, recip_toRat, or normalizeRatio_toRat). The residual rational identities are discharged by the three-adic twist lemmas on $\mathbb{Q}$: unit (threeAdicTwistRat_one), multiplicativity (threeAdicTwistRat_mul), inversion (threeAdicTwistRat_inv), and nonzero-preservation (threeAdicTwistRat_ne_zero). Normalization invariance collapses after both sides reduce to the same rational display.
why it matters
This is the character witness behind the headline blocker prc_single_prime_calibration_insufficient: there exists a PRC ratio character that fixes the prime-2 direction yet fails to fix the prime-3 direction. Together with the complementary orientation underdetermination that flips 2 while fixing odd primes, it shows that native-cost orientation freedom is genuinely per-prime; calibrating a single prime does not force the full character.
In the Recognition forcing chain this sits under native-cost uniqueness for the PRC J-cost (the T5 J-uniqueness lineage). The RCL and the unique cost $J(x)=\cosh(\log x)-1$ need a rigid character factorization; this lemma supplies the counterexample character that blocks premature uniqueness claims from single-prime data. Downstream uniqueness theorems must therefore pin every prime axis, not just one.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.