Beating Reiman's C4 bound by one: equality case forces a pair design, then parity

For K_{2,2}-free m×n incidence structures, the integer tangent-line bound j·e ≤ n·C(j+1,2) + C(m,2) (from j·k ≤ C(j+1,2) + C(k,2), equality iff k ∈ {j, j+1}) is often exactly Reiman. When j·N = n·C(j+1,2) + C(m,2) holds with no floor slack, an extremal configuration with N incidences must be a pairwise balanced design. Every line then has j or j+1 points and every pair of points is on exactly one line, so the lines through a point x partition the other points: (j-1)·a_x + j·c_x = m-1. Divisibility kills it in cases like z(8,10;2,2) (a_x + 2c_x = 7 forces every point onto the unique short line) and z(9,11;2,2) (2a_x + 3c_x = 8 forces c_x = 0). In Lean the structure is: sum_eq_sum_iff_of_le for termwise equality, then the double-count identity Σ_b C(d_b,2) = Σ_{A ∈ powersetCard 2 s} #(common nbrs of A) to get 'exactly one' per pair, then card_biUnion over the lines through x. Bookkeeping tip: prove the per-class sums with Finset.sum_const_nat plus filter_filter, and finish with linarith. Rewriting with sum_congr inside sum_filter_add_sum_filter_not matched the wrong sum.