PRCTwoThreeCompositeLocalOrientationFailureCharacter_absurd_of_prime_identity_forces_two
plain-language theorem explainer
Under the hypothesis that prime calibration forces identity on the orbit-2 axis whenever any calibrated prime is identity, the constructive 2·3 composite-local orientation failure cannot exist. Native-cost uniqueness and the universal-foundation certificate cite this to rule out the two-adic twist countermodel. The proof is a two-step term composition: lift the prime-identity force to the two-three orientation target, then apply the existing absurdity lemma.
Claim. Assume that every ratio character which is prime-direction calibrated forces identity at the orbit-$2$ prime axis whenever it is identity at any calibrated prime axis. Then there is no ratio character $\chi$ that twists the two-adic axis and fails the $2\cdot 3$ composite-local orientation condition.
background
In the Primitive Recognition Calculus, ratio characters are maps $\chi$ on ratio orbits that encode how multiplicative directions are oriented (identity versus reciprocal branch). Prime-direction calibration restricts which primes may sit on which branch. The one-sided distinguished-axis target says: if any calibrated prime axis is identity, then the orbit-$2$ axis must also be identity.
The $2\cdot 3$ composite-local orientation failure is the constructive countermodel surface for the reduced two-adic ratio-character obstruction: existence of a ratio character that twists the two-adic axis and fails local orientation on the composite direction $2\cdot 3$. That witness is equivalent to the reduced two-adic target used in native-cost uniqueness.
This module builds uniqueness of the native cost (the $J$-cost of the forcing chain) from character and trace constraints. Upstream, the prime-identity-forces-two target already implies the two-three local-orientation-for-two-adic-twist target; a separate lemma turns that target into absurdity of the failure witness.
proof idea
Pure term-mode composition, no tactics. First apply the upstream lift ...ForTwoAdicAxisTwistTarget_of_prime_identity_forces_two to the given prime-calibration hypothesis; that yields the two-three composite local-orientation target for two-adic axis twist. Feed that target into ...FailureCharacter_absurd_of_two_three_local_orientation_target, which already proves that the orientation target contradicts existence of a twisted failure witness. The composite is therefore $\neg$ of the failure character.
why it matters
Closes one link in the native-cost uniqueness chain: the two-adic twist countermodel for $2\cdot 3$ composite orientation is incompatible with the distinguished-axis prime-calibration force. Downstream it is consumed by prc_universal_foundation_conditional_certificate, which packages kernel, real-complete ordered field, and trace-logic certificates into the conditional universal foundation.
In the broader Recognition Science forcing chain this supports $J$-uniqueness (T5): ruling out exotic ratio-character orientations is part of forcing the cost $J(x)=(x+x^{-1})/2-1$ as the unique native cost. Without this absurdity, a two-adic reciprocal branch could survive prime calibration and spoil uniqueness of the doubled-trace cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.