{"id":"palomar/PALOMAR-2026-10-30-000003","url":"https://github.com/benkeene/sink-reset-thresholds/tree/517b2cd82a8f3ee66476b90ee38a34d6cb9843f6","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-30-000003-v1.json","repo":"https://github.com/benkeene/sink-reset-thresholds","tags":["cs.FL","math.CO","msc:68Q45","msc:68Q70"],"score":0,"title":"Sharp reset thresholds for bounded-response synchronization games with a sink","trust":"high","domain":"cs.FL","source":"palomar","authors":["Ben Keene"],"reviews":0,"subject":"cs.FL","summary":"Lean 4 / Mathlib statements of the theorem M(n,k) = sum_{i=1}^{n-1} ceil(i/k) for k = 1 or n = 2, including the non-divisible pairs (4,2) and (5,3), which the Lipin-Volkov conjecture (stated for k | n-1 only) does not cover; (5,2) is the first pair that is neither endpoint.","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-10-30","reactions":{},"formalized":true}