PRCCharacterOrbitIdentitySuccessorTransport_of_additive_compat
plain-language theorem explainer
Additive compatibility of a ratio-orbit character with the δ-successor forces the full successor-step transport package: both the forward extension and the backward contraction one-step identity laws. Anyone proving trace coherence or native-cost uniqueness from multiplicative characters cites this bridge. The proof is a two-constructor packaging of the already-proved extend and contract lemmas.
Claim. Let $\chi$ map rational orbits to rational orbits. If $\chi$ is additively compatible with the $\delta$-successor on every nonzero orbit direction (i.e., $\chi$ of the successor direction is cross-equal to $\chi$ of the direction plus the unit orbit), then $\chi$ satisfies successor-step identity transport: both the one-step extension law and the one-step contraction law hold.
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: signed-orbit numerator over a nonzero distinction-natural denominator. Characters $\chi$ act on these orbits and are the multiplicative side of the native cost story.
Successor-step identity transport bundles two one-step laws needed for trace coherence: extending an identity across a $\delta$-successor, and contracting an identity back across a successor. Additive compatibility is the bridge hypothesis: for every nonzero direction $p$, $\chi$ of the successor direction is cross-equal (the orbit equality relation) to $\chi(p)$ plus the unit orbit. The module doc frames this as the missing link between multiplicative ratio characters and the additive/trace structure on orbits.
Upstream, the two directed lemmas already convert additive compatibility into the extend law and the contract law separately. This declaration only packages them.
proof idea
Term-mode packaging, not a new argument. The goal is a conjunction (the transport Prop). Apply PRCCharacterOrbitIdentityExtendsSuccessorStep_of_additive_compat to the additive-compatibility hypothesis for the left conjunct, and PRCCharacterOrbitIdentityContractsSuccessorStep_of_additive_compat for the right. Each of those lemmas opens the successor step, invokes additive compatibility at $p$, and rearranges via cross-equality on orbits.
why it matters
Native-cost uniqueness needs characters that talk to the additive/trace side of the orbit, not only the multiplicative side. This lemma is the clean interface: once additive compatibility is known, full successor transport is free.
Downstream, PRCPrimeCalibrationForcesOrbitSuccessorTransportTarget_of_additive_compat applies it under prime-calibration hypotheses, and the uniqueness blocker certificate chain ultimately depends on this transport package being available. In the broader Recognition forcing picture, this is local infrastructure for identifying the native cost with the J-cost lineage (T5 uniqueness of $J(x)=(x+x^{-1})/2-1$), not a global forcing step itself. It closes the multiplicative-to-additive gap at the one-step successor level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.