English
If f is primitive recursive, there exists m such that f(n) < ack(m,n) for all n.
Русский
Если f примитивно рекурсивна, существует m такое, что для всех n выполняется f(n) < ack(m,n).
LaTeX
$$$$\\forall f:\\mathbb{N}\\to\\mathbb{N}, \\text{Nat.Primrec}(f) \\Rightarrow \\exists m\\forall n, \\ f(n) < \\operatorname{ack}(m,n).$$$$
Lean4
/-- If `f` is primitive recursive, there exists `m` such that `f n < ack m n` for all `n`. -/
theorem exists_lt_ack_of_nat_primrec {f : ℕ → ℕ} (hf : Nat.Primrec f) : ∃ m, ∀ n, f n < ack m n := by
induction hf with
| zero => exact ⟨0, ack_pos 0⟩
| succ =>
refine ⟨1, fun n => ?_⟩
rw [succ_eq_one_add]
apply add_lt_ack
| left =>
refine ⟨0, fun n => ?_⟩
rw [ack_zero, Nat.lt_succ_iff]
exact unpair_left_le n
| right =>
refine ⟨0, fun n => ?_⟩
rw [ack_zero, Nat.lt_succ_iff]
exact unpair_right_le n
| pair hf hg IHf IHg =>
obtain ⟨a, ha⟩ := IHf; obtain ⟨b, hb⟩ := IHg
refine
⟨max a b + 3, fun n =>
(pair_lt_max_add_one_sq _ _).trans_le <|
(Nat.pow_le_pow_left (add_le_add_right ?_ _) 2).trans <| ack_add_one_sq_lt_ack_add_three _ _⟩
rw [max_ack_left]
exact max_le_max (ha n).le (hb n).le
| comp hf hg IHf IHg =>
obtain ⟨a, ha⟩ := IHf; obtain ⟨b, hb⟩ := IHg
exact
⟨max a b + 2, fun n => (ha _).trans <| (ack_strictMono_right a <| hb n).trans <| ack_ack_lt_ack_max_add_two a b n⟩
| @prec f g hf hg IHf IHg =>
obtain ⟨a, ha⟩ := IHf; obtain ⟨b, hb⟩ := IHg
have : ∀ {m n}, rec (f m) (fun y IH => g <| pair m <| pair y IH) n < ack (max a b + 9) (m + n) :=
by
intro m n
induction n with
| zero => -- The base case is easy.
apply (ha m).trans (ack_strictMono_left m <| (le_max_left a b).trans_lt _)
cutsat
| succ n IH => -- We get rid of the first `pair`.
simp only
apply
(hb _).trans
((ack_pair_lt _ _ _).trans_le _)
-- If m is the maximum, we get a very weak inequality.
rcases lt_or_ge _ m with h₁ | h₁
· rw [max_eq_left h₁.le]
gcongr <;> omega
rw [max_eq_right h₁]
-- We get rid of the second `pair`.
apply (ack_pair_lt _ _ _).le.trans
rcases lt_or_ge _ n with h₂ | h₂
· rw [max_eq_left h₂.le, add_assoc]
exact ack_le_ack (Nat.add_le_add (le_max_right a b) <| by simp) ((le_succ n).trans <| self_le_add_left _ _)
rw [max_eq_right h₂]
-- We now use the inductive hypothesis, and some simple algebraic manipulation.
apply (ack_strictMono_right _ IH).le.trans
rw [add_succ m, add_succ _ 8, succ_eq_add_one, succ_eq_add_one, ack_succ_succ (_ + 8), add_assoc]
exact
ack_mono_left _
(Nat.add_le_add (le_max_right a b) le_rfl)
-- The proof is now simple.
exact ⟨max a b + 9, fun n => this.trans_le <| ack_mono_right _ <| unpair_add_le n⟩
