PRCCharacterPrimeFloorNoAdjacentMixedOrientation_of_nonunit_coherent
plain-language theorem explainer
Global orientation coherence on nonunit ratio orbits (all identity, or all reciprocal) implies the prime-floor adjacent no-mix law: successive nonunit steps cannot flip identity versus reciprocal. Native-cost uniqueness and prime-calibration forcing cite this to block mixed character factors. The proof cases on the two coherent branches and reduces each mixed pair to a nonunit direction cross-equal to its reciprocal.
Claim. Let $\chi$ map ratio orbits to ratio orbits. Suppose nonunit orbit orientation is coherent: either every nonunit orbit direction is identity-oriented under $\chi$, or every nonunit orbit direction is reciprocal-oriented. Then for every nonzero nonunit distinction $p$, $\chi$ cannot orient $p$ by identity and $\mathrm{succ}(p)$ by reciprocal, nor $p$ by reciprocal and $\mathrm{succ}(p)$ by identity.
background
In the Primitive Recognition Calculus native-cost uniqueness module, characters act on ratio orbits. Each nonzero orbit carries a direction that $\chi$ may treat as identity-oriented or reciprocal-oriented. Reciprocal is the orbit-level inverse (cross-ratio swap); identity is the fixed branch. The unit orbit is self-reciprocal, so orientation laws are stated off the unit floor.
Nonunit orientation coherence is the strong global dichotomy: every nonunit direction chooses the same branch (all identity, or all reciprocal). That rules out mixed product factors in the character factorization used for native cost.
The prime-floor no-adjacent-mixed-orientation predicate is the local adjacent form of the same idea: for nonzero nonunit $p$, the pair $(p,\mathrm{succ},p)$ cannot mix identity on one side with reciprocal on the other. Successor is the one-step generator on distinction naturals; nonunit successors of nonunits remain nonunit.
proof idea
Introduce a nonzero nonunit $p$. First record that $\mathrm{succ},p$ is nonunit via orbit_succ_not_unit_of_nonzero_not_unit. Case-split the coherence hypothesis into the all-identity branch and the all-reciprocal branch.
In the all-identity branch, each mixed adjacent assumption produces, by symmetry and transitivity of RatioOrbit.crossEq, a witness that some nonunit orbit direction is cross-equal to its reciprocal; orbitDirection_nonunit_not_crossEq_recip contradicts that. The two mixed patterns (identity then reciprocal, or reciprocal then identity) are handled symmetrically, using coherence at $p$ or at $\mathrm{succ},p$ as needed.
The all-reciprocal branch is dual: the same crossEq sandwich against the forced reciprocal orientation again yields a self-reciprocal nonunit direction, which is impossible.
why it matters
Native cost uniqueness needs characters free of mixed orientation factors along the prime floor. This lemma converts the global nonunit coherence hypothesis into the adjacent no-mix target used by prime calibration.
Downstream, PRCPrimeCalibrationForcesPrimeFloorNoAdjacentMixedOrientationTarget_of_nonunit_coherent is a one-line application under the prime-calibration coherence target. The same coherence package feeds successor-transport forcing (PRCPrimeCalibrationForcesPrimeFloorSuccessorTransportTarget_of_nonunit_coherent) and sits in the native-cost uniqueness blocker certificate that packages zero-calibrated factorization and signed-admissible refutation.
In the broader Recognition chain this is bookkeeping on the character side of the cost functional equation path toward J-uniqueness (T5): orientations must be globally consistent so the doubled-trace d'Alembert data cannot reintroduce mixed reciprocal/identity factors above the unit floor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.