PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget_iff_no_mixed_prime_orientation
plain-language theorem explainer
Equivalence of two no-mixed-prime targets under prime cost calibration: the existential witness form and the orientation form. Native-cost uniqueness and blocker-certificate work cite it to move freely between those phrasings. The proof is a pure Iff constructor from the two already-proved one-direction 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 no mixed prime orientation (no independent identity versus reciprocal choices on distinct prime axes).
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits that encodes how multiplicative structure is read as cost. Prime-direction calibration fixes the cost response on prime axes so that each prime is treated in a calibrated identity or reciprocal sense rather than arbitrarily.
Two target Props package the same intended constraint. The orientation target demands that calibration forbid independent mixed identity/reciprocal choices across different prime axes. The witnesses target is the existential form of that demand: once an identity-oriented prime witness exists, no reciprocal-oriented prime witness is allowed (and symmetrically in the supporting lemmas).
This module develops native-cost uniqueness for PRC characters. The two targets sit among a chain of equivalent blockers (orientation, witnesses, trace coherence) used to classify which calibration hypotheses actually force a unique native cost.
proof idea
Term-mode Iff introduction. The forward direction applies the upstream lemma that the witnesses target implies the orientation target (by specializing the universal quantifier over characters and invoking the character-level orientation-from-witnesses fact). The reverse direction applies the dual upstream lemma that orientation implies witnesses. No new arithmetic or case analysis appears here.
why it matters
This bridge lets the development treat witness-exclusion and orientation-no-mixing as interchangeable calibration goals. Downstream, the orientation target is refuted by transporting the witnesses-target refutation across this equivalence. The same link is the first half of the chain equating the witnesses target with prime-identity trace coherence, which feeds native-cost uniqueness blocker certificates and the conditional universal-foundation certificate.
In framework terms it is bookkeeping inside the PRC native-cost uniqueness story, not a T5–T8 forcing step. It clarifies that mixed-prime freedom, if present, can be detected either as orientation mixing or as concrete prime witnesses, so a single refutation kills both phrasings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.