PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget_of_prime_pair_product_cost_consistency
plain-language theorem explainer
Prime-pair product cost consistency forces every two-adic axis-twisting ratio character to pick a canonical local orientation at the 2×3 composite. Branch-rigidity arguments in the native-cost uniqueness chain cite this reduction. The proof is a short term application of the orientation-target ↔ no-twist-character equivalence to the already-proved absurdity of a two-adic axis twist under product calibration.
Claim. If prime calibration propagates to cost consistency on products of any two native prime directions, then every ratio character that carries a two-adic axis twist still selects one of the two canonical local orientations at the mixed composite $2\cdot 3$.
background
In the Primitive Recognition Calculus, ratio characters assign costs along ratio orbits. A character is prime-direction calibrated when its cost on each native prime direction matches the native cost. The product-calibration target asks that this calibration extend to products of any two prime directions via cross-equality of costs; its documentation calls this "the natural composite surface whose $2\cdot p$ mixed-orientation instance is the current branch-rigidity blocker."
The two-adic axis twist is a residual branch of ratio characters that flip orientation along the $2$-adic direction. The $2\cdot 3$ composite-local orientation target is the positive form of that blocker: any such twisting character must still choose one of the two canonical local orientations at the first mixed composite $2\cdot 3$.
An upstream theorem already shows that product cost consistency makes a two-adic axis-twist ratio character absurd. A companion equivalence identifies the composite-local orientation target with the nonexistence of such a twist character.
proof idea
One-line term wrapper. Apply the right-to-left direction of the equivalence between the $2\cdot 3$ composite-local orientation target and the nonexistence of a two-adic axis-twist ratio character, feeding it the upstream absurdity that product cost consistency already rules out any such twist character. The product-calibration hypothesis is threaded straight into that absurdity lemma and rephrased as the positive orientation target; no extra case analysis.
why it matters
Feeds the companion absurdity of a $2\cdot 3$ composite-local orientation failure character under the same product-calibration hypothesis, and is consumed by the conditional universal-foundation certificate in UniversalFoundation. Within native-cost uniqueness this closes the positive orientation form of the two-adic branch blocker once prime-pair product consistency is assumed, advancing the forcing path that pins the Recognition cost (J-uniqueness at T5 and the Recognition Composition Law) against residual ratio-character branches. The remaining open surface is discharge of the product-calibration hypothesis itself on the full prime lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.