PRCCharacterTwoPrimeReciprocalIdentityNonTwoPrimeMixed_of_composite_defect
plain-language theorem explainer
If a ratio-orbit character sends the orbit-2 axis to its reciprocal and some other native prime p to the identity, and also forces the composite 2p direction to the mixed value p/2, then the weaker mixed-branch configuration already holds. Anyone classifying two-prime reciprocal/identity branch patterns cites this. The proof is a one-line projection that drops the composite conjunct.
Claim. Let $\chi$ be a map on rational orbits. Suppose $\chi$ sends the orbit-$2$ direction to its reciprocal, there is a native prime $p\neq 2$ sent to the identity direction, and $\chi$ sends the composite direction $2\cdot p$ to the mixed value $p/2$. Then $\chi$ satisfies the sharpened mixed-branch configuration: orbit $2$ is reciprocal-oriented and some native prime other than $2$ is identity-oriented.
background
In the Primitive Recognition Calculus, characters act on RatioOrbit displays (signed numerator over a nonzero distinction-nat denominator). Branch orientation is recorded by crossEq: identity keeps a prime direction fixed; reciprocal sends it to its inverse orbit.
The mixed configuration asserts that orbit $2$ is reciprocal while some other native prime axis $p$ is identity. The composite-defect form strengthens this by requiring that the product direction $2\cdot p$ land on the mixed value $p/2$. That extra clause is the obstruction signature used later when matching characters against native cost and doubled-trace D'Alembert data.
Locally this sits in the native-cost uniqueness development: one classifies which ratio characters can arise from a cost functional, and the two-adic reciprocal / non-two identity mixed branch is a principal obstruction case.
proof idea
Term-mode projection. Unpack the composite-defect hypothesis as the reciprocal-on-2 fact together with a witness prime $p\neq 2$ that is identity-oriented and the composite clause on $2p$. Rebuild the mixed configuration from the same $p$ witness, discarding the composite conjunct. No arithmetic or character axioms are invoked.
why it matters
Feeds the biconditional that, for genuine ratio characters, mixed configuration is equivalent to composite defect, and the prime-calibrated lift that turns a composite-defect character package into a mixed-character package. Those equivalences let the uniqueness argument switch freely between the short mixed witness and the stronger composite obstruction when ruling out non-native costs.
In the broader Recognition forcing chain this is bookkeeping inside the native $J$-cost uniqueness layer (the T5 uniqueness of $J(x)=(x+x^{-1})/2-1$), not a new physical constant. It closes a small interface gap so later prime-calibrated theorems can quote either form without re-proving witness extraction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.