PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget_of_coherent_prime_orientation
plain-language theorem explainer
Prime cost calibration that forces one coherent orientation on all native prime axes also forces the existential no-mixed-prime-witnesses form. Native-cost uniqueness and universal-foundation certificates cite this implication when collapsing orientation blockers. The proof is a short unpacking: feed the orientation target into the character-level coherence-to-no-mixed lemma.
Claim. Assume that whenever $\chi$ is a ratio character that is prime-direction calibrated, prime cost calibration forces $\chi$ to have a single coherent prime orientation. Then the same hypotheses force the existential no-mixed form: $\chi$ cannot simultaneously admit an identity-oriented prime witness and a reciprocal-oriented prime witness.
background
In the primitive recognition calculus, a ratio character $\chi$ is a map on ratio orbits that encodes how multiplicative structure is read by the native cost. Prime-direction calibration means each native prime axis is assigned a definite branch (identity versus reciprocal). Coherent prime orientation strengthens that: the branch choice is globally consistent across all native primes, so independent prime inversions cannot be mixed.
The no-mixed-prime-witnesses target is the existential twin of that coherence demand. It asks that no calibrated character carry both an identity-oriented prime witness and a reciprocal-oriented prime witness at once. The module treats these two Props as interchangeable blockers on the path to native-cost uniqueness.
Upstream, the character-level lemma already shows that coherence of a single $\chi$ yields the no-mixed property for that $\chi$. The present declaration lifts that implication to the quantified calibration targets.
proof idea
Term-style unpacking of the two target Props. Introduce a ratio character $\chi$ together with the ratio-character and prime-direction-calibration hypotheses. Apply the coherent-orientation target hypothesis to those data to obtain coherence of $\chi$. Discharge the goal by the character-level theorem that coherence implies no mixed prime witnesses. No extra algebraic work.
why it matters
Closes one direction of the equivalence between the coherent-orientation blocker and the existential no-mixed-witnesses blocker, so either form may be used in certificates. Downstream, the iff theorem packages both directions; the prime-pair product-cost-consistency route reduces to this implication after it first obtains coherent orientation. The native-cost uniqueness blocker certificate and the conditional universal-foundation certificate both depend on this family of orientation blockers. In the Recognition forcing chain this sits inside the foundation layer that pins the native cost before J-uniqueness (T5) and the phi fixed point (T6) are consumed by physics constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.