PRCPrimeCalibrationForcesPrimeFloorIdentitySuccessorStepPairTarget_of_identity_comparable_trace
plain-language theorem explainer
Assuming prime calibration forces identity orientation to respect comparability of finite δ-orbit traces on nonunit directions, the split one-step prime-floor identity successor target follows (both extends and contracts components). Cited by anyone closing the native-cost uniqueness blocker or the comparable-trace ↔ successor-step equivalence. Proof is a pure term composition through the successor-transport intermediate.
Claim. If prime calibration forces every prime-direction-calibrated ratio character to have identity orientation that respects comparability of finite $\delta$-orbit traces on nonunit directions, then prime calibration forces the split one-step prime-floor identity successor target: both the extends-successor-step and contracts-successor-step components hold.
background
In the Primitive Recognition Calculus (PRC), native cost uniqueness is approached by forcing a ratio character $\chi$ on ratio orbits to match the J-cost structure once it is calibrated on prime directions. A ratio character is a map on ratio orbits obeying the PRC character axioms; prime-direction calibration means $\chi$ is pinned on prime axes.
The hypothesis is the trace-order sharpening of nonunit identity-branch transport: under prime calibration, identity orientation must respect comparability of finite $\delta$-orbit traces on nonunit directions. The conclusion is the split one-step form of the corrected prime-floor successor target, namely the conjunction of an extends-successor-step component and a contracts-successor-step component.
Two upstream bridges sit between them: identity-comparable-trace implies the prime-floor successor-transport target, and successor-transport implies the split step-pair target.
proof idea
Term-mode composition of two already-proved bridges. First apply the lemma that the identity-comparable-trace hypothesis yields the prime-floor successor-transport target (by specializing the character-level transport lemma at each prime-calibrated $\chi$). Then feed that transport witness into the lemma that successor transport splits into the extends and contracts one-step components, returning the desired conjunction.
why it matters
This is a link in the native-cost uniqueness blocker chain inside PRC. It is one direction of the equivalence between the identity-comparable-trace target and the prime-floor identity successor step-pair target, and it is the route by which the product-no-mixed-orientation hypothesis reaches the step-pair target.
Downstream it appears in the native-cost uniqueness blocker certificate and in the universal foundation conditional certificate. In the broader Recognition Science forcing picture it supports the uniqueness side of the native cost that must match the T5 J-cost $J(x)=(x+x^{-1})/2-1$ once prime calibration and trace-order constraints are imposed; without this bridge the successor-step half of the blocker stays open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.