PRCPrimeCalibrationForcesNonunitNoMixedWitnessesTarget_iff_identity_witness_excludes
plain-language theorem explainer
Under prime direction calibration of a ratio character, forbidding mixed nonunit witnesses is equivalent to one-sided exclusion: any identity-oriented nonunit witness rules out every reciprocal-oriented one. Native-cost uniqueness and the universal-foundation certificate cite this bridge when collapsing witness-orientation variants. The proof is a two-constructor Iff built from the already-proved directions.
Claim. The following are equivalent. (A) Every prime-direction-calibrated ratio character $\chi$ admits no mixed nonunit witnesses (no identity-oriented nonunit witness coexists with a reciprocal-oriented one). (B) Every such $\chi$ satisfies one-sided exclusion: the existence of an identity-oriented nonunit witness rules out every reciprocal-oriented nonunit witness.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits obeying the multiplicative character laws used to build native cost. Prime direction calibration fixes how $\chi$ treats prime generators, so orientation (identity versus reciprocal) is no longer free local data.
Two Prop-level targets package the same global constraint in different shapes. The existential no-mixed-witness target asserts that, after prime calibration, no identity-oriented nonunit witness coexists with any reciprocal-oriented nonunit witness. The one-sided exclusion target asserts that a single identity-oriented nonunit witness already excludes every reciprocal-oriented nonunit witness, stripping local orientation out of witness globalization.
Both targets quantify over the same class: ratio characters that are prime-direction calibrated. The surrounding uniqueness development reduces native-cost uniqueness blockers to such orientation-free witness statements.
proof idea
Term-mode Iff constructor. The forward arrow applies the lemma that no-mixed-witnesses implies one-sided identity-excludes-reciprocal (pointwise on $\chi$, after the character and prime-calibration hypotheses). The reverse arrow applies the converse lemma that one-sided exclusion implies the existential no-mixed statement. No new algebra is done here; the two directed theorems already discharge the character-level implications.
why it matters
This equivalence lets the native-cost uniqueness stack treat the existential mixed-witness ban and the one-sided exclusion form as interchangeable under prime calibration. Downstream, prc_native_cost_uniqueness_blocker_certificate and prc_universal_foundation_conditional_certificate sit on the uniqueness and foundation certificate spine that needs orientation-free witness control.
In Recognition Science terms, the step is local bookkeeping inside the PRC native-cost uniqueness path that feeds the forcing chain toward a unique cost (the J-cost of T5 and the Recognition Composition Law). It does not itself force $\phi$, the eight-tick octave, or $D=3$; it only collapses two formulations of the nonunit-witness constraint so later certificates can cite either shape.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.