PRCCharacterOrbitSuccessorAdditiveCompatible
plain-language theorem explainer
Defines when a ratio-orbit map χ respects δ-successor additively: on every nonzero orbit direction p, χ(direction of succ p) is cross-equivalent to χ(direction of p) plus the unit orbit. Native-cost uniqueness work cites it as the bridge from multiplicative characters to trace/additive orbit structure. The body is a pure Prop abbreviation, not a proved statement.
Claim. A map $\chi$ on ratio orbits is successor-additive compatible when, for every nonzero distinction position $p$, $\chi$ of the orbit direction of $\mathrm{succ}(p)$ is cross-equivalent (balanced cross-multiplication of signed numerators and denominators) to the ratio-orbit sum of $\chi$ of the direction of $p$ with the unit ratio orbit.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (zero and successor). A RatioOrbit is a rational display: signed-orbit numerator over a nonzero distinction denominator. Two ratio orbits are related by crossEq when cross-multiplication balances as signed orbits; that is the internal PRC stand-in for rational equality.
orbitDirection sends a nonzero distinction position $p$ to the ratio orbit with numerator the signed orbit of $p$ and denominator one. Successor on distinction positions is the generator step; orbit_succ_ne_zero records that successors never hit zero, so directions of successors are always defined.
This module develops native cost uniqueness for PRC characters. Multiplicative ratio characters alone do not automatically talk to the additive/trace side of the orbit. The present predicate packages exactly the missing compatibility: χ should turn δ-successor on directions into addition of the unit ratio orbit, up to cross-equivalence.
proof idea
Definitional Prop, not a theorem. The body quantifies over nonzero distinction positions $p$ and asserts RatioOrbit.crossEq between χ applied to orbitDirection of succ p (using orbit_succ_ne_zero) and RatioOrbit.add of χ on orbitDirection p with RatioOrbit.one. No tactics or lemmas are invoked; downstream theorems assume this Prop as a hypothesis.
why it matters
Doc-comment frames this as the missing bridge between multiplicative ratio characters and the trace/additive structure of the orbit. Downstream, three transport lemmas discharge identity-extension, identity-contraction, and full successor-transport for character orbit identity once this compatibility is assumed. It is also the conclusion of the sharper target PRCPrimeCalibrationForcesOrbitSuccessorAdditiveCompatibilityTarget (prime calibration should force the property) and appears in the Pass-25 native-cost uniqueness blocker certificate as an exact open Lean target.
A concrete negative result already uses it: the reciprocal character is proved not successor-additive compatible, so reciprocity alone cannot serve as the native cost character. In the broader RS forcing picture this sits under native J-cost uniqueness (T5 lineage): characters must match the additive doubled-trace/D'Alembert side, not merely multiply ratios.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.