PRCPrimeCalibrationForcesPrimeFloorIdentitySuccessorStepPairTarget_of_successor_transport
plain-language theorem explainer
If prime calibration forces successor transport of identity above the self-reciprocal unit floor for every ratio character, then the split one-step form also holds: identity both extends and contracts along successor steps. Native-cost uniqueness and the universal-foundation certificate cite this packaging. The proof is a term-mode pair of the two component projections.
Claim. Assume that for every ratio-orbit map $\chi$ that is a ratio character and is prime-direction calibrated, prime calibration forces prime-floor orbit identity successor transport. Then the split one-step target holds: prime calibration forces both the identity-extends successor-step target and the identity-contracts successor-step target.
background
In the Primitive Recognition Calculus, ratio characters are maps on ratio orbits that encode multiplicative recognition structure. Prime-direction calibration orients those characters along prime axes. The corrected successor target says that such calibration should force successor transport of identity above the self-reciprocal unit floor, not additive transport out of the unit orbit itself.
The split one-step form factors that global successor-transport statement into a conjunction: an extends component and a contracts component. Both live in the native-cost uniqueness module, which isolates blockers preventing non-unique native costs built from characters and doubled traces.
Upstream, the two component lemmas already project the successor-transport hypothesis onto extends and contracts separately. This declaration only reassembles those projections into the paired target used by later certificates.
proof idea
Term-mode pair constructor. Apply the extends-of-successor-transport lemma to the hypothesis for the first conjunct, and the contracts-of-successor-transport lemma for the second. No extra rewriting or case analysis; the pair is exactly the definition of the split one-step target.
why it matters
This is the packaging step that equates the corrected successor-transport target with its split one-step form (via the companion iff). Downstream, identity-comparable-trace and nonunit-coherent routes both reduce to this pair, and the native-cost uniqueness blocker certificate consumes the resulting orientation control. The universal-foundation conditional certificate sits further up the same chain.
In framework terms it tightens the prime-floor side of native cost uniqueness: once prime axes are calibrated, identity must propagate by successor steps on every nonunit orbit direction. That is a local forcing ingredient toward uniqueness of the native cost (the J-cost side of the Recognition Composition Law), not yet the full T5 J-uniqueness theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.