PRCPrimeCalibrationForcesCoherentPrimeOrientationTarget
plain-language theorem explainer
Defines the sharper orientation blocker: every ratio character whose cost matches canonical J-cost on all native prime orbits must pick one global orientation (all identity or all reciprocal) on those primes. Native-cost uniqueness work cites it as the place mixed prime inversions are forbidden. The body is a pure Prop abbreviation, not a proof.
Claim. The following assertion holds as a named target: for every map $\chi$ on ratio orbits that is a ratio character (unit at $1$, multiplicative up to cross-equivalence) and whose induced cost agrees with the canonical $J$-cost on every native prime direction, $\chi$ is prime-orientation coherent: either $\chi(p)\sim p$ for every prime orbit $p$, or $\chi(p)\sim p^{-1}$ for every such $p$.
background
In the primitive recognition calculus, costs live on ratio orbits: each orbit is an integer numerator over a nonzero distinction-nat denominator (K4.7). A ratio character $\chi$ is a quotient-native candidate for the d'Alembert factorization of a PRC cost: it fixes the unit orbit and is multiplicative up to cross-equivalence rather than definitional equality.
Prime-direction calibration means the cost generated from $\chi$ matches the canonical on-orbit $J$-cost on every native prime orbit. Prime-orientation coherence is stronger and coarser: $\chi$ must act as the identity on all prime directions, or as reciprocal on all of them; mixed choices (invert some primes, leave others) are excluded.
This module packages native-cost uniqueness into exact Lean targets. The present definition is the sharper orientation blocker A from the doc-comment: calibration on primes is required to force a single coherent orientation across all native prime axes.
proof idea
No proof: the declaration is a def of a Prop. It quantifies over maps $\chi$ on ratio orbits and conjoins three named predicates already defined in-module: ratio-character structure, prime-direction cost calibration, and prime-orientation coherence. Downstream lemmas discharge or refute instances of this target by reducing it to local orientation plus no-mixed-witnesses, or to two-prime branch controls.
why it matters
Native cost uniqueness is not closed; the Pass-25 blocker certificate splits the missing mathematics into exact targets, and this orientation blocker is one of them. It feeds the certificate structure and a family of reduction theorems: equivalence with two-prime branch controls, discharge from local orientation plus no mixed prime orientation, discharge from no mixed prime witnesses, and discharge from prime-pair product cost consistency.
In the Recognition forcing picture this sits under J-uniqueness (T5) and the Recognition Composition Law: characters that reproduce $J$ on primes must not introduce independent prime inversions, or the factorization would leave the canonical cost class. The companion comment records the distinguished-prime normal form: the branch at orbit $2$ should control every native prime branch. Open work is whether the target holds, is refuted, or reduces fully to already-proved local controls.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.