PRCPrimeCalibratedTwoPrimeReciprocalIdentityPrimeMixedCharacter
plain-language theorem explainer
Existence of a prime-calibrated ratio character that is reciprocal on the orbit-2 axis while identity-oriented on some other native prime. Researchers closing native cost uniqueness via character rigidity cite this as the exact mixed model whose nonexistence matches the orbit-2 exclusion target. The body is a pure Prop: three conjuncts under an existential, no proof content.
Claim. There exists a map $\chi$ on ratio orbits that is a ratio character, is prime-direction calibrated (its generated cost agrees with canonical $J$-cost on every native prime orbit), and is mixed: $\chi$ sends the distinguished prime-$2$ direction to its reciprocal while sending some other native prime direction to itself (identity orientation).
background
In the Primitive Recognition Calculus, a ratio orbit is a rational display: signed numerator over a nonzero distinction-nat denominator. Ratio characters are maps $\chi$ on those orbits used to manufacture a candidate cost via costFromCharacter. Calibration on prime directions means that manufactured cost matches the canonical $J$-cost on every native prime orbit (cross-equality of orbit values).
Two orientations appear throughout the forcing chain. The reciprocal automorphism (and the reciprocal recognition event) inverts the ratio; the identity event sits at the $J$-minimum $x=1$. The mixed branch packages a split: the distinguished axis at prime $2$ is reciprocal-oriented, while at least one other native prime axis stays identity-oriented.
This module isolates exact Lean targets that would finish native cost uniqueness. The present Prop is the sharpened calibrated mixed-character model whose nonexistence is equivalent to the orbit-$2$ mixed-witness exclusion target.
proof idea
Definitional packing only: the Prop is the existential
$\exists,\chi$ such that $\chi$ is a ratio character, $\chi$ is prime-direction calibrated, and $\chi$ satisfies the two-prime reciprocal / prime-identity mixed configuration. No tactics, no lemmas applied, no reduction. Downstream theorems unpack the triple by rcases and reassemble sibling mixed-character Props.
why it matters
Native cost uniqueness is the PRC route toward the unique $J$-cost of the forcing chain (T5: $J(x)=(x+x^{-1})/2-1$). This Prop is the exact calibrated mixed model that would break the character-rigidity path if inhabited. Downstream, its nonexistence is equivalent to the prime-calibration forces two-prime-reciprocal excludes prime-identity witness target, and thence to the stronger prime-identity forces two-prime-identity target. The blocker certificate lists the remaining open factorization and mixed-character obligations; this definition is one of those named obligations. Constructing a witness would refute the current rigidity route; proving $\neg$ of this Prop closes the orbit-$2$ exclusion branch.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.