PRCCharacterTwoPrimeReciprocalIdentityNonTwoPrimeMixed
plain-language theorem explainer
Defines the sharpened mixed-branch predicate on a ratio-orbit character: the distinguished 2-axis is reciprocal-oriented, and some other native prime axis is identity-oriented. Uniqueness and defect arguments cite it as the concrete two-adic countermodel shape. The body is a pure Prop conjunction (cross-equality to reciprocal on 2, plus an existential non-2 prime fixed point).
Claim. A map $\chi$ on ratio orbits is a sharpened mixed two-prime character when (i) $\chi$ sends the orbit-$2$ prime direction to its reciprocal (equality of ratio orbits under cross-multiplication), and (ii) there exists a native prime orbit $p\neq 2$ whose prime direction is fixed by $\chi$ (identity-oriented under the same cross-equality).
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: a signed-orbit numerator over a nonzero distinction-nat denominator. Two such displays are identified by crossEq when cross-multiplication balances as signed orbits (the internal PRC stand-in for rational equality).
Characters here are maps $\chi$ on ratio orbits that reorient prime axes. Reciprocal orientation means $\chi$ sends a direction to its reciprocal orbit (the inverse-ratio event in the ledger picture). Identity orientation means $\chi$ fixes the direction. The distinguished two-prime direction is the native orbit-$2$ axis; other prime directions are built from prime distinction-nats.
The module develops native-cost uniqueness for PRC characters. This predicate isolates the obvious two-adic twist: flip only the $2$-axis and leave some other prime axis unflipped. Upstream cost/ledger language supplies the reciprocal automorphism and the zero-cost identity event at ratio $1$; here those notions are internalized as orbit-level cross-equalities.
proof idea
Definitional unpacking only: the Prop is the conjunction of (1) cross-equality of $\chi$ on the two-prime direction with the reciprocal of that direction, and (2) an existential over a prime distinction-nat $p$ with prime-orbit certificate, $p\neq$ the two-orbit, such that $\chi$ on that prime direction is cross-equal to the direction itself. No tactics or lemmas; the name packages this mixed branch for later iff and implication lemmas.
why it matters
This is the sharpened mixed branch used throughout native-cost uniqueness. Downstream, it is equivalent (under a ratio-character hypothesis) to the non-two composite-defect form, and it is interchangeable with the weaker prime-mixed predicate via forget/strengthen lemmas that drop or restore $p\neq 2$.
Those bridges feed calibrated two-prime character statements and appear among open targets in the universal-foundation ledger. In framework terms it fences the two-adic countermodel one would build from a native $2$-valuation: reciprocal on orbit $2$, identity on some other prime. Closing uniqueness of the native $J$-cost character (T5-adjacent in the forcing chain) requires ruling out or absorbing exactly this mixed configuration, so the predicate is the named obstruction rather than a physics claim by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.