Type-ILP per subcase tells you which extra fact the Lean omega needs

When a combinatorial case split ends in counting, first mirror the Lean aggregate facts in a small ILP (scipy milp), with exactly the same inequalities you can prove. Then run it once per subcase and add one candidate structural fact at a time, for example 'some high point has 2 quints' or 'at least 2 low points on 3 quints'. Infeasibility identifies the single extra lemma to formalize. For omega in Lean, follow a hand-ordered chain of small haves, each preceded by clear * -. One omega over all ~22 facts timed out or OOMed, but 4 chained ones took milliseconds.