toNat_add
plain-language theorem explainer
The map from logic-forced naturals to ordinary naturals preserves addition. Researchers building the Recognition Science arithmetic layer cite this result when transferring cancellation, ordering, and other properties to the standard model. The proof is by induction on the second argument, reducing each case via the recursive definitions of addition and the map.
Claim. Let $N_L$ be the inductive type of naturals forced by the Law of Logic, with addition $+$ defined by the rules $n + 0 = n$ and $n + S(m) = S(n + m)$. Let $phi: N_L to N$ send the identity constructor to 0 and each step constructor to the successor in $N$. Then for all $a, b in N_L$, $phi(a + b) = phi(a) + phi(b)$.
background
LogicNat is the inductive type whose identity constructor represents the zero-cost element and whose step constructor represents one further iteration of the generator; this structure encodes the orbit closed under multiplication by the self-similar fixed point. The function toNat extracts the iteration count by sending identity to 0 and step n to succ (toNat n). Addition on LogicNat satisfies the two simp lemmas add_zero (n + zero = n) and add_succ (n + succ m = succ (n + m)), which are the only recursive clauses used here.
proof idea
The proof is by induction on b. The identity case rewrites a + zero via add_zero, applies toNat_zero, and closes with Nat.add_zero. The step case rewrites a + succ b via add_succ, applies toNat_succ on both sides, invokes the induction hypothesis, and finishes with Nat.add_succ.
why it matters
This recovery theorem supplies the addition-preservation step required by add_left_cancel, le_antisymm, lt_iff_le_and_ne, toNat_le, and toNat_mul. It completes the bridge that lets every arithmetic fact proved in Nat transfer back to the logic-forced structure, thereby supporting the later construction of the phi-ladder and the eight-tick octave in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Perturbation around Koebe function closes Li-Keiper equations
"λ(n) = ∑ (-1)^{k-n+1} binom(n,k) λ(k) + Δ (Eq. 12); λ_n = (-1)^n ∑ (-1)^k binom(2n,n-k) λ_k (Eq. 18); discrete derivative Δ^n f(m) = ∑ (-1)^k binom(n,k) f(m+(n-k)) (Appendix 3)"