PRCCharacterPrimeFloorNoAdjacentMixedOrientation
plain-language theorem explainer
Adjacent non-unit orbit steps of a ratio character cannot mix identity orientation on one side with reciprocal on the other. This is the prime-floor form of the no-mixed-orientation law in native cost uniqueness. Anyone proving successor transport or orientation coherence for characters cites it. The body is a pure Prop packaging the two forbidden mixed patterns at p and succ p.
Claim. For a map $\chi$ on ratio orbits, and every nonzero non-unit distinction natural $p$: $\chi$ does not have identity orientation at $p$ together with reciprocal orientation at $p+1$, and does not have reciprocal orientation at $p$ together with identity orientation at $p+1$.
background
In the Primitive Recognition Calculus, ratio orbits are integer-numerator / nonzero-orbit-denominator displays. Distinction naturals are the base-neutral finite orbits of repeated distinction; the native unit predicate holds only for the one-step orbit. A character $\chi$ acts on ratio orbits.
Identity orientation at a nonzero orbit direction $p$ means $\chi$ fixes that direction up to the native cross-equality on ratio orbits. Reciprocal orientation means $\chi$ sends the direction to its reciprocal. The successor of any distinction natural is automatically nonzero.
This module develops uniqueness of the native cost from character data. The prime-floor no-mixed law is the local adjacency constraint used when transporting identity orientation across successive non-unit steps.
proof idea
Definitional packaging, not a proved theorem. The Prop is the universal quantification over nonzero non-unit distinction naturals $p$ of the conjunction of two negated mixed patterns: identity at $p$ with reciprocal at $\mathrm{succ},p$, and reciprocal at $p$ with identity at $\mathrm{succ},p$. It reuses the identity and reciprocal orientation predicates and the fact that successors are nonzero.
why it matters
This Prop is the local adjacency hinge for prime-floor orbit-identity successor transport. Downstream, nonunit orientation coherence and successor-transport hypotheses each imply it; conversely, together with local nonunit orientation it yields the extend and contract successor-step lemmas, and thus the iff between successor transport and this no-mix law.
It also feeds the native-cost uniqueness blocker certificate and the prime-calibration target that forces the no-adjacent-mixed property. In the Recognition forcing chain this sits under character/cost uniqueness toward the unique J-cost (T5) and the Recognition Composition Law, by ruling out orientation flips on adjacent non-unit steps that would break native cost transport.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.