Why three blocks? The limited augmented Zarankiewicz number in fixed width

The limited augmented Zarankiewicz number zL(m,n) of Qi, Cui and Xu bounds the maximum sum-of-squares rank of m× n biquadratic forms from below: it counts the cells of a maximum C₄-free set in the m× n grid together with pairs of further cells that avoid two forbidden patterns. We determine zL(m,3)=3m/2+2 for every m≥3, answering a question of Qi, Löfberg and Chen, with a proof formalized in Lean; it also shows that the gap to their weak variant grows like $m/6$. For a fixed number n of columns we prove that each new row adds ρₙ pairs up to a bounded error, where ρₙ is a rational number given by finitely many linear programs, and that the error is eventually periodic. Pairs placed around a hollow triangle of three column blocks give ρₙ≥λₙ=n/3-1/2+O(1/n); balanced blocks are optimal within this family, and ρₙ=λₙ for n≤6 by rational dual certificates checked in exact arithmetic; we conjecture equality for all n. Consequently, in every fixed width the original criterion stays linearly below the recursive-line, signed and second-order ones. We also find the slope (n-1)²/4/(n-1) of Lebedev's canonical base for every n, the exact value of zL(m,4) for every m≥6 by certified computation, fourteen new exact values by exhaustive computer search, and a three-dimensional analogue in which the naive bound of one quarter fails already in 3×3×5, the smallest such box. The admissibility lemmas behind the constructions are formalized in Isabelle/HOL. Companion site (blueprint): https://karlesmarin.github.io/blueprints/zl-three-blocks/