PRCPrimeCalibrationForcesPrimeFloorNoAdjacentMixedOrientationTarget
plain-language theorem explainer
Defines the open target that every ratio-orbit character which is a PRC ratio character and is calibrated on native prime directions must forbid adjacent nonunit orbits from mixing identity with reciprocal orientation. Native-cost uniqueness work cites it as the second half of the prime-floor successor blocker. The body is a pure Prop abbreviation, not a proved implication.
Claim. The following target holds: for every map $\chi$ on rational orbits, if $\chi$ is a ratio character (unit-preserving and multiplicative up to cross-equivalence) and is prime-direction calibrated (its generated cost matches canonical $J$-cost on every prime orbit), then $\chi$ satisfies the prime-floor law that adjacent nonunit orbit steps cannot mix identity orientation on one side with reciprocal orientation on the other.
background
In the primitive recognition calculus, costs are reconstructed from ratio characters on RatioOrbit displays (integer numerator over a nonzero orbit denominator). A ratio character is a map $\chi$ that fixes the unit orbit and is multiplicative up to cross-equivalence, so the construction stays quotient-native rather than demanding definitional equality.
Prime-direction calibration asks that the cost generated from $\chi$ agree with the canonical $J$-cost on every prime orbit direction. Separately, the prime-floor no-adjacent-mixed-orientation law forbids a character from treating one side of an adjacent nonunit step as identity-oriented while treating the other as reciprocal-oriented.
This module packages native-cost uniqueness gaps as exact Lean targets. The present definition is the second component of the prime-floor successor blocker: calibration on primes should force that orientation-mixing ban.
proof idea
Definitional Prop only. The body is the universal implication $\forall\chi,;\mathrm{PRCRatioCharacter}(\chi)\to\mathrm{PRCCharacterPrimeDirectionCalibrated}(\chi)\to\mathrm{PRCCharacterPrimeFloorNoAdjacentMixedOrientation}(\chi)$. No tactics or lemmas are applied; discharge is deferred to named reduction theorems (from nonunit coherence, or from successor transport) and to an explicit refutation against a two-adic axis-twist character.
why it matters
Native cost uniqueness is not closed; the Pass-25 blocker certificate splits the missing mathematics into exact targets, and this proposition is one of them. Downstream it appears in the local-adjacent and sharpened prime-floor successor-transport targets, which separate local nonunit orientation from adjacent no-mixing instead of bundling both under a single transport claim.
Two reduction theorems show the target would follow from nonunit orbit-orientation coherence or from prime-floor successor transport. A later theorem refutes the target outright via a two-adic axis-twist character that is prime-calibrated yet violates the mixed-orientation ban. That refutation feeds the universal-foundation open-target list and forces the uniqueness program to replace this naive forcing claim with a sharpened local formulation.
In the broader RS chain this sits under native $J$-cost uniqueness (T5 landmark: $J(x)=(x+x^{-1})/2-1$), not under the geometric forcing steps T6–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.