PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter_of_two_adic_axis_twist
plain-language theorem explainer
A prime-calibrated two-adic axis-twist character immediately yields the sharpened mixed model in which orbit 2 is reciprocal and some non-2 native prime orbit is identity-oriented. Character-rigidity and native-cost uniqueness arguments cite this as the bridge from the twist model to the mixed-character target. The proof is a short existential unpack that instantiates the non-2 witness at the three-orbit.
Claim. If there exists a ratio-orbit map $\chi$ that is a PRC ratio character, prime-direction calibrated, and a two-adic axis twist, then there exists such a $\chi$ that is reciprocal on the orbit of $2$ and identity-oriented on some native prime orbit other than $2$.
background
In the primitive recognition calculus, ratio-orbit characters $\chi : \mathrm{RatioOrbit} \to \mathrm{RatioOrbit}$ encode orientation data on multiplicative orbits. Prime-direction calibration restricts how $\chi$ acts on native prime orbits. A two-adic axis twist is the concrete model in which the orbit of $2$ is reciprocal while non-$2$ primes stay identity-oriented; constructing it is the native-valuation route toward refuting the current character-rigidity branch.
The target mixed-character proposition sharpens that picture: orbit $2$ reciprocal, plus an explicit non-$2$ native prime witness that is identity-oriented. The module uses threeOrbit (the successor of twoOrbit) as the canonical non-$2$ prime witness, with proved facts that it is a prime orbit and distinct from twoOrbit.
Locally this sits inside native-cost uniqueness: characters are tied to doubled-trace cost data and d'Alembert-type identities, so orientation failures on the $2$-axis become cost-consistency contradictions downstream.
proof idea
Term-mode existential surgery. Unpack the hypothesis into a character $\chi$ with ratio-character, prime-calibration, and two-adic axis-twist data; the twist package already supplies reciprocity on orbit $2$ and a universal identity clause on non-$2$ primes. Rebuild the mixed-character witness with the same $\chi$, keep reciprocity on $2$, and instantiate the non-$2$ identity clause at threeOrbit, discharging the prime-orbit and inequality side conditions by threeOrbit_primeOrbit and threeOrbit_ne_twoOrbit.
why it matters
This is the one-step specialization from the concrete two-adic twist model to the sharpened mixed-character interface used throughout the uniqueness cascade. Downstream, PRCPrimeCalibratedTwoAdicAxisTwistCharacter_absurd_of_no_non_two_mixed is literally the contrapositive wrapper, and PRCPrimeCalibratedTwoAdicAxisTwistCharacter_absurd_of_mixed_composite_cost_consistency routes the twist into a cost-consistency absurdity. A parallel path lifts two-three local orientation failure through this lemma into the same mixed target.
In the broader Recognition stack it feeds prc_universal_foundation_conditional_certificate in UniversalFoundation, part of the conditional certificate that the primitive recognition calculus closes under the native cost. Relative to the forcing chain, it is foundation-layer character rigidity work that underwrites uniqueness of the J-cost (T5) rather than a direct T6--T8 step: without killing exotic prime-orbit orientations, the native cost need not be forced to $J(x)=\cosh(\log x)-1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.