axisTwistCharacter_off_axis_identity
plain-language theorem explainer
On any prime axis other than p, the p-axis twist character acts as the identity (cross-equivalence of ratio orbits). Anyone proving per-prime orientation freedom for native PRC cost characters cites this. The proof reduces cross-equivalence to rational equality, evaluates the twist on the off-axis prime direction, and uses vanishing p-adic valuation plus a numeric check.
Claim. Let $p$ and $r$ be distinct prime orbits in the distinction naturals. Then the $p$-axis twist character, applied to the prime-direction ratio orbit of $r$, is cross-equivalent (as ratio orbits) to that same prime-direction orbit of $r$.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction, and a prime orbit is a nonzero non-unit with no nontrivial factorization. Ratio orbits package a signed-orbit numerator over a nonzero distinction-orbit denominator; two ratio orbits are related by cross-equivalence when the cross-multiplied signed orbits balance (K4.10), which is equivalent to equality of their rational verifier displays.
The axis-twist character attached to a prime orbit $p$ is the ratio-orbit map realizing the $b$-axis twist with $b = p$ as a natural number: it multiplies the rational display by a pure $p$-power determined by the $p$-adic valuation of the input. The prime-direction orbit of another prime $r$ is the canonical ratio-orbit display of that axis.
This lemma lives in the native-cost uniqueness module, which classifies how much freedom remains in PRC ratio characters once native cost hypotheses are imposed. Off-axis identity is the algebraic fact that a pure $p$-twist does not move any other prime axis.
proof idea
Term-mode, four steps. Rewrite cross-equivalence via crossEq_iff_toRat_eq to equality of rational displays, then apply axisTwistCharacter_toRat so the claim is about the rational axis-twist map. Unfold axisTwistRat. The key lemma padicValRat_axis_primeDirection_eq_zero_of_ne (using both prime-orbit hypotheses and $r \neq p$) shows the $p$-adic valuation of the off-axis prime direction vanishes, so the twist multiplies by $p^0 = 1$. Finish with norm_num.
why it matters
Feeds the headline theorem prc_every_prime_axis_orientation_free: for every prime orbit $p$ there exists a PRC ratio character that inverts the $p$-axis while fixing the orientation of every other prime axis. That result unifies the earlier per-prime witnesses (orientation underdetermined at $p=2$, single-prime calibration insufficient at $p=3$) into one statement that orientation freedom is genuinely per-prime on every axis at once.
In the Recognition framework this is a negative uniqueness fact inside the native cost calculus: δ-native cost structure does not force a global orientation on the prime axes. It sits upstream of cost-from-character and doubled-trace matching arguments in the same module, and clarifies what must still be supplied (extra calibration or external data) before a unique native cost character can be claimed. It does not itself invoke the T5 J-uniqueness or RCL forcing chain; it is a PRC-internal orientation lemma used to bound how far native cost alone can go.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.