forcingFn_add
plain-language theorem explainer
The universal forcing map between two strict logic realizations preserves addition on the forced naturals. Anyone building the forced-semiring certificate cites this equality. The proof is a one-line application of the general fact that any zero-fixing, successor-commuting self-map of the forced naturals preserves addition.
Claim. For any two strict logic realizations $R$ and $S$, and any forced naturals $a,b$, the universal forcing map $f_{R,S}\colon\mathrm{LogicNat}\to\mathrm{LogicNat}$ satisfies $f_{R,S}(a+b)=f_{R,S}(a)+f_{R,S}(b)$.
background
LogicNat is the inductive type of naturals forced by the Law of Logic: identity is the zero-cost element and step is one generator iteration, mirroring the orbit ${1,\gamma,\gamma^2,\ldots}$ as the smallest positive-real subset closed under multiplication by $\gamma$ and containing 1. Addition on LogicNat is the usual recursive sum.
A strict logic realization packages a concrete carrier that obeys the recognition axioms. The universal forcing map between two such realizations $R$ and $S$ is presented here as a self-map of LogicNat (the forced carriers are definitionally LogicNat). Prior lemmas already record that this map sends zero to zero and commutes with successor.
The local module assembles those facts into a forced-semiring certificate: the forcing map must be a bijective semiring homomorphism on the forced naturals. Preservation of addition is the additive half of that homomorphism property.
proof idea
One-line term wrapper. Apply the general lemma that any self-map $h$ of LogicNat with $h(0)=0$ and $h(\mathrm{succ},n)=\mathrm{succ}(h,n)$ preserves addition: the proof of that lemma is a single induction on the second summand, matching the recursive definition of $+$. Instantiate $h$ by the forcing map, and feed the already-proved zero and successor preservation facts for that map.
why it matters
This is the additive clause of the forced-semiring certificate. Downstream, forcedSemiringCert_holds packages the forcing map together with bijectivity, zero, one, addition, and multiplication preservation; the add field is exactly this theorem. Without it the certificate cannot assert that the universal forcing map is a semiring homomorphism on the forced naturals.
In the broader Recognition foundation, the forced naturals and their unique (up to unique isomorphism) strict realizations sit under the universal-forcing layer that precedes the T0–T8 chain. Establishing that the comparison map between any two strict realizations is a semiring map is the algebraic content of uniqueness of the forced arithmetic, which later supports the unique J-cost, the self-similar fixed point $\varphi$, and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.