{"id":"hexagon/2611.00061","pdf":"https://hexagonmath.org/pdf/2611.00061v1","url":"https://hexagonmath.org/abs/2611.00061v1","tags":["math.SP","cs.LO","cs.MS","msc:05C50","msc:05C22","msc:68V20","msc:68V15","AI-assisted mathematics","Lean 4","connection Laplacian"],"score":0,"title":"Kernel Dimension of the Z/2 Connection Laplacian on a Finite Simple Graph (A Formalisation in Lean 4 / Mathlib v4.11.0)","domain":"math.CO","origin":"ai-generated","source":"hexagon","authors":["Jesus Vilela Jato"],"reviews":0,"subject":"math.CO","summary":"We present a Lean 4/Mathlib v4.11.0 formalization of the kernel-dimension theory of the $\\mathbb{Z}/2$ connection Laplacian on finite simple graphs equipped with designated wrap edges. Each edge carries either the identity or the coordinate-swap matrix. A Hadamard–Kronecker change of basis decomposes the resulting rank-two connection Laplacian into the ordinary and signed graph Laplacians. An analogous splitting holds for the scalar Laplacian of the associated two-sheeted cover. A connected component is balanced precisely when its covering preimage has two connected components, equivalently…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"ai_models":["Claude Opus","ChatGPT"],"discussed":0,"published":"2026-11-04","reactions":{},"withdrawn":false,"authorship":"no-human-author-claimed","formalized":false,"human_understanding":"some"}