PRCPrimeFloorSuccessorTransportLocalAdjacentTarget_iff_nonunit_coherent
plain-language theorem explainer
Local adjacent successor-transport (local nonunit orientation plus adjacent no-mixing under prime calibration) is equivalent to global nonunit-orbit orientation coherence. Native-cost uniqueness certificates and the local-target refutation cite this bridge. The proof is a pure Iff packaging of the two already-proved one-way implications.
Claim. The following are equivalent: (i) prime calibration forces local nonunit-orbit orientation together with no adjacent mixed orientation; (ii) prime calibration forces a single coherent orientation across all nonunit orbit directions (for every ratio character that is prime-direction calibrated).
background
In the Primitive Recognition Calculus, ratio characters assign orientations on ratio orbits. Prime-direction calibration is the constraint that prime generators pick a preferred direction. Two strength levels of orientation control appear in the native-cost uniqueness program.
The local adjacent target is the conjunction of local nonunit orientation with adjacent no-mixing: no identity-oriented nonunit direction sits next to a reciprocal-oriented one. The coherent target is the global statement that every nonunit orbit direction shares one orientation once the character is prime-calibrated. The module doc for the coherent target calls it a stronger replacement for product no-mixing: mixed product factors then become impossible by nonunit non-self-reciprocity.
Pass-39 refined the older successor-transport blocker by separating local orientation from adjacent no-mixing rather than bundling both under successor transport. This declaration equates that refined local package with the global coherence target.
proof idea
Term-mode Iff constructor. The forward direction applies the already-proved implication from the local adjacent target to global nonunit-orbit orientation coherence (which itself routes through local orientation plus prime-floor successor transport). The reverse direction applies the already-proved implication that global coherence yields both local nonunit orientation and adjacent no-mixing, hence the local adjacent target. No new arithmetic or case analysis is performed here.
why it matters
This equivalence is the hinge that lets the uniqueness program treat the local adjacent formulation and the global coherence formulation as interchangeable. Downstream, the local adjacent target is refuted by transporting the known refutation of global coherence across the forward direction of this iff. The same bridge feeds the native-cost uniqueness blocker certificate and appears in the universal-foundation conditional certificate.
In the Recognition Science forcing chain, native cost uniqueness is the step that pins the J-cost (T5: $J(x)=(x+x^{-1})/2-1$) as the unique cost compatible with the Recognition Composition Law. Orientation coherence is the combinatorial obstruction that blocks mixed-factor characters from spoiling that uniqueness. Closing the local/global dictionary here keeps the blocker certificate honest: whatever is refuted on one side is refuted on the other.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.