PRCPrimeCalibrationForcesPrimeIdentityWitnessExcludesReciprocalTarget_of_no_mixed_prime_witnesses
plain-language theorem explainer
Prime calibration that rules out mixed prime witnesses automatically rules out reciprocal-oriented prime witnesses once any identity-oriented one exists. Anyone tracking the native-cost uniqueness ladder cites this as the one direction of the equivalence between those two calibration targets. The proof is a one-line lift: apply the character-level exclusion lemma to the no-mixed hypothesis at each calibrated character.
Claim. If every prime-direction-calibrated ratio character has no mixed prime witnesses, then every such character also satisfies: the existence of an identity-oriented native prime witness excludes any reciprocal-oriented native prime witness.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits that encodes orientation data for the native cost. Prime-direction calibration fixes how $\chi$ treats prime axes. A mixed prime witness is a pair consisting of an identity-oriented native prime witness and a reciprocal-oriented one on the same character; the no-mixed target asserts that calibrated characters never carry both.
The one-sided exclusion target is weaker in appearance: once an identity-oriented prime witness exists, no reciprocal-oriented prime witness is allowed. At the single-character level this is immediate from no-mixed data, since a reciprocal witness together with an identity witness is exactly a mixed pair.
This module packages those properties as universal "target" propositions quantified over all ratio characters that are prime-direction calibrated. The present result lifts the character-level implication to those targets.
proof idea
Term-mode one-liner. Introduce a calibrated ratio character $\chi$. Instantiate the no-mixed target hypothesis at $\chi$ to obtain PRCCharacterNoMixedPrimeWitnesses χ. Feed that into the upstream lemma PRCCharacterPrimeIdentityWitnessExcludesReciprocal_of_no_mixed_prime_witnesses, which itself is a one-line contradiction: an identity witness plus a reciprocal witness is a mixed pair. The result is exactly the one-sided exclusion property at $\chi$, hence the target.
why it matters
Closes one half of the equivalence between the existential no-mixed prime-witness target and the one-sided identity-excludes-reciprocal target (PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget_iff_identity_witness_excludes_reciprocal). That equivalence is bookkeeping inside the native-cost uniqueness development: both formulations appear as calibration obligations on characters before the cost functional is forced.
Downstream it is wired into prc_native_cost_uniqueness_blocker_certificate and, via the broader certificate stack, into prc_universal_foundation_conditional_certificate. In the Recognition forcing chain this sits under the J-uniqueness / native-cost layer (T5 and the Recognition Composition Law), where orientation of prime witnesses must be rigid before the cost $J(x)=(x+x^{-1})/2-1$ is identified as the unique native cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.