PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget_of_no_calibrated_two_adic_axis_twist
plain-language theorem explainer
Under the hypothesis that no prime-calibrated two-adic axis-twist ratio character exists, every ratio character carrying a two-adic axis twist must still choose one of the two canonical local orientations at the mixed composite 2·3. Native-cost uniqueness and character-rigidity arguments cite this as the positive form of the two-adic branch blocker. The proof is a short term application of an equivalence plus a prior absurdity lemma.
Claim. If there does not exist a ratio character that is simultaneously prime-direction calibrated and two-adic axis-twisted, then every ratio character carrying a two-adic axis twist must select one of the two canonical local orientations at the first mixed composite $2\cdot 3$.
background
In the primitive recognition calculus, a ratio character is a map on ratio orbits obeying the multiplicative character laws used to build native cost. The two-adic axis-twist branch is the residual freedom in which a character can flip orientation along the 2-primary axis. The calibrated model packages that twist with prime-direction calibration; constructing such a model is the native-valuation route to refuting the current character-rigidity branch.
The target proposition is the positive $2\cdot 3$ composite-local form of the two-adic branch blocker: any ratio character that carries the two-adic axis twist must still choose one of the two canonical local orientations at the first mixed composite. Its failure character is the constructive countermodel surface equivalent to the reduced two-adic ratio-character target.
Upstream, the target is already known equivalent to the non-existence of that failure character, and non-existence of a calibrated two-adic axis-twist character already forces the failure character to be absurd.
proof idea
Term-mode one-liner. Apply the right-to-left direction of the equivalence between the $2\cdot 3$ composite-local orientation target and the negation of the failure character. The hypothesis that no calibrated two-adic axis-twist character exists is fed into the prior absurdity lemma, which yields negation of the failure character and closes the goal.
why it matters
This is the hypothesis-to-target bridge on the two-adic side of native cost uniqueness: it turns the global non-existence of a calibrated two-adic axis-twist character into the positive local-orientation constraint at $2\cdot 3$. Downstream it is consumed by 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 Science forcing picture this sits inside character rigidity for the native cost (the J-cost uniqueness branch of the foundation), not yet at T5–T8 landmarks, but as scaffolding that keeps the two-adic residual from spoiling uniqueness of the recognition cost before the octave and dimension steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.