PRCCharacterTwoAdicAxisTwist_two_three_local_orientation_absurd
plain-language theorem explainer
Any ratio-orbit character that flips the prime-2 axis and fixes every other prime axis cannot be locally oriented at the composite 2·3: its image of 2·3 is forced to a mixed direction, neither the composite nor its reciprocal. Cost-uniqueness arguments cite this to kill the obvious two-adic valuation countermodel. The proof is a short case split on the two local-orientation disjuncts after applying the mixed-image lemma.
Claim. Let $\chi$ be a ratio-orbit character (unit-preserving, multiplicative, and reciprocal up to cross-equivalence). Suppose $\chi$ is a two-adic axis twist: $\chi(2)\sim 2^{-1}$ and $\chi(p)\sim p$ for every native prime $p\neq 2$. Then $\chi$ fails local orientation at the first mixed composite: $\chi(2\cdot 3)$ is cross-equivalent neither to $2\cdot 3$ nor to $(2\cdot 3)^{-1}$.
background
The ambient setting is native cost uniqueness for the Primitive Recognition Calculus: candidate d'Alembert factorizations are ratio-orbit maps $\chi$, compared by cross-equivalence rather than definitional equality, so the development stays quotient-native.
A PRCRatioCharacter is such a map with three axioms: it sends the unit orbit to itself, multiplies under the orbit product, and intertwines reciprocal. The two-adic axis twist is the concrete countermodel one would build from a native 2-valuation: flip the prime-2 direction to its reciprocal, and fix every other prime axis by identity. Local orientation at the first mixed composite $2\cdot 3$ asks that $\chi(2\cdot 3)$ land on either that composite or its reciprocal.
The immediate upstream fact is the mixed-image lemma: under character axioms plus the two-adic twist, $\chi(2\cdot 3)$ is forced cross-equivalent to a mixed direction built from the twisted 2-axis and the fixed 3-axis. Cross-equivalence is an equivalence relation (symmetry and transitivity are used explicitly).
proof idea
Term-mode proof by contradiction. Assume local orientation at $2\cdot 3$. Invoke the mixed-image lemma to obtain $\chi(2\cdot 3)\sim$ mixed direction. Case-split the local-orientation disjunction.
Identity case: symmetrize the mixed-image equality and transitively compose with $\chi(2\cdot 3)\sim 2\cdot 3$, yielding mixed $\sim$ composite; discharge by the named non-cross-equivalence of mixed direction with the composite.
Reciprocal case: same symmetrize-and-transit, now against $\chi(2\cdot 3)\sim(2\cdot 3)^{-1}$; discharge by the reciprocal non-cross-equivalence lemma. No further character axioms are reopened.
why it matters
This is a local blocker in the two-adic branch of native cost uniqueness. Downstream, it feeds the existence statement that every two-adic-axis-twist ratio character fails $2\cdot 3$ local orientation, and the absurdity theorem that a local-orientation target for that twist cannot coexist with such a character. It is also used to refute the prime-calibration forcing target for nonunit-orbit local orientation, and appears in the conditional universal-foundation certificate.
In framework terms it closes the obvious valuation-style escape from J-cost uniqueness (T5 / RCL factorization): a character that only twists the 2-axis still cannot stay canonically oriented on the first mixed composite, so it cannot serve as a global d'Alembert factor for the native cost. The parent chain is eliminating non-J factorizations before promoting the PRC kernel into the universal foundation certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.