PRCCharacterTwoPrimeReciprocalExcludesPrimeIdentity_of_identity_forces_two
plain-language theorem explainer
If identity orientation of a ratio-orbit character on any native prime axis forces identity on the distinguished prime-2 axis, then reciprocal orientation at prime 2 excludes identity on every native prime. Cost-uniqueness and mixed-witness blocker arguments cite this as the one-way bridge between those two normal forms. The proof is a short term argument: force identity at 2, transit to self-reciprocality, and contradict non-self-reciprocality of prime directions.
Claim. Let $\chi$ map ratio orbits to ratio orbits. Suppose that whenever $\chi$ is cross-equivalent to the identity on any native prime direction, it is likewise identity-oriented on the distinguished prime-$2$ direction. Then, if $\chi$ is reciprocal-oriented on the prime-$2$ direction, $\chi$ cannot be identity-oriented on any native prime direction.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer (signed-orbit) numerator over a nonzero distinction-nat denominator. Cross-equivalence is the internal PRC stand-in for rational equality: two ratio orbits match when scaled numerators balance as signed orbits. Reciprocal is the total multiplicative inverse on ratio orbits (zero maps to zero), matching the $\mathbb{Q}$ convention.
Characters in this module are maps $\chi$ on ratio orbits that feed native cost displays. Orientation language distinguishes identity orientation (cross-equivalent to the prime direction itself) from reciprocal orientation (cross-equivalent to that direction's reciprocal). The two-step orbit supplies a distinguished calibrated prime axis used as an anchor in uniqueness arguments.
The hypothesis is the one-sided normal form: identity at any calibrated prime axis forces identity at this orbit-2 axis. The conclusion is the contrapositive branch form: reciprocal orientation at orbit 2 forbids identity orientation at every native prime.
proof idea
Assume the forcing hypothesis, reciprocal orientation of $\chi$ at the two-prime direction, and identity orientation at some prime $p$. Apply the forcing hypothesis at $p$ to obtain identity orientation at the two-prime direction. Symmetrize that identity witness and compose it with the reciprocal witness by cross-equivalence symmetry and transitivity, yielding that the two-prime direction is cross-equivalent to its own reciprocal. Close by the lemma that no prime direction is cross-equivalent to its reciprocal, instantiated at the two-orbit.
why it matters
This implication is one half of the local biconditional between the two normal forms of the orbit-2 mixed-witness obstruction (under a local-orientation hypothesis on the character). Downstream it is reused both in that iff and in the target-level lift that turns prime-calibration forcing into the reciprocal-exclusion target. The native-cost uniqueness blocker certificate packages these orientation constraints: they rule out mixed identity/reciprocal prime witnesses that would permit non-unique native cost characters.
In the Recognition framework this sits in the foundation layer that pins native cost uniqueness on the path to J-uniqueness (T5) and the Recognition Composition Law, before $\phi$ is forced as the self-similar fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.