PRCPrimeCalibrationForcesOrbitSuccessorIdentityTarget_of_transport
plain-language theorem explainer
If prime calibration forces directional successor transport on every ratio character, then it also forces identity-orientation invariance under one successor step. Native-cost uniqueness work cites this as the reduction from the stronger transport target to the weaker identity target. The proof is a one-line pointwise application of the transport-to-identity packaging lemma under the shared universal quantifiers.
Claim. Assume that every prime-direction-calibrated ratio character $\chi$ satisfies successor transport of the identity orientation in both one-step directions. Then every such $\chi$ has identity orientation invariant under one successor step on every nonzero orbit direction.
background
In the primitive recognition calculus, a ratio character is a map $\chi$ on ratio orbits obeying the multiplicative character laws used to build native cost. Prime-direction calibration is the extra constraint that $\chi$ is pinned on the distinguished prime directions of the orbit lattice.
Two sharper one-step targets sit above those laws. The identity target asks that prime calibration force identity orientation to be invariant under a single successor step on every nonzero orbit direction. The transport target is strictly stronger: it asks that both one-step directions be forced separately, exposing the additive-trace compatibility missing from purely multiplicative ratio-character laws.
Upstream, the pointwise lemma already records that successor transport of the identity orientation packages into the single identity-respects-successor-step predicate: both directed legs are just the two components of the transport pair.
proof idea
Term-mode reduction under the shared quantifiers. Introduce a ratio character $\chi$ together with the character and prime-calibration hypotheses. Apply the assumed transport target at $(\chi, h\chi, h\mathrm{prime})$ to obtain successor transport for that $\chi$. Feed the resulting transport witness into the upstream packaging lemma, which splits transport into the two directed legs and reassembles them as identity-respects-successor-step. Discharge.
why it matters
This implication is the bridge used to refute the stronger transport target from the already-refuted identity target: the refutation theorem assumes transport, applies this lemma, and contradicts the identity-target refutation. That pair of refutations feeds the native-cost uniqueness blocker certificate, which records which factorization and calibration targets are proved versus refuted inside the PRC native-cost uniqueness module.
In the broader Recognition forcing chain, native cost uniqueness is the local uniqueness engine behind the J-cost (T5) and the Recognition Composition Law. Closing or blocking candidate character-calibration routes is how the calculus pins the admissible cost before phi, the eight-tick octave, and $D=3$ are forced downstream. This declaration does not itself settle uniqueness; it only tightens the blocker lattice by making the transport target inherit the identity target's failure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.