PRCTwoThreeCompositeLocalOrientationFailureCharacter_iff_ratio_character_axis_twist
plain-language theorem explainer
The constructive 2·3 composite-local orientation failure is equivalent to the bare existence of a ratio character with two-adic axis twist. Anyone tracking the native-cost uniqueness fork or the composite-local certificate cites this bridge. The proof is a two-constructor Iff assembled from the two one-way implications already proved in-module.
Claim. The following are equivalent: (i) there exists a ratio-orbit character $\chi$ that exhibits two-adic axis twist and fails $2\cdot 3$ composite-local orientation; (ii) there exists a ratio-orbit character $\chi$ that exhibits two-adic axis twist (with no further local-orientation demand).
background
In the Primitive Recognition Calculus native-cost uniqueness development, ratio characters are maps $\chi$ on ratio orbits that preserve the multiplicative structure used to build cost. The two-adic axis twist is the branch behavior that sends the orbit of $2$ to the reciprocal branch while keeping other native primes on the identity branch.
The composite-local orientation condition asks that such a twisted character still orient the mixed composite direction $2\cdot 3$ correctly. Its failure form is the constructive countermodel surface: a character that is a ratio character, carries the two-adic axis twist, and violates $2\cdot 3$ local orientation. The reduced target drops the orientation-failure conjunct and keeps only the twisted ratio character.
Upstream, one direction projects a failure witness to a twisted character by discarding the orientation negation; the converse invokes the forcing lemma that any two-adic axis-twist ratio character already forces the $2\cdot 3$ local-orientation failure.
proof idea
Term-mode Iff constructor. Left-to-right applies the projection lemma: from a failure witness $\langle\chi, h_\chi, h_{\mathrm{branch}}, \neg h_{\mathrm{local}}\rangle$ keep $\langle\chi, h_\chi, h_{\mathrm{branch}}\rangle$. Right-to-left applies the forcing theorem that every two-adic axis-twist ratio character yields a $2\cdot 3$ composite-local orientation failure, then packages that as the failure character. No new algebra is done here.
why it matters
This equivalence is the spine of the $2\cdot 3$ composite-local fork certificate: that certificate records exactly that failure iff ratio-character axis twist (and the calibrated two-adic variant). Downstream it is chained to the calibrated two-adic axis-twist character and to the dual form "local orientation for the twist target iff no failure character."
It also feeds the universal-foundation conditional certificate path, where native-cost uniqueness and character-branch control sit under the broader PRC foundation stack. In Recognition terms this is bookkeeping on the cost-character side of the forcing chain (J-uniqueness and the Recognition Composition Law live upstream of these character targets): it collapses the composite-defect obstruction to the reduced two-adic twist target so later calibration passes can treat one Prop instead of two.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.