PRCCharacterPrimeFloorOrbitIdentityExtendsSuccessorStep
plain-language theorem explainer
Packages the forward one-step identity-orientation transport rule for ratio characters along the distinction orbit, restricted to non-unit floors. Anyone proving prime-floor successor coherence or native-cost uniqueness blockers cites this Prop. It is a pure predicate definition: a universal quantification over nonzero non-unit orbits, not a proved statement.
Claim. For a map $\chi$ from ratio orbits to ratio orbits, the following holds: for every nonzero distinction-orbit $p$ that is not the multiplicative unit, if $\chi$ has identity direction at $p$, then $\chi$ has identity direction at the successor of $p$.
background
In the Primitive Recognition Calculus, distinction orbits (DistinctionNat) are the base-neutral finite orbits generated by repeated distinction acts; successor is one more generator application. The native unit predicate singles out the one-step orbit as the only multiplicative unit. Ratio orbits display a signed numerator over a nonzero distinction-orbit denominator.
A ratio character $\chi$ assigns to each ratio orbit another ratio orbit. Identity direction at an orbit means the character realizes the canonical identity event (the J-cost minimum at state $1$). The unit orbit is self-reciprocal, so identity transport must not be forced out of the unit itself: that would exclude the globally reciprocal character branch.
This definition lives in the native-cost uniqueness module, which isolates exact Lean targets for when a character-derived cost coincides with the unique J-cost forced by the Recognition Composition Law.
proof idea
Definitional packaging only. The body is the Prop $\forall p\neq 0,; \neg\mathrm{unit}(p);\Rightarrow; \mathrm{Id}(\chi,p);\Rightarrow; \mathrm{Id}(\chi,\mathrm{succ},p)$, using the already-proved fact that successors of nonzero orbits remain nonzero. No tactics or lemmas are applied; downstream theorems discharge or refute instances of this predicate.
why it matters
This is the forward half of the corrected prime-floor successor-transport rule. Downstream, it is conjoined with the backward (contracting) half to form the full successor-transport Prop needed for prime-to-prime trace coherence. A local non-mixing orientation hypothesis implies this Prop. It appears as an exact target in the prime-calibration forcing chain and inside the Pass-25 native-cost uniqueness blocker certificate, which records that uniqueness is not yet closed but the missing mathematics is split into named Lean goals. One of those goals (that prime calibration alone forces this transport for every ratio character) has already been refuted, so the definition marks a precise boundary rather than a free assumption. Framework-wise it sits under the J-uniqueness / native-cost uniqueness thread (T5 and the RCL), not under dimensional or octave forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.