PRCPrimeCalibrationForcesNonunitIdentityComparableTraceTarget_of_successor_step_pair
plain-language theorem explainer
From the split one-step prime-floor successor pair (extends and contracts), prime calibration forces identity orientation to respect comparability of finite δ-orbit traces on nonunit directions. Cited by anyone closing the native-cost uniqueness blocker or the comparable-trace iff. Proof is a pure two-step term composition through the successor-transport intermediate.
Claim. Assume the prime-floor identity successor step pair: both the one-step extends target and the one-step contracts target hold under prime calibration. Then every ratio-orbit character that is prime-direction calibrated has identity orientation respecting comparability of finite $\delta$-orbit traces on all nonunit directions.
background
In the Primitive Recognition Calculus native-cost uniqueness module, ratio-orbit characters encode admissible multiplicative orientations of the recognition lattice. Prime-direction calibration restricts those characters on prime axes. The nonunit identity comparable-trace target sharpens identity-branch transport: under that calibration, identity orientation must respect order-comparability of finite $\delta$-orbit traces off the unit direction.
The hypothesis is the split one-step form of the corrected prime-floor successor target: the conjunction of the extends and contracts successor-step goals. Upstream, the successor-transport target packages those two one-step facts into a single transport statement, and a prior lemma already derives the comparable-trace target from full successor transport. This declaration simply routes the split pair through that chain.
proof idea
Term-mode composition, no tactics. First apply the lemma that turns the successor step pair into the prime-floor successor-transport target (pairing the extends and contracts components). Feed that transport hypothesis into the existing lemma that derives the nonunit identity comparable-trace target from successor transport. The result is exactly the desired Prop.
why it matters
Closes one direction of the equivalence between the comparable-trace target and the successor step pair, and supplies the comparable-trace half used to reach the orbit-product no-mixed-orientation target from the same pair. Both feed the native-cost uniqueness blocker certificate and, farther up, the conditional universal-foundation certificate. In the Recognition forcing picture this is bookkeeping on the identity branch of the cost character, not a new physical constant, but it is required before native $J$-cost uniqueness can be certified without residual orientation gaps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.