PRCPrimeCalibratedTwoAdicAxisTwistCharacter_absurd_of_no_non_two_mixed
plain-language theorem explainer
If no prime-calibrated mixed character exists with orbit 2 reciprocal and some non-2 prime identity-oriented, then no prime-calibrated two-adic axis-twist character exists either. Character-rigidity and native-cost uniqueness arguments cite this as the contrapositive gate on the two-adic valuation branch. The proof is a one-line modus tollens via the implication from axis-twist to mixed character.
Claim. Assume there is no ratio-orbit map $\chi$ that is a PRC ratio character, prime-direction calibrated, and mixed in the sense that orbit $2$ is reciprocal while some non-$2$ native prime is identity-oriented. Then there is also no ratio-orbit map that is a PRC ratio character, prime-direction calibrated, and a two-adic axis twist.
background
In the Primitive Recognition Calculus native-cost uniqueness development, candidate cost characters are maps $\chi$ on ratio orbits. A PRC ratio character is such a map satisfying the structural character axioms; prime-direction calibration fixes how $\chi$ acts on native prime orbits.
Two concrete obstruction models are isolated. The mixed model asserts existence of a calibrated $\chi$ with orbit $2$ reciprocal and some non-$2$ prime identity-oriented. The two-adic axis-twist model asserts existence of a calibrated $\chi$ realizing a two-adic axis twist; the module notes that constructing it is "the native valuation route to refuting the current character-rigidity branch."
Upstream, axis-twist already implies the mixed model: any witness of the two-adic twist unpacks to reciprocal-on-$2$ plus identity-on-a-non-$2$-prime data, hence yields a mixed character. The present result is the logical dual of that implication.
proof idea
Pure modus tollens. Assume a two-adic axis-twist character witness htwist. Apply PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter_of_two_adic_axis_twist to obtain a mixed-character witness. Feed that into the hypothesis that no mixed character exists, yielding absurdity. Hence no axis-twist character exists. No case splits or algebraic computation beyond the upstream implication.
why it matters
Closes the contrapositive door on the two-adic valuation attack against character rigidity: ruling out the sharpened mixed model automatically rules out the concrete two-adic axis-twist model. Downstream it is consumed by prc_universal_foundation_conditional_certificate in UniversalFoundation, which assembles the conditional universal-foundation certificate (kernel, real complete ordered field, trace logic).
In the broader Recognition Science stack this sits inside native-cost uniqueness for the Primitive Recognition Calculus, the layer that forces the J-cost shape before the T5 J-uniqueness and T6 $\varphi$ fixed-point steps of the forcing chain. It does not itself prove uniqueness of $J$; it only prunes one calibrated counter-model branch so the rigidity argument can proceed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.