PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget_of_mixed_composite_cost_consistency
plain-language theorem explainer
Mixed composite cost consistency under prime calibration forces every ratio character on the two-adic axis branch to pick a canonical local orientation at the 2·3 composite. Downstream failure-character absurdity and the universal foundation certificate cite this bridge. The proof is a one-line reverse application of the iff that equates the orientation target with nonexistence of a two-adic axis-twist ratio character.
Claim. Assume prime calibration forces cost consistency on mixed composites $2\cdot p$ (orbit $2$ sent reciprocal, a distinct native prime $p$ sent identity). Then every ratio character that carries a two-adic axis twist still selects one of the two canonical local orientations at the first mixed composite $2\cdot 3$.
background
In the Primitive Recognition Calculus native-cost uniqueness development, ratio characters are maps on ratio orbits that encode orientation data for the cost. A two-adic axis twist is the branch where the character treats the prime-2 direction in the twisted (non-identity) way. The first mixed composite is the orbit of $2\cdot 3$; local orientation there means the character must land in one of the two canonical choices rather than an exotic failure mode.
The hypothesis is the universal cost-visible blocker: once a character is prime-direction calibrated, sending orbit $2$ reciprocal and a distinct native prime $p$ identity still forces calibration of the composite direction $2\cdot p$. The conclusion is the positive $2\cdot 3$ composite-local form of the two-adic branch blocker: every ratio character on that branch obeys the canonical local orientation at $2\cdot 3$.
An upstream iff equates that orientation target with the bare nonexistence of any two-adic axis-twist ratio character. A companion absurdity theorem already derives that nonexistence from the mixed-composite cost-consistency hypothesis.
proof idea
One-line term proof. Apply the reverse direction of the iff between the $2\cdot 3$ local-orientation target and the negation of a two-adic axis-twist ratio character. The required negation is supplied by the upstream absurdity theorem that mixed composite cost consistency rules out any such axis-twist character. No further case analysis or arithmetic is performed here.
why it matters
This is a packaging bridge inside native-cost uniqueness: it turns the mixed-composite consistency hypothesis into the positive local-orientation target used by the two-adic branch. The immediate parent is the absurdity of a $2\cdot 3$ local-orientation failure character under the same hypothesis, which quotes this theorem directly. It also feeds the conditional universal-foundation certificate in UniversalFoundation, which assembles kernel, real-complete ordered field, and trace-logic certificates into the PRC foundation package.
In the broader Recognition forcing picture this sits under cost uniqueness for the native $J$-cost (the T5 landmark $J(x)=(x+x^{-1})/2-1$), restricting admissible orientation data before the self-similar fixed point and eight-tick structure are imposed. It does not itself force $\varphi$ or $D=3$; it clears a two-adic orientation obstruction so later uniqueness steps can run.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.