PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget_of_no_non_two_mixed_character
plain-language theorem explainer
Assuming there is no calibrated mixed ratio character with reciprocal 2-orbit and identity orientation on a non-2 prime, every two-adic axis-twist character is forced to pick a canonical local orientation at the 2·3 composite. Cost-uniqueness and universal-foundation certificates cite this as the positive form of the two-adic branch blocker. The proof is a two-step term: absurdity of the failure character, then the target↔no-failure equivalence.
Claim. If there is no ratio character $\chi$ that is prime-direction calibrated with orbit $2$ reciprocal and some non-$2$ native prime identity-oriented, then every ratio character carrying the two-adic axis twist still chooses one of the two canonical local orientations at the mixed composite $2\cdot 3$.
background
In the Primitive Recognition Calculus native-cost uniqueness module, ratio characters are maps on ratio orbits that encode local orientation data for the cost functional. The two-adic axis-twist branch is the remaining obstruction: characters that twist along the $2$-orbit must still be pinned down at the first mixed composite $2\cdot 3$.
The target proposition asserts exactly that pinning: every ratio character with the two-adic axis twist satisfies the $2\cdot 3$ composite-local orientation condition. Its failure form is a constructive countermodel surface (a character that twists on the two-adic axis yet refuses both canonical orientations at $2\cdot 3$).
The hypothesis rules out a sharpened calibrated mixed model: existence of a character that is prime-direction calibrated, reciprocal on orbit $2$, and identity-oriented on some non-$2$ native prime. An upstream lemma already shows that ruling out this mixed model makes the failure character absurd; another equates the positive target with absence of that failure character.
proof idea
Term-mode composition of two prior results. First apply the absurdity lemma: from $\neg$ (calibrated two-prime reciprocal / non-two identity mixed character), conclude $\neg$ (two-three composite local-orientation failure character). Then apply the right-to-left direction of the equivalence target $\leftrightarrow$ no failure character, yielding the positive $2\cdot 3$ composite-local orientation target for two-adic axis-twist characters.
why it matters
This is the positive packaging of the two-adic branch blocker used by the conditional universal-foundation certificate in UniversalFoundation. That certificate assembles kernel, real-complete ordered field, and trace-logic passes; the present lemma supplies the orientation rigidity step needed so native cost uniqueness can close under the two-adic axis branch.
In the Recognition Science forcing chain, native cost uniqueness feeds J-uniqueness (T5) and the Recognition Composition Law. Clearing mixed-character countermodels at the first composite $2\cdot 3$ is a concrete gate on that path: without local orientation rigidity, the doubled-trace / d'Alembert route to the unique J-cost does not lock.
The result is conditional on excluding the calibrated non-two mixed character; it does not by itself discharge that exclusion, but converts it into the form the foundation certificate consumes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.