PRCTwoThreeCompositeLocalOrientationFailureCharacter_absurd_of_two_three_local_orientation_target
plain-language theorem explainer
If every two-adic-axis ratio character is forced to pick a canonical local orientation at the mixed composite 2·3, then no countermodel character can exist that carries the two-adic twist yet fails that orientation. Native-cost uniqueness arguments cite this to discharge the constructive failure surface for the first mixed composite. The proof is a two-step term composition: failure yields a two-adic twist character, which the target already rules out.
Claim. Assume that every ratio character $\chi$ that carries the two-adic axis twist still satisfies the canonical local-orientation condition at the mixed composite $2\cdot 3$. Then there is no ratio character that simultaneously carries the two-adic axis twist and fails that $2\cdot 3$ local-orientation condition.
background
In the primitive recognition calculus, ratio characters are maps on ratio orbits that encode admissible branch choices for the native cost. The two-adic axis twist singles out characters that send the orbit of $2$ to the reciprocal branch. At the first mixed composite $2\cdot 3$, local orientation demands that such a character still choose one of the two canonical mixed values rather than an inconsistent assignment.
The positive target packages the universal claim: every ratio character with the two-adic axis twist obeys $2\cdot 3$ local orientation. The failure character is the existential dual: some ratio character has the twist yet violates that orientation. The doc-comment calls the failure form "the constructive countermodel surface equivalent to the reduced two-adic ratio-character target."
Upstream, the same module already proves that the failure character implies a bare two-adic-axis-twist ratio character, and that the positive target rules out any such twist character. The present result simply closes the dual pair.
proof idea
Term-mode composition of two sibling lemmas. Introduce the failure hypothesis. From it, PRCTwoAdicAxisTwistRatioCharacter_of_two_three_local_orientation_failure_character extracts a two-adic-axis-twist ratio character (forgetting the local-orientation negation). Feed that character into PRCTwoAdicAxisTwistRatioCharacter_absurd_of_two_three_local_orientation_target applied to the given positive target, which already asserts that no such twist character exists. The resulting contradiction discharges the failure.
why it matters
This lemma is the dual bridge that turns positive $2\cdot 3$ orientation targets into absurdity of the constructive failure surface. Three immediate parents re-apply it under stronger calibration hypotheses: mixed-composite cost consistency, prime-identity-forces-two, and prime-pair product cost consistency, each first promoting its hypothesis to the positive orientation target, then invoking this absurdity.
It also feeds prc_universal_foundation_conditional_certificate in UniversalFoundation, part of the conditional certificate stack for the primitive recognition calculus. In the Recognition forcing picture this sits inside native-cost uniqueness: ruling out non-canonical mixed branches at $2\cdot 3$ is a concrete obstruction step toward uniqueness of the J-cost (T5) and the forced self-similar structure downstream. No scaffolding remains here; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.