PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget_iff_no_ratio_character_axis_twist
plain-language theorem explainer
The 2·3 composite-local orientation obligation on two-adic axis-twist ratio characters is equivalent to there being no such ratio character at all. Downstream fork certificates and cost-consistency discharge lemmas cite this bridge. The proof is a pure term pairing of the two directed lemmas already proved in-module.
Claim. The assertion that every ratio character carrying a two-adic axis twist must adopt one of the two canonical local orientations at the mixed composite $2\cdot 3$ is equivalent to the nonexistence of any ratio character that carries a two-adic axis twist.
background
In the Primitive Recognition Calculus native-cost uniqueness development, a ratio character is a map on ratio orbits obeying the PRC character axioms. The two-adic axis twist is a branch behavior on such characters: the uncalibrated construction target asserts existence of some ratio character that carries this twist.
The positive $2\cdot 3$ composite-local form of the current two-adic branch blocker demands more: every ratio character that carries the two-adic axis branch must still choose one of the two canonical local orientations at the first mixed composite $2\cdot 3$. Doc-comment: "Positive 2*3 composite-local form of the current two-adic branch blocker."
The two directed lemmas already establish that this universal orientation obligation forces nonexistence of any twisting ratio character, and conversely that nonexistence yields the obligation vacuously. This theorem packages that logical equivalence.
proof idea
Term-mode Iff introduction by pairing the two directed results already in the module. Left-to-right applies the absurdity lemma: from the composite-local orientation target one obtains $\neg$ of the two-adic axis-twist ratio-character existence claim. Right-to-left applies the vacuous discharge: from nonexistence of any twisting ratio character, the universal orientation obligation holds by ex falso on any candidate witness. No new algebraic content is introduced.
why it matters
This equivalence is the hinge that lets the $2\cdot 3$ composite-local orientation target be rewritten as absence of a two-adic axis-twist ratio character, and then chained further to absence of a failure character. Downstream, prcTwoThreeCompositeLocalForkCertificate records the fork; the sibling iff-to-no-failure-character theorem is obtained by composing this result with the failure-character equivalence.
Several discharge lemmas (mixed-composite cost consistency, prime-identity forces two, prime-pair product cost consistency) obtain the orientation target by modus ponens through this iff after proving the corresponding axis-twist character is absurd. The same bridge is consumed by the universal-foundation conditional certificate in UniversalFoundation, tying the local two-adic branch blocker into the broader PRC foundation stack that supports native-cost uniqueness and the J-cost forcing chain (T5).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.