PRCTwoThreeCompositeLocalOrientationFailureCharacter_of_ratio_character_axis_twist
plain-language theorem explainer
A ratio character carrying the two-adic axis twist yields a constructive witness that fails two-three composite-local orientation. Cite this when equating the reduced twist target with the composite failure surface, or when assembling the conditional universal-foundation certificate. The proof is a one-line application of the forcing lemma that already builds the witness.
Claim. If there exists a map $\chi$ on ratio orbits that is a ratio character and realizes the two-adic axis twist, then there exists a ratio character that realizes that same twist and fails two-three composite-local orientation (i.e., $\neg$ of the local orientation condition on the $2\cdot 3$ composite).
background
In the Primitive Recognition Calculus native-cost uniqueness module, cost candidates are probed through ratio characters: maps $\chi$ on ratio orbits that preserve the multiplicative structure used to read off a cost. The two-adic axis twist is a branch condition on such a character (sending the orbit of $2$ to the reciprocal branch). The named target "two-adic axis twist ratio character" is the bare existence of a ratio character with that twist; Pass 115 notes that prime calibration becomes automatic once this branch is carried by a character.
The two-three composite-local orientation failure is the constructive countermodel surface equivalent to that reduced target: a ratio character with the two-adic twist that moreover fails local orientation on the composite direction $2\cdot 3$. Upstream, the forcing lemma already shows that any two-adic twist ratio character produces an explicit witness of that failure (the same $\chi$ with the negated orientation predicate).
proof idea
One-line term wrapper. Apply the upstream forcing theorem PRCTwoAdicAxisTwistRatioCharacter_forces_two_three_local_orientation_failure to the hypothesis. That lemma unpacks the existential twist character and returns a witness of ratio character, two-adic twist, and failure of two-three composite-local orientation, which is definitionally the failure-character Prop.
why it matters
Closes one direction of the equivalence between the reduced two-adic ratio-character target and the $2\cdot 3$ composite-local failure surface. Downstream, the iff theorem packages this arrow with its converse, so either formulation may be used as the obstruction. That equivalence feeds the conditional universal-foundation certificate in UniversalFoundation, which bundles kernel, real-complete ordered field, and trace-logic certificates. In the broader Recognition chain this sits inside native-cost uniqueness for the J-cost (T5), ensuring mixed-branch characters cannot quietly restore a second cost law on composite primes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.