PRCCharacterTwoPrimeReciprocalIdentityNonTwoPrimeMixed_of_mixed
plain-language theorem explainer
If a ratio-orbit character sends the distinguished two-prime axis to its reciprocal while some native prime axis stays identity-oriented, the identity witness can be taken strictly off the two-orbit. Anyone classifying mixed branch characters for native cost uniqueness cites this sharpening. The proof is a short case split: the two-orbit itself cannot be both reciprocal and identity, by the prime-direction non-self-reciprocal lemma.
Claim. Let $\chi$ be a map on ratio orbits. Suppose $\chi$ sends the distinguished two-prime direction to its reciprocal (under cross-equivalence), and there exists some native prime orbit that $\chi$ fixes up to cross-equivalence. Then there exists a native prime orbit $p$ with $p \neq 2$ that $\chi$ likewise fixes up to cross-equivalence.
background
In the Primitive Recognition Calculus, ratio data live on RatioOrbit: a signed-orbit numerator over a nonzero distinction-nat denominator. Equality of displays is the internal cross-multiplication relation crossEq (K4.10): two orbits match when scaled numerators balance. Reciprocals are total on this type, sending zero to zero as in $\mathbb{Q}$.
Characters here are maps $\chi$ on ratio orbits that orient prime axes either as identity or as reciprocal. The mixed branch of interest has the distinguished two-prime direction reciprocal-oriented, while at least one native prime axis remains identity-oriented. The sharpened form of that mixed branch requires the identity witness to be explicitly not the two-orbit.
The two-orbit is the two-step distinction position. Upstream, crossEq is symmetric and transitive (choice-free via an integer bridge), so orientation data can be transported along the relation.
proof idea
Destructure the mixed hypothesis into the two-prime reciprocal fact and a witness prime $p$ that is identity-oriented. Keep the reciprocal half and case on whether $p$ equals the two-orbit.
If $p$ is the two-orbit, the identity orientation becomes an identity orientation of the two-prime direction. Transporting with crossEq_symm and crossEq_trans against the reciprocal half yields that the two-prime direction is cross-equivalent to its own reciprocal. That contradicts primeDirection_not_crossEq_recip on the two-orbit (which is prime).
If $p$ is not the two-orbit, repackage the same witness into the sharpened existential.
why it matters
Native cost uniqueness in PRC needs a clean partition of character branches on prime axes. The mixed configuration (two-prime reciprocal, some prime identity) is the dangerous residual case; this lemma removes the degenerate subcase where the identity witness is two itself, so later arguments can treat a genuine off-two identity prime.
Downstream, it feeds the equivalence PRCCharacterTwoPrimeReciprocalIdentityPrimeMixed_iff_non_two (mixed iff sharpened mixed) and the calibrated lift PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter_of_mixed. Those sit on the path that forces characters compatible with the native J-cost, tying into T5 J-uniqueness ($J(x)=(x+x^{-1})/2-1$) and the Recognition Composition Law in the forcing chain.
Without the sharpening, case analyses on prime-calibrated characters would carry a vacuous two-as-identity branch already ruled out by non-self-reciprocal primes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.