PRCCharacterOrbitIdentityContractsSuccessorStep_of_additive_compat
plain-language theorem explainer
Additive compatibility of a ratio-orbit character with the successor step forces the backward identity-orientation law: identity at succ(p) implies identity at p for every nonzero distinction natural p. Anyone proving successor transport or native-cost uniqueness for PRC characters cites this. The proof reduces both sides to rational displays via crossEq ↔ toRat and finishes by linarith on the +1 cast.
Claim. Let $\chi$ be a map on ratio orbits. Suppose that for every nonzero distinction natural $p$, $\chi$ of the orbit direction of $\mathrm{succ}(p)$ is cross-equal to $\chi$ of the orbit direction of $p$ plus the unit ratio orbit. Then $\chi$ contracts identity orientation along successor: whenever $\chi$ is identity-oriented at $\mathrm{succ}(p)$, it is identity-oriented at $p$.
background
Primitive Recognition Calculus builds arithmetic and cost from orbit data rather than posited Peano structure. Distinction naturals carry a successor (one more generator application) with a faithful toNat reading; ratio orbits are the signed rational displays of those orbits, with addition and a unit orbit whose rational image is $1$. Cross-equality of ratio orbits is equivalent to equality of their rational displays (crossEq_iff_toRat_eq).
A ratio character $\chi$ acts on ratio orbits. Additive compatibility with successor says that on every nonzero orbit direction, $\chi$ at the successor direction matches $\chi$ at the present direction plus the unit: the missing bridge from multiplicative character data to the additive/trace side of the orbit. Identity orientation of $\chi$ at a direction is the predicate that the character lands on the identity class there.
The local goal is the backward one-step law: identity orientation at $\mathrm{succ}(p)$ forces identity orientation at $p$. Together with the matching forward extension law, this is the successor-step transport package needed for trace coherence of native cost characters.
proof idea
Tactic proof, about a dozen steps. Fix nonzero $p$ and assume identity orientation at $\mathrm{succ}(p)$. Additive compatibility supplies cross-equality of $\chi(\mathrm{succ},p)$ with $\chi(p)+1$. Unfold identity orientation on both the hypothesis and the goal, then replace every cross-equality by rational equality via crossEq_iff_toRat_eq. Push addition and the unit through add_toRat and one_toRat, substitute the compatibility identity, and rewrite orbit directions by orbitDirection_toRat together with toNat_succ. The remaining arithmetic is the cast identity $(\mathrm{Nat.succ},n:\mathbb{Q})=n+1$, discharged by norm_num, after which linarith closes the goal.
why it matters
Native-cost uniqueness in PRC needs characters whose multiplicative ratio action is coherent with the additive trace on orbits. This lemma discharges the backward half of that coherence: additive successor compatibility implies identity orientation contracts along successor.
It is paired immediately with the forward extension law inside PRCCharacterOrbitIdentitySuccessorTransport_of_additive_compat, which bundles both one-step laws into the successor-step transport required for trace coherence. That transport feeds the native-cost uniqueness blocker certificate in the same module, the certificate that records which factorization targets are proved and which signed-admissible routes are refuted.
In the broader Recognition forcing picture this is foundation work beneath J-uniqueness and the cost calculus: it locks the character side of the native cost so later uniqueness and d'Alembert/trace matching arguments can treat successor steps as identity-preserving transport rather than free data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.