{"id":"palomar/PALOMAR-2026-10-19-000015","url":"https://github.com/JD-Jones-ASES/ob-lean/tree/7826a8c0249678cfcb4c606e88d9fb978b316989","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-19-000015-v1.json","repo":"https://github.com/JD-Jones-ASES/ob-lean","tags":["math.CO","math.NT","msc:11B83","msc:05B10","msc:94A55","barker-sequences","combinatorics","formalization"],"score":0,"title":"Barker sequences of odd length have length 1, 3, 5, 7, 11 or 13","trust":"high","domain":"math.CO","source":"palomar","authors":["JD Jones"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 development of the classification of Barker sequences of odd length. A Barker sequence of length n is a sequence h of n signs whose aperiodic autocorrelations C(k), the sum over j 1 has length 3, 5, 7, 11 or 13 (length 1 is admitted here: it has no nontrivial shift). Theorem 1(iv) of Turyn–Storer, on which their proof relies, is false as stated (Willms 2014, explicit counterexamples); per Schmidt–Willms (footnote 1) parts (ii) and (iii) imply (iv) on a corrected range that suffices for the induction, and independent proofs exist (Borwein–Erdélyi 2013; Schmidt–Willms 2016, the proof…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-19","reactions":{},"formalized":true,"formalizes":[{"title":"Barker sequences of odd length","identifier":"doi:10.1007/s10623-015-0104-4","relationship":"adapts"},{"title":"openai/math (family 179: The circulant Hadamard and Barker-sequence conjectures)","identifier":"https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a","relationship":"adapts"}]}