PRCTwoThreeCompositeLocalOrientationFailureCharacter_iff_calibrated_two_adic_axis_twist
plain-language theorem explainer
The 2·3 composite-local orientation failure (a ratio character with two-adic axis twist that breaks orientation on the composite 2·3) is equivalent to existence of a prime-calibrated two-adic axis-twist character. Anyone closing the native-cost uniqueness fork or the universal-foundation certificate cites this bridge. The proof is a two-step Iff.trans through the shared reduced two-adic ratio-character target.
Claim. The following are equivalent: (i) there exists a ratio-orbit character $\chi$ with two-adic axis twist that fails $2\cdot 3$ composite-local orientation; (ii) there exists a ratio-orbit character $\chi$ that is prime-direction calibrated and carries a two-adic axis twist.
background
In the Primitive Recognition Calculus, cost uniqueness is attacked via characters on ratio orbits. A ratio character is a multiplicative map $\chi$ on ratio orbits compatible with the native cost axioms. Two-adic axis twist means $\chi$ sends the orbit of $2$ to the reciprocal branch rather than the identity branch.
The composite-local orientation failure is the constructive countermodel surface: a character with two-adic axis twist that refuses the mixed-branch rule on the composite direction $2\cdot 3$ (equivalently $2\cdot p$ for a distinct native prime). The calibrated two-adic axis-twist character is the native-valuation packaging of the same obstruction: prime-direction calibration plus two-adic axis twist.
Both sides were already reduced, separately, to the same intermediate proposition (existence of a two-adic axis-twist ratio character). This theorem simply identifies the two surfaces.
proof idea
One-line term proof by Iff.trans. First apply the upstream equivalence of the $2\cdot 3$ composite-local orientation failure character with the reduced two-adic axis-twist ratio character. Then compose with the symmetric form of the upstream equivalence of the prime-calibrated two-adic axis-twist character with that same reduced target. No new algebraic work; pure identification of the two witness surfaces.
why it matters
Closes the identification step inside the $2\cdot 3$ composite-local fork certificate, which packages both failure-to-ratio and calibrated-to-ratio bridges. Downstream, the orientation-for-target theorem uses this equivalence (via not_congr) to restate the target as absence of a calibrated two-adic axis-twist character. That package feeds the conditional universal-foundation certificate in UniversalFoundation.
In the Recognition forcing chain this sits inside native-cost uniqueness for the J-cost (T5), before phi is forced as the self-similar fixed point (T6). The two-adic twist is the concrete obstruction branch that must be ruled out or absorbed before character rigidity can pin the cost to $J(x)=(x+x^{-1})/2-1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.