threeAdicAxisTwistCharacter_three_reciprocal
plain-language theorem explainer
The three-adic axis twist character sends the prime-3 ratio orbit to its reciprocal orbit. Anyone tracking per-prime orientation freedom in PRC native cost uniqueness cites this. The proof reduces cross-equality to rational equality via toRat lemmas and finishes with the rational three-adic twist identity.
Claim. Let $\chi_3$ be the three-adic axis twist character $x \mapsto x \cdot 3^{-2 v_3(x)}$ on ratio orbits, and let $p_3$ be the prime-$3$ direction orbit. Then $\chi_3(p_3)$ is cross-equal to the reciprocal orbit of $p_3$: the twist inverts the orbit-$3$ axis.
background
In the Primitive Recognition Calculus, ratio orbits carry discrete multiplicative data on the rational carrier. A PRC ratio character is a map on orbits that preserves the algebraic structure used to build a native cost. Cross-equality of orbits means they induce the same rational representative under the standard toRat embedding, so they are interchangeable for cost evaluation.
The three-adic axis twist is the character $\chi_3(x)=x\cdot 3^{-2 v_3(x)}$. It is the identity on the $2$-adic valuation and multiplies by a pure power of $3$ controlled by $v_3$. The reciprocal orbit map flips orientation on a single prime axis. Native cost uniqueness asks whether fixing a cost (or orientation) at one prime forces the canonical $J$-cost everywhere on $\mathbb{Q}^\times$.
Upstream, the continuous Law of Logic theorem (law_of_logic_forces_jcost) forces $J$ from reciprocity, normalization, the Recognition Composition Law, calibration, and continuity. The discrete PRC setting lacks that neighborhood calibration, so per-prime orientation twists remain candidates for non-uniqueness.
proof idea
Term-mode rewrite proof. First rewrite cross-equality as equality of rational images via RatioOrbit.crossEq_iff_toRat_eq. Unfold the three sides with threeAdicAxisTwistCharacter_toRat, RatioOrbit.recip_toRat, and threePrimeDirection_toRat. The resulting rational identity is exactly threeAdicTwistRat_three, which is applied directly. No case splits or induction.
why it matters
This is the orbit-level witness that the three-adic twist inverts the prime-$3$ axis. The sole downstream consumer is prc_single_prime_calibration_insufficient, the headline blocker: there exists a PRC character that fixes the $2$-axis (identity orientation) yet fails cross-equality on the $3$-axis. Together with the complementary underdetermination result that flips $2$ while fixing odd primes, orientation freedom is genuinely per-prime.
In the Recognition framework this pins why discrete $\delta$-native cost cannot force $J$ from finitely many prime calibrations, while the continuous T5/J-uniqueness path (law_of_logic_forces_jcost) escapes via a second-derivative calibration at the unit that constrains a full neighborhood. The forward repair is therefore to derive that neighborhood-level calibration from the cost of one $\delta$ act, not from more prime pins.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.