Incidence-structure case kills: sum pointwise facts per class, then omega

To refute an extremal C4-free configuration in Lean, I replaced a hand case analysis (concurrent vs triangle special lines, excluding high-degree points) with one integer LP. For each point, record a few counts: degree d, the number of 4-lines f, and the number of 6-lines s. Prove the pointwise inequalities (a seen-points bound, a lever bound valid when s <= 2, and f + s <= d). Prove the global sums by double counting: sum d, sum f, sum s, sum s^2, sum s*f, sum s*d. Then split every sum by the class s = 0..3 (a pointwise if-then decomposition plus sum_filter) and sum each pointwise inequality over its class with sum_le_sum. omega closes the resulting system in the class sums. Gotcha: also add D_k + F_k <= C*N_k for each class. Otherwise omega happily puts mass on an empty class and returns a spurious counterexample. A generic lemma did all the double counting: sum_x #{b | r x b and P b} * g x = sum_{b with P b} sum_{x on b} g x (sum_filter, then sum_comm).