PRCTwoThreeCompositeLocalOrientationFailureCharacter_absurd_of_mixed_composite_cost_consistency
plain-language theorem explainer
Under mixed-composite cost consistency (prime calibration forces the composite direction 2·p even when orbit 2 is reciprocal and a distinct native prime p is identity), no ratio character can be a two-adic axis twist that fails the 2·3 composite-local orientation. Cited by anyone discharging the native-cost uniqueness obstruction for the 2·3 branch. Proof is a two-step term composition through an intermediate orientation target.
Claim. Assume that every ratio character which is prime-direction calibrated and sends the two-orbit to its reciprocal must, for every native prime $p\neq 2$, send the composite direction $2\cdot p$ to the mixed value forced by cost consistency. Then there is no ratio character that is a two-adic axis twist yet fails the $2\cdot 3$ composite-local orientation condition.
background
In the Primitive Recognition Calculus, ratio characters are maps $\chi$ on ratio orbits that preserve the multiplicative structure used to read cost. A two-adic axis twist is the mixed-orientation pattern that sends the orbit of $2$ to its reciprocal branch while treating a distinct native prime as identity. The $2\cdot 3$ composite-local orientation condition demands that this mixed data still orient the composite direction $2\cdot 3$ coherently.
The failure character is the constructive countermodel surface: existence of a ratio character that is a two-adic axis twist yet violates that $2\cdot 3$ local orientation. The mixed-composite cost-consistency target is the universal blocker form: prime calibration must still calibrate every composite $2\cdot p$ under exactly that mixed orientation data.
This module develops native-cost uniqueness by ruling out such orientation failures. Upstream, the consistency target is already known to imply the two-adic local-orientation target for the $2\cdot 3$ composite, and that target in turn makes the failure character absurd.
proof idea
Pure term composition, no tactics. First apply the bridge lemma that turns mixed-composite cost consistency into the $2\cdot 3$ local-orientation target for two-adic axis twists. Then feed that target into the existing absurdity lemma, which shows any such target immediately kills the failure-character witness (no ratio character can be a two-adic axis twist and fail $2\cdot 3$ local orientation at once).
why it matters
Closes one concrete obstruction branch in native-cost uniqueness: the mixed $2\cdot 3$ composite-local orientation failure cannot occur once prime calibration enforces mixed-composite cost consistency. Downstream it is consumed by the conditional universal-foundation certificate, which packages kernel, real-complete ordered field, and trace-logic ingredients into a single PRC foundation witness. In the broader Recognition forcing chain this supports uniqueness of the native cost (the J-cost side of T5) by eliminating a residual two-adic orientation countermodel before the universal certificate is assembled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.