PRCPrimeCalibratedTwoAdicAxisTwistCharacter_absurd_of_two_three_local_orientation_target
plain-language theorem explainer
If every two-adic axis-twist ratio character is forced to pick a canonical local orientation at the first 2·3 composite, then no prime-calibrated two-adic axis-twist character exists. Character-rigidity and native-cost uniqueness arguments cite this as the absurdity half of the 2·3 fork. The proof is a one-line application of the corresponding biconditional.
Claim. Assume that 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$. Then there is no ratio character that is simultaneously prime-direction calibrated and two-adic axis-twisted.
background
In the Primitive Recognition Calculus, cost uniqueness is attacked through ratio characters $\chi:\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$. A two-adic axis twist is a branch of such characters that twists along the $2$-adic direction; a prime-calibrated two-adic axis-twist character is an existential witness that is also calibrated in the prime directions. Building that witness is the native-valuation route to killing the current character-rigidity branch.
The positive blocker is the $2\cdot 3$ composite-local orientation target: every ratio character that carries the two-adic axis branch must still choose one of the two canonical local orientations at the first mixed composite $2\cdot 3$. The module packages this as a universal statement over characters, and records an equivalence between that target and the non-existence of a prime-calibrated two-adic axis-twist model.
Local setting is native-cost uniqueness inside PRC: characters, doubled-trace d'Alembert structure, and composite-local orientation constraints that feed the universal foundation certificate.
proof idea
One-line term proof. Apply the forward direction (.mp) of the already-proved biconditional
PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget_iff_no_calibrated_two_adic_axis_twist,
which states that the $2\cdot 3$ composite-local orientation target is equivalent to the negation of a prime-calibrated two-adic axis-twist character. The hypothesis is exactly the left-hand side, so the right-hand side is immediate. No further case analysis or character construction is performed here.
why it matters
This is the absurdity arrow of the $2\cdot 3$ composite-local fork: the orientation target rules out the calibrated two-adic axis-twist model that would otherwise refute character rigidity. Downstream it is wired into prcTwoThreeCompositeLocalForkCertificate, which packages the failure/axis-twist equivalences used by the fork, and into prc_universal_foundation_conditional_certificate in UniversalFoundation, which assembles kernel, real-complete ordered field, and trace-logic certificates for the conditional universal foundation.
In the broader Recognition Science chain this sits under native J-cost uniqueness (T5 J-uniqueness and the Recognition Composition Law), where ratio-character rigidity is the algebraic gate before phi-forcing and the eight-tick structure. It does not itself force $\phi$ or $D=3$; it closes one concrete obstruction branch on the way to those landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.