PRCPrimeCalibrationForcesNonunitOrbitLocalOrientationTarget
plain-language theorem explainer
Names the open target that prime-axis J-calibration of a ratio character should force local orientation (identity or reciprocal) on every nonunit orbit direction, not only primes. Native-cost uniqueness work cites it as the first prime-floor successor blocker component. The body is a pure Prop abbreviation packaging three character hypotheses into one universal claim.
Claim. Every multiplicative ratio character $\chi$ on rational orbits that is calibrated to the canonical $J$-cost on every prime direction is locally oriented on every nonunit orbit direction: for each nonunit $p$, either $\chi$ acts as the identity direction or as the reciprocal direction at $p$.
background
In the Primitive Recognition Calculus, costs are reconstructed from ratio characters on RatioOrbit (signed numerator over a nonzero distinction-nat denominator). A ratio character is a multiplicative map $\chi$ with $\chi(1)\sim 1$ up to cross-equivalence, intended as the d'Alembert factor of a native cost.
Prime-direction calibration means the cost generated by $\chi$ agrees with the canonical $J$-cost on every prime orbit direction. Local nonunit orientation is the nonprime analogue of the already-proved prime orientation alternative: at each nonunit $p$, $\chi$ is either the identity direction or the reciprocal direction.
The module packages native-cost uniqueness as a ladder of exact Lean targets rather than a single closed theorem. This definition is the first component of the prime-floor successor blocker: calibration on primes should propagate orientation through composite (nonunit) orbits.
proof idea
No proof: the declaration is a def equating a name to a universal Prop. It quantifies over maps $\chi$ on ratio orbits, assumes the ratio-character axioms and prime-direction calibration, and concludes nonunit local orientation. Downstream lemmas discharge or refute instances by reducing to coherent orientation, product-local orientation, or identity-comparable trace hypotheses.
why it matters
Native cost uniqueness aims to force the unique $J$-cost (T5: $J(x)=(x+x^{-1})/2-1$) from PRC character data. This target is the first half of the split witness-globalization goal: local orientation plus one-sided witness exclusion. It appears in the Pass-25 blocker certificate that records which exact targets remain open.
Several reduction theorems already show how to obtain it from stronger coherent or product-local orientation packages, and a refutation theorem exhibits a two-adic axis-twist character that is prime-calibrated yet fails the conclusion. Closing or permanently refuting this target therefore decides whether prime-floor calibration alone can force full nonunit orientation in the uniqueness chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.