map_preserves_add
plain-language theorem explainer
Any endomorphism of the logic naturals that fixes zero and commutes with successor automatically preserves addition. Foundation workers building the forced semiring cite this when showing the unique forcing map between strict logic realizations is additive. The argument is a single induction on the second summand, rewriting with the recursive clauses for addition.
Claim. Let $h:\mathbb{N}_{\mathrm{L}}\to\mathbb{N}_{\mathrm{L}}$ satisfy $h(0)=0$ and $h(n+1)=h(n)+1$ for every $n$. Then $h(a+b)=h(a)+h(b)$ for all $a,b\in\mathbb{N}_{\mathrm{L}}$.
background
LogicNat is the inductive type of natural numbers forced by the Law of Logic. Its constructors are identity (the zero-cost element, multiplicative identity of the orbit) and step (one more iteration of the generator). Successor is one application of step. Addition is defined by recursion on the second argument; the simp lemmas are $n+0=n$ and $n+\mathrm{succ},m=\mathrm{succ}(n+m)$.
The module sits in UniversalForcing and prepares the unique structure-preserving map between strict logic realizations. Maps that fix zero and commute with successor are the candidates for that forcing map; additivity is the first algebraic property required.
proof idea
Fix the first summand and induct on the second. Zero case: rewrite both sides by the zero clause of addition and apply the hypothesis that $h$ fixes zero. Successor case: rewrite by the successor clause of addition, push $h$ through successor via the commuting hypothesis, apply the inductive hypothesis, then rewrite again by the commuting hypothesis and the successor clause. Every step is a definitional or simp rewrite from the arithmetic-from-logic layer.
why it matters
This is the additivity engine for the forced semiring. Downstream, forcingFn_add instantiates it on the canonical forcing map between two strict logic realizations, proving that map preserves addition. The sibling map_preserves_mul reuses the same two hypotheses together with this lemma, because multiplication recurses on its second argument via addition. Both feed the certificate that the unique forcing function is a semiring homomorphism. In the Recognition Science stack this belongs to universal forcing of arithmetic from logic, upstream of the T0–T8 physical forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.