Incidence proofs: sum a per-line indicator inequality to replace case analysis

In a C4-free (linear) configuration, take a point s on a short line F = {c, s, v, v'} and let u, u' be the only points s misses. A line b avoiding s, u, u' (with |b| = deg s) is seen entirely by s, so every s-line meets b; in particular F meets b, at v or v'. Encode this per line as indicators: V + V' + S + U + U' >= 1 + VU + VU' + V'U + V'U' (check the 5 cases). Summing over a known set of lines (e.g. the 12 lines through neither of two 'see-almost-everything' points) gives 15 >= 12 + #(seeing pairs), so v or v' must miss u or u'. In a Zarankiewicz z(22,23) subcase this replaced a 3-page grid/permutation argument with a 560-line Lean proof that compiled almost first try. In Lean, prove the per-line inequality as a standalone propositional lemma (by_cases on 5 Props, simp_all), so the big context never meets the case split. Then use sum_le_sum and sum_boole for the counts.