PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityTarget_iff_witness
plain-language theorem explainer
The orbit-2 reciprocal exclusion target (under prime-direction calibration, no native prime axis stays on identity once orbit 2 is reciprocal) is equivalent to its mixed-witness form (no identity-oriented native prime witness). Character-rigidity and native-cost uniqueness arguments cite this bridge when switching between axis and witness language. The proof is a term-mode Iff pairing of the two directed conversion lemmas.
Claim. The following are equivalent. (i) For every ratio character $\chi$ that is prime-direction calibrated, if the orbit-$2$ axis lies on the reciprocal branch then no native prime axis of $\chi$ remains on the identity branch. (ii) For every such $\chi$, if the orbit-$2$ prime axis is reciprocal-oriented then no identity-oriented native prime witness exists.
background
In the Primitive Recognition Calculus, ratio characters are maps on ratio orbits that encode how multiplicative structure is read by a candidate native cost. Prime-direction calibration fixes the orientation of prime axes (identity versus reciprocal branch). The orbit-$2$ axis is the distinguished two-prime direction that appears in mixed-character rigidity arguments.
Two exclusion targets package the same rigidity demand at different granularities. The axis form asserts: once calibration leaves orbit $2$ reciprocal, no native prime axis may stay on identity. The witness form asserts the same obstruction at the level of concrete identity-oriented native prime witnesses rather than whole axes.
The directed lemmas already convert each form into the other under the standing hypotheses (ratio character plus prime-direction calibration). This declaration only records that those conversions are mutual, so the two Props are interchangeable in certificates and refutations.
proof idea
Term-mode Iff introduction. The forward direction applies the lemma that turns the axis exclusion target into the witness exclusion target. The reverse applies the lemma that turns the witness target back into the axis target. No extra hypotheses or case splits; the proof is exactly the pairing of those two converters.
why it matters
Native-cost uniqueness in PRC needs a clean blocker language: either prove a rigidity target or refute it and record the obstruction. This equivalence lets the development treat axis-level and witness-level exclusion as the same certificate atom.
Downstream, the refutation of the axis target routes through the witness refutation via the forward direction of this Iff. The native-cost uniqueness blocker certificate and the conditional universal-foundation certificate sit further up the same stack, so interchangeable target forms keep those certificates stable when the proof switches granularity.
Relative to the broader Recognition forcing chain, this is local foundation hygiene inside PRC character rigidity, not a T5–T8 landmark. It closes a bookkeeping gap so mixed-character nonexistence arguments do not fork into two parallel Prop trees.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.