🦑 N ⟶ N, 0 + n = n 💎 Take 2

• 03 August 2025
• Mathematics,
• Process book,
• Learning

💎 -- I felt a bit lost, and now I find it is sort of simple to get back to this :quest of 0 + n = n
-- Wow zero_add is the proof in mathlib!

zero_add is the proof of
   ∀ n, 0 + n = n

     "built from the inductive definition of + on ℕ" ?


pattern matching + simp + inductive base case

theorem zero_add (n : ℕ) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ n ih => simp [Nat.add_succ, ih]

ih 🦑 is strong swimmer
   in inductive sea
      "I proved it for n"
            ~ let’s tackle succ n

ride it using add_succ 🏄

*-- How to write zero_add it from first principles? *

theorem zero_add : ∀ n : ℕ, 0 + n = n
| 0     => rfl
| succ n => congrArg succ (zero_add n)

-- This looks like definition of ℕ !

Maybe this is cause we are showing something holds in the natural numbers, so it has the same structure. Iff it has the same structure?

🤖🦑💎

Proof unfolds like ℕ’s definition
  — recursion and induction perfectly aligned. 🐚✨

-- The proof is the structure. 🎯

    #maybe harmony of recursion & induction is the essence of ℕ’s algebraic beauty.

succ n => congrArg succ (zero_add n)

apply succ (zero_add n) to each side of the equation until zero rfl?

zero_add 3
= congrArg succ (zero_add 2)
= congrArg succ (congrArg succ (zero_add 1))
= congrArg succ (congrArg succ (congrArg succ (zero_add 0)))
= congrArg succ (congrArg succ (congrArg succ rfl))   -- base case: 0 + 0 = 0
= congrArg succ (congrArg succ rfl)
= congrArg succ rfl
= rfl

lifting an equality    - like stepping up a staircase while keeping balance       - applying a function (succ) to both sides of an equation, preserving equality at each step
I don't yet understand how to show 0 + 0 = 0
0 + 0 = 0 is base case we can show with rfl? 0 + n = n is different?

inductive N : Type
| zero : N
| succ : N → N

def add : N → N → N
| .zero, n => n
| .succ m, n => .succ (add m n)

#eval add N.zero N.zero

🐚 crafting a synthetic geometry of numbers in type theory.
   numbers as geometric/structural objects,
      defined via their relations

This seems really cool also, because it seems like a simple idea, but I don't yet understand it so I am learning it by looking at so many aspects of it! This is an advantage to not yet understanding something.

-- Wow composition = add, identity morphism = zero

   I didn't see this!

def add … is defining the composition?

🤖 synthetic because you define the geometry from type/logic, not by referencing ℝ-line, graphs, etc. 🖇 1 ⟶ 🍩
   1 ⟶ 🍩 is a logical path from point to donut

      building “geometry” from logic — no need for ℝ,          but types, terms, morphisms

add m n ≅ composition of m and n

obj: natural numbers
mor: paths from 0 to n (built by succ)
id: `zero ≅ id : 0 + n = n

com: add sequences steps

   🧅 succ (succ (succ zero)) + succ (succ zero)

      ⟶ gluing morphisms ⇒ longer path ⛵

-- 🧷 local data stitched into global coherence?
   geometry via logic

• Previous: N ⟶ N, 0 + n = n
• Next: take3 -- sheaf.notes ∈ day