{"id":"palomar/PALOMAR-2026-09-30-000002","url":"https://github.com/JD-Jones-ASES/l2-lean/tree/c4cbeafac7e44ebcbbee9a8839f70278bb19b6ab","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-30-000002-v1.json","repo":"https://github.com/JD-Jones-ASES/l2-lean","tags":["math.CO","msc:05A05","msc:11B83","lean","combinatorics","langford-sequences","design-theory"],"score":0,"title":"Two-fold Langford sequences exist exactly when 3l ≥ 2d − 1; the m-fold counting bound and its attainment, and a residue bound","trust":"high","domain":"math.CO","source":"palomar","authors":["JD Jones"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 characterization of two-fold Langford sequences. An m-fold Langford sequence of order l and defect d fills the positions 1, ..., 2ml so that every p in [d, d + l - 1] occupies the endpoints of m pairwise disjoint pairs of positions at distance p. For d, l >= 1 a two-fold sequence exists exactly when 3l >= 2d - 1. For every m, (2m - 1)l >= 2d - 1 is necessary, with l(2d + l + 1) = 0 (mod 4) for odd m, and the bound is attained whenever 2d + l = 2ml + 1; the row of order one exists exactly when d divides m; no three-fold sequence of order 3 and defect 6 exists; and for every m >= 3…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-30","reactions":{},"formalized":true,"formalizes":[{"title":"Graceful labellings of variable windmills using Skolem sequences","identifier":"arXiv:2112.04265","relationship":"adapts"}]}