ack_zero
theorem ack_zero : ∀ (n : ℕ), ack 0 n = n + 1
The theorem `ack_zero` asserts that for every natural number `n`, the Ackermann function `ack` with first argument as zero and second argument as `n` equals `n + 1`. In other words, if the first parameter to the Ackermann function is zero, the function simply increments the second parameter by one.
More concisely: The Ackermann function `ack` with argument `0` equals `n + 1` for every natural number `n`.
|
ack_mono_left
theorem ack_mono_left : ∀ (n : ℕ), Monotone fun m => ack m n
This theorem states that for every natural number `n`, the Ackermann function `ack` is monotone when its first argument varies while the second argument remains fixed to `n`. In other words, if `m1 ≤ m2` for any two natural numbers `m1` and `m2`, then `ack m1 n ≤ ack m2 n`.
More concisely: For all natural numbers `n`, the Ackermann function `ack` is monotone in its first argument, i.e., `ack m1 n ≤ ack m2 n` for all `m1 ≤ m2`.
|
ack_strictMono_left
theorem ack_strictMono_left : ∀ (n : ℕ), StrictMono fun m => ack m n
This theorem states that for every natural number `n`, the Ackermann function `ack` is strictly monotone when considered as a function of its first argument `m`. This means that for all pairs of natural numbers `(m1, m2)` where `m1 < m2`, it holds that `ack m1 n < ack m2 n`. In other words, increasing the first argument of the Ackermann function (while keeping the second argument fixed) results in a larger output value.
More concisely: For all natural numbers `n` and `m1` < `m2`, `ack (m1) n` < `ack (m2) n` holds for the Ackermann function.
|
exists_lt_ack_of_nat_primrec
theorem exists_lt_ack_of_nat_primrec : ∀ {f : ℕ → ℕ}, Nat.Primrec f → ∃ m, ∀ (n : ℕ), f n < ack m n
This theorem states that if `f` is a primitive recursive function (a function which can be calculated by a finite number of steps from certain initial functions using only composition and primitive recursion), then there exists a natural number `m` such that for all natural numbers `n`, `f(n)` is less than the value of the Ackermann function at `m` and `n`. The Ackermann function is of interest as an example of a recursive function that grows very quickly and is not primitive recursive.
More concisely: For every primitive recursive function `f`, there exists a natural number `m` such that for all `n`, `f(n)` is strictly less than Ackermann(`m`, `n`).
|
not_primrec₂_ack
theorem not_primrec₂_ack : ¬Primrec₂ ack
The theorem `not_primrec₂_ack` asserts that the Ackermann function, which is a two-argument function often used as an example of a recursive but not primitive recursive function, is indeed not primitive recursive. In other words, the theorem verifies the property that the Ackermann function cannot be expressed as a function that can be obtained through a finite sequence of certain simple operations, which is the definition of a primitive recursive function.
More concisely: The Ackermann function is not primitive recursive.
|
ack_succ_succ
theorem ack_succ_succ : ∀ (m n : ℕ), ack (m + 1) (n + 1) = ack m (ack (m + 1) n)
The theorem `ack_succ_succ` states that for all natural numbers `m` and `n`, the value of the Ackermann function at `(m + 1, n + 1)` is equal to the Ackermann function at `(m, ack(m + 1, n))`. In other words, it is validating one of the recursive case definitions for the Ackermann function, specifically the case where both arguments are successors of some natural numbers.
More concisely: The Ackermann function satisfies the recursive relation A(m + 1, n + 1) = A(m, A(m + 1, n)).
|
add_lt_ack
theorem add_lt_ack : ∀ (m n : ℕ), m + n < ack m n
This theorem states that for all natural numbers `m` and `n`, the sum of `m` and `n` is less than the value of the two-argument Ackermann function applied to `m` and `n`. The Ackermann function, known for its rapid growth, is defined by three conditions: when the first argument is 0, it returns `n + 1`; when the first argument is `m + 1` and the second argument is 0, it returns the Ackermann function of `m` and 1; and when both arguments are `m + 1` and `n + 1` respectively, it returns the Ackermann function of `m` and the Ackermann function of `m + 1` and `n`. This theorem essentially points to the extreme growth rate of the Ackermann function.
More concisely: For all natural numbers m and n, m + n is strictly less than Ackermann(m, n).
|
ack_mono_right
theorem ack_mono_right : ∀ (m : ℕ), Monotone (ack m)
The theorem `ack_mono_right` asserts that for every natural number `m`, the Ackermann function `ack m` is monotone. In other words, if `n₁ ≤ n₂` for any natural numbers `n₁` and `n₂`, then `ack m n₁ ≤ ack m n₂`. This signifies that the Ackermann function, when fixed with a particular value of `m`, never decreases as its second argument increases. The Ackermann function is well-known in computer science as an example of a function that grows very rapidly and is not primitive recursive.
More concisely: For all natural numbers m and n₁, n₂, if n₁ ≤ n₂ then Ackermann function ack m with argument n₁ is less than or equal to the Ackermann function ack m with argument n₂.
|
ack_strictMono_right
theorem ack_strictMono_right : ∀ (m : ℕ), StrictMono (ack m)
The theorem `ack_strictMono_right` states that for every natural number `m`, the Ackermann function `ack m` is strictly monotonic. In other words, if `n1` and `n2` are any natural numbers such that `n1 < n2`, then `ack m n1 < ack m n2`. The Ackermann function is thus strictly increasing in its second argument for each fixed first argument.
More concisely: For all natural numbers m and n1 < n2, the Ackermann function ack m is strictly increasing in the second argument: ack m n1 < ack m n2.
|