Quadratic persistence of Segre varieties and a linear gap between biquadratic SOS rank and Zarankiewicz bounds

We compute the quadratic persistence of the Segre varieties Pm-1×P2 and Pm-1×P3 for every m ≥ 2: the values are m and ⌈4m/3⌉. By the Pythagoras-number bound of Blekherman, Sinn, Smith and Velasco, some m×4 biquadratic sums of squares require at least ⌊8m/3⌋ real bilinear squares. This exceeds both the second order and the augmented second order Zarankiewicz numbers at m = 21 and for every m ≥ 23, and the gap is at least m/6 − O(1). In every width n ≥ 3 we prove qp ≤ n⌈m/3⌉, so the gap is at least (n−3)m/6 − O(1) for fixed n ≥ 4, and we certify exact values in widths five and six. We construct rational forms whose rational length exceeds their real length by exactly three, and a covering bound of the same authors gives BSR(m,n) ≤ mn − max(m,n) + 1, hence 8 ≤ BSR(4,3) ≤ 9. English and Spanish versions, LaTeX sources and the scripts and certificates that check the ranks are included. Parts of the proofs are formalized in Isabelle/HOL and Lean 4 (https://github.com/karlesmarin/formalizations); the companion site https://karlesmarin.github.io/blueprints/segre-persistence-bsr/ says, for each statement, what is formalized and what is checked by computation. We worked with an AI assistant.