PRCCharacterOrbitIdentitySuccessorTransport
plain-language theorem explainer
Bundles forward and backward one-step successor laws for identity orientation of a map on rational orbits. Anyone proving trace coherence of ratio characters cites this as the transport package. It is a pure conjunction definition: extend-step and contract-step on nonzero orbit directions.
Claim. For a map $\chi$ on rational orbits, successor-step transport holds when identity orientation is preserved both forward and backward under the $\delta$-successor on every nonzero orbit direction: if identity holds at $p\neq 0$ then it holds at $\mathrm{succ}\,p$, and conversely.
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: signed-orbit numerator over a nonzero distinction-natural denominator. Ratio characters act multiplicatively on these orbits. Trace coherence, however, needs additive structure along the $\delta$-successor that steps the denominator (or direction) by one.
The forward law says identity orientation at a nonzero direction $p$ implies identity at $\mathrm{succ},p$. The backward law is the converse contraction. Multiplicativity of $J$-automorphisms (CostAlgebra) does not by itself give these one-step additive moves; they are the bridge from multiplicative characters to the orbit's trace/additive skeleton.
This module packages native-cost uniqueness infrastructure: doubled-trace d'Alembert structure, character-trace matching, and calibration targets that force additive compatibility.
proof idea
Definitional abbreviation only: the proposition is the conjunction of the forward one-step law and the backward one-step law. No tactics or lemmas fire at this site. Downstream, additive compatibility of $\chi$ with the successor supplies both conjuncts via the corresponding of_additive_compat constructors; the dual direction unpacks the pair into the full respects-successor-step statement.
why it matters
This is the missing bridge named in the module comment: multiplicative ratio characters alone do not talk to the additive successor on orbit directions. Downstream, PRCCharacterOrbitIdentityRespectsSuccessorStep_of_transport unpacks the bundle into the full successor-respect law, and PRCCharacterOrbitIdentitySuccessorTransport_of_additive_compat shows additive compatibility implies the bundle.
It appears as the conclusion of the sharper target PRCPrimeCalibrationForcesOrbitSuccessorTransportTarget: prime-direction calibration of a ratio character should force both one-step directions separately. That target is listed among the exact Lean holes in PRCNativeCostUniquenessBlockerCertificate (Pass-25), so closing native cost uniqueness routes through discharging this transport. In the broader RS chain, native $J$-cost uniqueness (T5 landmark $J(x)=(x+x^{-1})/2-1$) needs characters that match both multiplicative RCL structure and additive orbit traces; this definition isolates that interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.