PRCPrimeCalibrationForcesPrimeFloorSuccessorTransportTarget_of_local_adjacent_nomix
plain-language theorem explainer
Prime calibration of a ratio character forces identity successor transport above the self-reciprocal unit floor, once a sharpened Pass-39 package is assumed. That package splits local nonunit orientation from adjacent no-mixing. Anyone closing the native-cost uniqueness blocker or the prime-calibration propagation chain cites this bridge. The proof is a short composition: extract the two sharpened conjuncts and feed them into the local-adjacent-nomix successor lemma.
Claim. Assume the sharpened prime-floor successor package: under prime calibration, every ratio character has coherent local nonunit orientation, and no adjacent mixed orientation at the prime floor. Then every ratio character $\chi$ that is prime-direction calibrated satisfies prime-floor identity successor transport: identity on the self-reciprocal unit floor extends by successor steps along the prime axis (not by additive escape from the unit orbit).
background
In the Primitive Recognition Calculus, ratio characters $\chi:\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$ encode admissible cost data on multiplicative orbits. Prime-direction calibration fixes the action on a distinguished prime axis. The prime floor is the self-reciprocal unit orbit; successor transport means identity there extends along successive prime powers rather than by additive escape from the unit orbit itself.
The corrected successor target packages the claim that prime calibration forces this transport for every ratio character. Pass-39 refines it by splitting two obligations that used to be bundled: (i) local orientation of nonunit orbits under the product structure, and (ii) absence of adjacent mixed orientations at the prime floor.
Upstream, coherence of nonunit orientation already implies the local orientation predicate, and the local-plus-no-mix pair yields successor transport for a single character. This declaration only globalizes that pair under the sharpened package.
proof idea
After introducing the character $\chi$ and its ratio-character and prime-calibration hypotheses, apply the two conjuncts of the sharpened package to $\chi$. The first conjunct gives coherent nonunit orientation; convert it to local orientation by the coherence-to-local lemma. The second conjunct gives the no-adjacent-mixed fact at the prime floor. Hand both witnesses to the local-adjacent-nomix successor-transport lemma, which assembles the required identity-successor transport for $\chi$. Pure packaging: no new arithmetic.
why it matters
This is the discharge step that turns the Pass-39 sharpened orientation package into the corrected prime-floor successor target used throughout native-cost uniqueness. Downstream, the propagation theorem chains it into global orientation and then into the full prime-calibration propagation target; the uniqueness blocker certificate sits on the same lineage.
In the Recognition Science forcing chain the native cost is the $J$-cost $J(x)=(x+x^{-1})/2-1$ (T5 / RCL). Uniqueness of that cost on ratio characters is the algebraic backbone before $\phi$ and the eight-tick structure appear. Closing successor transport above the unit floor removes one of the remaining orientation blockers on that path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.