PRCPrimeCalibrationForcesPrimeFloorSuccessorTransportTarget_of_nonunit_coherent
plain-language theorem explainer
If prime calibration forces a single coherent orientation on every nonunit ratio-orbit direction, then it also forces identity successor transport above the self-reciprocal unit floor. Native-cost uniqueness arguments cite this to convert global orientation coherence into the corrected prime-floor transport target. The proof is a short term composition: coherence yields local orientation and no adjacent mixing, which together give successor transport.
Claim. Assume that every ratio-orbit character $\chi$ that is prime-direction calibrated has a single coherent orientation on all nonunit orbit directions. Then every such $\chi$ satisfies identity successor transport on orbits above the self-reciprocal unit floor: once a calibrated prime axis picks the identity orientation, successive steps along the prime floor remain identity-oriented.
background
In the Primitive Recognition Calculus, a ratio-orbit character $\chi$ assigns to each ratio orbit either the identity or the reciprocal orientation. Prime-direction calibration restricts how $\chi$ behaves on prime axes. The self-reciprocal unit orbit is the floor; nonunit directions sit above it.
The hypothesis target says prime calibration forces global nonunit orientation coherence: every nonunit direction is identity-oriented, or every one is reciprocal-oriented. The conclusion target is the corrected successor-transport statement: calibration forces identity successor transport above that unit floor, not additive transport out of the unit orbit itself.
Upstream, coherence already implies local nonunit orientation and rules out adjacent mixed orientations on the prime floor. Those two local facts are exactly the hypotheses of the lemma that builds prime-floor identity successor transport.
proof idea
Term-mode proof. Fix a character $\chi$ that is a ratio-orbit character and prime-direction calibrated. Apply the hypothesis to obtain nonunit orbit orientation coherence for $\chi$.
From that coherence, invoke the local-orientation theorem to get nonunit local orientation, and the no-adjacent-mixed-orientation theorem to get the prime-floor no-mix property. Feed both into the composition lemma that turns local orientation plus adjacent no-mix into prime-floor identity successor transport. Discharge the goal.
why it matters
This is a target-implication bridge inside native-cost uniqueness: the stronger coherence target implies the corrected prime-floor successor-transport target. Downstream it is packaged into the sharpened coherence target (local orientation paired with successor transport) and into the identity-successor step-pair target. Both feed the native-cost uniqueness blocker certificate that records which factorization and calibration targets are proved or refuted.
In the Recognition forcing picture this sits under uniqueness of the native cost built from the J-cost and the Recognition Composition Law: characters must not mix identity and reciprocal orientations once primes are calibrated. Closing these transport targets is part of pinning the cost to the unique J-shape forced at T5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.