PRCPrimeCalibrationForcesNonunitIdentityWitnessExcludesReciprocalTarget_iff_no_mixed
plain-language theorem explainer
Equivalence of two prime-calibration branch-coupling targets: one-sided exclusion of reciprocal nonunit witnesses by an identity-oriented witness is the same as forbidding mixed nonunit orbit orientations. Native-cost uniqueness and the universal-foundation certificate cite it when collapsing blocker formulations. Proof is a two-constructor term pairing the already-proved one-way implications.
Claim. The following are equivalent for the primitive recognition calculus. (i) Every prime-direction-calibrated ratio character makes any identity-oriented nonunit witness incompatible with every reciprocal-oriented nonunit witness. (ii) Every such character forbids coexistence of an identity-oriented nonunit direction with a reciprocal-oriented nonunit direction (no mixed nonunit orbit orientation).
background
In the primitive recognition calculus, a ratio character $\chi$ assigns to each ratio orbit another orbit and is required to obey the multiplicative character laws of the PRC kernel. Prime-direction calibration fixes how $\chi$ treats the distinguished prime generators, so orientation data on nonunit orbits is no longer free.
Two blocker targets package the same global-coherence demand. The no-mixed target asks that prime calibration prevent any identity-oriented nonunit direction from coexisting with any reciprocal-oriented nonunit direction; with local nonunit orientation this is exactly global nonunit orientation coherence. The one-sided witness-exclusion target asks that a single identity-oriented nonunit witness already rule out every reciprocal-oriented nonunit witness, stripping local orientation out of witness globalization.
Both targets are quantified over ratio characters that are prime-direction calibrated. The surrounding module develops native-cost uniqueness via doubled-trace and d'Alembert structure on those characters; these Props are the branch-coupling side of that uniqueness story.
proof idea
Term-mode biconditional: the proof is the pair of the two already-established implications. Left-to-right applies the theorem that identity-witness exclusion yields the no-mixed target (by specializing the character hypotheses and invoking the character-level no-mixed-from-exclusion lemma). Right-to-left applies the converse theorem that the no-mixed target yields identity-witness exclusion (again by specializing and calling the character-level exclusion-from-no-mixed lemma). No new arithmetic is done here.
why it matters
This iff lets the native-cost uniqueness development treat the one-sided witness-exclusion blocker and the existential no-mixed-orientation blocker as interchangeable. Downstream, the refutation of the identity-witness-exclusion target routes through the left-to-right direction and the already-refuted no-mixed target, so a single counterexample discharges both formulations. The same equivalence is wired into the native-cost uniqueness blocker certificate and, via that stack, into the conditional universal-foundation certificate.
In the broader Recognition forcing chain this sits under the J-uniqueness and composition-law layer (T5 / RCL): native cost is the unique cost compatible with the recognition composition law once orientation coherence is forced. Collapsing two blocker phrasings removes a bookkeeping fork before those uniqueness certificates close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.