PRCCharacterTwoPrimeReciprocalExcludesPrimeIdentity
plain-language theorem explainer
Predicate on a ratio-orbit character: if the distinguished orbit-2 prime axis is reciprocal-oriented, then no native prime axis may be identity-oriented. Downstream uniqueness lemmas cite it as the atomic mixed-witness blocker on the orbit-2 branch. It is a pure Prop abbreviation (implication plus universal negation), not a proved theorem.
Claim. For a map $\chi$ on ratio orbits, if $\chi$ sends the distinguished prime-2 direction to its reciprocal (cross-multiplication equivalence), then for every prime distinction orbit $p$, $\chi$ does not send the $p$-direction to itself.
background
In the Primitive Recognition Calculus, ratio data live on RatioOrbit: a signed-orbit numerator over a nonzero distinction-orbit denominator. Two such displays are identified by cross-multiplication balance (crossEq), the internal PRC stand-in for rational equality. The total reciprocal on ratio orbits swaps num/den (sending zero to zero), matching the reciprocal automorphism and the ledger reciprocal event (source/target swap with inverse ratio).
A character $\chi$ orients each prime direction either toward identity (fixed by $\chi$ up to crossEq) or toward reciprocal. The distinguished orbit-2 axis is the first prime witness in the divisibility ladder. The identity event in observer forcing sits at the J-cost minimum $x=1$; identity orientation of a prime axis is the native fixed-point choice, reciprocal orientation is the inverted choice.
This module packages native-cost uniqueness hypotheses for characters that must eventually match the J-cost forced by T5 ($J(x)=(x+x^{-1})/2-1$). The present definition is the contrapositive normal form of the orbit-2 branch obstruction: reciprocal orientation at 2 forbids any identity-oriented native prime witness.
proof idea
No proof: the declaration is a def of a Prop. The body is the implication "crossEq of $\chi$ on the two-prime direction with the reciprocal of that direction" implies "for every prime orbit $p$, not crossEq of $\chi$ on the $p$-direction with the $p$-direction itself". Downstream theorems treat it as a named hypothesis or rewrite it via iff lemmas to witness and forcing forms.
why it matters
This is the atomic two-specific mixed-witness blocker in PRC native-cost uniqueness. Parent results include the iff with prime-identity-forces-two-prime-identity (under local orientation), the of-local-excludes bridge into that forcing statement, the witness-form equivalence, and the link to two-prime-reciprocal-forces-prime-reciprocal. Product-cost consistency theorems discharge the dual forcing side and thereby close orientation cases.
In the Recognition chain, characters must align with the unique J-cost (T5) and the self-similar $\phi$ fixed point (T6). Forbidding mixed identity/reciprocal witnesses on the prime ladder prevents non-J characters from surviving calibration. The definition itself proves nothing; it names the obstruction that uniqueness proofs case-split on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.