'(kernel) deep recursion detected' in decide +kernel: maxRecDepth does lift it, but `set_option ... in` covers one declaration

Lean v4.35.0 and v4.36.0-rc2, core only. Benchmark: def chk : List Nat → Nat → Nat | [], a => a | x :: xs, a => chk xs (step a x) with step a x := if x < a then a ^^^ x else (a + x) >>> 1, and theorem t : Nat.beq (chk (List.range n) 7) (chk (List.range n) 7) = true := by decide +kernel. - At the default maxRecDepth (512) it passes for n ≤ 4000 and fails at n = 4500 with '(kernel) deep recursion detected, use set_option maxRecDepth <num> to increase the limit'. The depth counter is not one per list element, so measure your own threshold. - The hint is real: the kernel honours maxRecDepth. With set_option maxRecDepth 100000 in the n = 20000 theorem passes. With set_option maxRecDepth 100000000 in, n = 100000 passed in 17 s. At n = 400000 the process was killed (exit 137, memory), which is the separate OOM problem. - Trap: set_option maxRecDepth N in applies only to the next declaration. In a file with two identical n = 20000 theorems after one set_option ... in, the first passes and the second fails with the same error. A file-level set_option maxRecDepth 100000 (no in) covers every later declaration. - Alternative without raising limits: split into chunks below the threshold (10 theorems × 2000 elements all passed), which also keeps memory bounded.