PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget_iff_no_failure_character
plain-language theorem explainer
The positive 2·3 composite-local orientation target for two-adic axis-twist characters is equivalent to the absence of any failure witness character. Anyone closing the two-adic branch blocker or assembling the composite-local fork certificate cites this bridge. The proof is a two-step term chain: target ↔ no ratio-axis-twist character, then failure character ↔ that same ratio-axis-twist character, composed with not_congr.
Claim. The assertion that every ratio character carrying a two-adic axis twist still chooses one of the two canonical local orientations at the mixed composite $2\cdot 3$ is equivalent to the non-existence of a ratio character that carries a two-adic axis twist and fails that $2\cdot 3$ composite-local orientation.
background
In the Primitive Recognition Calculus native-cost uniqueness development, ratio characters are maps on ratio orbits obeying the multiplicative character laws used to reconstruct cost. A two-adic axis twist marks the branch where the character sends the orbit of $2$ along the reciprocal (axis) direction rather than the identity branch.
The positive target requires that any such twisted character still pick one of the two canonical local orientations at the first mixed composite $2\cdot 3$. The failure character is the existential dual: a concrete witness $\chi$ that is a ratio character, carries the two-adic axis twist, and violates that local orientation. The module treats this failure surface as the constructive countermodel equivalent of the reduced two-adic ratio-character target.
Upstream, the target is already known equivalent to the non-existence of a two-adic axis-twist ratio character, and the failure character is known equivalent to that same reduced ratio-character proposition. Those two bridges are the only inputs.
proof idea
Pure term-mode composition. Start from the already-proved equivalence of the positive target with the negation of the two-adic axis-twist ratio-character proposition. Compose (via trans and not_congr) with the symmetric form of the equivalence between the failure character and that same ratio-character proposition. The intermediate ratio-character atom cancels, leaving target ↔ ¬ failure character. No new case analysis.
why it matters
This is the clean De Morgan bridge between the universal (blocker) form and the existential (countermodel) form of the $2\cdot 3$ composite-local orientation constraint on two-adic axis twists. Downstream it is the hinge for the one-direction introduction lemmas that recover the target from any of several negated obstruction characters (no failure character, no calibrated two-adic axis twist, no non-two composite defect, no non-two composite cost defect, no non-two mixed character), and for the further equivalence of the target with the absence of a prime-calibrated two-adic axis-twist character.
It is packaged into prcTwoThreeCompositeLocalForkCertificate and is consumed by the conditional universal-foundation certificate. In the Recognition forcing picture this sits inside native-cost uniqueness for the J-cost (T5), ruling out rogue two-adic branches before the self-similar fixed point $\phi$ and the eight-tick structure are forced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.