 200    show n + succ zero = succ n
 201    rw [add_succ, add_zero]
 202
 203theorem mul_add (a b c : LogicNat) : a * (b + c) = a * b + a * c := by
 204  induction c with
 205  | identity =>
 206    show a * (b + zero) = a * b + a * zero
 207    rw [add_zero, mul_zero, add_zero]
 208  | step c ih =>
 209    show a * (b + succ c) = a * b + a * succ c
 210    rw [add_succ, mul_succ, mul_succ, ih, add_assoc]
 211
 212/-! ## 5. Recovery Theorem: LogicNat ≃ Nat
 213
 214Lean's built-in `Nat` has the same inductive shape as `LogicNat`. The
 215two are isomorphic. This is the recovery: the natural numbers Lean
 216already has are exactly the structure forced by the Law of Logic, with
 217no base 10, no positional representation, and no arithmetic axioms
 218posited. -/
 219
 220/-- The forward map: read off the iteration count. -/
 221def toNat : LogicNat → Nat
 222  | .identity => 0
 223  | .step n   => Nat.succ (toNat n)
 224
 225/-- The inverse map: build the orbit by iterating the step. -/
 226def fromNat : Nat → LogicNat
 227  | 0          => .identity
 228  | Nat.succ n => .step (fromNat n)
 229
 230@[simp] theorem toNat_zero : toNat zero = 0 := rfl
 231@[simp] theorem toNat_succ (n : LogicNat) : toNat (succ n) = Nat.succ (toNat n) := rfl
 232@[simp] theorem fromNat_zero : fromNat 0 = zero := rfl
 233@[simp] theorem fromNat_succ (n : Nat) : fromNat (Nat.succ n) = succ (fromNat n) := rfl

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.