HEXAGONbeta

Kernel Dimension of the Z/2 Connection Laplacian on a Finite Simple Graph (A Formalisation in Lean 4 / Mathlib v4.11.0)

Primarily AI-generated textHuman understanding: some partsmath.CO — Combinatoricsmath.SP — Spectral Theorycs.LO — Logic in Computer Sciencecs.MS — Mathematical Software

Contributed by Jesus Vilela Jato ↗

Version 1 / Nov 04, 2026 / CC BY 4.0

Abstract

We present a Lean 4/Mathlib v4.11.0 formalization of the kernel-dimension theory of the Z/2\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 when its sign holonomy is trivial along every closed walk. Consequently, the nullity of the signed Laplacian equals the number of balanced connected components, while the nullity of the full connection Laplacian equals the number of connected components plus the number of balanced components. For the flat connection, the nullity is twice the number of connected components. We also formalize exact characteristic polynomials and eigenvalue multisets, including multiplicities, for explicit ordinary and one-wrap signed cycle matrices for n≥3n \geq 3. Transfer to general connection-graph encodings remains conditional on specified matrix-reindexing identities. The contribution is a machine-checked formalization, exposition, and documented verification of results rooted in classical signed-graph spectral theory, rather than a claim of priority for those identities. The accompanying repository preserves proof artifacts, computational cross-checks, historical verification evidence, and documented corrections.

Provenance statement

This work was developed under the conceptual direction of Jesús Vilela Jato, an independent researcher. The author originated the initial research questions and conjectures, directed the formalization and verification process, evaluated mathematical objections and counterexamples, and retained responsibility for the final contribution. AI systems, including OpenAI ChatGPT and Anthropic Claude, were used extensively for mathematical exploration, derivation, LaTeX exposition, Lean 4 formalization, proof construction, numerical testing, adversarial review, and subsequent corrections. The author does not claim to have independently derived or fully understood every formal proof. The formal development is pinned to Lean 4/Mathlib v4.11.0. Verification includes successful Lean compilation, selected standard-axiom audits, independent comparator replays of seven historical theorem targets and five additional cycle-spectrum targets, and numerical cross-checks. These checks have distinct scopes and are documented separately. The submitted manuscript corresponds to release v.0.0.7 of the original repository: https://github.com/jesusvilela/connection_laplacian_lean/releases/tag/v.0.0.7 The historical verification baseline is v.0.0.6. The current manuscript incorporates subsequent editorial corrections and explicit statements of remaining formalization obligations. The contribution concerns the formal verification and exposition of mathematical results grounded in classical signed-graph theory. No priority claim is made for those established identities.

Tools used

Anthropic
Claude Opus
OpenAI
ChatGPT
Lean
Lean

References

  1. F. Harary. On the notion of balance of a signed graph . Michigan Math.\ J.\ 2 (1953/54), 143--146.
  2. T. Zaslavsky. Signed graphs . Discrete Appl.\ Math.\ 4 (1982), 47--74.
  3. T. Zaslavsky. Matrices in the Theory of Signed Simple Graphs . arXiv:1303.3083 (https://arxiv.org/abs/1303.3083), 2013, Section IV.D, Lemma IV.2.arXiv
  4. F. R. K. Chung. Spectral Graph Theory , CBMS Regional Conference Series in Mathematics 92 , American Mathematical Society, Providence, 1997.
  5. Y. Bilu and N. Linial. Lifts, discrepancy and nearly optimal spectral gap . Combinatorica 26 (2006), 495--519. Preprint: Constructing expander graphs by 2-lifts and discrepancy vs.\ spectral gap , arXiv:math/0312022 (https://arxiv.org/abs/math/0312022).arXiv
  6. F. Diaz-Diaz, K. Devriendt and R. Lambiotte. Gremban expansion for signed networks: algebraic and combinatorial foundations for community--faction detection . arXiv:2509.14193 (https://arxiv.org/abs/2509.14193), 2025.arXiv
  7. K. D. Gremban. Combinatorial Preconditioners for Sparse, Symmetric, Diagonally Dominant Linear Systems . PhD thesis, Carnegie Mellon University, 1996. Technical report CMU-CS-96-123.
  8. D. A. Spielman and S.-H. Teng. Nearly-linear time algorithms for preconditioning and solving symmetric, diagonally dominant linear systems . arXiv:cs/0607105 (https://arxiv.org/abs/cs/0607105).arXiv
  9. The Mathlib Community. The Lean Mathematical Library . In: CPP 2020 Proceedings , 367--381, 2020.
  10. L. de Moura and S. Ullrich. The Lean 4 theorem prover and programming language . In: CADE 28 Proceedings , LNCS 12699, 625--635, 2021.

Version history

  1. v1 · 18 pagesSubmitted by Jesus Vilela JatoInitial depositCurrentNov 03, 2026