PRCTwoThreeCompositeLocalOrientationFailureCharacter_absurd_of_no_non_two_mixed_character
plain-language theorem explainer
Assuming no calibrated mixed character (orbit 2 reciprocal, some other native prime identity-oriented), the 2·3 composite-local orientation failure witness is impossible. Character-rigidity and native-cost uniqueness arguments cite this to convert a global nonexistence hypothesis into a local obstruction ban. The proof is a one-line contrapositive via the upstream implication from failure character to mixed character.
Claim. If there is no ratio-orbit character that is prime-direction calibrated with orbit $2$ reciprocal and some non-$2$ native prime identity-oriented, then there is no ratio-orbit character that is a two-adic axis twist yet fails $2\cdot 3$ composite-local orientation.
background
In the Primitive Recognition Calculus native-cost uniqueness development, ratio-orbit characters $\chi$ encode how multiplicative ratio orbits are reoriented. A two-adic axis twist sends the orbit of $2$ to the reciprocal branch. Composite-local orientation at $2\cdot 3$ asks that the character respect the expected orientation on the composite direction rather than collapsing to a mixed value.
The failure character is the constructive countermodel surface: some $\chi$ that is a ratio character and a two-adic axis twist, yet fails $2\cdot 3$ composite-local orientation. The calibrated mixed-character model is sharper: orbit $2$ reciprocal while a distinct native prime is identity-oriented. Upstream, any $2\cdot 3$ failure character already yields such a calibrated mixed character (via the two-adic axis-twist intermediate). The local setting is the character-rigidity branch of native cost uniqueness for the recognition cost $J$.
proof idea
Term-mode contrapositive. Assume a $2\cdot 3$ composite-local orientation failure character $h_{\mathrm{fail}}$. Apply the upstream lemma that turns any such failure into a prime-calibrated two-prime reciprocal/identity mixed character. That contradicts the hypothesis that no mixed character exists. Discharge by exact on the negated mixed-character assumption.
why it matters
Closes one direction of the bridge between the global "no non-two mixed character" hypothesis and the positive $2\cdot 3$ composite-local orientation target for two-adic axis twists. The immediate parent is PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget_of_no_non_two_mixed_character, which packages the target via the failure-character iff. That target feeds the conditional universal-foundation certificate in UniversalFoundation, tying character rigidity on the $2$-adic axis into the broader PRC foundation stack (kernel, ordered field, trace logic).
In Recognition Science terms this is foundation scaffolding under the forcing chain toward unique native cost structure (J-uniqueness at T5 and the Recognition Composition Law), not a direct physical constant claim. It rules out a concrete countermodel surface that would otherwise block uniqueness of the native cost on composite directions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.