PRCCharacterPrimeFloorOrbitIdentitySuccessorTransport_of_nonunit_identity_comparable_trace
plain-language theorem explainer
From a nonunit identity-transport law that only needs comparable δ-orbit traces, one obtains the prime-floor successor transport rule for a ratio-orbit character: identity orientation moves one successor step above the unit orbit in both directions. Anyone proving prime-to-prime trace coherence or native cost uniqueness cites this bridge. The proof is a two-sided constructor that feeds successor non-unit and structural trace comparability into the comparable-trace hypothesis.
Claim. Let $\chi$ map ratio orbits to ratio orbits. Suppose that whenever two nonzero nonunit finite $\delta$-orbit directions have comparable position traces (one extends the other), identity orientation of $\chi$ at the first direction implies identity orientation at the second. Then identity orientation of $\chi$ transports along a single $\delta$-successor step once the path is above the self-reciprocal unit orbit: both the extends-successor and contracts-successor forms hold.
background
In the primitive recognition calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (zero and successor). The native unit is the one-step orbit; everything else nonzero is nonunit. Ratio orbits display a signed numerator over a nonzero distinction denominator. Characters here are maps $\chi$ on ratio orbits whose identity orientation along an orbit direction is the algebraic content being transported.
Orbit position traces record the finite $\delta$-path up to a given distinction index. Any two such traces are comparable under the extension order: one always extends the other (proved by comparing underlying naturals). The hypothesis packages global nonunit identity-branch transport as a trace-order law: identity at one nonunit direction moves to another nonunit direction whenever traces are comparable.
The target packages the corrected successor-transport rule needed for prime-to-prime coherence: identity orientation moves along exactly one $\delta$-successor step, but only above the self-reciprocal unit orbit, in both the extends and contracts directions.
proof idea
Term-mode proof by constructor, splitting the target into extends-successor and contracts-successor.
Extends direction: fix nonzero nonunit $p$ with identity at $p$. The successor of $p$ is nonzero (orbit_succ_ne_zero) and nonunit (orbit_succ_not_unit_of_nonzero_not_unit). Position traces of $p$ and its successor are comparable (orbitPositionTrace_comparable). Feed these into the comparable-trace hypothesis to move identity from $p$ to $\mathrm{succ},p$.
Contracts direction: same lemmas with the roles of $p$ and $\mathrm{succ},p$ swapped, so identity at the successor pulls back to $p$. No extra arithmetic is needed beyond those orbit facts.
why it matters
This is the exact layer the module flags for prime-to-prime trace coherence: successor transport of identity orientation above the unit floor. Downstream, prime calibration that already forces the comparable-trace nonunit identity law upgrades immediately to the prime-floor successor-transport target by applying this theorem. That target sits on the path toward the native-cost uniqueness blocker certificate, which packages zero-calibrated factorization and signed-admissible refutation results for the uniqueness program.
In the broader Recognition stack, native cost uniqueness is the bridge from the Recognition Composition Law and J-uniqueness (forcing chain T5) to a unique cost character on ratio orbits. Closing successor transport above the unit orbit is a structural step in that uniqueness ladder, not a physical constant claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.