PRCCharacterOrbitIdentityExtendsSuccessorStep_of_additive_compat
plain-language theorem explainer
Additive compatibility of a ratio-orbit character χ with the δ-successor forces the forward one-step identity-orientation law: identity at p implies identity at succ p. Cited by anyone transporting identity orientation along the orbit ladder toward native cost uniqueness. Proof rewrites both sides to rational equality via toRat and closes with the successor formula for orbit directions.
Claim. Let $\chi$ map ratio orbits to ratio orbits. Suppose that for every nonzero distinction index $p$, $\chi(\mathrm{dir}(\mathrm{succ}\, p))$ is cross-equal to $\chi(\mathrm{dir}\, p)+1$. Then whenever $\chi$ is identity-oriented at $p$, it is identity-oriented at $\mathrm{succ}\, p$.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (zero and successor). Nonzero indices carry an orbit direction orbitDirection p. A RatioOrbit is an integer numerator over a nonzero distinction denominator; its verifier display is the rational toRat. Cross-equality of two ratio orbits is equivalent to equality of those rationals (crossEq_iff_toRat_eq).
A character here is a self-map χ on ratio orbits. Additive compatibility with the δ-successor says that on nonzero directions, χ at the successor direction is cross-equal to χ at the present direction plus the unit ratio orbit. Identity orientation at p means χ fixes the direction of p (in the sense of the identity predicate unfolded in the proof).
The local module builds native cost uniqueness from character/trace structure. Upstream arithmetic lemmas supply add_toRat, one_toRat, and toNat_succ, so successor steps become ordinary +1 on ℚ.
proof idea
Tactic proof, short rewrite chain. Fix nonzero p and assume identity orientation at p. Instantiate additive compatibility at p to get crossEq of χ(dir(succ p)) with χ(dir p)+1. Unfold the identity-orientation predicate on hypothesis and goal. Convert all crossEq statements to toRat equality. Push toRat through addition and the unit (add_toRat, one_toRat), substitute the compatibility and identity hypotheses, then rewrite both orbit directions via orbitDirection_toRat and DistinctionNat.toNat_succ. The remaining rational identity is norm_num.
why it matters
This is the forward half of successor transport for identity orientation under additive compatibility. Downstream, PRCCharacterOrbitIdentitySuccessorTransport_of_additive_compat packages it with the matching contraction step into full bidirectional transport. That transport sits on the path recorded by prc_native_cost_uniqueness_blocker_certificate, which certifies the zero-calibrated native-cost character factorization target and related refutations.
In the broader Recognition stack, native cost uniqueness is the bridge from multiplicative ratio characters to the additive/trace side that forces the J-cost (T5: $J(x)=(x+x^{-1})/2-1$) and the Recognition Composition Law. Closing successor identity transport removes a discrete obstruction on the orbit ladder before continuous uniqueness arguments apply.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.