PRCPrimeFloorSuccessorTransportLocalAdjacentTarget_of_nonunit_coherent
plain-language theorem explainer
Global nonunit-orbit orientation coherence under prime calibration yields the local successor-blocker package: local nonunit orientation together with no adjacent mixed orientations. Anyone closing the native-cost uniqueness blocker cites this reduction. The proof is a two-field constructor that applies the two component implications to the same coherence hypothesis.
Claim. If prime calibration forces a single coherent orientation on every nonunit ratio-orbit direction for every ratio character, then the local adjacent successor target holds: prime calibration forces local nonunit orientation, and it forces the absence of adjacent mixed orientations at the prime floor.
background
In the Primitive Recognition Calculus, ratio characters assign orientations (identity vs reciprocal) to ratio-orbit directions. Prime-direction calibration is the constraint that characters respect the prime generators of the orbit lattice. The stronger coherence target asserts that, once a character is prime-calibrated, every nonunit orbit direction shares one common orientation; mixed product factors are then impossible by nonunit non-self-reciprocity.
The local adjacent successor target is the Pass-39 refinement of the corrected successor blocker. It is the conjunction of two separate props: local nonunit orientation under prime calibration, and no adjacent mixed orientation at the prime floor. The module treats this conjunction as equivalent (in the local sense) to local orientation plus prime-floor successor transport, separating the two facts instead of bundling them under a single transport statement.
Upstream, each conjunct is already known to follow from global nonunit-orbit orientation coherence: one lemma specializes coherence to local orientation, the other specializes it to prime-floor adjacent no-mixing.
proof idea
Term-mode pair constructor. Apply the upstream implication that coherence yields local nonunit orientation, then the upstream implication that coherence yields prime-floor no-adjacent-mixed orientation, both to the same hypothesis hcoh. The resulting pair inhabits the conjunction that defines the local adjacent target. No further rewriting or case analysis.
why it matters
Native cost uniqueness in PRC needs a blocker certificate that rules out rogue factorizations of calibrated characters. The local adjacent successor target is the refined local form of that blocker: local orientation plus adjacent no-mixing. This theorem shows the target is an immediate consequence of the stronger global coherence hypothesis, so the uniqueness pipeline can discharge the local package once coherence is in hand.
It is one direction of the biconditional equating the local adjacent target with nonunit-orbit orientation coherence, and it feeds the native-cost uniqueness blocker certificate assembly. In the broader Recognition forcing chain this sits in the foundation layer that pins the unique native cost (the J-cost of T5) before phi, the eight-tick octave, and D = 3 are forced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.