PRCCharacterPrimeDirectionCalibrated_of_two_adic_axis_twist
plain-language theorem explainer
Any ratio character that twists only the two-axis (reciprocal on orbit 2, identity on every other prime axis) is automatically calibrated on all native prime directions: its induced cost matches canonical J-cost there. Native-cost uniqueness and countermodel refutations cite this to show the two-adic twist is still prime-calibrated. The proof splits on whether the prime is 2, using reciprocal symmetry of J for the twist and congruence for the identity axes.
Claim. Let $\chi$ be a map on ratio orbits. Suppose $\chi$ is a two-adic axis twist: $\chi$ sends the prime direction of $2$ to its reciprocal (up to cross-equivalence), and fixes every other native prime direction. Then $\chi$ is prime-direction calibrated: for every native prime orbit $p$, the cost generated by $\chi$ on the prime direction of $p$ is cross-equivalent to the canonical rational $J$-cost $J(q)=((q+q^{-1})/2)-1$ on that same direction.
background
In the Primitive Recognition Calculus, ratio orbits are rational displays built from signed numerator orbits over nonzero distinction denominators. Cross-equivalence equates two ratio orbits when cross-multiplication balances as signed orbits (the internal PRC stand-in for rational equality).
The canonical cost on a ratio orbit is the rational $J$-object $J(q)=((q+q^{-1})/2)-1$. It is reciprocal-symmetric: $J(q)$ and $J(q^{-1})$ are cross-equivalent. A ratio character $\chi$ induces a cost by composing with this $J$; prime-direction calibration asks that this induced cost match canonical $J$ on every native prime axis.
A two-adic axis twist is the concrete countermodel shape suggested by a native two-adic valuation: reciprocal orientation only on the orbit of $2$, identity orientation on every other prime axis. The module studies whether such branch behavior can still force (or fail to force) global native-cost uniqueness.
proof idea
Fix a native prime $p$. Case-split on whether $p$ is the two-orbit.
If $p=2$, unfold the character cost and chain cross-equivalence: the twist hypothesis gives $\chi$ of the two-direction cross-equivalent to its reciprocal; congruence of $J$ under that equivalence, then reciprocal symmetry of $J$, yields cross-equivalence to canonical $J$ on the two-direction (via crossEq_trans and crossEq_symm).
If $p\neq 2$, the twist hypothesis already says $\chi$ fixes the prime direction of $p$. Unfold the character cost and apply congruence of $J$ under that identity cross-equivalence.
why it matters
This lemma closes the prime-calibration field for the two-adic axis-twist character: the twist is still calibrated on every prime direction. Downstream, PRCPrimeCalibratedTwoAdicAxisTwistCharacter_of_ratio_character_axis_twist packages that fact, and a family of refutation theorems (...NonunitOrbitLocalOrientationTarget_refuted, ...ReciprocalBranchTransportTarget_refuted, prime-floor successor and mixed-orientation targets, and the absurdity of prime-identity branch uniformity under the twist) all invoke it to show that prime calibration alone does not kill the two-adic countermodel.
In the Recognition forcing picture this sits under native $J$-uniqueness (T5 / RCL): it separates prime-axis calibration from full character rigidity, so later steps must control non-prime orbits and branch transport. It also feeds the conditional universal-foundation certificate in UniversalFoundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.