PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget_iff_no_calibrated_two_adic_axis_twist
plain-language theorem explainer
The positive 2·3 composite-local orientation target on two-adic axis-twist characters is equivalent to the non-existence of any prime-calibrated two-adic axis-twist character. Character-rigidity and native-cost uniqueness arguments cite this bridge when converting a local orientation obligation into a global non-existence claim. The proof is a two-step equivalence chain: target iff no failure character, then failure character iff calibrated twist, composed by not_congr.
Claim. The following are equivalent: (i) every ratio character $\chi$ that carries a two-adic axis twist still admits one of the two canonical local orientations at the mixed composite $2\cdot 3$; (ii) there is no ratio character that is simultaneously prime-direction calibrated and two-adic axis-twisted.
background
In the Primitive Recognition Calculus, ratio characters are maps on ratio orbits obeying the multiplicative character laws used to build native cost. A two-adic axis twist is a branch of such a character that privileges the prime-2 direction; the calibrated form strengthens this by requiring prime-direction calibration, yielding a concrete countermodel surface against character rigidity.
The positive target asserts that any character on that two-adic branch must still pick one of the two canonical local orientations at the first mixed composite $2\cdot 3$. Its failure form is the constructive countermodel: a character that is a ratio character, two-adic axis-twisted, and fails that local orientation. Upstream, failure is already identified with the calibrated two-adic axis-twist existence statement, and the positive target is identified with the negation of failure.
This module sits in the native-cost uniqueness development, where J-cost uniqueness and d'Alembert/trace constraints force character rigidity; the two-adic branch is the remaining blocker being reduced to local composite orientation.
proof idea
Pure term-mode equivalence algebra. Start from the upstream fact that the positive $2\cdot 3$ local-orientation target is equivalent to the negation of the failure character. Compose with not_congr applied to the upstream equivalence identifying that failure character with the existence of a prime-calibrated two-adic axis-twist character. The result is target $\leftrightarrow$ no calibrated twist. No new analytic content; only transport of negations across already-proved biconditionals.
why it matters
This lemma is the clean interface between the positive local-orientation obligation and the global non-existence of a calibrated two-adic countermodel. Immediately downstream, it yields the one-line absurdity theorem: assume the orientation target, conclude there is no prime-calibrated two-adic axis-twist character. That absurdity feeds the $2\cdot 3$ composite-local fork certificate, which packages the failure/calibrated equivalences used in the native-cost uniqueness fork.
Further downstream it appears in the universal-foundation conditional certificate chain, so discharging or assuming the orientation target becomes a single switch for the two-adic branch blocker. In Recognition Science terms this is part of the foundation forcing that pins native cost (and thereby the J-cost uniqueness step T5) by eliminating exotic ratio characters before the phi fixed-point and eight-tick structure are imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.