Barker sequences of odd length have length 1, 3, 5, 7, 11 or 13
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-19-000015
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-19-000015/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-19-000015/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'