twoAdicAxisTwistCharacter
plain-language theorem explainer
Defines the ratio-orbit lift of the classical two-adic branch twist: send a ratio orbit to the orbit of x·2^(-2·v₂(x)). It is the concrete PRC ratio character that fixes every odd-prime axis and inverts the orbit-2 axis. Downstream uniqueness and calibration targets cite it as the countermodel that shows native cost orientation is underdetermined. The body is a two-step transport wrapper through rationals.
Claim. For a ratio orbit $q$, the two-adic axis twist character returns the ratio orbit of the rational $x\cdot 2^{-2\,v_2(x)}$, where $x$ is the rational display of $q$. Equivalently, it realizes on ratio orbits the map that fixes every odd-prime axis and inverts the exponent of the orbit-$2$ axis.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer-numerator / nonzero-denominator display of a rational (K4.7). The verifier map toRat recovers the ordinary rational by cross-multiplication transport; ratioOrbitOfRat is the deliberately non-primitive section back into ratio orbits, used only to test whether the character interface already admits classical rational countermodels.
The classical two-adic branch twist on rationals is $x\mapsto x\cdot 2^{-2,v_2(x)}$. It leaves every odd-prime valuation untouched and replaces the $2$-adic valuation $v$ by $-v$, so the orbit-$2$ axis is inverted while all other prime axes stay fixed.
This module studies whether $\delta$-native cost data force a unique ratio character (and thus a unique native cost). The two-adic twist is the standard candidate for a nontrivial automorphism of the character interface that still satisfies the PRC ratio-character axioms.
proof idea
One-line definitional wrapper. Convert the input ratio orbit to a rational via the verifier display, apply the classical two-adic twist $x\mapsto x\cdot 2^{-2,v_2(x)}$, then re-embed via the rational-to-orbit section. No lemmas are proved here; noncomputability is inherited from the $2$-adic valuation on rationals.
why it matters
This character is the headline countermodel for native-cost uniqueness in PRC. The theorem prc_native_cost_orientation_underdetermined exhibits it as a full PRC ratio character that is identity-oriented on every odd prime and reciprocal-oriented on orbit $2$, so $\delta$-native cost data do not force a unique orientation.
It feeds the refutations of several upgrade and calibration targets: factorization-admissibility upgrade fails for the twist-generated cost; no admissible factor exists for that cost; and prime-calibration targets that would force nonunit local orientation, reciprocal-branch transport, or prime-floor successor identities are all refuted by calibrating this same character. In short, it closes the uniqueness program negatively: the native cost interface admits a genuine two-adic axis flip.
Within the broader Recognition forcing chain this sits upstream of J-uniqueness (T5) and the composition law: before the cost functional can be forced, the character that feeds it must be shown unique or else the residual freedom must be classified. The twist records that residual freedom on the prime-$2$ axis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.