{"id":"palomar/PALOMAR-2026-09-02-000008","url":"https://github.com/lennrt/palomar-formalizations/tree/a7cc03716e7683cfc0c66cfc0d3b30e00a7a2923/zenodo-21892995/palomar","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-02-000008-v1.json","repo":"https://github.com/lennrt/palomar-formalizations","tags":["math.CO","math.SP","msc:05C22","msc:05C50","msc:68R10","msc:15A18","spectral-graph-theory","circulant-graphs","lean","signed-graphs"],"score":0,"title":"An explicit periodic signing of C_n(1,2) below the conjectured minimum","trust":"high","domain":"math.CO","source":"palomar","authors":["Lennart Rudolph"],"reviews":0,"subject":"math.CO","summary":"The paper's disproof of Suvagiya's signed-circulant minimum conjecture on an infinite arithmetic progression, formalized at the matrix level. For every n divisible by 8, Lean defines the paper's period-8 triangle-flux signing of the circulant graph C_n(1,2) as an explicit signed adjacency matrix, proves it is a plus-minus-one signing of mathlib's circulant graph, and proves by exact rational sum-of-squares window certificates that every eigenvalue has absolute value at most 1397/500. For every n >= 32 this rational separator lies strictly below the conjectured minimum rho_-(n) =…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-02","reactions":{},"formalized":true,"formalizes":[{"title":"Periodic Signings of C_n(1,2): An Exact Band Edge and Short-Period Classification","identifier":"10.5281/zenodo.21892995","relationship":"formalizes"}]}