PRCCharacterTwoPrimeReciprocalExcludesPrimeIdentityWitness
plain-language theorem explainer
Atomic mixed-witness blocker for ratio-orbit characters: reciprocal orientation on the distinguished orbit-2 axis cannot coexist with identity orientation on any native prime axis. Cost-uniqueness arguments cite it to rule out mixed branch configurations. It is a pure Prop abbreviation packaging an implication to False from two cross-equality hypotheses.
Claim. For a map $\chi$ on ratio orbits, the following is contradictory: $\chi$ sends the distinguished prime-$2$ direction to its reciprocal (cross-equality), and there exists at least one native prime orbit $p$ such that $\chi$ fixes the corresponding prime direction (cross-equality to the identity orientation).
background
In the Primitive Recognition Calculus, ratio data live as RatioOrbit displays: a signed-orbit numerator over a nonzero distinction-nat 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 numerator and denominator (sending zero to zero), matching the reciprocal automorphism and the ledger reciprocal event that inverts recognition ratios.
A ratio character $\chi$ orients each prime direction either toward the identity axis or toward its reciprocal. The distinguished orbit-$2$ direction is the two-prime axis; native primes supply further axes via prime-orbit witnesses. The local setting is native cost uniqueness: characters that feed the doubled-trace / d'Alembert cost must not mix reciprocal orientation at $2$ with identity orientation at any other prime.
Upstream, identity is the zero-cost recognition event at ratio $1$; reciprocal is the inverse-ratio event. Those ledger notions are mirrored here purely on $\delta$-orbit positions.
proof idea
No proof body: this is a def of a Prop. The right-hand side is the implication
$(\chi(\text{two-prime direction})\sim\mathrm{recip}(\text{two-prime direction}))\to\bigl(\exists,p\text{ prime}:\ \chi(\text{prime direction of }p)\sim\text{that direction}\bigr)\to\mathrm{False},$
with $\sim$ written as RatioOrbit.crossEq. It packages the atomic mixed-witness obstruction as a single predicate on $\chi$.
why it matters
This witness is the atomic two-specific mixed-branch blocker used throughout native cost uniqueness. Downstream, it is equivalent to the non-witness exclusion predicate and to the negation of the mixed configuration (reciprocal at $2$ plus some identity prime). It converts into the global statement that reciprocal orientation at the two-prime axis excludes every identity-oriented native prime, and under local prime-orientation hypotheses it is equivalent to “prime identity forces two-prime identity.”
Those bridges feed the theorems that derive prime-identity-forces-two-prime-identity from prime-pair product cost consistency for calibrated PRC ratio characters. In the broader Recognition forcing chain this sits under uniqueness of the native cost (the J-cost side of T5): mixed reciprocal/identity orientations on prime axes would spoil the d'Alembert / doubled-trace match that pins $J(x)=(x+x^{-1})/2-1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.