axisTwistCharacter
plain-language theorem explainer
Ratio-orbit lift of the prime-axis twist: given a distinction orbit p and a ratio orbit q, send q to its rational display, invert the exponent on the prime axis b equal to the verifier nat of p, and return the resulting ratio orbit. Orientation-freedom theorems cite it to exhibit, for every prime axis, a character that flips that axis and fixes the others. The body is a one-line transport through the rational display and back.
Claim. For a finite distinction orbit $p$ and a ratio orbit $q$ (signed-orbit numerator over nonzero distinction denominator), the axis-twist character of $p$ at $q$ is the ratio orbit whose rational display equals $x\cdot b^{-2v_b(x)}$, where $x$ is the rational display of $q$ and $b$ is the verifier natural number of $p$. Off the $b$-axis the display is fixed; on the $b$-axis the exponent is inverted.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction, with verifier map to ordinary naturals. A RatioOrbit is an integer (signed-orbit) numerator over a nonzero distinction denominator; its verifier display toRat is the corresponding rational, characterized internally by cross-multiplication rather than by the display itself.
The rational-level map axisTwistRat is the base-parameterized axis twist: on $\mathbb{Q}$, multiply $x$ by $b^{-2v_b(x)}$. That inverts the exponent on the prime axis $b$ and fixes every other prime axis. Special cases $b=2$ and $b=3$ recover the two-adic and three-adic twists used earlier in the native-cost uniqueness development.
This definition lives in the native-cost uniqueness module, which studies which ratio characters are compatible with a $\delta$-native cost and which orientation data that cost fails to force.
proof idea
One-line transport definition. Read $b$ as the verifier nat of $p$, send the ratio orbit $q$ to its rational display, apply the rational axis twist at base $b$, and re-embed via ratioOrbitOfRat. No algebraic content beyond that composition; the companion lemma axisTwistCharacter_toRat records that the round-trip recovers axisTwistRat on displays.
why it matters
This is the orbit-level character used to prove that $\delta$-native cost does not force prime-axis orientation. Downstream, axisTwistCharacter_ratio_character shows it is a PRC ratio character whenever $p$ is a prime orbit; axisTwistCharacter_on_axis_reciprocal and axisTwistCharacter_off_axis_identity show it inverts the $p$-axis and fixes every other prime axis.
Those facts feed the headline theorem prc_every_prime_axis_orientation_free: for every prime orbit $p$ there exists a PRC ratio character that flips the $p$-axis and fixes all others. That single statement replaces the earlier per-prime witnesses for $p=2$ and $p=3$, establishing genuine per-prime orientation freedom on every axis at once. In the Recognition forcing chain this is a non-forcing result: native cost uniqueness stops short of calibrating axis orientation, so further structure (not cost alone) must supply it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.