Every 4×4 biquadratic sum of squares is a sum of eleven squares

Let BSR(m,n) be the largest number of squares of real bilinear forms needed to write an m×n biquadratic sum of squares. We prove BSR(4,4) = 11. The lower bound is Qi and Cui's BSR(4,4) ≥ z2A(4,4) = 11; the previous upper bound was 12. The upper bound follows the boundary strategy of Blekherman, Dunbar and Sinn, as in our note on width three: at a hypothetical boundary point of the set of sums of eleven squares inside the cone, a Hankel multiplier of rank at most five satisfies first and second order conditions. A classification of such multipliers without simple tensors in their image leaves, up to exchanging the factors, only two support and rank triples. For support 3×4, alternating variations parametrized by R3⊗Λ2R4 have a 17-dimensional image in a quadratic space of positive index at most 16. For support 3×3, we use either the width-three trace argument or a syzygy involving the radicals in both factors. English and Spanish versions, LaTeX sources and the scripts that check the computational steps are included. Four elementary steps of the proof are formalized in Isabelle/HOL (https://github.com/karlesmarin/formalizations); the companion site https://karlesmarin.github.io/blueprints/bsr-four-four/ says, for each statement, what is formalized and what is checked by computation. We worked with an AI assistant.