PRCPrimeCalibrationForcesPrimeFloorIdentityContractsSuccessorStepTarget_of_successor_transport
plain-language theorem explainer
Assuming prime calibration forces successor transport above the self-reciprocal unit floor, the backward half follows: every prime-direction-calibrated ratio character contracts the successor step on the prime-floor orbit identity. Native-cost uniqueness and universal-foundation certificates cite this projection. Proof is a one-line second-component extraction from the successor-transport witness.
Claim. If prime calibration forces successor transport above the self-reciprocal unit floor (for every ratio-orbit character $\chi$ that is a ratio character and prime-direction calibrated), then the backward half holds: every such $\chi$ contracts the successor step on the prime-floor orbit identity.
background
In the Primitive Recognition Calculus, native cost uniqueness is attacked through ratio-orbit characters: maps $\chi$ on ratio orbits that preserve the multiplicative structure used to build the doubled-trace cost. Prime-direction calibration pins how $\chi$ acts along a distinguished prime axis. The self-reciprocal unit floor is the orbit fixed by inversion; above that floor one expects genuine successor transport, not mere additive drift out of the unit orbit.
The corrected successor-transport target packages that expectation: calibrated prime characters force prime-floor orbit-identity successor transport. That target splits into a forward (extends) half and a backward (contracts) half. This declaration isolates the contracts half as a standalone Prop so later certificates can name it independently.
Upstream, the full successor-transport target is the hypothesis; its doc-comment stresses the correction after the reciprocal-character check, ruling out additive transport out of the unit orbit itself.
proof idea
One-line term projection. Introduce the character $\chi$ and the two hypotheses (ratio character, prime-direction calibrated). Apply the assumed successor-transport target at $(\chi, h_\chi, h_{\mathrm{prime}})$ and take the second component of the resulting pair, which is exactly the contracts-successor-step statement. No further rewriting.
why it matters
Closes the backward half of the corrected prime-floor successor target inside PRC native-cost uniqueness. Downstream it is paired with the matching extends projection to form the full identity-successor-step pair target, and both feed prc_native_cost_uniqueness_blocker_certificate. That blocker is part of the certificate stack consumed by prc_universal_foundation_conditional_certificate in UniversalFoundation.
In the broader Recognition Science forcing chain this sits under native-cost uniqueness for the J-cost (T5: $J(x)=(x+x^{-1})/2-1$), ensuring calibrated prime axes cannot invent non-contracting successor steps above the unit floor. It does not itself finish uniqueness; it discharges one named half of a structured blocker.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.