PRCPrimeCalibrationForcesPrimeFloorNoAdjacentMixedOrientationTarget_of_nonunit_coherent
plain-language theorem explainer
If prime calibration forces a single coherent orientation on every nonunit orbit direction, then it also forbids opposite identity/reciprocal orientations on adjacent nonunit prime-floor directions. Native-cost uniqueness and the prime-floor successor-transport blocker cite this reduction. The proof is a one-line target lift of the character-level no-adjacent-mixed lemma.
Claim. Assume that every ratio character $\chi$ that is prime-direction calibrated has a single coherent orientation on all nonunit orbit directions. Then every such $\chi$ also satisfies the prime-floor condition that no two adjacent nonunit orbit directions carry opposite identity versus reciprocal orientations.
background
In the Primitive Recognition Calculus, ratio characters $\chi$ act on ratio orbits and may be prime-direction calibrated. Orientation on a nonunit direction is either identity-type or reciprocal-type. Global nonunit orientation coherence means every nonunit direction shares one orientation; the adjacent mixed-orientation ban is the local prime-floor restriction that neighboring nonunit directions never disagree.
The hypothesis target packages the claim that prime calibration forces full nonunit orientation coherence. The conclusion target packages the weaker adjacent-no-mix claim used as the second component of the prime-floor successor blocker. Upstream, the character-level lemma already shows that any single coherent character automatically has no adjacent mixed orientations on the prime floor.
This module develops native-cost uniqueness for PRC cost functionals built from characters and doubled traces, feeding the uniqueness blocker certificate.
proof idea
Term-mode one-line lift. Introduce a character $\chi$ together with the ratio-character and prime-calibration hypotheses. Apply the assumed coherence target at $\chi$ to obtain nonunit orbit orientation coherence, then feed that into the character-level theorem that coherence implies the prime-floor no-adjacent-mixed-orientation property. Discharge the goal by exact application; no extra algebraic work.
why it matters
This is the second half of the prime-floor successor-transport local-adjacent target under the nonunit-coherence hypothesis. Downstream, PRCPrimeFloorSuccessorTransportLocalAdjacentTarget_of_nonunit_coherent pairs it with the local-orientation half to assemble the full adjacent-transport blocker. That package feeds the native-cost uniqueness blocker certificate, which records the proved factorization and refutation limbs of PRC native-cost uniqueness.
In the Recognition forcing picture, unique native cost is the bridge from the Recognition Composition Law and J-uniqueness (T5) toward the forced self-similar fixed point $\phi$ (T6). Closing orientation-mixing loopholes at the prime floor keeps reciprocal and identity branches from coexisting in calibrated characters, which is required before mass-ladder and constant extractions can treat the cost as unique.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.