PRCPrimeCalibrationForcesGlobalOrientationTarget
plain-language theorem explainer
Named Prop target asserting that prime-direction calibration of a ratio-orbit character forces global cost orientation: every rational direction maps to itself or its reciprocal. Native-cost uniqueness work cites it as a sharper propagation blocker (independent prime inversions can keep prime costs while breaking composites). Pure definition of a universal quantification; not a proved theorem. Downstream the claim is refuted.
Claim. The proposition that for every map $\chi$ on rational orbits, if $\chi$ is a ratio character and is calibrated on native prime directions, then $\chi$ has global cost orientation: for every rational orbit $q$, either $\chi(q)$ is cross-equal to $q$ or $\chi(q)$ is cross-equal to the reciprocal of $q$.
background
In the primitive recognition calculus, rational directions are packaged as RatioOrbit values (signed numerator over a nonzero distinction denominator). A ratio character is a map on those orbits preserving the algebraic structure used to read costs. J-cost is reciprocal-symmetric, so the only orientation data needed for cost propagation is whether each direction is sent to itself or to its reciprocal.
Global cost orientation means exactly that choice, for every rational orbit: $\chi(q)$ matches $q$ or $\mathrm{recip}(q)$ under cross-equality. Prime-direction calibration restricts the same choice only on native prime axes. The module studies whether local prime calibration propagates to the full rational lattice, which is required for native cost uniqueness along the Recognition Composition Law and the T5 J-uniqueness chain.
The surrounding development treats this statement as a sharper blocker: without forced global coherence, one can invert primes independently, preserve prime costs, and still break composite costs.
proof idea
Definitional Prop, not a proof. The body is the universal closure: for all maps $\chi$ on ratio orbits, the conjunction of being a ratio character and being prime-direction calibrated implies global cost orientation (every orbit sent to itself or its reciprocal under cross-equality). No tactics or lemmas are applied at this declaration; downstream theorems either assume the target, derive it from two subtargets (coherent prime orientation plus propagation), or refute it.
why it matters
Sits in the native-cost uniqueness blocker stack for the primitive recognition calculus. The Pass-25 certificate PRCNativeCostUniquenessBlockerCertificate and the historical ledger PRCUniversalFoundationOpenTargets track exact open or refuted surfaces; this target is one of those surfaces.
It is the bridge between prime-axis calibration and full cost propagation: PRCPrimeCalibrationPropagationTarget_of_global_orientation shows the propagation target follows from this one, and PRCPrimeCalibrationForcesGlobalOrientationTarget_of_prime_orientation_targets factors it into coherent prime orientation plus propagation. Critically, PRCPrimeCalibrationForcesGlobalOrientationTarget_refuted proves the Prop is false, so prime calibration alone does not force a single global orientation. That closes a tempting route toward forcing the unique J-cost (T5 / RCL) from prime data and forces the program onto other factorization or zero-calibration interfaces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.