PRCPrimeCalibrationForcesPrimeIdentityWitnessExcludesReciprocalTarget
plain-language theorem explainer
Packages the one-sided prime witness-exclusion claim as a universal target: every ratio character that is prime-direction calibrated must forbid reciprocal-oriented prime witnesses once any identity-oriented prime witness exists. Native-cost uniqueness work cites it as a named blocker target and as one side of the equivalence with no-mixed-prime orientation. Pure definitional Prop packaging; no proof content.
Claim. For every map $\chi$ from ratio orbits to ratio orbits, if $\chi$ is a ratio character and is calibrated on every native prime direction (its generated cost agrees with canonical $J$-cost on each prime orbit), then once an identity-oriented native prime witness exists for $\chi$, no reciprocal-oriented native prime witness can coexist with it.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero orbit denominator. A ratio character $\chi$ acts on these orbits. Prime-direction calibration means that the cost generated from $\chi$ agrees with the canonical $J$-cost on every native prime orbit (cross-equality of cost values on each prime direction).
The atomic witness property says: if there exists at least one native prime $p$ with $\chi$ fixing the prime direction of $p$ (identity orientation), then for every native prime $r$, $\chi$ cannot send the prime direction of $r$ to its reciprocal. Reciprocal orientation is the inverse-ratio automorphism on recognition events and on the cost algebra.
This module isolates native-cost uniqueness blockers as exact Lean targets. The present declaration is the globalized form of that atomic exclusion: calibration on all prime directions should force the exclusion property for every ratio character.
proof idea
Definitional packaging only. The body is the universal quantification over ratio-orbit maps $\chi$: assume the ratio-character hypothesis and prime-direction calibration, conclude the atomic identity-witness-excludes-reciprocal property. No tactics, no lemmas applied at this site; downstream theorems discharge or refute the packaged Prop.
why it matters
Sits in the Pass-25 native-cost uniqueness blocker certificate, which records that uniqueness is not closed but is split into exact targets. Downstream, it is equivalent to the no-mixed-prime-orientation target and to the no-mixed-prime-witnesses target: each implication is a short wrapper applying the corresponding character-level lemma under calibration.
Those equivalences let the uniqueness program treat one-sided witness exclusion, orientation non-mixing, and witness non-mixing as interchangeable calibration consequences. The target is the natural globalization of atomic prime no-mixing toward forcing the unique $J$-cost (T5 in the forcing chain) on native prime axes. A separate refuted variant appears in the used-by graph, marking where the claim fails without further hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.