PRCPrimeCalibrationForcesLocalPrimeOrientationTarget
plain-language theorem explainer
Names the local-orientation target: any ratio character whose generated cost matches canonical J-cost on every prime orbit must send each prime axis to itself or its reciprocal. Downstream uniqueness and coherent-orientation arguments cite this Prop as the local half of the calibration-to-orientation bridge. The body is a pure universal quantification over characters, not a proof.
Claim. The following statement is the local orientation target: for every map $\chi$ on rational orbits that is a ratio character and is prime-direction calibrated (its induced cost agrees with canonical $J$-cost on every prime orbit), $\chi$ is locally prime-oriented, i.e. for each prime direction $p$ one has $\chi(p)\sim p$ or $\chi(p)\sim p^{-1}$ under cross-equivalence.
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 $\chi$ is a multiplicative, unit-preserving map up to cross-equivalence, the quotient-native equality used throughout this module.
Prime-direction calibration means the cost generated by $\chi$ agrees with the canonical $J$-cost on every prime orbit: $\mathrm{costFromCharacter}(\chi)(p)\sim J(p)$ for each prime direction $p$. Local prime orientation is the weaker algebraic statement that each such $p$ is sent by $\chi$ to $p$ or to $p^{-1}$. As the upstream doc notes, that is "the algebraic content of equality of $J$-costs on a single prime direction," since $J(x)=J(x^{-1})$.
This definition packages the implication "calibrated character $\Rightarrow$ local orientation" as a named target Prop inside the native-cost uniqueness development.
proof idea
No proof: the declaration is a definitional Prop. It is the universal statement that every ratio character which is prime-direction calibrated is locally prime-oriented. The actual argument appears in the sibling theorem that discharges this target by reducing calibration on a prime direction to a rational nonzero comparison and invoking the two-point fiber of $J$ on a single axis.
why it matters
This target is the local half of the calibration-to-orientation bridge in native cost uniqueness. The coherent-orientation theorem is obtained by combining it with the no-mixed-orientation target: given local orientation and no mixed signs, one gets a single global coherent choice of identity versus reciprocal on all primes.
It is also listed among the exact Lean targets in the Pass-25 blocker certificate, which records that native cost uniqueness is not yet closed but has been split into named obligations. In the broader Recognition chain this sits under J-uniqueness (T5) and the Recognition Composition Law: forcing characters that reproduce $J$ on primes to be orientation-trivial is a step toward uniqueness of the native cost factorization.
The proved discharge of this Prop is the immediate sibling theorem; the coherent target and the blocker certificate are the main consumers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.