PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget
plain-language theorem explainer
Packages the positive 2·3 composite-local orientation target on the two-adic branch: every ratio character that twists the prime-2 axis must still send the first mixed composite 2·3 to either itself or its reciprocal. Native-cost uniqueness proofs cite it as the constructive blocker that kills two-adic axis-twist countermodels. The body is a pure Prop abbreviation, not a proved statement.
Claim. Every map $\chi$ on ratio orbits that is a ratio character (unit-preserving and multiplicative up to cross-equivalence) and that realizes the two-adic axis twist (sends the orbit $2$ to its reciprocal while fixing every other native prime axis) must satisfy local orientation at the first mixed composite: $\chi(2\cdot 3)$ is cross-equivalent either to $2\cdot 3$ itself or to its reciprocal.
background
In the Primitive Recognition Calculus, costs are recovered from ratio-orbit characters via a d'Alembert-style factorization. A ratio orbit is an integer numerator over a nonzero orbit denominator. A ratio character $\chi$ preserves the unit orbit and is multiplicative up to cross-equivalence (the quotient-native equality on orbits), so it can serve as the multiplicative skeleton of a candidate cost.
The two-adic axis twist is the obvious countermodel one would build from a native two-adic valuation: $\chi$ sends the prime orbit $2$ to its reciprocal while leaving every other native prime axis identity-oriented. Local orientation at the first mixed composite $2\cdot 3$ asks that $\chi(2\cdot 3)$ still land on either the composite itself or its reciprocal, i.e. that the character not invent a third local choice at that composite.
This module develops uniqueness of the native PRC cost. The present definition is the positive (orientation-forcing) form of the current two-adic branch blocker at that first mixed composite.
proof idea
Definitional packaging only: the declaration is a bare Prop abbreviation whose body is the universal quantification
$\forall,\chi,;\mathrm{ratio,character}(\chi)\to\mathrm{two\text{-}adic,axis,twist}(\chi)\to\mathrm{local,orientation,at,}2\cdot 3(\chi)$.
No tactics or lemmas are applied. Downstream theorems treat the name as a single hypothesis and discharge it via the recorded equivalences to the failure-character, ratio-twist, and calibrated-twist witnesses.
why it matters
This target is the positive face of the exact $2\cdot 3$ two-adic fork that the native-cost uniqueness argument must close. Downstream it feeds the absurdity lemmas that kill every two-adic axis-twist ratio character, every prime-calibrated two-adic axis-twist character, and every local-orientation failure character, once the target is assumed. It also appears in the three iff theorems equating the target with the negations of those three countermodel surfaces, and it is packaged into the closed fork certificate that wires failure / ratio twist / calibrated twist against the positive local-orientation branch under one name.
In the broader Recognition forcing chain this sits inside the uniqueness of the J-cost (T5) and the d'Alembert factorization that recovers native cost from ratio characters: ruling out two-adic axis twists at the first mixed composite is part of forcing the unique admissible character skeleton. The open work it supports is discharging the fork certificate so that no residual two-adic countermodel survives into the native-cost uniqueness theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.