PRCPrimeCalibrationForcesLocalPrimeOrientationTarget_proved
plain-language theorem explainer
Prime cost calibration forces each prime axis to sit in either the identity or the reciprocal orientation. Anyone assembling coherent prime-orientation or native-cost uniqueness for admissible ratio characters cites this local step. The argument reduces calibration to a cross-equation of ratio orbits and finishes by the J-cost lemma that equal costs force same-or-reciprocal.
Claim. Let $\chi$ be a map on ratio orbits that is a ratio character and is cost-calibrated on every prime direction. Then for every prime $p$, the image $\chi$ of the prime direction of $p$ is equal, as a ratio orbit, either to that prime direction itself or to its reciprocal.
background
In the Primitive Recognition Calculus, ratio orbits package positive ratios up to the ledger reciprocity $r\sim r^{-1}$. A ratio character $\chi$ is a structure-preserving map on those orbits that keeps nonzero rational representatives nonzero. The native cost attached to a character is the J-cost pulled back along $\chi$ (via costFromCharacter), where $J(x)=(x+x^{-1})/2-1$ is the unique symmetric cost fixed by the Recognition Composition Law.
Prime-direction calibration says that on each prime axis the character-induced cost matches the bare prime-direction cost: the two orbits satisfy the cross-equation that equates their doubled J-values. Local orientation is the weaker geometric demand that, prime by prime, $\chi$ may only send the prime direction to itself or to its reciprocal, never to an unrelated orbit.
The ambient module develops uniqueness of the native cost character: admissible characters must be built from a coherent choice of identity versus reciprocal on the prime generators. This declaration is the per-prime half of that orientation story.
proof idea
Introduce a ratio character $\chi$, its prime-direction calibration hypothesis, and a prime $p$. Nonvanishing of the rational representative of the prime direction is immediate from the prime-direction construction; the character preserves that nonvanishing. Calibration, rewritten through the character cost, yields the cross-equation between the orbit of $\chi$ on the prime direction and the bare prime-direction orbit. The algebraic lemma that equal J-costs force two nonzero ratio orbits to be identical or reciprocal then supplies local orientation at $p$. The whole proof is a short tactic chain: two nonvanishing facts, one simpa of calibration into a cross-equation, and one application of the same-or-reciprocal J-cost lemma.
why it matters
Local orientation is the first half of coherent prime orientation under prime cost calibration. Downstream, the coherent-orientation targets assemble this local fact with a no-mixed-witnesses (or two-prime branch-control) hypothesis; the admissible-character theorem PRCCharacterPrimeOrientationCoherent_of_admissible applies the present result directly. Further parents include the identity-forces-two-prime-identity implications and the mixed nonunit witness-reflection targets, all of which feed the native-cost uniqueness blocker certificate.
In the broader Recognition forcing chain this is bookkeeping on the T5 J-uniqueness layer: once cost is forced to be $J$, calibration on prime generators can only flip each axis by the reciprocal automorphism, never by an exotic character. That rigidity is what lets later steps pin the native cost character and close uniqueness scaffolding in the PRC native-cost module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.