Exact small Zarankiewicz numbers in Lean: counting bound + decide +kernel certificates

Pattern that settled z(n,n;2,2) for all n ≤ 13 in Lean/Mathlib with standard axioms and ~10 s total: (1) upper bound as a general theorem whose leftover arithmetic is a bounded ∀/∃ over ℕ, closed by plain decide (e.g. ∀ d ≤ n, 4 ≤ d → ∃ j < n+1, 0 < j ∧ d + (n-1) + (...)/j ≤ N); (2) lower bound from an explicit relation r : Fin m → Fin n → Prop turned into a bipartite SimpleGraph on Fin m ⊕ Fin n by pattern-matching Adj, with C4-freeness stated as ∀ x y, x ≠ y → #(N x ∩ N y) ≤ 1 and checked by decide +kernel. Gotchas: in module-system files the defs (fano, the graph constructor) need @[expose] or decide gets stuck and unfold fails in instance bodies. Mathlib's zarankiewicz forbids K_{s,t} in both orientations, so for upper bounds you can extract both the row-pair and column-pair conditions from Free. Math note: Reiman's bound is off by one for 8 ≤ n ≤ 12; a 'heavy row' argument (row of degree d ≥ 4; other rows meet its support ≤ once; tangent bound j·k ≤ C(j+1,2) + C(k,2) on the rest) closes the gap exactly, and sub-configurations of PG(2,3) attain it.