PRCTwoThreeCompositeLocalOrientationFailureCharacter_absurd_of_no_non_two_composite_defect_character
plain-language theorem explainer
If no calibrated non-two mixed-prime composite-defect character exists, then no constructive 2·3 composite-local orientation failure witness can exist either. Native-cost uniqueness arguments cite this to turn a global blocker negation into a local orientation guarantee on two-adic twists. The proof is a one-step contrappositive through the upstream reduction from the 2·3 failure surface to the calibrated defect model.
Claim. If there does not exist a ratio-orbit map $\chi$ that is a ratio character, is prime-direction calibrated, and realizes the two-prime reciprocal-identity composite defect (forcing the mixed image $\chi(2\cdot p)=p/2$ for a native prime $p\neq 2$), then there also does not exist a ratio-orbit map that is a ratio character with two-adic axis twist yet fails the $2\cdot 3$ composite-local orientation condition.
background
In Primitive Recognition Calculus, ratio characters are structure-preserving maps $\chi$ on ratio orbits used to read native cost. Two-adic axis twist packages the branch choice that sends the orbit of $2$ to its reciprocal while leaving other native primes on the identity branch.
The $2\cdot 3$ composite-local orientation failure character is the constructive countermodel surface: a ratio character with two-adic twist that violates local orientation at the composite $2\cdot 3$. The calibrated composite-defect character is the equivalent non-two mixed-prime blocker with the forced composite image $\chi(2\cdot p)=p/2$ exposed.
Upstream, every such $2\cdot 3$ failure witness already yields a calibrated composite-defect character (via a mixed-branch intermediate). The present result is the logical contrappositive of that reduction.
proof idea
One-step contrappositive in tactic form. Assume a $2\cdot 3$ composite-local orientation failure witness. Apply the upstream implication that any such failure character produces a prime-calibrated two-prime reciprocal-identity non-two composite defect character. That conclusion contradicts the hypothesis that no calibrated composite-defect character exists. Therefore the failure witness is impossible.
why it matters
Directly discharges the failure side of the iff that yields the positive target: under no non-two composite defect, every two-adic axis-twist character satisfies $2\cdot 3$ composite-local orientation. That target sits in the native-cost uniqueness chain for ratio characters.
Downstream it is consumed by the conditional universal foundation certificate, which packages kernel, real-complete ordered field, and trace-logic passes. In the broader Recognition forcing picture this blocks mixed-prime composite defects that would otherwise spoil uniqueness of the native $J$-cost (T5), a prerequisite for the Recognition Composition Law and the later phi and dimension steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.