PRCCharacterPrimeFloorOrbitIdentitySuccessorTransport_iff_local_adjacent_nomix
plain-language theorem explainer
Under local identity-or-reciprocal orientation of every nonunit orbit, the prime-floor identity successor-transport law is equivalent to the ban on adjacent mixed orientations. Anyone proving native-cost uniqueness for PRC characters will cite this bridge. The proof is a two-line Iff packaging of the two already-proved one-way implications.
Claim. Let $\chi$ map rational orbits to rational orbits, and assume every nonunit orbit direction is locally either identity-oriented or reciprocal-oriented. Then the following are equivalent: (i) identity orientation transports (extends and contracts) along one $\delta$-successor step above the self-reciprocal unit orbit; (ii) no adjacent pair of nonunit orbits mixes identity orientation on one side with reciprocal orientation on the other.
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: signed-orbit numerator over a nonzero distinction-nat denominator. A character $\chi$ acts on these orbits. Local orientation of nonunit orbits means that for every nonunit $p$, the direction of $\chi$ at $p$ is either the identity orientation or the reciprocal orientation (the nonprime analogue of the already-proved local-prime alternative).
Successor transport is the corrected prime-floor rule: once the path sits above the self-reciprocal unit orbit, identity orientation both extends and contracts along a single $\delta$-successor step. That layer is exactly what prime-to-prime trace coherence needs. The no-adjacent-mixed law forbids identity on one side of a nonunit adjacent pair together with reciprocal on the other (and the swapped mix).
The module builds native-cost uniqueness for PRC characters from doubled-trace and d'Alembert structure; this equivalence sits in the orientation-coherence layer that feeds the uniqueness blocker certificate.
proof idea
Term-mode Iff constructor. The forward arrow is the already-proved implication from successor transport to no-adjacent-mixed orientation. The reverse arrow applies the companion implication that, given local nonunit orientation, no-adjacent-mixed yields successor transport (itself built by packaging the extend and contract successor-step lemmas). The local-orientation hypothesis is threaded only into the reverse direction.
why it matters
Native-cost uniqueness for PRC characters needs a clean bridge between the transport formulation of identity coherence and the combinatorial no-mix law on adjacent floors. This Iff is that bridge under the standing local-orientation hypothesis, so either formulation can be used downstream without bookkeeping loss.
It is consumed by prc_native_cost_uniqueness_blocker_certificate, which packages the zero-calibrated factorization target and the refutation of signed-admissible factorization. In the broader Recognition chain this sits under T5 J-uniqueness and the Recognition Composition Law: characters that respect local orientation and either transport or no-mix are forced toward the unique native cost $J(x)=(x+x^{-1})/2-1$. Closing orientation coherence at the prime floor is a necessary step before global uniqueness of the native cost functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.