PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget_iff_coherent_prime_orientation
plain-language theorem explainer
The existential no-mixed-prime-witness target is equivalent to the coherent prime-orientation target under prime direction calibration of ratio characters. Anyone tracking the native-cost uniqueness blockers can cite this to swap formulations freely. The proof is a two-constructor Iff built from the two already-proved one-way implications.
Claim. The following are equivalent: (i) every prime-direction-calibrated ratio character has no mixed prime witnesses; (ii) every prime-direction-calibrated ratio character has coherent prime orientation across all native prime axes.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits that encodes multiplicative cost structure. Prime direction calibration means $\chi$ has already fixed a preferred branch at each native prime axis (the identity-oriented versus reciprocal-oriented choice).
Two blocker formulations appear. The no-mixed-prime-witnesses target asserts that, once an identity-oriented prime witness exists, no reciprocal-oriented prime witness may coexist: an existential witness-exclusion form of orientation purity. The coherent prime-orientation target is the sharper global form: calibration must pick one coherent orientation across every native prime axis, ruling out independent mixed inversions.
Both sit inside the native-cost uniqueness development, where the goal is to force the cost functional toward the unique $J$-shape (the T5 landmark $J(x)=(x+x^{-1})/2-1$) by eliminating competing character branches.
proof idea
Term-mode Iff constructor. The forward direction applies the upstream theorem that no-mixed prime witnesses (plus the already-proved local orientation target) imply coherent prime orientation. The reverse direction applies the upstream theorem that coherent orientation immediately yields no mixed prime witnesses, by specializing the universal quantifier over characters and invoking the pointwise coherence-to-no-mixed lemma. No new algebra is done here.
why it matters
This equivalence lets the uniqueness pipeline treat the existential witness form and the global coherence form as interchangeable. Downstream, the refutation of the no-mixed-witnesses target is obtained by transporting the coherent-orientation refutation across the forward map of this Iff. The same link feeds the native-cost uniqueness blocker certificate and the conditional universal-foundation certificate.
In framework terms it tightens the orientation half of the native-cost uniqueness argument that supports J-uniqueness (T5) and the Recognition Composition Law. It does not itself close uniqueness; it only identifies two blocker phrasings so that a single counterexample or proof discharges both.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.