PRCPrimeCalibrationForcesPrimeFloorSuccessorTransportTarget
plain-language theorem explainer
Defines the corrected prime-floor successor-transport target: every prime-calibrated ratio character must transport identity orientation by one successor step once above the self-reciprocal unit orbit. Cited by the native-cost uniqueness blocker certificate and by the iff linking this target to nonunit identity-comparable trace. Pure Prop packaging of two already-named successor-step conjuncts; no proof content.
Claim. The following target holds: for every map $\chi$ on ratio orbits that is a ratio character and is calibrated on every native prime direction (its generated cost agrees with canonical $J$-cost on each prime orbit), $\chi$ satisfies prime-floor identity successor transport: identity orientation both extends and contracts along one $\delta$-successor step once the path is above the self-reciprocal unit orbit.
background
In the Primitive Recognition Calculus, costs are recovered from ratio-orbit characters via a d'Alembert-style factorization. A ratio character $\chi$ is a map on RatioOrbit (signed numerator over nonzero distinction denominator) that fixes the unit orbit up to cross-equivalence and is multiplicative under orbit multiplication, again up to cross-equivalence rather than definitional equality.
Prime-direction calibration means that on every native prime orbit the cost generated from $\chi$ cross-agrees with the canonical on-orbit $J$-cost. The identity event sits at the $J$-cost minimum $x=1$. After the reciprocal-character check, the right transport rule is not additive escape from the unit orbit itself, but successor transport only above the self-reciprocal unit floor: identity orientation extends and contracts by one $\delta$-successor step on that layer. That two-conjunct property is exactly what is needed for prime-to-prime trace coherence.
proof idea
Definitional packaging only. The target is the universal closure: for every $\chi$, if $\chi$ is a ratio character and is prime-direction calibrated, then $\chi$ satisfies the already-defined prime-floor identity successor-transport predicate (the conjunction of the extend-successor-step and contract-successor-step rules above the unit floor). No tactics, no lemmas applied inside the body.
why it matters
This is the corrected successor target in the native-cost uniqueness program: prime calibration is required to force successor transport above the unit floor, not additive transport out of the unit orbit. Downstream it is the right-hand side of the iff with the nonunit identity-comparable trace target, and the hypothesis of the one-line projections that recover the extend-step and contract-step targets separately. It is conjoined with local nonunit orientation into the sharpened nonunit orbit-orientation coherence target, and it appears among the exact Lean targets listed by the Pass-25 native-cost uniqueness blocker certificate (uniqueness not yet closed, but missing mathematics split into named Props). In the broader RS forcing picture this sits under cost uniqueness for the $J$-factorization that feeds T5 $J$-uniqueness and the Recognition Composition Law, without yet discharging uniqueness itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.