PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget
plain-language theorem explainer
Prime calibration of a ratio character is packaged as forcing the existential no-mixed-prime-witnesses property: an identity-oriented prime witness cannot coexist with a reciprocal-oriented one. Native-cost-uniqueness work cites this as the witness-form target in the prime-orientation chain. It is a pure Prop definition, not a proved theorem.
Claim. For every map $\chi$ on ratio orbits that is a ratio character and is prime-direction calibrated (its generated cost agrees with canonical $J$-cost on every prime orbit), $\chi$ has no mixed prime witnesses: it is impossible that some prime is identity-oriented under $\chi$ while some (possibly other) prime is reciprocal-oriented under $\chi$.
background
Ratio orbits are rational displays: a signed numerator over a nonzero distinction-nat denominator. A ratio character is a map $\chi$ on those orbits; cost is recovered from $\chi$ and compared to the canonical $J$-cost $J(x)=(x+x^{-1})/2-1$ forced by the Recognition Composition Law.
Prime-direction calibration means that on every native prime orbit the character-derived cost matches $J$ (cross-equality with the on-orbit $J$ value). The no-mixed-prime-witnesses predicate is the existential form of prime-axis no-mixing: there cannot simultaneously exist a prime $p$ with $\chi$ identity-oriented on the $p$-direction and a prime $r$ with $\chi$ reciprocal-oriented on the $r$-direction.
This module splits native cost uniqueness into exact Lean targets. The present definition is the one-sided witness-exclusion target: prime calibration should forbid any reciprocal-oriented prime witness once an identity-oriented prime witness exists.
proof idea
Definition only: the body is the universal Prop that every ratio character which is prime-direction calibrated satisfies the existential no-mixed-prime-witnesses predicate. No lemmas are applied and no goals are closed. Downstream proofs treat the packaged Prop as a hypothesis, discharge side of an iff, or input to absurdity lemmas against mixed-witness characters.
why it matters
This target is a named blocker in the native cost uniqueness program. It feeds the pass-25 blocker certificate that records which uniqueness subgoals remain open, and it is proved equivalent to the coherent-prime-orientation target. From it one derives the no-mixed-prime-orientation target and refutes existence of any prime-calibrated mixed-prime-witnesses character.
In the RS forcing picture this supports uniqueness of the native cost aligned with T5 $J$-uniqueness: mixed identity/reciprocal orientations on prime axes are exactly the residual freedom that would allow non-$J$ costs after prime calibration. Closing the target would collapse that residual on the prime skeleton.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.