PRCCharacterOrbitIdentityRespectsSuccessorStep_of_transport
plain-language theorem explainer
If a ratio-orbit character admits both forward and backward one-step successor transport for identity orientation, then identity orientation is invariant under a single δ-successor step on every nonzero orbit direction. Native-cost uniqueness and prime-calibration arguments cite this to pass from bundled transport hypotheses to the one-step trace-order law. The proof is a three-line term unpack: the two conjuncts of transport are the two directions of the biconditional.
Claim. Let $\chi$ map rational orbits to rational orbits. Suppose $\chi$ satisfies both the forward and backward one-step successor laws for identity orientation on nonzero $\delta$-orbit directions. Then for every nonzero distinction $p$, identity orientation of $\chi$ at $p$ holds if and only if it holds at the successor of $p$.
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: signed-orbit numerator over a nonzero distinction-nat denominator. Characters act as maps $\chi$ on these orbits. Identity orientation on a nonzero orbit direction records whether the character preserves the distinguished identity ray at that direction.
The one-step trace-order law asks that this identity orientation be invariant under a single $\delta$-successor step: it holds at $p\neq 0$ exactly when it holds at $\mathrm{succ},p$. That law is deliberately weaker than prime-to-prime transport; it is imposed before primality.
Successor transport packages the two directed one-step laws (extends and contracts) into a single hypothesis. The module develops native-cost uniqueness by forcing characters that match the doubled-trace cost to obey such coherence constraints along the orbit.
proof idea
Term-mode unpack of a conjunction into an iff. Introduce a nonzero distinction $p$. The transport hypothesis is the pair of directed one-step laws. Apply the first conjunct at $p$ for one direction of the biconditional and the second conjunct at $p$ for the converse; pack them with a pair constructor. No further lemmas are needed.
why it matters
This bridge sits on the path from successor transport to the one-step identity law that prime calibration must force. Downstream, PRCPrimeCalibrationForcesOrbitSuccessorIdentityTarget_of_transport applies it directly: given prime-calibration transport on $\chi$, it concludes the successor-identity target by invoking this theorem. That target feeds the native-cost uniqueness blocker certificate, which records the proved zero-calibrated factorization target and the refuted signed-admissible factorization path. In the Recognition forcing chain, native cost uniqueness is the local uniqueness engine behind the J-cost (T5) and the Recognition Composition Law; securing orbit-level identity coherence under successor is a necessary intermediate before global cost uniqueness can be certified.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.