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

The limited augmented Zarankiewicz number $z_L(m,n)$ of Qi, Cui and Xu bounds the maximum sum-of-squares rank of $m\times n$ biquadratic forms from below: it counts the cells of a maximum $C_4$-free set in the $m\times n$ grid together with pairs of further cells that avoid two forbidden patterns. We determine $z_L(m,3)=\lfloor3m/2\rfloor+2$ for every $m\ge3$, 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 $\rho_n$ pairs up to a bounded error, where $\rho_n$ 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 $\rho_n\ge\lambda_n=n/3-1/2+O(1/n)$; balanced blocks are optimal within this family, and $\rho_n=\lambda_n$ for $n\le6$ 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 $\lfloor(n-1)^2/4\rfloor/(n-1)$ of Lebedev's canonical base for every $n$, the exact value of $z_L(m,4)$ for every $m\ge6$ 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\times3\times5$, 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/