PRCPrimeCalibrationForcesPrimeFloorSuccessorTransportTarget_of_local_adjacent_target
plain-language theorem explainer
If prime calibration already forces local nonunit-orbit orientation and adjacent no-mixing on the prime floor, then it forces identity successor transport above the self-reciprocal unit floor for every ratio character. Native-cost uniqueness and orientation-coherence lifts cite this bridge. Term proof: project the conjunction and apply the character-level successor-transport lemma.
Claim. Assume the local adjacent target: under prime calibration, every ratio-orbit character has nonunit-orbit local orientation and no adjacent mixed orientation on the prime floor. Then the corrected successor target holds: for every ratio-orbit map $\chi$ that is a ratio character and is prime-direction calibrated, $\chi$ satisfies prime-floor identity successor transport (transport above the self-reciprocal unit floor, not additive exit from the unit orbit).
background
In the Primitive Recognition Calculus, ratio characters are maps on ratio orbits that encode multiplicative cost structure. Prime-direction calibration pins how a character acts along a distinguished prime axis. The corrected successor target says calibration should force identity successor transport above the self-reciprocal unit floor, not additive transport out of the unit orbit itself.
Pass-39 splits that bundled claim into a local adjacent package: nonunit-orbit local orientation conjoined with no adjacent mixed orientation on the prime floor. The character-level lemma already shows that those two local facts imply prime-floor identity successor transport for a fixed character.
This declaration globalizes that implication: the quantified local package yields the quantified successor-transport target over all calibrated characters.
proof idea
Term-mode, four lines. Introduce a ratio-orbit map $\chi$ with the ratio-character and prime-direction-calibration hypotheses. Project the local-adjacent hypothesis into its two conjuncts and specialize each at $(\chi, h_\chi, h_{\mathrm{prime}})$. Feed those two specialized facts to the character-level lemma that turns local nonunit orientation plus adjacent no-mixing into prime-floor identity successor transport. No extra algebra.
why it matters
Closes the Pass-39 refinement path from the split local adjacent package to the corrected prime-floor successor target used in native-cost uniqueness. Downstream, the orientation-coherence lift applies this theorem inside a pair with the local-orientation conjunct; the iff theorem records equivalence of the local-adjacent package with local orientation plus successor transport. The native-cost uniqueness blocker certificate sits at the end of that chain, so this bridge is load-bearing for uniqueness of the native cost functional in the PRC foundation (the J-cost uniqueness strand of the forcing chain).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.