PRCPrimeCalibrationForcesNonunitIdentityWitnessExcludesReciprocalTarget_refuted
plain-language theorem explainer
Prime calibration does not force one-sided exclusion: an identity-oriented nonunit witness need not rule out every reciprocal-oriented nonunit witness. Native-cost uniqueness and foundation-certificate work cite this negative result. The proof is a short transport of an already-refuted no-mixed orientation target across a proved equivalence.
Claim. It is false that every prime-direction-calibrated ratio character $\chi$ makes any identity-oriented nonunit witness incompatible with every reciprocal-oriented nonunit witness. Equivalently, the one-sided witness-exclusion target under prime calibration fails.
background
In the Primitive Recognition Calculus, ratio characters $\chi$ act on ratio orbits and encode how multiplicative structure is read as cost. Prime-direction calibration fixes the preferred orientation of prime generators so that the character is aligned with a chosen prime basis rather than its reciprocal.
The one-sided witness-exclusion target asserts that, once $\chi$ is a ratio character and is prime-calibrated, the existence of a single identity-oriented nonunit witness should already exclude every reciprocal-oriented nonunit witness. The intent is to strip local orientation choices out of witness globalization when building a native cost.
An equivalent formulation forbids mixed nonunit orbit orientations under the same calibration hypotheses. That mixed-orientation target has already been refuted upstream; a separate equivalence theorem identifies the one-sided exclusion target with the no-mixed target.
proof idea
Assume the one-sided exclusion target. Apply the forward direction of the equivalence
PRCPrimeCalibrationForcesNonunitIdentityWitnessExcludesReciprocalTarget_iff_no_mixed
to obtain the no-mixed nonunit orbit-orientation target. Discharge the goal by the already-proved refutation
PRCPrimeCalibrationForcesNoMixedNonunitOrbitOrientationTarget_refuted.
The argument is a pure logical transport: no new analytic or arithmetic work.
why it matters
This closes one candidate route by which prime calibration might have forced orientation-free witness globalization for native cost uniqueness. Downstream it is consumed by the native-cost uniqueness blocker certificate, which packages proved and refuted factorization targets into a single status object, and by the conditional universal-foundation certificate that records which PRC foundation legs are settled versus blocked.
In the broader Recognition forcing picture, native cost uniqueness is the bridge from the Recognition Composition Law and J-uniqueness (T5) toward a unique cost functional on the phi-ladder. Refuting this witness-exclusion shortcut shows that orientation mixing survives prime calibration, so uniqueness arguments cannot rely on one-sided identity witnesses alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.