PRCPrimeCalibrationForcesPrimeIdentityWitnessExcludesReciprocalTarget_refuted
plain-language theorem explainer
The one-sided prime witness-exclusion target is false: prime-direction calibration of a ratio character does not force identity-oriented prime witnesses to exclude reciprocal-oriented ones. Anyone tracking native-cost uniqueness blockers or the PRC universal-foundation certificate would cite this. The proof is a short reduction through an equivalence to the already-refuted no-mixed-prime-orientation target.
Claim. It is not the case that every prime-direction-calibrated ratio character $\chi$ satisfies the one-sided exclusion law that the existence of an identity-oriented prime witness forbids any reciprocal-oriented prime witness.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits that encodes how multiplicative structure is read by the native cost. Prime-direction calibration restricts how $\chi$ orients along prime axes. An identity-oriented prime witness points along a prime in the forward sense; a reciprocal-oriented witness points the opposite way.
The target under study asserts a one-sided exclusion law: once calibration admits an identity-oriented prime witness, no reciprocal-oriented prime witness may remain. A sibling target forbids mixed prime orientations outright. An in-module equivalence identifies those two targets, so a refutation of either is a refutation of both.
This module maps the native-cost uniqueness landscape by proving some structural constraints on characters and deliberately refuting others. The upstream refutation of the no-mixed-prime-orientation target is the immediate prior result used here.
proof idea
Assume the one-sided exclusion target holds. Transport it along the left-to-right direction of the equivalence with the no-mixed-prime-orientation target. The resulting mixed-orientation prohibition is already known to be false, by the upstream refutation of that target. The argument is a three-line reduction: introduce the hypothesis, apply mp on the iff, then invoke the prior refutation.
why it matters
This refutation closes one candidate constraint path in the native-cost uniqueness program. It is consumed by the native-cost uniqueness blocker certificate, which packages proved factorization facts against over-strong targets that fail, and it appears in the conditional universal-foundation certificate.
In the Recognition Science forcing chain, native cost uniqueness is the bridge from J-cost uniqueness (T5) and the Recognition Composition Law toward a unique cost functional on ratio structure. Ruling out one-sided witness exclusion prevents an overly rigid orientation law from being smuggled into that uniqueness claim. The result is negative evidence: it tells the framework which calibration-to-orientation implications do not hold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.