PRCPrimeCalibrationForcesNoMixedPrimeOrientationTarget
plain-language theorem explainer
Names the no-mixing target: any ratio character whose cost matches canonical J-cost on every prime direction must not pick identity on one prime axis and reciprocal on another. Native-cost uniqueness proofs cite it as the global coherence half of prime orientation. The body is a pure Prop abbreviation, not a proved implication.
Claim. The following proposition is the no-mixing target: for every map $\chi$ on rational orbits, if $\chi$ is a ratio character (unit at $1$, multiplicative up to cross-equivalence) and is prime-direction calibrated (its induced cost agrees with canonical $J$-cost on every prime orbit), then $\chi$ has no mixed prime orientation (identity on one prime axis forces identity on every prime axis).
background
In the primitive recognition calculus, costs factor through ratio characters on RatioOrbit (signed numerator over a nonzero distinction-nat denominator). A ratio character is quotient-native: it fixes the unit orbit and is multiplicative up to cross-equivalence, the native equality on orbits.
Prime-direction calibration means the cost generated by $\chi$ agrees with the canonical $J$-cost on every prime orbit direction. No mixed prime orientation is the trace-coherence condition: if $\chi$ acts as the identity on one prime direction, it cannot act as reciprocal on another; independent prime-axis inversions are forbidden.
This module packages native-cost uniqueness into exact Lean targets. The present declaration is the global no-mixing half of that package: calibration on primes should force a single coherent orientation across all primes.
proof idea
There is no proof. The declaration is a def equating a name to the universal statement
$\forall,\chi,;\mathrm{RatioCharacter}(\chi)\to\mathrm{PrimeCalibrated}(\chi)\to\mathrm{NoMixedOrientation}(\chi)$.
Downstream lemmas discharge or relate this target by applying character-level lemmas such as no-mixed-from-branch-uniformity, no-mixed-from-identity-witness-excludes-reciprocal, or the iff with prime-identity trace coherence.
why it matters
Native cost uniqueness needs characters that match $J$ on primes to be globally orientation-coherent; mixed identity/reciprocal choices on different primes would break the d'Alembert factorization path to unique $J$. This target is the named Prop for that demand.
It feeds the coherent-orientation target via the local-and-nomixed combiner, the blocker certificate that splits remaining uniqueness gaps into exact Lean goals, and a family of discharge lemmas (branch uniformity, no mixed witnesses, reciprocal globalization, trace coherence, and the iff with prime-identity trace coherence). In the forcing chain it sits under T5 $J$-uniqueness and the Recognition Composition Law: only a single coherent character branch is compatible with calibrated prime costs.
The target itself is still open as a theorem; several _of_* lemmas reduce it to narrower witness or uniformity goals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.