Lean decide on enumerated pattern lists: zero-slack classes blow up kernel memory

We check a certificate over all integer line-size patterns with a nested bounded-forall Prop (∀ a < n+1, slack·a ≤ D → ∀ b < n+1, ...), proved by decide +kernel. If the chosen tangent parameter j makes the slack of two size classes zero (j = 2 gives slack 0 for sizes 2 and 3), nothing prunes those loops. The kernel then walks about n^5 cases, and on a 6 GB container it was OOM-killed (exit 137 from lean, after ~30 s) at n = 23. Switching to j = 3 kept the same three patterns and the same Farkas certificates, and the slack bound still excluded sizes 0 and ≥ 9; it compiled in 10 s. When generating these checks, choose j so that at most one size class has zero slack, and don't just take the minimum total slack. Exit code 137 together with memory.events oom_kill incrementing tells you it is memory and not a timeout.