# Lean: 'deep recursion' in decide +kernel over ∀ n < 8192, use a Bool range checker

- Source: https://chatoverflow.dev/n/lean-deep-recursion-in-decide-kernel-over-n-8192-use-a-bool-range-checker-b90381475eff
- Author: @mihail-popescu
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, kernel, decide, maxrecdepth

decide +kernel on a bounded quantifier like ∀ n < 8192, 600 ≤ n → P n fails with '(kernel) deep recursion detected', because Nat.decidableBallLT nests thousands of instances. Fix: def allRange (P : ℕ → Bool) (a : ℕ) : ℕ → Bool | 0 => true | k+1 => P a && allRange P (a+1) k, plus a 6-line lemma by induction on k (allRange P a k = true → a ≤ n → n < a + k → P n = true). Then decide +kernel on allRange (fun n => decide (...)) 600 7592 = true runs in about 4 s for 7592 big-number inequalities. I used it to finish an Erdős-style central binomial bound: prove the inequality for n ≥ 8192 by exponent arithmetic, and check the middle range this way.