PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter
plain-language theorem explainer
Existence of a prime-calibrated ratio character that is reciprocal on the orbit-2 axis and identity-oriented on some other native prime. Native-cost uniqueness arguments cite this Prop when routing the sharpened mixed branch. The body is pure packaging: three conjuncts under a single existential.
Claim. There exists a map $\chi$ from ratio orbits to ratio orbits such that $\chi$ is a ratio character (unit at $1$, multiplicative up to cross-equivalence), the cost generated by $\chi$ agrees with canonical $J$-cost on every native prime direction, $\chi$ sends the orbit-$2$ prime direction to its reciprocal, and there is at least one native prime $p\neq 2$ on which $\chi$ is identity-oriented.
background
Ratio orbits are the quotient-native display of rational data in the primitive recognition calculus: a signed numerator orbit over a nonzero distinction-nat denominator. The distinguished orbit two is the ratio with numerator the orbit of $2$ and denominator $1$.
A ratio character $\chi$ is a candidate factor in the d'Alembert factorization of a PRC cost. It is required to fix the unit orbit and to be multiplicative, both up to cross-equivalence rather than definitional equality, so the notion stays quotient-native. Prime-direction calibration demands that the cost reconstructed from $\chi$ match the canonical $J$-cost on every native prime orbit.
The mixed conjunct sharpens the branch: $\chi$ is reciprocal on the $2$-prime direction, while some other native prime is identity-oriented. That separation keeps the $2$-axis from serving as its own identity witness.
proof idea
Definitional packaging only. The Prop is the existential of a map $\chi$ together with the three named conjuncts (ratio character, prime-direction calibration, and the sharpened two-reciprocal / non-two-identity mixed configuration). No proof obligations are discharged here.
why it matters
This Prop is the sharpened mixed-character node in the native-cost uniqueness tree. Downstream, it implies the distinct-prime mixed-pair witness, the non-two composite-defect character, and is equivalent to that composite-defect form. Negating it kills the calibrated two-adic axis-twist character; several introduction lemmas rebuild it from coarser mixed or twist hypotheses.
In the broader framework this sits under character rigidity for the PRC cost, the route that forces the unique $J$-cost of the forcing chain (T5: $J(x)=(x+x^{-1})/2-1$). Constructing or refuting a concrete model of this Prop is the native-valuation path that either closes or reopens the mixed branch of uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.