PRCCharacterTwoPrimeReciprocalIdentityPrimeMixed
plain-language theorem explainer
Names the mixed character configuration that would break orbit-2 witness exclusion: the map sends the distinguished prime-2 axis to its reciprocal, yet fixes some native prime axis. Downstream uniqueness and exclusion lemmas cite it as the forbidden mixed branch. The body is a bare Prop conjunction of two cross-equality conditions; no proof work.
Claim. A map $\chi$ on ratio orbits is two-prime-reciprocal / prime-identity mixed when $\chi$ of the distinguished orbit-$2$ axis is cross-equivalent to the reciprocal of that axis, and there exists a native prime orbit $p$ such that $\chi$ of the $p$-axis is cross-equivalent to the $p$-axis itself.
background
In the Primitive Recognition Calculus, ratio orbits are rational displays built from signed orbits over nonzero distinction-nat denominators. Cross-equivalence (crossEq) is the internal PRC rational relation: two ratio orbits match when the scaled numerators balance under cross-multiplication, the orbit-level stand-in for equality in $\mathbb{Q}$. Reciprocal is the total inversion map on ratio orbits (zero to zero).
Distinction-nats are the base-neutral finite orbits of repeated distinction; a prime orbit is a nonzero non-unit with no nontrivial factorization. The distinguished orbit-$2$ axis and the prime-direction axes are the native prime directions on which a ratio-orbit character $\chi$ can act either by identity orientation or by reciprocal orientation.
The surrounding module develops native cost uniqueness for PRC characters. This definition isolates the exact mixed branch that would refute exclusion of an identity-oriented prime witness once the orbit-$2$ axis is already reciprocal-oriented.
proof idea
Definitional unpacking only: the Prop is the conjunction of (i) cross-equivalence of $\chi$ on the two-prime direction with the reciprocal of that direction, and (ii) existence of a prime orbit $p$ whose prime direction is fixed by $\chi$ up to cross-equivalence. No tactics, no lemmas applied.
why it matters
This is the sharpened mixed-branch witness used throughout native cost uniqueness. Downstream, exclusion of a prime-identity witness is literally the negation of this Prop (PRCCharacterTwoPrimeReciprocalExcludesPrimeIdentityWitness_iff_not_mixed and the two one-direction implications). It also feeds the non-two mixed variant and the calibrated two-prime character package, and appears among the open targets listed by PRCUniversalFoundationOpenTargets.
In the Recognition forcing chain, native cost uniqueness sits under the J-cost / character layer that eventually forces $J(x)=(x+x^{-1})/2-1$ (T5) and the self-similar fixed point $\phi$ (T6). Pinning which mixed orientations are admissible is part of closing that uniqueness path: a character cannot be reciprocal on the orbit-$2$ axis and identity on another native prime axis at once if the exclusion theorems hold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.