{"id":"palomar/PALOMAR-2026-10-17-000006","url":"https://github.com/JD-Jones-ASES/rr-exact/tree/141bddb9f263aa99c0c6a8be4af469389d2afca2","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-17-000006-v1.json","repo":"https://github.com/JD-Jones-ASES/rr-exact","tags":["math.OC","math.FA","msc:15A45","msc:15A60","msc:47A30","matrix-inequalities","operator-norm","semidefinite-matrices","counterexamples"],"score":0,"title":"Low-dimensional exact counterexamples to the Recht–Ré inequality","trust":"high","domain":"math.OC","source":"palomar","authors":["JD Jones"],"reviews":0,"subject":"math.OC","summary":"Five real symmetric PSD 3×3 integer matrices and five complex Hermitian PSD 2×2 Gaussian-integer matrices each have sum 100I and exact norm-of-averaged-product ratio 10329/10000 at n=k=5. The Lean statements use Mathlib positive semidefiniteness over the real and complex fields and the Euclidean operator norm. The rational formalization of De Sa's dimension-five norm-19/16 example is included as a supporting benchmark. The real symmetric dimension-two case is not resolved.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-17","reactions":{},"formalized":true}