PRCCharacterTwoPrimeReciprocalIdentityPrimeMixed_of_non_two_mixed
plain-language theorem explainer
The sharpened mixed-branch character hypothesis (orbit-2 reciprocal, some prime p≠2 identity-oriented) implies the unsharpened mixed-branch form (orbit-2 reciprocal, some prime identity-oriented). Anyone collapsing the two mixed predicates, or lifting calibrated characters, cites this. The proof is a one-line projection that forgets the p≠2 constraint.
Claim. Let $\chi$ be a map on rational orbits. If the distinguished two-prime axis is reciprocal-oriented under $\chi$ and there exists a native prime axis $p\neq 2$ that is identity-oriented under $\chi$, then the two-prime axis is reciprocal-oriented and some native prime axis is identity-oriented under $\chi$.
background
In the primitive recognition calculus, a RatioOrbit is a rational display: signed-orbit numerator over a nonzero distinction-nat denominator. Characters here are maps $\chi$ on those orbits. Orientation of an axis is recorded by crossEq: identity-oriented means $\chi$ fixes the axis up to that equivalence; reciprocal-oriented means $\chi$ sends it to its reciprocal.
The mixed-branch predicates isolate a configuration that would challenge orbit-2 witness exclusion: the distinguished two-prime direction is reciprocal, while at least one native prime direction stays identity. The sharpened form (NonTwoPrimeMixed) forces the identity witness to be a prime other than the orbit-2 axis; the unsharpened form (PrimeMixed) allows any native prime witness.
This module develops native-cost uniqueness via character and doubled-trace constraints (d'Alembert-type identities, cost-from-character reconstructions). The present lemma is a pure logical weakening between those two mixed configurations.
proof idea
Term-mode destructuring. Unpack the sharpened hypothesis into the two-prime reciprocal fact together with a witness triple $(p, hp, p\neq 2, \text{identity on }p)$. Rebuild the unsharpened mixed package from the same two-prime fact and the same $(p, hp, \text{identity})$, discarding only the inequality $p\neq 2$. No arithmetic or orbit algebra is invoked.
why it matters
Closes the easy direction of the equivalence between sharpened and unsharpened mixed branches (PRCCharacterTwoPrimeReciprocalIdentityPrimeMixed_iff_non_two). Also feeds the calibrated lift PRCPrimeCalibratedTwoPrimeReciprocalIdentityPrimeMixedCharacter_of_non_two_mixed, which carries the same forgetting step at the prime-calibrated character level.
In the native-cost uniqueness program these mixed configurations are the residual branch shapes that must be ruled out (or absorbed) before the character is forced onto the pure reciprocal or pure identity pattern tied to the J-cost. The lemma itself is bookkeeping, but without it the sharpened and unsharpened exclusion arguments cannot be identified. It sits upstream of the forcing path that eventually pins the unique native cost compatible with the Recognition Composition Law and T5 J-uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.