PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter_of_mixed
plain-language theorem explainer
Any prime-calibrated mixed character (orbit 2 reciprocal, some native prime identity-oriented) yields the sharpened non-2 mixed character (orbit 2 reciprocal, a non-2 prime identity-oriented). Used to equate the two mixed-character obstruction models and to restate the orbit-2 exclusion target. Proof unpacks the existential witness and applies the character-level mixed-to-non-2 reduction.
Claim. If there exists a ratio-orbit map $\chi$ that is a PRC ratio character, prime-direction calibrated, and mixed in the two-prime reciprocal/identity sense (orbit $2$ reciprocal and some native prime identity-oriented), then there exists such a $\chi$ that is mixed in the sharpened sense: orbit $2$ is reciprocal while some non-$2$ native prime is identity-oriented.
background
In the Primitive Recognition Calculus native-cost uniqueness development, ratio-orbit characters $\chi : \mathrm{RatioOrbit} \to \mathrm{RatioOrbit}$ encode how multiplicative ratio classes transform under the cost-compatible symmetry. A character is prime-direction calibrated when its action on native prime orbits matches the calibration demanded by the two-adic axis of the uniqueness argument.
Two mixed-character obstruction models sit above that calibration. The coarser model asserts existence of a calibrated $\chi$ with orbit $2$ reciprocal and some native prime identity-oriented. The sharpened model requires the identity-oriented prime witness to be non-$2$. Doc-comment on the coarser model: its nonexistence is equivalent to the orbit-$2$ mixed-witness exclusion target; constructing it would refute the character-rigidity route.
The character-level lemma already reduces prime-mixed data to non-two-prime-mixed data on a fixed $\chi$. This theorem lifts that reduction through the existential packaging that includes the ratio-character and calibration hypotheses.
proof idea
Term-mode unpack-and-repack. Destructure the hypothesis existential as $\langle \chi, h_\chi, h_{\mathrm{prime}}, h_{\mathrm{charMix}} \rangle$. Rebuild the target existential on the same $\chi$, keeping the ratio-character and prime-calibration witnesses, and replace the mixed-character conjunct by the upstream lemma PRCCharacterTwoPrimeReciprocalIdentityNonTwoPrimeMixed_of_mixed applied to $h_{\mathrm{charMix}}$. No new arithmetic; pure transport of the character-level implication through the calibrated packaging.
why it matters
Closes one direction of the equivalence between the coarser and sharpened calibrated mixed-character models, so the orbit-$2$ mixed-witness exclusion target can be stated indifferently with either packaging. Downstream, that equivalence feeds the restatement of the prime-calibration exclusion target as nonexistence of the sharpened non-two mixed character, and is consumed by the conditional universal-foundation certificate in UniversalFoundation.
In the broader Recognition Science forcing picture this sits inside native-cost uniqueness for the J-cost character calculus (the T5 uniqueness of $J(x)=(x+x^{-1})/2-1$ and the Recognition Composition Law). The character-rigidity branch aims to rule out mixed reciprocal/identity orientations on prime orbits; equating the two mixed models removes a packaging ambiguity before that exclusion is discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.