PRCTwoThreeCompositeLocalOrientationFailureCharacter_absurd_of_no_non_two_composite_cost_defect_character
plain-language theorem explainer
If no prime-calibrated ratio character carries a non-two composite J-cost defect, then no ratio character can witness a 2×3 composite-local orientation failure. Downstream orientation targets and the conditional universal-foundation certificate cite this. The proof is a one-step contrappositive: the upstream implication turns any failure witness into a cost-defect model, contradicting the hypothesis.
Claim. Assume there is no ratio character $\chi$ that is prime-direction calibrated and exhibits a two-prime reciprocal-identity non-two composite cost defect. Then there is no ratio character that carries a two-adic axis twist and fails the $2\cdot 3$ composite-local orientation condition.
background
In the Primitive Recognition Calculus, a ratio character is a map $\chi$ on ratio orbits that encodes how multiplicative directions are oriented (identity versus reciprocal branch). The native cost is the J-cost $J(x)=(x+x^{-1})/2-1$ forced by the Recognition Composition Law; composite defects are cost-visible mismatches when mixed-prime directions are oriented inconsistently.
PRCTwoThreeCompositeLocalOrientationFailureCharacter is the constructive countermodel surface for the reduced two-adic target: existence of a ratio character with a two-adic axis twist that fails $2\cdot 3$ composite-local orientation. The calibrated cost-defect character is the Pass-95-equivalent blocker that exposes the actual composite J-cost failure on a non-two mixed branch (prime calibration plus reciprocal-identity composite defect).
Upstream, any $2\cdot 3$ local-orientation failure witness already implies the calibrated non-two composite cost-defect character. This lemma is the logical dual of that implication.
proof idea
One-step contrappositive. Introduce a hypothetical failure witness hfail. Apply the upstream theorem that converts any two-three composite local-orientation failure character into a prime-calibrated two-prime reciprocal-identity non-two composite cost-defect character. Feed that derived witness to hno to obtain absurdity. No further case analysis or cost algebra is performed here.
why it matters
Closes the failure branch of the two-adic orientation target: the sibling theorem PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget_of_no_non_two_composite_cost_defect_character obtains the positive orientation target by rewriting "no failure character" via this absurdity. That target sits on the path that discharges composite-local orientation once the Pass-95 cost-defect blocker is ruled out.
It is also referenced by prc_universal_foundation_conditional_certificate in UniversalFoundation, so the conditional certificate for the PRC universal foundation inherits the same contrappositive link between cost-defect nonexistence and orientation success. In framework terms this is local bookkeeping inside native-cost uniqueness for the mixed-prime branch, not a new forcing step (T5–T8 already fix $J$, $\varphi$, the eight-tick octave, and $D=3$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.