import Omega.Floor

namespace Omega

def threshold : ℕ → ℕ
  | 0 => 1
  | n+1 => (S*threshold n+Q-1)/Q

theorem step_threshold (d t : ℕ) : F d < t ↔ d < (S*t+Q-1)/Q := by
  unfold F Q S
  omega

theorem extinction_threshold (n d : ℕ) : F^[n] d=0 ↔ d < threshold n := by
  induction n generalizing d with
  | zero => simp [threshold]
  | succ n ih =>
    rw [Function.iterate_succ_apply,ih,step_threshold]
    rfl

theorem threshold_values : (List.range 11).map threshold=
    [1,3,9,27,80,236,695,2045,6016,17697,52058] := by decide

theorem extinction_by_ten (d : ℕ) (hd : d < domainSize) : F^[10] d=0 := by
  rw [extinction_threshold]
  have ht : threshold 10=52058 := by decide
  rw [ht]
  unfold domainSize at hd
  omega

theorem deepest_seeds (d : ℕ) (hd : d < domainSize) :
    F^[9] d ≠ 0 ∧ F^[10] d=0 ↔ 17697 ≤ d := by
  simp only [ne_eq,extinction_threshold]
  have ht9 : threshold 9=17697 := by decide
  have ht10 : threshold 10=52058 := by decide
  rw [ht9,ht10]
  unfold domainSize at hd
  omega

theorem all_twenty_three_steps (d : ℕ) (hd : d < domainSize) : F^[23] d=0 := by
  have hm : F^[23] d=F^[13] (F^[10] d) := by rw [← Function.iterate_add_apply]
  rw [hm,extinction_by_ten d hd]
  have hz (n : ℕ) : F^[n] 0=0 := by
    induction n with
    | zero => rfl
    | succ n ih => rw [Function.iterate_succ_apply',ih,step_zero]
  exact hz 13

end Omega