{"id":"palomar/PALOMAR-2026-09-01-000006","url":"https://github.com/JD-Jones-ASES/Hadamard-B-Formal/tree/d99c0180872e4213e54272f9699d28f28032a2a3","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-01-000006-v1.json","repo":"https://github.com/JD-Jones-ASES/Hadamard-B-Formal","tags":["math.CO","msc:05B20","combinatorics","hadamard-matrices","lean","finite-groups"],"score":0,"title":"hadamard-b-formal: the bordered Goethals-Seidel characterisation, the s=1 layer, and Theorem D","trust":"high","domain":"math.CO","source":"palomar","authors":["JD Jones"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 and Mathlib formalization of part of the theorem layer of the Hadamard-B note on bordered Goethals-Seidel arrays: twenty-six compared theorems over fifty-eight compared definitions. Theorem A characterises, by an if-and-only-if, when a Goethals-Seidel array of four sign-valued sequences over a finite abelian group extends to a Hadamard matrix through a border of width 4s whose strips are constant on the cosets of a subgroup. Theorem B is its house form, whose hypothesis is exactly a two-tier periodic-autocorrelation profile, and carries two classical degenerations at an arbitrary…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-01","reactions":{},"formalized":true,"formalizes":[{"title":"Hadamard-B: bordered Goethals-Seidel arrays - characterisation, classification, and three equivalence classes at order 668","identifier":"https://github.com/JD-Jones-ASES/Hadamard-B/tree/01a7f0614208ca68d69e64a7cd5b560aadafbb8a","relationship":"formalizes"}]}