PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget_not_of_two_three_local_orientation_failure_character
plain-language theorem explainer
A constructive 2·3 composite-local orientation failure character falsifies the universal mixed two-prime cost-consistency target. Anyone tracking the PRC native-cost uniqueness obstruction chain cites this bridge. The proof is a two-step term composition: promote the failure witness to a two-adic axis-twist ratio character, then apply the already-proved axis-twist negation.
Claim. If there exists a ratio-orbit character $\chi$ that is a two-adic axis twist and fails $2\cdot 3$ composite-local orientation, then it is not the case that every prime-direction-calibrated ratio character sending the $2$-orbit to its reciprocal must send every mixed composite direction $2\cdot p$ (for native primes $p\neq 2$) to the mixed value required by cost consistency.
background
In the Primitive Recognition Calculus native-cost uniqueness module, ratio characters are maps $\chi$ on ratio orbits that preserve the multiplicative structure used to read cost. A two-adic axis twist is a character that flips the $2$-orbit onto its reciprocal branch while leaving a distinct native prime orbit fixed. Composite-local orientation for $2\cdot 3$ asks that the image of the composite direction agree with the mixed value forced by those branch choices.
The failure character is the constructive countermodel surface: existence of a ratio character that is a two-adic axis twist yet fails $2\cdot 3$ composite-local orientation. The cost-consistency target is the universal blocker form: every prime-calibrated ratio character that sends orbit $2$ reciprocal must still calibrate every mixed composite $2\cdot p$ for native primes $p\neq 2$.
Upstream, the axis-twist form already negates that universal target, and a short extraction lemma turns any $2\cdot 3$ failure witness into an axis-twist ratio character by dropping the unused local-orientation conjunct.
proof idea
Pure term composition, no tactics. Apply PRCTwoAdicAxisTwistRatioCharacter_of_two_three_local_orientation_failure_character to the hypothesis: unpack the existential witness $\langle\chi, h_\chi, h_{\mathrm{branch}}, _\rangle$ and repackage $\langle\chi, h_\chi, h_{\mathrm{branch}}\rangle$ as a two-adic axis-twist ratio character. Feed that into PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget_not_of_ratio_character_axis_twist, which itself reduces to the core two-adic axis-twist negation. The composite-local failure is therefore strictly stronger input than needed; only the twist data is used to kill the universal target.
why it matters
This lemma closes one concrete countermodel surface in the PRC native-cost uniqueness stack: the $2\cdot 3$ composite-local orientation failure is enough to defeat the mixed two-prime cost-consistency target that prime calibration would otherwise force. Downstream it is consumed by prc_universal_foundation_conditional_certificate in UniversalFoundation, which assembles the conditional universal-foundation certificate from kernel, real-complete ordered field, and trace-logic pieces.
In the broader Recognition forcing picture this sits inside the cost-uniqueness layer that underwrites J-uniqueness (T5) and the Recognition Composition Law: mixed-orientation characters that break composite calibration cannot be cost-visible under prime calibration. It does not itself force $\phi$ or the eight-tick octave; it only removes one obstruction branch on the path to a unique native cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.