twoAdicAxisTwistCharacter_branch
plain-language theorem explainer
The two-adic axis-twist character realizes the concrete branch form: reciprocal on the orbit-2 axis and identity on every other native prime axis. Anyone citing native-cost orientation underdetermination or the uniqueness-target refutations needs this certificate. The proof splits the conjunction, reduces both sides to rational equality via the toRat display, and applies the corresponding two-adic twist lemmas on ℚ.
Claim. The ratio-orbit map $\chi$ induced by the two-adic twist $x \mapsto x \cdot 2^{-2 v_2(x)}$ satisfies the two-adic axis-twist branch law: $\chi$ sends the prime-$2$ direction to a display cross-equal to its reciprocal, and for every native prime $p \neq 2$, $\chi$ fixes the $p$-direction up to cross-equality.
background
In the Primitive Recognition Calculus, a RatioOrbit is an integer-numerator / nonzero-orbit-denominator display of a rational. Cross-equality of two such displays is equivalent to equality of their rational verifier values (crossEq_iff_toRat_eq). Reciprocal on a ratio orbit inverts that rational display.
A PRC ratio character is a map on ratio orbits used to generate a native cost. The two-adic axis-twist form is the obvious countermodel built from a native two-adic valuation: orbit $2$ is reciprocal-oriented while every other native prime axis is identity-oriented. Concretely the character is realized by pushing each orbit through its rational display, applying the two-adic twist on $\mathbb{Q}$, and lifting back.
This module studies whether $\delta$-native cost axioms force a unique orientation on prime axes. The branch certificate below is the first half of exhibiting a full character that is identity on odd primes and reciprocal on $2$.
proof idea
Tactic proof by constructor on the conjunction defining the two-adic axis-twist form.
First conjunct (orbit-$2$ reciprocal): rewrite cross-equality to rational equality, unfold the character via twoAdicAxisTwistCharacter_toRat, push reciprocal through recip_toRat, and finish with the rational identity that the twist sends $2$ to $2^{-1}$.
Second conjunct (odd primes identity): introduce a prime $p \neq 2$, again reduce cross-equality to toRat equality, and apply the rational lemma that the twist fixes every prime direction other than $2$.
why it matters
This is the branch half of the headline countermodel. Downstream, prc_native_cost_orientation_underdetermined packages it into an existence statement: there is a full PRC ratio character that is identity-oriented on every odd prime axis yet reciprocal-oriented on orbit $2$. That underdetermination is then the engine for refuting uniqueness and forcing targets, including PRCNativeCostUniquenessTarget_refuted, PRCNoAdmissibleFactorForTwoAdicAxisTwistGeneratedCost, and the family of prime-calibration force refutations (nonunit local orientation, reciprocal branch transport, prime-floor identity contracts/extends successor, no adjacent mixed orientation).
In the Recognition forcing chain the point is negative but sharp: native cost axioms alone do not pin the $2$-axis orientation, so uniqueness of the J-cost path (T5) cannot be read off from prime-axis calibration without extra structure. The certificate closes the constructive side of that blocker.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.