PRCPrimeCalibrationForcesNonunitIdentityWitnessLocalExclusionTarget
plain-language theorem explainer
Packages local nonunit-orbit orientation with one-sided reciprocal-witness exclusion as a single Prop. That conjunction is the split form of identity-witness globalization under prime calibration of ratio characters. Downstream work equates it to the globalized target and then refutes the package. Pure definitional conjunction of the two component targets.
Claim. The following two claims hold simultaneously: (i) every prime-calibrated ratio character orients every nonunit orbit direction locally; (ii) every such character makes any identity-oriented nonunit witness incompatible with every reciprocal-oriented nonunit witness.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ assigns to each ratio orbit another orbit and is required to respect the multiplicative structure of positive ratios. Prime-direction calibration means $\chi$ is fixed on the prime axes of the orbit lattice. Nonunit orbits are those away from the identity class.
Local orientation asks that prime calibration force a coherent orientation on every nonunit orbit, not only on prime axes. Separately, one-sided witness exclusion asks that an identity-oriented nonunit witness be incompatible with every reciprocal-oriented nonunit witness (reciprocal being the automorphism $x\mapsto x^{-1}$ on positive ratios, or the inverse-ratio recognition event).
The module packages native-cost uniqueness blockers as exact Lean targets. The doc-comment states the design: local-orientation plus one-sided witness exclusion is the split form of witness globalization.
proof idea
Definitional abbreviation only: the Prop is the conjunction of the local-orientation target and the reciprocal-exclusion target. No tactics, no lemmas applied at this site. Downstream theorems reconstruct the globalized witness target from the conjunction and prove the converse, yielding an iff.
why it matters
This split is the working interface for the identity-witness half of the prime-floor successor blocker in native cost uniqueness. Downstream, the globalized target is equivalent to this local-exclusion package, and the package is refuted, so the globalized route is closed as well.
It appears in the Pass-25 blocker certificate that records which uniqueness routes remain open versus refuted, and in the universal-foundation open-target ledger. Relative to the forcing chain, the surrounding work aims at uniqueness of the native J-cost (T5: $J(x)=(x+x^{-1})/2-1$) under recognition composition; this declaration isolates one failed forcing path rather than establishing J-uniqueness itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.