\documentclass[11pt,a4paper]{amsart}

\usepackage[margin=1.1in]{geometry}
\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage{mathrsfs}
\usepackage{stmaryrd}
\usepackage{enumitem}
\usepackage{booktabs}
\usepackage{longtable} % page-breaking formalisation index
\usepackage{etoolbox}
% TeX Live 2025 compatibility for the longtable output routine.
% In its two page-output branches, longtable inserts \vss (infinite shrink).
% The LaTeX mark-extraction \vsplit can then emit the otherwise harmless
% "ignored error: Infinite glue shrinkage found in box being split" message.
% Hexagon's strict preview reports that log message as a compilation error.
% Replace both \vss tokens with finite shrink, following the LaTeX project's
% upstream analysis: https://github.com/latex3/latex2e/issues/1907
% On newer longtable versions without these \vss tokens, this is a no-op.
\makeatletter
\patchcmd{\LT@output}{\vss}%
  {\vskip 0pt plus \maxdimen minus \normalbaselineskip}{}{}
\patchcmd{\LT@output}{\vss}%
  {\vskip 0pt plus \maxdimen minus \normalbaselineskip}{}{}
\makeatother
\usepackage{xcolor}
\usepackage[colorlinks=true,linkcolor=black!70!blue,citecolor=black!70!blue,urlcolor=black!70!blue]{hyperref}
\usepackage{xurl}
\usepackage{microtype}

\theoremstyle{plain}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}

\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{notation}[theorem]{Notation}
\newtheorem{example}[theorem]{Example}

\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}

\DeclareMathOperator{\Adj}{Adj}
\DeclareMathOperator{\Ker}{ker}
\DeclareMathOperator{\Img}{im}
\DeclareMathOperator{\diag}{diag}
\DeclareMathOperator{\rank}{rank}
\DeclareMathOperator{\tr}{tr}
\DeclareMathOperator{\id}{id}
\DeclareMathOperator{\End}{End}
\DeclareMathOperator{\Aut}{Aut}
\DeclareMathOperator{\sgn}{sgn}
\newcommand{\RR}{\mathbb{R}}
\newcommand{\ZZ}{\mathbb{Z}}
\newcommand{\NN}{\mathbb{N}}
\newcommand{\FF}{\mathbb{F}}
\newcommand{\II}{\mathbb{I}}
\newcommand{\CC}{\mathbb{C}}
\newcommand{\HH}{\mathbb{H}}
\newcommand{\cC}{\mathcal{C}}
\newcommand{\cE}{\mathcal{E}}
\newcommand{\cF}{\mathcal{F}}
\newcommand{\cV}{\mathcal{V}}
\newcommand{\cL}{\mathcal{L}}
\newcommand{\cG}{\mathcal{G}}
\newcommand{\cN}{\mathcal{N}}
\newcommand{\kronprod}{\otimes_{\!K}}
\newcommand{\sheet}{\text{\rm sh}}
\newcommand{\wrap}{\operatorname{wrap}}
\newcommand{\tG}{\widetilde{G}}
\newcommand{\tV}{\widetilde{V}}
\newcommand{\tL}{\widetilde{L}}
\newcommand{\Lscalar}{L^{\operatorname{sc}}}
\newcommand{\Lsigned}{L^{\operatorname{sg}}}
\newcommand{\comp}{\pi_0}
\newcommand{\pair}[2]{\langle #1, #2 \rangle}
\newcommand{\defeq}{\mathrel{\mathop:}=}

\begin{document}

\title[Kernel Dimension of the $\ZZ/2$ Connection Laplacian]{%
Kernel Dimension of the $\ZZ/2$ Connection Laplacian \\
on a Finite Simple Graph \\
{\small (A Formalisation in Lean~4 / Mathlib v4.11.0)}}

\author{Jes\'us Vilela Jato}
\thanks{Independent Researcher. Correspondence: \texttt{jesusvilela@outlook.com}.}
\date{3 November 2026}

\subjclass[2020]{05C50, 05C22, 68V20, 68V15}
\keywords{signed graph, connection Laplacian, double cover, balanced
  component, formal proof, Lean, Mathlib}

\begin{abstract}
We present a fully formalised, machine-checked proof library in
Lean~4 / Mathlib~v4.11.0 for the kernel-dimension theory of the
$\ZZ/2$ \emph{connection Laplacian} of a finite simple graph~$G$.
A connection graph is a finite simple graph equipped with a
designated set $W\subseteq E(G)$ of \emph{wrap edges}; on each
edge~$e$ we attach a $2\times 2$ real matrix (the Pauli~$\sigma_x$
on wrap edges, $\II_2$ otherwise), yielding a block Laplacian
$L_{\operatorname{Mob}}$.
Our principal results, each proved from the three standard Lean
axioms (\texttt{propext}, \texttt{Classical.choice},
\texttt{Quot.sound}) and nothing else, are the following.

\begin{enumerate}[label=\textbf{(\roman*)}]
  \item A Hadamard--Kronecker conjugation decomposes
    $L_{\operatorname{Mob}}$ into the block-diagonal sum of the
    ordinary (\emph{scalar}) Laplacian and a \emph{signed} Laplacian,
    both on~$G$.
  \item The orientation double cover $\tG$ of~$G$ inherits a trivial
    connection, and its scalar Laplacian splits similarly.
  \item A base connected component $C\in \comp(G)$ is
    \emph{balanced} iff the induced map $\comp(\tG)\to \comp(G)$ has
    fibre of cardinality~$2$ over~$C$.
  \item The kernel dimension of the signed Laplacian equals the number
    of balanced components; the full $\ZZ/2$-connection Laplacian has
    kernel dimension $\# \comp(G) + \#\{\text{balanced components}\}$
    (Möbius) and $2\,\#\comp(G)$ (flat).
  \item On the $n$-cycle ($n\ge 3$) the scalar and the one-wrap signed
    Laplacians have explicit cosine spectra: their characteristic
    polynomials and eigenvalue multisets, with multiplicities, are
    proved for the explicit cycle matrices.
\end{enumerate}

The bespoke arguments are the Hadamard rotation of part~(i)--(ii)
(a Kronecker-conjugation computation) and the double-cover lift
of part~(iii) (a walk induction). Along the way we observe and
correct an incorrect statement in our initial written plan: the identity
$\dim\Ker L^{\operatorname{sg}}(G) = \#\comp(G) -
  \#\{\text{components of odd total wrap}\}$
holds for every wrap assignment on a cycle, but fails for some wrap assignments
on general graphs; the universally valid replacement is the
cohomological formula $\dim\Ker L^{\operatorname{sg}}(G) =
\#\{\text{balanced components}\}$, which is the content of
Theorem~\ref{thm:signed-kernel}. The Lean sources and a numerical
cross-check on every simple graph of order~$\le 5$
($3{,}456$ configurations, zero disagreements)~--~and an extended
fuzzer sweep at orders $n\le 7$ ($456{,}950$ configurations, also zero
disagreements) accompany this paper.
\end{abstract}

\maketitle

\tableofcontents

%=============================================================
\section{Introduction}
%=============================================================

Let $G=(V,E)$ be a finite simple graph and let $W\subseteq E$ be
a distinguished set of \emph{wrap} edges. Attach to each
$e\in E$ a $2\times 2$ real matrix $\Phi(e)$ by
\[
  \Phi(e) \defeq \begin{cases} \sigma_x & \text{if } e\in W,\\
    \II_2 & \text{if } e\notin W, \end{cases}
\qquad
  \sigma_x = \begin{pmatrix}0&1\\1&0\end{pmatrix}.
\]
The \emph{$\ZZ/2$-connection Laplacian} of $(G,W)$ is the
$V\times V$ block matrix with $2\times 2$ blocks
\begin{equation}\label{eq:connection-laplacian}
  L_{\operatorname{Mob}}[u,v] \defeq
    \begin{cases}
      \deg(u)\,\II_2 & u=v,\\
      -\,\Phi(\{u,v\}) & \{u,v\}\in E,\\
      0 & \text{otherwise.}
    \end{cases}
\end{equation}
Equivalently, $L_{\operatorname{Mob}} = D\otimes \II_2 -
\sum_{e\in E} \mathbf{1}_e\otimes \Phi(e)$, where, for $e=\{u,v\}$,
$\mathbf{1}_e$ is the symmetric $V\times V$ edge-indicator with entries
$1$ at $(u,v)$ and at $(v,u)$ and $0$ elsewhere (both Kronecker factors ordered
vertex-major, matching the $V\times \operatorname{Fin}\,2$ index set of
Equation~(1)).
The \emph{flat} Laplacian $L_{\operatorname{flat}}$ is obtained by
the same recipe with $\Phi\equiv \II_2$, i.e. by ignoring the wrap
structure; it agrees with two copies of the ordinary graph Laplacian.
The guiding question answered in this paper is:

\begin{center}
  \emph{In terms of $(G,W)$, what is $\dim\Ker L_{\operatorname{Mob}}$
  and when is it strictly smaller than $\dim\Ker L_{\operatorname{flat}}$?}
\end{center}

This is the finite-dimensional, discrete analogue of the spectrum of
the Laplacian on a rank-two flat vector bundle over a graph: the
kernel detects global \emph{parallel} sections, not arbitrary sections.
The representation splits as a trivial line, spanned by $(1,1)^\top$,
and a signed line, spanned fibrewise by $(1,-1)^\top$. Thus the
rank-two bundle always admits the nowhere-zero parallel section
$s(v)=(1,1)^\top$, regardless of the wrap data. The signed line admits
a nonzero parallel section over a component exactly when the wrap
holonomy around every cycle in that component is trivial. Equivalently,
the rank-two bundle has two independent parallel sections there rather
than just one; this is the condition of
\emph{balance} in the language of Harary, Cartwright and Zaslavsky
\cite{HararyCartwright, Zaslavsky82}.

\subsection*{Contribution and prior work}

The contribution is a Lean formalisation and a documented verification
process for classical spectral graph theory~\cite{Chung}. We do not claim new
mathematical discovery of the balance--nullity or lift-splitting formulas.
For the signed Laplacian $D-A_{\mathrm{sg}}$, the standard nullity
formula is stated explicitly in Zaslavsky's survey
\cite[Lemma~IV.2]{ZaslavskyMatrices}.
Bilu and Linial's $2$-lift result gives the adjacency spectrum as the
base and signed spectra with multiplicities
\cite[preprint Lemma~3.1]{BiluLinial}. Our Laplacian splitting uses
the same sheet-symmetric and sheet-antisymmetric subspaces: the
degree block acts as $D$ in both. This also works for irregular
finite simple graphs; it does not require replacing $D$ by a scalar.
The orientation double cover of Definition~\ref{def:cover} is the
\emph{Gremban expansion} of the signed graph whose negative edges
are~$W$; Diaz-Diaz, Devriendt and Lambiotte prove that its Laplacian is
similar to the direct sum of the unsigned and signed Laplacians
\cite[Def.~2.1, Cor.~3.8]{DiazDevriendtLambiotte}, which is the content
of Theorem~\ref{thm:cover-splits}. The doubling goes back to Gremban's
reduction of symmetric diagonally dominant systems to systems of twice
the dimension with non-positive off-diagonal entries~\cite{Gremban},
recalled in \cite[\S2.2]{SpielmanTeng}.
On the formal side, Mathlib's \texttt{SimpleGraph} library at the pinned
revision provides the scalar Laplacian \texttt{lapMatrix}, its positive
semidefiniteness, and the identification of its kernel dimension with
the number of connected components~\cite{Mathlib}. It has no signed or
connection Laplacian and no orientation double cover; those, and the
results above, are developed here in Lean~4~\cite{Lean4}.
The repository certifies the resulting identities and records the
remaining specification and formalisation obligations.
The numerical work is a cross-check, not an ML application or a
scalability benchmark.

\subsection*{Organisation and results}

Section~\ref{sec:prelim} sets the notation and fixes the
Lean-formalised data. Section~\ref{sec:decomp} proves the
Hadamard--Kronecker decomposition that reduces the block
Laplacian to two ordinary Laplacians (one scalar, one signed).
Section~\ref{sec:cover} constructs the orientation double cover
and proves that its scalar Laplacian splits as the direct sum of
the scalar and signed Laplacians of~$G$. Section~\ref{sec:coho}
formalises the balance notion as the vanishing of a
$\ZZ/2$-cohomology class and
computes the fibre cardinality of the induced map on
$\pi_0$. Section~\ref{sec:recognition} assembles everything into
the \emph{recognition theorems} which count kernel dimension by
balanced components. Section~\ref{sec:cycles} specialises to the
$n$-cycle, where the Fourier basis diagonalises both
Laplacians. Section~\ref{sec:formalisation} summarises the
formal Lean development.

The main structural decomposition, cover-splitting, cohomological
recognition, kernel-dimension, and auxiliary identities are
machine-checked in Lean~4 against Mathlib~v4.11.0. The \emph{complete}
flat and one-wrap signed cycle characteristic polynomials and real
root multisets, including algebraic multiplicities for every $n\ge3$,
are also machine-checked in \texttt{CycleMultiset.lean}; see
Remark~\ref{rem:cycle-spectrum-lean}. The claims concern the explicit
cycle matrices used in the Lean project. A further graph-level
identification with arbitrary \texttt{ConnGraph} cycle instances
is not asserted. The complete proof scripts and independent numerical
checks are included in the accompanying repository.

%=============================================================
\section{Preliminaries}\label{sec:prelim}
%=============================================================

\subsection{Connection graphs}

A \emph{connection graph} is a quadruple $G=(V,E,\Adj,W)$ where
$V$ is a finite type, $\Adj\subseteq V\times V$ defines a
(mathematically simple) graph on~$V$, $E=\{\{u,v\}:\Adj(u,v)\}$
is its edge set and $W\subseteq E$ is an arbitrary subset, the
\emph{wrap} edges. In Lean we keep the wrap data as a predicate
\texttt{wrap : G.graph.edgeSet $\to$ Prop} and carry explicit
\texttt{Fintype}/\texttt{DecidableEq}/\texttt{DecidableRel}
instances throughout.

\subsection{Pauli and Hadamard}

The $2\times 2$ Pauli matrix $\sigma_x=\begin{pmatrix}0&1\\1&0\end{pmatrix}$
is involutive, symmetric and has eigenvalues~$\pm 1$, with
symmetric eigenvector $(1,1)^\top$ and antisymmetric
$(1,-1)^\top$. The \emph{Hadamard rotation}
\begin{equation}\label{eq:Rhat}
  \widehat R \defeq \begin{pmatrix} 1 & 1 \\ 1 & -1 \end{pmatrix},
  \qquad \widehat R\,\widehat R = 2\,\II_2,
\end{equation}
simultaneously diagonalises $\sigma_x$ and $\II_2$ in the sense
that $\widehat R\,\sigma_x\,\widehat R = 2\,\diag(1,-1)$ and
$\widehat R\,\II_2\,\widehat R = 2\,\II_2$. In the Lean
formalisation we keep two copies of~$\widehat R$: one indexed by
$\{0,1\}=\operatorname{Fin}2$ (for the connection-block
decomposition of Section~\ref{sec:decomp}) and one indexed by
$\operatorname{Bool}$ (for the cover-sheet decomposition of
Section~\ref{sec:cover}). They are the same matrix under the
obvious bijection $\operatorname{Bool}\cong \operatorname{Fin}2$.

\subsection{Scalar and signed Laplacians}

Let $G$ be a connection graph. The ordinary \emph{scalar}
Laplacian $\Lscalar \in \RR^{V\times V}$ is
\[
  \Lscalar[u,v] \defeq
    \begin{cases} \deg(u) & u=v,\\
      -1 & \{u,v\}\in E,\\ 0 & \text{otherwise,}\end{cases}
\]
i.e.\ Mathlib's
\texttt{SimpleGraph.lapMatrix}.
The \emph{signed Möbius} Laplacian $\Lsigned \in \RR^{V\times V}$
encodes the wrap sign on the off-diagonal:
\[
  \Lsigned[u,v] \defeq
    \begin{cases} \deg(u) & u=v,\\
      +1 & \{u,v\}\in E,\ \{u,v\}\in W,\\
      -1 & \{u,v\}\in E,\ \{u,v\}\notin W,\\
      0 & \text{otherwise.}\end{cases}
\]
Both are real symmetric and positive semidefinite as quadratic forms
on $\RR^V$. For $\Lscalar$ this is Mathlib's
\path{SimpleGraph.posSemidef_lapMatrix}. For $\Lsigned$ we use the
direct sum-of-squares expression
\[
  \pair{x}{\Lsigned x}
  = \!\!\sum_{\{u,v\}\in E\setminus W}\! (x_u - x_v)^2
  + \sum_{\{u,v\}\in W} (x_u + x_v)^2,
\]
which Lemma~\ref{lem:signed-psd} (\S\ref{sec:bounds}) turns into the
Lean fact \path{signedLaplacianMobius_posSemidef}
(\texttt{L13\_PSD.lean}). Equivalently --- but through a heavier route
not used by the Lean proof --- PSD follows from the cover splitting
(Theorem~\ref{thm:cover-splits}): the orientation double cover's
scalar Laplacian is PSD, and similarity to
$\operatorname{diag}(\Lscalar,\Lsigned)$ preserves the PSD property of
each diagonal block.
The Fourier diagonalisation in \S\ref{sec:cycles} below regards both
matrices as acting on $\CC^V$, but the matrices themselves remain
real; complexification is a computational convenience, not a domain
change.

%=============================================================
\section{The Block Decomposition}\label{sec:decomp}
%=============================================================

The connection Laplacian
$L_{\operatorname{Mob}}$ of~\eqref{eq:connection-laplacian}
lives on the product index set $V\times \operatorname{Fin}2$.
Reindexing via the canonical bijection
\[
  \varphi : V\times \operatorname{Fin}2 \;\xrightarrow{\;\sim\;}\; V\sqcup V,
  \qquad (u,0)\mapsto \iota_\ell u,\ (u,1)\mapsto \iota_r u,
\]
we get a matrix on the sum index $V\sqcup V$; the block-diagonal
decomposition then becomes a genuine \emph{block-diagonal} form
\texttt{Matrix.fromBlocks}.

\begin{theorem}\label{thm:decomp}
Let $G$ be a connection graph and $\epsilon \in\{\text{flat},\text{Mob}\}$.
There exists an invertible $P\in\RR^{(V\times\operatorname{Fin}2)
  \times (V\times\operatorname{Fin}2)}$ such that
\[
  \varphi_* \bigl( P\, L_\epsilon\, P^{-1} \bigr)
    = \begin{pmatrix}\Lscalar & 0 \\ 0 & B_\epsilon \end{pmatrix},
    \qquad
  B_\epsilon = \begin{cases}
    \Lsigned & \epsilon=\text{Mob},\\
    \Lscalar & \epsilon=\text{flat.}
  \end{cases}
\]
\end{theorem}

\begin{proof}
Set $P = \II_V \kronprod \widehat R$ (Kronecker product with the
Hadamard~$\widehat R$ of~\eqref{eq:Rhat} acting on the
$\operatorname{Fin}2$ fibre). By functoriality of the Kronecker
product,
\[
  P\cdot P
  = (\II_V\cdot \II_V) \kronprod (\widehat R\,\widehat R)
  = \II_V \kronprod (2\II_2)
  = 2\,\II_{V\times \operatorname{Fin}2},
\]
so $P^{-1} = \tfrac{1}{2}P$, and in particular $\det P\ne 0$.

A direct entrywise calculation using
$\widehat R\,\sigma_x\,\widehat R = 2\diag(1,-1)$
and $\widehat R\,\II_2\,\widehat R = 2\,\II_2$ yields, for
$u,v\in V$ and $i,j\in\operatorname{Fin}2$,
\[
  \tfrac{1}{2}\,\bigl(P\, L_\epsilon\, P\bigr)\bigl[(u,i),(v,j)\bigr]
    = \begin{cases}
      \Lscalar[u,v] & i=j=0,\\
      B_\epsilon[u,v] & i=j=1,\\
      0 & i\ne j.
    \end{cases}
\]
Reindexing via $\varphi$ and using
$P^{-1}=\tfrac{1}{2}P$ turns the left-hand side into
$\varphi_*\bigl(P\,L_\epsilon\,P^{-1}\bigr)$, giving the claim.
The flat case is the special case $W=\emptyset$ of the Möbius
case, or equivalently the fact that $\widehat R\,\II_2\,\widehat R=
2\II_2$ collapses both diagonal blocks to the scalar Laplacian.
\end{proof}

\begin{remark}
In the Lean formalisation \texttt{laplacian\_decomposes} the two
$\epsilon$-branches are proved separately: the Möbius branch uses
$P=\II_V\kronprod \widehat R$ as above, while the flat branch takes
the simpler $P=\II_{V\times\operatorname{Fin}2}$ (identity
similarity) and reduces the claim to
$L_{\mathrm{flat}}=\diag(\Lscalar,\Lscalar)$ after reindex via
$\varphi$. Mathematically the flat case is the specialisation of the
Möbius case at $W=\emptyset$, but the two Lean branches are
syntactically disjoint.
\end{remark}

\begin{remark}
In the Lean script the bijection $\varphi$ is
\texttt{prodFinTwoEquivSum} and the Kronecker-product
identity is the lemma \texttt{mul\_kronecker\_mul} from
\path{Mathlib.Data.Matrix.Kronecker}. The entrywise
calculation is made into a single-sum \texttt{Finset.sum\_eq\_single}
reduction that kills $V$-off-diagonal terms using the
$\II_V$ factor of~$P$, and then reduces the remaining
$\operatorname{Fin}2\times \operatorname{Fin}2$ block to one of
three cases by matching on equality of vertices and wrap status.
\end{remark}

%=============================================================
\section{The Orientation Double Cover}\label{sec:cover}
%=============================================================

The preceding decomposition separates the flat part of~$G$ from
its wrap data inside a single graph. The cover perspective lifts
the wrap data into a \emph{branching} structure on a new,
connection-free graph.

\begin{definition}\label{def:cover}
The \emph{orientation double cover} of the connection graph
$(G,W)$ is the simple graph $\tG$ on vertex set
$\tV \defeq V\times \operatorname{Bool}$, with adjacency
\[
  (u,b)\sim_{\tG} (v,c) \iff
    \{u,v\}\in E \;\text{and}\; \bigl(\{u,v\}\in W \Leftrightarrow b\ne c\bigr).
\]
We view $\tG$ as a connection graph with $\widetilde W=\emptyset$:
every edge of $\tG$ is ``interior'', the cover has \emph{trivial}
connection.
\end{definition}

Equivalently, $\tG$ is the $\ZZ/2$-covering space determined by
the $1$-cochain $\sigma_W:E\to \ZZ/2,\ e\mapsto \mathbf{1}_{e\in W}$
(which is automatically a $1$-cocycle since the graph has no
$2$-cells; see~\S\ref{sec:coho}).
The non-trivial \emph{deck transformation}
$\delta:\tV\to\tV,\ (v,b)\mapsto (v,\neg b)$ is a free graph
involution.

\begin{lemma}\label{lem:deck}
  $\delta$ is a graph automorphism of~$\tG$ of order~$2$ with
  no fixed points.
\end{lemma}

\begin{proof}
Involutivity is immediate from $\neg\neg b = b$. The
adjacency $(\delta x)\sim_{\tG}(\delta y)\Leftrightarrow x\sim_{\tG}y$
follows from the identity
$(\neg b)\ne (\neg c) \Leftrightarrow b\ne c$ and fixity of the
underlying edge $\{u,v\}$. Absence of fixed points is trivial:
$(v,b)\ne (v,\neg b)$.
\end{proof}

\begin{lemma}\label{lem:cover-degree}
  For every $(u,b)\in \tV$, $\deg_{\tG}(u,b) = \deg_G(u)$.
\end{lemma}

\begin{proof}
We construct a bijection $\cN_G(u)\to \cN_{\tG}(u,b)$ by
\[
  v \;\longmapsto\; \bigl(v,\ b\oplus \mathbf{1}_{\{u,v\}\in W}\bigr),
\]
where $\oplus$ is the $\operatorname{Bool}$ XOR. Correctness is the
definition of~$\sim_{\tG}$; injectivity follows by reading the
first coordinate; surjectivity uses the biconditional
$\{u,v\}\in W \Leftrightarrow b\ne c$ to recover the unique~$v$
with $(u,b)\sim_{\tG}(v,c)$.
\end{proof}

We write $\tL\defeq \Lscalar(\tG)$ for the scalar Laplacian of
the cover.

\subsection*{The Hadamard rotation on the $\operatorname{Bool}$-fibre}

Replace the $\operatorname{Fin}2$-fibre of Section~\ref{sec:decomp}
by the $\operatorname{Bool}$-fibre, viewing
\[
  \widehat R : \RR^{\operatorname{Bool}\times \operatorname{Bool}},
  \qquad \widehat R[i,j] = \begin{cases}
    -1 & i=j=\top,\\
    \phantom{-}1 & \text{otherwise},
  \end{cases}
\]
so $\widehat R\,\widehat R = 2\,\II$ on
$\RR^{\operatorname{Bool}\times \operatorname{Bool}}$. Set
\[
  P_{\mathrm{cov}} \defeq \II_V\kronprod \widehat R \quad \in \RR^{\tV\times \tV}.
\]

\begin{theorem}\label{thm:cover-splits}
Under the canonical bijection
$\varphi:\tV\xrightarrow{\sim} V\sqcup V$,
$(v,\bot)\mapsto \iota_\ell v,\ (v,\top)\mapsto \iota_r v$,
we have
\[
  \varphi_*\bigl(P_{\mathrm{cov}}\,\tL\,P_{\mathrm{cov}}^{-1}\bigr)
  = \begin{pmatrix} \Lscalar(G) & 0 \\ 0 & \Lsigned(G)\end{pmatrix}.
\]
In particular, $P_{\mathrm{cov}}$ is invertible and
$\tL\sim \Lscalar(G)\oplus\Lsigned(G)$.
\end{theorem}

\begin{proof}
Write every $2\times 2$ block
\[
  B_{u,v} \defeq \widehat R\,\tL[u,v]\,\widehat R \in
  \RR^{\operatorname{Bool}\times\operatorname{Bool}}
\]
where $\tL[u,v]$ is the $\{u\}\times\operatorname{Bool}$-rows,
$\{v\}\times \operatorname{Bool}$-columns sub-block of $\tL$. A
direct Kronecker calculation gives
\begin{equation}\label{eq:Pcov-identity}
  \bigl(P_{\mathrm{cov}}\,\tL\,P_{\mathrm{cov}}\bigr)\bigl[(u,i),(v,j)\bigr]
    = (\widehat R\,\tL[u,v]\,\widehat R)[i,j]
    = B_{u,v}[i,j].
\end{equation}

Split $B_{u,v}$ into four structural cases:
\begin{enumerate}[label=\textbf{(\alph*)}]
  \item \textit{Diagonal.} If $u=v$, then
  by Lemma~\ref{lem:cover-degree}, $\tL[u,u] = \deg(u)\,\II$,
  whence $\widehat R(\deg(u)\,\II)\widehat R =
  \deg(u)\cdot 2\II$, so $B_{u,u}[i,j] = 2\deg(u)\cdot \delta_{ij}$.
  \item \textit{Adjacent, non-wrap.} If $\{u,v\}\in E\setminus W$,
  then $\tL[u,v]$ has $-1$ on the \emph{diagonal} of
  $\operatorname{Bool}$ (sheets match) and $0$ off-diagonal:
  $\tL[u,v] = (-1)\II$. So
  $B_{u,v}[i,j] = -2\delta_{ij}$.
  \item \textit{Adjacent, wrap.} If $\{u,v\}\in E\cap W$, then
  $\tL[u,v]$ has $-1$ off the diagonal (sheets flip) and $0$ on
  the diagonal: $\tL[u,v] = -\sigma_x$. So
  $\widehat R(-\sigma_x)\widehat R = -2\diag(1,-1)$, i.e.\
  $B_{u,v}[i,j] = -2\delta_{ij}\,(-1)^{\mathbf{1}_{i=\top}}$.
  \item \textit{Non-adjacent.} If $\{u,v\}\notin E$, then
  $\tL[u,v]=0$ and $B_{u,v}=0$.
\end{enumerate}

Collecting cases and matching against the defining formulas of
$\Lscalar$ and $\Lsigned$:
\[
  B_{u,v}[i,j] = 2\cdot \delta_{ij}\cdot
  \begin{cases} \Lscalar[u,v] & i=\bot,\\
    \Lsigned[u,v] & i=\top. \end{cases}
\]
Because $P_{\mathrm{cov}}^{-1} = \tfrac{1}{2}P_{\mathrm{cov}}$
(by $P_{\mathrm{cov}}^2 = 2\II$, exactly as in Section~\ref{sec:decomp}),
reindexing through~$\varphi$ gives the claimed block-diagonal
form.
\end{proof}

\begin{corollary}\label{cor:cover-kernel}
$\dim_\RR \Ker\tL = \dim_\RR\Ker \Lscalar(G) +
    \dim_\RR\Ker \Lsigned(G)$.
\end{corollary}

\begin{proof}
Kernel dimension is invariant under similarity by an invertible
matrix and under reindexing by a bijection of the index set; for
a block-diagonal matrix it is additive in the blocks. Apply these
three standard linear-algebra facts to the similarity of
Theorem~\ref{thm:cover-splits}.
\end{proof}

\begin{remark}
In the Lean code these three standard facts are the lemmas
\begin{center}
  \texttt{finrank\_ker\_toLin'\_conj},\quad
  \texttt{finrank\_ker\_toLin'\_reindex},\quad
  \texttt{finrank\_ker\_toLin'\_fromBlocks\_diag}.
\end{center}
They are proved once, over an arbitrary field, in
\texttt{KernelDimension.lean} and reused for both the
block-decomposition Theorem~\ref{thm:decomp} and the
cover-splitting Corollary~\ref{cor:cover-kernel}.
\end{remark}

%=============================================================
\section{$\ZZ/2$ Cohomology and Balanced Components}\label{sec:coho}
%=============================================================

The wrap predicate $W\subseteq E$ reifies canonically as a
$\ZZ/2$-valued $1$-cochain
\[
  \sigma_W : E \;\longrightarrow\; \ZZ/2,\qquad
  \sigma_W(e) \defeq \mathbf{1}_{e\in W}.
\]
It is automatically a $1$-cocycle (there is no $2$-skeleton to
impose constraints on it). Its cohomology class
$[\sigma_W]\in H^1(G;\ZZ/2)$ is the obstruction to
$W$ arising as the coboundary of a vertex $\ZZ/2$-colouring:
$[\sigma_W]=0$ iff there exists $\varepsilon:V\to\operatorname{Bool}$
with $W = \{\,\{u,v\}\in E : \varepsilon(u)\ne \varepsilon(v)\,\}$.
This is the classical notion of \emph{balance} for signed graphs.

\begin{definition}\label{def:balanced}
A connected component $C\in\comp(G)$ is \emph{balanced} iff there
is a map $\varepsilon:V\to\operatorname{Bool}$ such that for every
edge $\{u,v\}\in E$ with $[u]_{\sim_G} = C$,
\[
  \{u,v\}\in W \iff \varepsilon(u)\ne \varepsilon(v).
\]
We write $\comp^{\mathrm{bal}}(G)\subseteq \comp(G)$ for the
subset of balanced components, and
$\beta(G)\defeq \#\comp^{\mathrm{bal}}(G)$.
\end{definition}

\begin{remark}[Scope conventions for Definition~\ref{def:balanced}]
\label{rem:balance-scope}
Two conventions deserve to be flagged.
\begin{enumerate}[label=(\alph*)]
  \item \textbf{Component-local vs.\ graph-global.} The definition
    quantifies only over edges \emph{inside} the component~$C$; the
    values $\varepsilon(w)$ for $w$ outside~$C$ are unconstrained and
    play no role. For a \emph{connected} graph the present definition
    coincides with Harary's original graph-global notion of balance
    ($[\sigma_W]=0$ in $H^1(G;\ZZ/2)$); for disconnected graphs they
    differ, and \emph{every theorem below uses the component-local
    version.} Throughout the paper $\beta(G)$ denotes the
    component-local count.
  \item \textbf{Isolated vertices are vacuously balanced.} If
    $C=\{v_0\}$ is a singleton, the edge quantifier is vacuous and
    the condition holds with any~$\varepsilon$. Consequently every
    isolated vertex counts towards $\beta(G)$; this is load-bearing
    for Theorem~\ref{thm:signed-kernel} below, because an isolated
    vertex contributes a zero row to~$\Lsigned$ and hence~$+1$ to the
    kernel dimension.
\end{enumerate}
\end{remark}

The main combinatorial result of this section relates balance to
the fibres of the induced map on connected components.

\begin{theorem}\label{thm:fiber-card}
Let $\pi:\comp(\tG)\to\comp(G)$ be the map induced by the sheet
projection $\tG\to G,\ (v,b)\mapsto v$. For every
$C\in\comp(G)$,
\[
  \#\pi^{-1}(C) \;=\; \begin{cases} 2 & C \text{ balanced,}\\
    1 & \text{otherwise.} \end{cases}
\]
\end{theorem}

The proof occupies the remainder of this section. Fix
$C\in\comp(G)$ and choose a representative $v_0\in V$ with
$[v_0]_{\sim_G}=C$. Set the \emph{candidate lifts}
\[
  D_\bot \defeq [(v_0,\bot)]_{\comp(\tG)}, \qquad
  D_\top \defeq [(v_0,\top)]_{\comp(\tG)}.
\]

\paragraph{Step 1: every component in the fibre is a candidate lift.}

\begin{lemma}\label{lem:fiber-subset}
For every $D\in\pi^{-1}(C)$, either $D=D_\bot$ or $D=D_\top$.
\end{lemma}

\begin{proof}
Since $\pi([(w,b)]) = [w]_{\comp(G)}$ factors through the first
coordinate, $D=[(w,b)]$ for some $(w,b)\in\tV$ with $[w]=C$. By
connectedness of~$C$ there is a walk $w\to v_0$ in $G$; lifting
edge by edge and setting
\[
  \text{next sheet}\bigl(b,\ \{u,u'\}\bigr)
  \defeq \begin{cases} \neg b & \{u,u'\}\in W,\\
    b & \text{otherwise,} \end{cases}
\]
we obtain a walk $(w,b)\to (v_0,b'')$ in $\tG$ for some
$b''\in\operatorname{Bool}$ determined by the walk. So
$[(w,b)]=[(v_0,b'')]$, and $D\in\{D_\bot,D_\top\}$.
\end{proof}

\paragraph{Step 2: the balanced case.}

\begin{lemma}\label{lem:sep-if-balanced}
If $C$ is balanced, then $D_\bot\ne D_\top$, whence
$\#\pi^{-1}(C)=2$.
\end{lemma}

\begin{proof}
Let $\varepsilon$ witness balance. Define the \emph{XOR}
invariant $\chi:\tV\to \operatorname{Bool}$ by
\[
  \chi(v,b) \defeq \varepsilon(v)\oplus b.
\]
We claim $\chi$ is constant on every connected component
of~$\tG$ whose base image is~$C$. Indeed, for an edge
$(u,b)\sim_{\tG}(u',b')$ with $[u]_{\sim_G}=C$,
\[
  \chi(u,b)\oplus \chi(u',b')
    = \varepsilon(u)\oplus \varepsilon(u')\oplus b\oplus b'
    = \mathbf{1}_{\{u,u'\}\in W} \oplus \mathbf{1}_{\{u,u'\}\in W}
    = 0,
\]
using the definition of~$\sim_{\tG}$ and of balance. So $\chi$
is a locally constant function on the fibre over~$C$, hence
constant on components. But
\[
  \chi(v_0,\bot) = \varepsilon(v_0)\oplus \bot \ne
  \varepsilon(v_0)\oplus \top = \chi(v_0,\top),
\]
so $(v_0,\bot)$ and $(v_0,\top)$ lie in different components:
$D_\bot\ne D_\top$. Together with Lemma~\ref{lem:fiber-subset},
this forces $\pi^{-1}(C) = \{D_\bot,D_\top\}$, of cardinality~$2$.
\end{proof}

\paragraph{Step 3: the unbalanced case.}

\begin{lemma}\label{lem:merge-if-unbalanced}
If $C$ is not balanced, then $D_\bot=D_\top$, whence
$\#\pi^{-1}(C)=1$.
\end{lemma}

\begin{proof}
We prove the contrapositive: if $D_\bot\ne D_\top$, then $C$ is
balanced. Define
\[
  \varepsilon_0(v)\defeq \mathbf{1}_{(v,\bot)\in D_\bot}
  \qquad (v\in V),
\]
read in $\operatorname{Bool}$ via $0\mapsto\bot$, $1\mapsto\top$. We
show that $\varepsilon_0$ itself witnesses balance of~$C$
(Definition~\ref{def:balanced}). Two facts are used, for every $u$
with $[u]=C$.
First, some sheet over~$u$ lies in~$D_\bot$: lifting a walk
$v_0\to u$ in~$C$ edge by edge from $(v_0,\bot)$, as in the proof of
Lemma~\ref{lem:fiber-subset}, ends at $(u,b)$ for some~$b$.
Second, not both sheets over~$u$ lie in~$D_\bot$: the deck involution
$\delta$ is a graph automorphism (Lemma~\ref{lem:deck}), so it maps
components to components, and $\delta(v_0,\bot)=(v_0,\top)$ gives
$\delta(D_\bot)=D_\top$. If $(u,\bot)$ and $(u,\top)$ both lay
in~$D_\bot$, then $(u,\top)=\delta(u,\bot)$ would also lie in~$D_\top$,
so $D_\bot\cap D_\top\ne\emptyset$ and $D_\bot=D_\top$, contrary to
assumption. Together,
\[
  (u,\top)\in D_\bot \iff (u,\bot)\notin D_\bot
  \qquad\text{whenever } [u]=C. \tag{$\dagger$}
\]
Now let $\{u,u'\}\in E$ with $[u]=C$. If $\{u,u'\}\notin W$, then
$(u,\bot)\sim_{\tG}(u',\bot)$, so $(u,\bot)$ and $(u',\bot)$ lie in the
same component and $\varepsilon_0(u)=\varepsilon_0(u')$. If
$\{u,u'\}\in W$, then $(u,\bot)\sim_{\tG}(u',\top)$, so
$(u,\bot)\in D_\bot\iff(u',\top)\in D_\bot\iff(u',\bot)\notin D_\bot$
by~($\dagger$), that is, $\varepsilon_0(u)\ne\varepsilon_0(u')$. Hence
$\{u,u'\}\in W\iff\varepsilon_0(u)\ne\varepsilon_0(u')$ on every edge
of~$C$, and $C$ is balanced, contradicting the hypothesis. Therefore
$D_\bot = D_\top$, and $\pi^{-1}(C)=\{D_\bot\}$ by
Lemma~\ref{lem:fiber-subset}.

The Lean proof follows the same route.
\path{balanced_of_sheets_separated} (\path{L6_Cohomology.lean})
takes as witness the unique sheet $b(u)$ with $(u,b(u))\in D_\bot$,
which equals $\neg\varepsilon_0(u)$ and witnesses balance equally well;
its uniqueness, \path{unique_sheet_above}, is the
deck-involution argument above. \path{componentProj_fiber_card}
combines it with Lemmas~\ref{lem:fiber-subset}
and~\ref{lem:sep-if-balanced}.
\end{proof}

Lemmas~\ref{lem:fiber-subset}--\ref{lem:merge-if-unbalanced} together
prove Theorem~\ref{thm:fiber-card}. An immediate corollary is:

\begin{corollary}\label{cor:components-cover}
$\#\comp(\tG) \;=\; \#\comp(G) \;+\; \beta(G)$.
\end{corollary}

\begin{proof}
Summing $\#\pi^{-1}(C)$ over $C\in\comp(G)$: each balanced
component contributes $2$, each unbalanced contributes~$1$.
So $\#\comp(\tG) = 2\beta(G) + (\#\comp(G)-\beta(G))
  = \#\comp(G)+\beta(G)$.
\end{proof}

%=============================================================
\section{Recognition Theorems}\label{sec:recognition}
%=============================================================

We now reap the kernel-dimension formulas. Throughout, $G$ is a
finite simple connection graph.

\begin{theorem}[Scalar kernel dimension, Mathlib]\label{thm:scalar-ker}
$\dim_\RR \Ker \Lscalar(G) = \#\comp(G)$.
\end{theorem}

This is Mathlib's
\path{SimpleGraph.card_ConnectedComponent_eq_rank_ker_lapMatrix}
applied to the ordinary graph Laplacian and used as a primitive.

\begin{theorem}\label{thm:signed-kernel}
$\dim_\RR \Ker \Lsigned(G) = \beta(G)$.
\end{theorem}

\begin{proof}
By Corollary~\ref{cor:cover-kernel},
\[
  \dim \Ker\tL \;=\; \dim\Ker\Lscalar(G) + \dim \Ker\Lsigned(G),
\]
where $\tL = \Lscalar(\tG)$. Applying
Theorem~\ref{thm:scalar-ker} to~$\tG$ and to~$G$, and invoking
Corollary~\ref{cor:components-cover},
\[
  \#\comp(G) + \beta(G) = \#\comp(\tG) = \dim\Ker\tL
    = \dim\Ker\Lscalar(G) + \dim\Ker\Lsigned(G)
    = \#\comp(G) + \dim\Ker\Lsigned(G).
\]
Subtracting $\#\comp(G)$ yields the claim.
\end{proof}

\begin{theorem}\label{thm:connection-ker}
For $\epsilon\in\{\mathrm{flat},\mathrm{Mob}\}$,
\[
  \dim_\RR \Ker L_\epsilon
  \;=\; \begin{cases}
    2\,\#\comp(G) & \epsilon=\mathrm{flat},\\
    \#\comp(G)+\beta(G) & \epsilon=\mathrm{Mob}.
  \end{cases}
\]
\end{theorem}

\begin{proof}
By Theorem~\ref{thm:decomp}, $L_\epsilon$ is similar (through the
reindex $\varphi$) to
$\diag(\Lscalar, B_\epsilon)$ with
$B_{\mathrm{flat}}=\Lscalar$, $B_{\mathrm{Mob}}=\Lsigned$. So
\[
  \dim\Ker L_\epsilon
  = \dim\Ker\Lscalar + \dim \Ker B_\epsilon.
\]
Theorems~\ref{thm:scalar-ker} and~\ref{thm:signed-kernel} give the
two diagonal-block kernel dimensions, yielding the claim.
\end{proof}

\begin{theorem}\label{thm:strict}
$\dim\Ker L_{\mathrm{Mob}} < \dim\Ker L_{\mathrm{flat}}$
  iff $\beta(G) < \#\comp(G)$, equivalently, iff \emph{not every}
  component of~$G$ is balanced.
\end{theorem}

\begin{proof}
By Theorem~\ref{thm:connection-ker}, the strict inequality reduces
to $\#\comp(G)+\beta(G) < 2\#\comp(G)$, i.e.\ $\beta(G)<\#\comp(G)$.
The inequality $\beta(G)\le \#\comp(G)$ is immediate from the
inclusion $\comp^{\mathrm{bal}}(G)\subseteq\comp(G)$ of
Definition~\ref{def:balanced}.
\end{proof}

\begin{remark}[Initial written plan vs.\ correct statement]
\label{rem:initial-plan}
Our initial written plan contained the assertion
\[
  \dim\Ker\Lsigned(G) \;\overset{?}{=}\; \#\comp(G) -
    \#\{C\in\comp(G) : |W\cap E(C)|\text{ is odd}\}. \tag{$\star$}
\]
This is \emph{false} in general. Example: let $G=K_4$ with
$W=\{\{1,2\},\{3,4\}\}$, two disjoint wrap edges forming a
matching. The whole graph is one component, the total wrap count
is $2$ (even), so~$(\star)$ predicts
$\dim\Ker\Lsigned = 1$. The signed matrix has determinant $48$,
so its kernel is zero; eigenvalue computation agrees. Thus
$\dim \Ker\Lsigned = 0$, which is indeed~$\beta(K_4)=0$
from Theorem~\ref{thm:signed-kernel} (the two wrap edges
together form a non-trivial cohomology class on~$K_4$).
Equation~$(\star)$ is correct on $G=C_n$: there
$\dim H^1(C_n;\ZZ/2)=1$, no edge is a bridge, and total wrap-count
mod~$2$ detects the class. Beyond $C_n$, however, the correctness of
$(\star)$ depends on $W$, not on the component alone. Precisely,
$(\star)$ is correct on a component $C$ iff
\[
  \text{$C$ is balanced (Definition~\ref{def:balanced})}\;\Longleftrightarrow\;
  |W\cap E(C)| \text{ is even.}
\]
This characterises agreement component by component. On a disconnected
graph the global identity~$(\star)$ can also hold by cancellation: it
holds exactly when the number of balanced components with odd wrap
count equals the number of unbalanced components with even wrap count.
A useful \emph{sufficient} condition --- which is \emph{not} necessary ---
is: $\dim H^1(C;\ZZ/2)\le 1$ (i.e., by the Euler relation
$\dim H^1(C)=|E(C)|-|V(C)|+1$ on a connected component, $C$ is at most
unicyclic) \emph{and} $C$ carries an even number of wrapped bridges.
This condition is not necessary: on $K_4$ with a single wrapped triangle, $(\star)$
holds although $\dim H^1(K_4;\ZZ/2)=3$; with $W=\emptyset$ it holds
trivially on every graph. Failure takes exactly two forms: an
\emph{unbalanced} component with even total wrap ($K_4$ with a wrapped
matching; two triangles sharing a vertex with one wrap in each), and a
\emph{balanced} component with odd total wrap (a tree component with an
odd number of wrapped bridges, e.g.\ $P_3$ with one wrapped edge ---
where $\dim H^1=0$, so a small cohomology alone guarantees nothing).
All six example computations above are reproduced by the independent
implementation in \texttt{findings/round8}, written from the manuscript
alone without consulting Lean sources. The counterexample and corrected
formula are already present in the initial public commit (2026-04-22).
That record establishes neither which tool first found the error nor
a causal order between computation and formalisation. We have not
identified a timestamped preregistration. Exact rational checks for
both this matching and the different adjacent-edge example in the
Lean comment are in \path{findings/round10/test_k4_counterexamples.py}.
\end{remark}

%=============================================================
\section{The Cycle Spectrum}\label{sec:cycles}
%=============================================================

We close with an explicit diagonalisation in the case $G=C_n$, the
$n$-cycle. Identify $V(C_n)=\ZZ/n$, with edges $\{i,i+1\pmod n\}$.
Let $\mathbf{e}_k\in \CC^n$ be the Fourier basis vector
$\mathbf{e}_k[j]= e^{2\pi i k j/n}$ for $k\in\ZZ/n$. Every circulant
has this complex Fourier eigenbasis. For a \emph{real symmetric}
circulant, the eigenvalues are real, so the nonzero vectors
$\operatorname{Re}(\mathbf{e}_k)$ and $\operatorname{Im}(\mathbf{e}_k)$
are real eigenvectors. A real eigenbasis takes one sine--cosine pair
for each $1\le k<n/2$, together with $\mathbf{e}_0$ and, for even $n$,
$\mathbf{e}_{n/2}$. For a general real circulant, a conjugate pair of
non-real eigenvalues instead gives a real invariant plane; its sine
and cosine vectors need not be eigenvectors.

\begin{theorem}[Flat cycle spectrum]\label{thm:flat-cycle}
Let $n\ge 3$. As a multiset indexed by $k\in\ZZ/n$ (repeated values
counted with multiplicity), the scalar Laplacian $\Lscalar(C_n)$ has
spectrum
\[
  \operatorname{Spec}\Lscalar(C_n)
  = \bigl\{\, 2 - 2\cos(2\pi k/n) \,:\, k\in\ZZ/n\,\bigr\},
\]
with $\mathbf{e}_k$ an eigenvector for the eigenvalue
$2-2\cos(2\pi k/n)$.
\end{theorem}

\begin{theorem}[Möbius cycle spectrum]\label{thm:mobius-cycle}
Let $n\ge 3$ and $W=\{\{0,1\}\}$ (one wrap edge). Then, as a multiset
indexed by $k\in\ZZ/n$, $\Lsigned(C_n)$ has spectrum
\[
  \operatorname{Spec}\Lsigned(C_n)
  = \bigl\{\, 2 - 2\cos((2k+1)\pi/n) \,:\, k\in\ZZ/n\,\bigr\}.
\]
\end{theorem}

\begin{proof}[Sketch]
The scalar Laplacian is the circulant $2\II - (S+S^{-1})$ for the
shift $S:v\mapsto v(\cdot+1)$, so it commutes with the $\ZZ/n$-action
and is diagonalised by the Fourier basis with shift weight $+1$,
giving eigenvalues $2 - (e^{2\pi i k/n}+e^{-2\pi ik/n})$. The signed
Laplacian with a single wrap edge is \emph{not} circulant before
gauging; it commutes with the twisted shift $S_{\mathrm{sg}}$
satisfying $S_{\mathrm{sg}}^n=-\II$. Relabel cyclically so that the
wrap edge is the closing edge $\{n-1,0\}$, which is the convention of
the Lean matrix. Conjugation by $U=\diag(\alpha^j)_{0\le j<n}$ with
$\alpha=e^{i\pi/n}$ multiplies the interior off-diagonal entries by
$\alpha^{\pm1}$ and the closing-edge entries by
$\alpha^{\mp(n-1)}=-\alpha^{\pm1}$; since $\alpha^n=-1$, this cancels
the wrap sign, and $U^{-1}\Lsigned U = 2\II-(\alpha S+\alpha^{-1}S^{-1})$
is circulant, with eigenvalues
$2 - (e^{(2k+1)\pi i/n}+e^{-(2k+1)\pi i/n})$. (For the wrap edge
$\{0,1\}$ itself, use the exponents $(j-1)\bmod n$.)
The Lean proof in \texttt{CycleMultiset.lean} checks the complete
periodic and anti-periodic complex Fourier eigen-equations on the
explicit cycle matrices, including the signed closing-edge sign.
The distinct Fourier parameters yield an invertible Vandermonde
eigenbasis, hence similarity to a diagonal matrix and the full
characteristic-polynomial products. Euler's identity and injectivity
of the coefficient inclusion $\RR\hookrightarrow\CC$ descend the
products to real cosines; the polynomial-root theorems then certify
the stated eigenvalue multisets with all algebraic multiplicities.
The signed specialised matrix places its wrap on the closing edge;
the single-edge convention $W=\{\{0,1\}\}$ above is obtained by
cyclic relabelling, rather than by a separately formalised
\texttt{ConnGraph} matrix-equivalence theorem.
\end{proof}

\begin{remark}\label{rem:cycle-spectrum-lean}
The earlier \texttt{CycleSpectrum.lean} theorems
\path{scalarCycle_eigenvalue} and \path{signedCycle_eigenvalue}
produce one real eigenvector per frequency; these witnesses alone do
\emph{not} establish multiplicities because distinct frequencies can
yield the same cosine vector. This gap is now closed in
\texttt{CycleMultiset.lean}. The named theorems
\texttt{scalarCycle\_charpoly\_real} and
\texttt{signedCycle\_charpoly\_real} prove both entire cosine
characteristic-polynomial products for every $n\ge3$; the theorems
\texttt{scalarCycle\_roots\_real} and
\texttt{signedCycle\_roots\_real} establish the corresponding
\emph{multisets} of roots, including repeated eigenvalues. The
completeness argument uses the nonzero Vandermonde determinant of the
distinct \emph{complex} Fourier parameters and is itself formalised
as \path{charpoly_of_vandermonde_eigenbasis}.
\end{remark}

\begin{corollary}
Let $G=C_n$ with $n\ge 3$ and let $W=\{\{0,1\}\}$ consist of a single wrap
edge. Then $\Ker\Lsigned(C_n)=0$, equivalently $\beta(C_n)=0$, and hence
\[
  \dim\Ker L_{\operatorname{Mob}}(C_n,W) = 1
  \;<\; 2 = \dim\Ker L_{\operatorname{flat}}(C_n)
\]
for every $n\ge 3$.
\end{corollary}

\begin{proof}
By Theorem~\ref{thm:mobius-cycle} the signed eigenvalues are
$2-2\cos\bigl((2k+1)\pi/n\bigr)$ for $k\in\ZZ/n$. Such an eigenvalue can
vanish only if $(2k+1)/n$ is an even integer, which is impossible since
$2k+1$ is odd. Hence the signed kernel is zero. The single wrap edge gives
odd holonomy around the fundamental cycle, so the unique component is
unbalanced, confirming $\beta(C_n)=0$. The kernel dimensions then follow from
Theorem~\ref{thm:connection-ker}.
\end{proof}

\begin{remark}
The parity-in-$n$ variant arises for the all-edges-wrap pattern
$W=E(C_n)$: the total wrap parity around the fundamental cycle is then
$n\bmod 2$, so $C_n$ is balanced exactly when $n$ is even.
\end{remark}

%=============================================================
\section{The Lean Formalisation}\label{sec:formalisation}
%=============================================================

The central kernel-dimension and decomposition development is formalised
in Lean~4 against Mathlib~v4.11.0. The flat and one-wrap signed cycle
characteristic polynomials and real root multisets, for all $n\ge3$,
are formalised in \texttt{CycleMultiset.lean}, beyond the individual
eigenpairs from \texttt{CycleSpectrum.lean}.
The \texttt{CycleGraphTransfer.lean} theorem
\path{mobius_connection_roots_of_cycle_reindex} extends
the resulting union of scalar and signed spectral multisets to a
general \texttt{ConnGraph} \emph{provided} a vertex equivalence and
\emph{both} explicit scalar/signed matrix-reindexing equalities are
supplied. It does not derive those equalities from a cycle-graph
hypothesis: that separate graph-encoding proof remains open.
The dependency graph is linear:
\[
  \text{\texttt{Basic}} \to
  \text{\texttt{KernelDimension}} \to
  \text{\texttt{L5\_Cover}} \to \cdots \to
  \text{\texttt{L17\_TracesAndLipschitz}},
\]
with the \texttt{CycleSpectrum} file depending on \texttt{Basic}
and \texttt{KernelDimension}, and \texttt{CycleMultiset} extending
the cycle argument by Fourier-basis completeness (the full file list
is tabulated in Appendix~\ref{app:formal-index}).

\subsection*{Axiomatic footprint}

The formal development's source audit excludes \texttt{sorry},
\texttt{admit}, \texttt{native\_decide}, and project-local axiom
declarations. A selected set of representative end theorems,
including all nine stages of the cycle-spectrum proof, is checked
by \texttt{\#print axioms} against only the three standard Lean
axioms \texttt{propext}, \texttt{Classical.choice}, and
\texttt{Quot.sound}. The main paper-to-Lean correspondences are listed
below; this is not the list of explicit \texttt{\#print axioms} targets.
The exact $25$ selected targets are recorded in
\path{ConnectionLaplacian/AxiomAudit.lean}; their axiom reports also
check transitive proof dependencies. Inclusion in the correspondence
list alone does not establish coverage by that selected audit.
\begin{itemize}
  \item Theorem~\ref{thm:decomp} is
    \path{ConnGraph.laplacian_decomposes};
  \item Theorem~\ref{thm:cover-splits} is
    \path{ConnGraph.scalarLap_cover_splits};
  \item Theorem~\ref{thm:fiber-card} is
    \path{ConnGraph.componentProj_fiber_card};
  \item Theorem~\ref{thm:signed-kernel} is
    \path{ConnGraph.signedLaplacian_kernel_dim_general};
  \item Theorem~\ref{thm:connection-ker} is
    \path{ConnGraph.connectionLaplacian_kernel_dim_general};
  \item Theorem~\ref{thm:strict} is
    \path{ConnGraph.mobius_kernel_strict_iff_general};
  \item Theorems~\ref{thm:flat-cycle}--\ref{thm:mobius-cycle} are
    certified with \emph{all algebraic multiplicities} by
    \path{Cycle.scalarCycle_roots_real} and
    \path{Cycle.signedCycle_roots_real}; see
    Remark~\ref{rem:cycle-spectrum-lean}.
\end{itemize}

\subsection*{Numerical cross-check}

As an independent safety net against the formal statements being
merely \emph{provable} but not intended, the accompanying Python
script \path{findings/round2/fuzzer/fuzz.py} enumerates every
simple graph on
$n\in\{2,3,4,5\}$ vertices up to isomorphism (51~graphs, matching
OEIS A000088) and every $2^{|E|}$ wrap subset, totalling
$3{,}456$~configurations. For each~$(G,W)$ it checks:
\begin{itemize}
  \item Theorem~\ref{thm:cover-splits} via spectrum equality of
    $\tL$ and $\Lscalar(G)\oplus \Lsigned(G)$;
  \item Corollary~\ref{cor:cover-kernel} via SVD-based integer
    kernel-dimension arithmetic;
  \item Theorem~\ref{thm:fiber-card} via brute-force
    $\ZZ/2$-colouring search and connected-component counting.
\end{itemize}
All $3{,}456$ configurations agreed with the formal theorem
statements; zero disagreements were found.

\subsection*{Summary of effort distribution}

The ``mathematical'' content, in descending order of novelty:
\begin{enumerate}[label=\textbf{(\arabic*)}]
  \item The fibre-cardinality theorem
    (Theorem~\ref{thm:fiber-card}) has no counterpart in
    Mathlib; it requires the walk-lift construction,
    XOR-parity invariant, and deck-action freeness argument,
    all of which are built from scratch against Mathlib's
    \path{SimpleGraph.ConnectedComponent} eliminators.
  \item The cover-splitting Theorem~\ref{thm:cover-splits} is an
    entrywise matrix identity. Mathlib's Kronecker library
    (\texttt{Matrix.mul\_kronecker\_mul}, etc.) mechanises
    $\sim\!15\%$; the remaining work is a four-case matching on
    wrap/non-wrap adjacency and a 2x2 block calculation.
  \item The block-decomposition Theorem~\ref{thm:decomp} reuses
    the Kronecker pattern from (2) on the $\operatorname{Fin}2$
    fibre instead of the $\operatorname{Bool}$ fibre.
  \item Recognition Theorems~\ref{thm:signed-kernel} and
    \ref{thm:connection-ker} are a few lines of arithmetic
    conclusion once (1)--(3) are in place.
\end{enumerate}

\subsection*{Lessons}

The development corrected the false equation~$(\star)$ in the initial
written plan. Numerical counterexamples and the formal balanced-component
theorem supply different checks of that correction. The public history
already records both in its initial commit, so it does not determine
the first detector or the order of discovery. The methodological lesson
is to retain explicit counterexamples and verified replacement statements.

\bigskip

\noindent\textit{Acknowledgements and AI provenance.} This work was carried
out as an independent, AI-assisted formal-verification project on
combinatorial spectral identities. The human author directed the research
questions, mathematical scope, specification checks, and adversarial
review. Language models, including OpenAI ChatGPT and Anthropic Claude,
contributed substantially to exposition, Lean formalization, proof
construction, testing, and review. The author does not claim to have
independently reconstructed every formal proof. The source repository
records the development, corrections, and evidence boundaries in
\path{docs/methods-note.md} and \path{Hardening/EVIDENCE-MAP.md}.
Lean kernel acceptance establishes the formalized statements under
explicit assumptions, not their originality or their match to every
informal interpretation.

%=============================================================
\section{Further Identities: Traces, Bounds, and the
Characteristic Polynomial}\label{sec:bounds}
%=============================================================

The block decomposition (Theorem~\ref{thm:decomp}) and cover splitting
(Theorem~\ref{thm:cover-splits}) imply a family of exact spectral
identities that sit one inference-step away from the recognition
theorems. We collect the ones that admit a one-paragraph proof and
are stated at the level of generality on which the formalised
library already operates. Together they close the
``trace-and-inequality gap'' left open in earlier versions of this
manuscript. The scalar and signed trace formulas and the kernel
inequalities are formalised in \path{ConnectionLaplacian/L9_Bounds.lean};
the flat and Möbius traces and the quadratic-trace and Frobenius
identities in \path{ConnectionLaplacian/L17_TracesAndLipschitz.lean};
positive semidefiniteness in \path{ConnectionLaplacian/L13_PSD.lean};
and the multiplicative spectral partition
(Theorem~\ref{thm:cover-charpoly}) in
\path{ConnectionLaplacian/L10_CoverCharpoly.lean}.

\begin{proposition}[Trace formulas]\label{prop:traces}
For every connection graph $G=(V,E,W)$,
\begin{align*}
  \tr \Lscalar(G) \;&=\; 2\,\#E, &
  \tr \Lsigned(G) \;&=\; 2\,\#E, \\
  \tr L_{\mathrm{flat}}(G) \;&=\; 4\,\#E, &
  \tr L_{\mathrm{Mob}}(G) \;&=\; 4\,\#E.
\end{align*}
\end{proposition}

\begin{proof}
The diagonal entry of $\Lscalar$ at $v$ is
$\deg(v)$; irreflexivity of the underlying simple graph kills the
wrap off-diagonal contribution at the diagonal, so the diagonal of
$\Lsigned$ is also $\deg(v)$; and the diagonals of
$L_{\mathrm{flat}}, L_{\mathrm{Mob}}$ are each $\deg(v)\cdot\II_2$,
contributing $2\deg(v)$. Summing over $v$ and applying the
degree-sum identity
$\sum_v \deg(v) = 2\,\#E$
(Mathlib's
\path{SimpleGraph.sum_degrees_eq_twice_card_edges}) proves
all four equalities. The Lean names are
\path{trace_scalarLaplacian} and \path{trace_signedLaplacianMobius}
(\path{L9_Bounds.lean}), and \path{trace_laplacian_flat} and
\path{trace_laplacian_mobius} (\path{L17_TracesAndLipschitz.lean}).
\end{proof}

\begin{proposition}[Quadratic trace and Frobenius
identities]\label{prop:traces2}
For every connection graph $G=(V,E,W)$,
\begin{align*}
  \tr\bigl(L_{\mathrm{Mob}}(G)^2\bigr)
  \;&=\; \tr\bigl(\Lscalar(G)^2\bigr)
       + \tr\bigl(\Lsigned(G)^2\bigr), \\
  \|L_{\mathrm{Mob}}(G)\|_F^2
  \;&=\; \|\Lscalar(G)\|_F^2 + \|\Lsigned(G)\|_F^2,
\end{align*}
and the cross term obeys the polarisation identity
\[
  2\,\tr\!\bigl(\Lscalar(G)\cdot\Lsigned(G)\bigr)
  \;=\;
  \tr\!\bigl((\Lscalar(G){+}\Lsigned(G))^2\bigr)
  - \tr\!\bigl(\Lscalar(G)^2\bigr)
  - \tr\!\bigl(\Lsigned(G)^2\bigr).
\]
\end{proposition}

\begin{proof}
Starting from the Kronecker-conjugation similarity of
Theorem~\ref{thm:decomp} in its Möbius form, the trace-of-square and
Frobenius identities follow from invariance of $\tr(M^2)$ and of
$\tr(M^\top M)$ under orthogonal similarity and simultaneous row and
column reindexing. Here $P=\II_V\kronprod\widehat R$ satisfies
$P^2=2\II$ and $P^\top=P$, so $Q=P/\sqrt{2}$ is an orthogonal
involution and $QLQ^{-1}=PLP^{-1}$. Alternatively, as in Lean,
symmetry gives $\|L\|_F^2=\tr(L^2)$ for each of the three Laplacians,
reducing the Frobenius identity to the trace-of-square identity.
The cross-term identity is pure algebra: expand
$(\Lscalar+\Lsigned)^2$ and use symmetry of the scalar and signed
Laplacians together with the cyclic property
$\tr(\Lscalar\Lsigned)=\tr(\Lsigned\Lscalar)$. The Lean names are
\path{trace_sq_laplacian_decomposes},
\path{frobenius_laplacian_decomposes} and
\texttt{trace\_mul\_scalar\_signed\_eq}.
\end{proof}

\begin{remark}[Polarisation versus combinatorial form]
The cross-term identity above is stated in \emph{polarisation form}
and is pure matrix algebra. For these graph Laplacians the additional
combinatorial identity
$\tr(\Lscalar\cdot\Lsigned)=\tr\bigl((\Lscalar)^{2}\bigr)-4\,\#W$, which can be
read off the entrywise formula for $\Lscalar\cdot\Lsigned$ by
summing contributions at diagonal and off-diagonal positions, is
confirmed numerically by the R6 Stage-6 fuzzer (zero deviation
across $300$ random connected graphs at $n=7$) but is not yet a
separately named Lean theorem. Its proof needs the graph-entry
calculation and finite edge counting; the polarisation theorem alone
does not establish it. This remains an open formalisation obligation.
\end{remark}

\begin{proposition}[Kernel inequalities]\label{prop:kernel-ineq}
For every connection graph $G$,
\begin{align*}
  \dim\Ker \Lsigned(G) \;&\le\; \dim\Ker \Lscalar(G), \\
  \dim\Ker L_{\mathrm{flat}}(G) - \dim\Ker L_{\mathrm{Mob}}(G)
    \;&=\; \#\comp(G) - \beta(G),
\end{align*}
and in particular the difference is bounded by $\#\comp(G)$.
\end{proposition}

\begin{proof}
By Theorems~\ref{thm:scalar-ker}, \ref{thm:signed-kernel},
\ref{thm:connection-ker}, the LHS of the first line equals
$\beta(G)$, the RHS equals $\#\comp(G)$, and
$\beta(G)\le \#\comp(G)$ because
$\comp^{\mathrm{bal}}(G)\subseteq \comp(G)$. For the second line,
$\dim\Ker L_{\mathrm{flat}} = 2\,\#\comp(G)$ and
$\dim\Ker L_{\mathrm{Mob}} = \#\comp(G)+\beta(G)$, whose difference
is $\#\comp(G)-\beta(G)$, itself bounded by $\#\comp(G)$.
\end{proof}

\begin{lemma}[Positive semidefiniteness of the signed
Laplacian]\label{lem:signed-psd}
$\Lsigned(G) \succeq 0$. Indeed
\[
  \pair{x}{\Lsigned(G)\, x}
  = \!\!\sum_{e=\{u,v\}\in E\setminus W}\! (x_u - x_v)^2
  + \sum_{e=\{u,v\}\in W} (x_u + x_v)^2
\qquad \text{for all } x\in\RR^V.
\]
\end{lemma}

\begin{proof}
Fix $x\in\RR^V$. The off-diagonal entry of $\Lsigned$ at $(u,v)$
equals $+1$ when $\{u,v\}\in W$ and $-1$ when $\{u,v\}\in E\setminus W$;
the diagonal is $\deg(u)$. Since $\Lsigned$ is symmetric, each
unordered edge $\{u,v\}$ contributes the pair of entries $(u,v)$
and $(v,u)$ to the quadratic form, yielding a factor of~$2$:
\[
  \pair{x}{\Lsigned x}
  \;=\; \sum_u \deg(u)\,x_u^2
      \;+\; 2\!\!\sum_{\{u,v\}\in W}\!\!x_u x_v
      \;-\; 2\!\!\sum_{\{u,v\}\in E\setminus W}\!\!x_u x_v.
\]
Rewriting $\sum_u \deg(u)\,x_u^2
= \sum_{\{u,v\}\in E}\bigl(x_u^2 + x_v^2\bigr)$ (each edge
contributes to the degree of both endpoints) and splitting the
degree sum along $E = (E\setminus W)\sqcup W$:
\[
  \pair{x}{\Lsigned x}
  \;=\;\!\!\sum_{\{u,v\}\in E\setminus W}\!\!(x_u^2 + x_v^2 - 2 x_u x_v)
    \;+\;\sum_{\{u,v\}\in W}(x_u^2 + x_v^2 + 2 x_u x_v),
\]
which is exactly the announced sum of squares. Every summand is
$\ge 0$, so $\pair{x}{\Lsigned x}\ge 0$.
\end{proof}

\begin{theorem}[Multiplicative spectral partition: cover
characteristic polynomial]\label{thm:cover-charpoly}
Let $\tL = \Lscalar(\tG)$ be the scalar Laplacian of the orientation
double cover of~$G$. Then the characteristic polynomials factor as
\[
  \det\bigl(\lambda\,\II_{\tV} - \tL\bigr) \;=\;
  \det\bigl(\lambda\,\II_V - \Lscalar(G)\bigr)\cdot
  \det\bigl(\lambda\,\II_V - \Lsigned(G)\bigr).
\]
Equivalently, as multisets the spectra satisfy
$\operatorname{Spec}(\tL) = \operatorname{Spec}(\Lscalar(G)) \uplus
\operatorname{Spec}(\Lsigned(G))$.
\end{theorem}

\begin{remark}[Direct-bundle factorisation]\label{rem:direct-bundle-charpoly}
Composing Theorem~\ref{thm:cover-charpoly} with the similarity of
Theorem~\ref{thm:decomp} gives the same factorisation directly for
$L_{\mathrm{Mob}}$ without invoking the cover:
\[
  \det\bigl(\lambda\,\II_{V\times\operatorname{Fin}2} - L_{\mathrm{Mob}}(G)\bigr)
  \;=\;
  \det\bigl(\lambda\,\II_V - \Lscalar(G)\bigr)\cdot
  \det\bigl(\lambda\,\II_V - \Lsigned(G)\bigr),
\]
and for every $\alpha\in\RR$,
$\det(L_{\mathrm{Mob}}+\alpha\II_{V\times\operatorname{Fin}2})
=\det(\Lscalar+\alpha\II_V)\cdot
\det(\Lsigned+\alpha\II_V)$. As multisets,
$\operatorname{Spec}(L_{\mathrm{Mob}}) = \operatorname{Spec}(\Lscalar)
\uplus \operatorname{Spec}(\Lsigned)$. These are Lean theorems
\path{mobius_charpoly_eq_scalar_times_signed},
\texttt{shiftedDet\_factorises} and
\path{mobius_charpoly_roots_eq_union}.
\end{remark}

\begin{proof}
By Theorem~\ref{thm:cover-splits}, $\tL$ is similar (through an
invertible Hadamard--Kronecker change of basis composed with the
reindex $V\times\operatorname{Bool}\cong V\sqcup V$) to the block
matrix $\diag(\Lscalar(G),\Lsigned(G))$. Similarity preserves the
characteristic polynomial, and the characteristic polynomial of a
block-diagonal matrix factors into the product of its diagonal
blocks' characteristic polynomials. The multiset equality follows by
equating roots with multiplicity.
\end{proof}

\begin{remark}[Interlacing as a corollary]
Theorem~\ref{thm:cover-charpoly} strictly strengthens the Cauchy
interlacing one might expect between the spectra of $\Lsigned$ and
$\tL$: interlacing would merely bound each eigenvalue of $\Lsigned$
between two eigenvalues of $\tL$, whereas
Theorem~\ref{thm:cover-charpoly} pins down the spectrum of $\tL$
exactly as the disjoint union of the two smaller spectra. In
particular $\det\bigl(\lambda\II - L_{\mathrm{Mob}}(G)\bigr) =
\det\bigl(\lambda\II - L_{\mathrm{flat}}(G)\bigr)$ whenever every
component of~$G$ is balanced.
\end{remark}

\begin{corollary}[Pointwise multiplicity]\label{cor:mult-pointwise}
For every $\lambda\in\RR$,
\[
  m_\lambda(\tL) \;=\; m_\lambda(\Lscalar(G)) + m_\lambda(\Lsigned(G)),
\]
where $m_\lambda(M)$ denotes the multiplicity of~$\lambda$ as an
eigenvalue of~$M$.
\end{corollary}

\begin{proof}
Immediate from Theorem~\ref{thm:cover-charpoly}: the multiplicity of
$\lambda$ in a product of polynomials is the sum of multiplicities
in the factors.
\end{proof}

%=============================================================
\section{Structure Theorems for Trees, Forests, and Cycles}
\label{sec:structure}
%=============================================================

We record the ``topological'' side of the recognition theorems: on
graphs where $H^1$ is understood, the content of
Theorem~\ref{thm:signed-kernel} becomes explicit.

\begin{theorem}[Tree balance]\label{thm:tree-balanced}
If the underlying simple graph of~$G$ is a tree (connected and
acyclic), then its unique component is balanced for \emph{every}
choice of wrap set~$W\subseteq E(G)$. Consequently
\[
  \beta(G) = 1, \qquad
  \dim\Ker \Lsigned(G) = 1, \qquad
  \dim\Ker L_{\mathrm{Mob}}(G) = \dim\Ker L_{\mathrm{flat}}(G) = 2,
\]
and the strict inequality of Theorem~\ref{thm:strict} fails.
\end{theorem}

\begin{proof}
Fix a root~$r$. Because the tree is connected and acyclic, for every
vertex~$v$ there is exactly one path $p_{r\to v}$: any walk $r\to v$
shortens to a path, and two paths with the same endpoints coincide
(Mathlib's \path{SimpleGraph.IsAcyclic.path_unique}). Define
$\varepsilon(v)\defeq \sum_{e\in p_{r\to v}} \mathbf{1}_{e\in W}
  \pmod 2$, with $\varepsilon(r)=\bot$ by the empty sum. Let
$\{u,v\}\in E$. If $v$ does not lie on $p_{r\to u}$, then $p_{r\to u}$
followed by the edge $\{u,v\}$ is a path $r\to v$, so it is
$p_{r\to v}$. Otherwise the part of $p_{r\to u}$ up to~$v$ is a path
$r\to v$, so it is $p_{r\to v}$, and the remaining part is a path
$v\to u$, so it is the single edge $\{v,u\}$. In both cases
$\varepsilon(u)\oplus\varepsilon(v)=\mathbf{1}_{\{u,v\}\in W}$, so
$\varepsilon$ witnesses balance (Definition~\ref{def:balanced}). With
$\#\comp(G)=1$, the kernel dimensions follow from
Theorems~\ref{thm:signed-kernel} and~\ref{thm:connection-ker}.

The Lean proof (\path{L11_Trees.lean}) takes a different route: on
an acyclic graph the wrap parity of a walk depends only on its
endpoints (\path{walkWrapParity_acyclic_endpoints}), so the two sheets
over a vertex lie in different components of the double cover
(\path{candidateLift_ne_of_isTree}), and balance follows from
\path{balanced_of_sheets_separated} of Section~\ref{sec:coho}.
\end{proof}

\begin{corollary}\label{cor:forest-star-path}
Paths $P_n$ and stars $K_{1,n}$ have
$\dim\Ker L_{\mathrm{Mob}}(G)=2$ independently of~$W$. If the
underlying graph is a forest (acyclic, possibly disconnected), each
component is a tree; running the proof of
Theorem~\ref{thm:tree-balanced} inside each component (balance is
component-local, Remark~\ref{rem:balance-scope}) gives
$\beta(G)=\#\comp(G)$, $\dim\Ker\Lsigned(G)=\#\comp(G)$ and
$\dim\Ker L_{\mathrm{Mob}}(G)=2\,\#\comp(G)$. The forest statement is
not a separately named Lean theorem; only the connected
\texttt{IsTree} case is formalised.
\end{corollary}

\begin{theorem}[Walk-sum detector for balance]\label{thm:walk-sum}
Let $C\in\comp(G)$. Then $C$ is balanced iff every closed walk
$w:v\to v$ with $v\in C$ satisfies
$\sum_{e\in w} \mathbf{1}_{e\in W} \equiv 0 \pmod 2$.
\end{theorem}

\begin{proof}
$(\Rightarrow)$ If $\varepsilon$ witnesses balance then for each
edge $e=\{u,u'\}$ in~$C$, $\varepsilon(u)\oplus \varepsilon(u') =
\mathbf{1}_{e\in W}$. Summing along a closed walk $v\to v$, the
$\varepsilon$-terms telescope, leaving
$\sum_e \mathbf{1}_{e\in W}\equiv 0$.
$(\Leftarrow)$ Pick $v_0\in C$ and define
$\varepsilon(v)\defeq \sum_{e\in w} \mathbf{1}_{e\in W}\pmod 2$
for any walk $w:v_0\to v$, and $\varepsilon(u)\defeq\bot$ for
$u\notin C$ (Definition~\ref{def:balanced} leaves those values
unconstrained); the closed-walk-even hypothesis makes
$\varepsilon$ walk-independent. By construction
$\varepsilon(u)\oplus \varepsilon(v)\equiv \mathbf{1}_{e\in W}$ on
every edge $e=\{u,v\}$ of~$C$, so $\varepsilon$ witnesses balance.
\end{proof}

\begin{corollary}[Cycle even-wrap formula]\label{cor:cycle-ew}
If $G=C_n$ is a single cycle of length~$n\ge 3$, then
\[
  \beta(C_n,W) = \begin{cases} 1 & \#W \equiv 0\pmod 2,\\
    0 & \#W \equiv 1\pmod 2,\end{cases}
  \qquad
  \dim\Ker \Lsigned(C_n,W) = \begin{cases} 1 & \#W \text{ even,}\\
    0 & \#W \text{ odd.}\end{cases}
\]
In particular the initial plan's formula
$\dim\Ker\Lsigned = \#\comp(G) - \#\{\text{odd-wrap components}\}$
holds for \emph{every wrap assignment} on a connected cycle graph.
It is not a valid formula for arbitrary graphs. For a \emph{particular}
wrap assignment, however, it can also hold on non-cycle graphs,
as discussed in Remark~\ref{rem:initial-plan}; thus this is not a
pointwise characterisation of cycles. The Lean certificate for this
corollary is the weak, conditional form described in
Remark~\ref{rem:cycle-ew-lean}.
\end{corollary}

\begin{proof}
The first homology of an $n$-cycle with $\ZZ/2$-coefficients is
one-dimensional, $H_1(C_n;\ZZ/2)\cong\ZZ/2$, generated by the
fundamental cycle~$\gamma$. Every closed walk $w$ at a basepoint
decomposes, modulo back-tracking (which contributes
edges twice and hence~$0$ to the $\ZZ/2$-sum of wrap indicators),
into an integer multiple of~$\gamma$; its wrap-parity therefore
equals $[w:\gamma]\cdot\#W \pmod 2$. The walk-sum detector of
Theorem~\ref{thm:walk-sum} therefore reduces to the parity
of~$\#W$ and Theorem~\ref{thm:signed-kernel} converts
$\beta\in\{0,1\}$ to $\dim\Ker\Lsigned\in\{0,1\}$.
\end{proof}

\begin{remark}\label{rem:cycle-ew-lean}
The Lean certificate
\path{cycle_isBalanced_iff_even_wrap_weak}
(\path{L14_CycleEw.lean}) names this a \emph{weak} form: it
takes an Eulerian closed walk and the reverse implication as explicit
inputs. Its signature quantifies over a general \texttt{ConnGraph};
a cycle-graph identification is not constructed there.
Only balancedness implying even total wrap is proved from the Eulerian
walk. The reverse implication needs a cycle-space argument, together
with an explicit \texttt{fundamentalCycleWalk}; both remain open.
\end{remark}

%=============================================================
\section{Counter-claims: What the Formalisation Does
\emph{Not} Prove}\label{sec:counter}
%=============================================================

The extended fuzzer (\S\ref{sec:formalisation}) and the
\texttt{NEGATOR} pass of our discovery swarm refuted four naive
statements that were, at various points, attempted drafts of the
identities above. We record them here both for historical honesty
and as explicit boundary markers for the theorems that \emph{did}
survive.

\begin{example}[Naive equality of M\"obius and scalar kernels is
false]\label{ex:naive-eq}
A tempting but wrong reformulation of Theorem~\ref{thm:strict} is:
``$\dim\Ker L_{\mathrm{Mob}} = \dim\Ker \Lscalar$ iff
every component of~$G$ is balanced.'' This fails already on the
empty graph on $n=3$ vertices with $W=\emptyset$: every
component is trivially balanced (vacuously so, cf.\
Remark~\ref{rem:balance-scope}), yet
$\dim\Ker L_{\mathrm{Mob}} = 6$ (a kernel inside
$\RR^{V\times\operatorname{Fin}2}$) while
$\dim\Ker \Lscalar = 3$ (a kernel inside $\RR^{V}$): the
two kernels sit in different ambient spaces, so the attempted
identity already fails on dimensional grounds. The correct
equivalence uses
the \emph{flat} Laplacian: $\dim\Ker L_{\mathrm{Mob}} =
\dim\Ker L_{\mathrm{flat}} = 2\,\#\comp(G)$ iff every component is
balanced, which is Theorem~\ref{thm:connection-ker} combined with
Theorem~\ref{thm:scalar-ker}.
\end{example}

\begin{example}[A single wrap edge can leave the graph
balanced]\label{ex:bridge-wrap}
The implication ``$G$ connected and $\#W=1$ $\Rightarrow$ $G$ is not
balanced'' is false. Counterexample: the path $P_3$ with vertices
$v_0\text{-}v_1\text{-}v_2$ and the single wrap edge
$\{v_0,v_1\}$ (a bridge) is balanced: the assignment
$\varepsilon(v_0)=\top,\ \varepsilon(v_1)=\bot,\
\varepsilon(v_2)=\bot$ witnesses balance, since
$\varepsilon(v_0)\oplus\varepsilon(v_1)=1=\mathbf{1}_{\{v_0,v_1\}\in W}$
and $\varepsilon(v_1)\oplus\varepsilon(v_2)=0=
\mathbf{1}_{\{v_1,v_2\}\in W}$. The correct form is: a single wrap
edge unbalances the graph iff the wrap edge lies on a cycle.
\end{example}

\begin{example}[Adding a non-wrap edge between components can
\emph{decrease} $\beta$]\label{ex:cross-merge}
The fuzzy-logic sweep (discovery shorthand: claims are labelled
\texttt{C1}, \texttt{C2}, \dots in the order the swarm proposed them,
and $\tau\in[0,1]$ is the empirical satisfaction rate of a claim over
its tested configurations, so $\tau=0$ refutes and $\tau=1$ confirms;
\S\ref{sec:formalisation}, claim \texttt{C2}, $\tau=0.0000$) refutes
the naive monotonicity
``adding a non-wrap edge can only preserve or increase
$\beta$''. On three isolated vertices ($W=\emptyset$, so
$\beta=3$), adding the non-wrap edge $\{v_0,v_1\}$ merges two
balanced components into one still-balanced component and drops
$\beta$ to $2$. The correct law is bidirectional: for a non-wrap
edge $e$ joining two distinct components,
$\beta(G+e)\in\{\beta(G)-1,\beta(G)\}$, with $-1$ when \emph{at
least one} endpoint lies in a balanced component and $0$ when both
endpoints lie in unbalanced components. (In the mixed
balanced-plus-unbalanced case, the merged component is unbalanced,
so the pre-existing balanced component is lost and $\beta$ drops
by~$1$.)
\end{example}

The correct monotonicity law concerns \emph{deleting} edges, and it is
sensitive to bridges rather than to wrap status.

\begin{theorem}[Bridge-deletion monotonicity]\label{thm:bridge-monotone}
Deleting a non-bridge edge cannot decrease $\beta$: for any edge
$e\in E(G)$ that is not a bridge of the underlying graph,
\[
  \beta(G) \;\le\; \beta(G - e).
\]
\end{theorem}

\begin{proof}[Proof (formalised)]
The Lean theorem \path{numBalancedComponents_monotone_remove_nonbridge}
(\path{L15_BridgeMonotone.lean}) has exactly this statement. Deleting a
non-bridge edge preserves reachability, so the components of $G$ and
of $G-e$ correspond bijectively. A balanced component of~$G$ stays
balanced in $G-e$, because the same~$\varepsilon$ witnesses balance:
every edge of $G-e$ is an edge of~$G$. This injects the balanced
components of~$G$ into those of $G-e$. The earlier declaration
\path{numBalancedComponents_monotone_remove_nonwrap_nonbridge} carries
an additional, unused non-wrap hypothesis inherited from the discovery
sweep; it is kept unchanged because the archived comparator challenge
replays it.
\end{proof}

\begin{example}[Non-wrap edge contraction is not kernel-stable]
\label{ex:contraction}
On $K_3$ with $W=\{\{v_0,v_1\}\}$ the signed Laplacian has
kernel dimension~$0$. Contracting the non-wrap edge $\{v_0,v_2\}$
identifies $v_0$ and $v_2$, leaving the single wrap edge
$\{v_0,v_1\}$, a tree on $2$ vertices: the signed Laplacian
now has kernel dimension~$1$. So non-wrap edge contraction does
\emph{not} preserve $\dim\Ker\Lsigned$ in general. Contraction is taken
here in the category of simple graphs: the two parallel edges between
the merged vertex and~$v_1$ (one wrap, one non-wrap) collapse to a
single edge, and the resulting two-vertex tree is balanced whichever
wrap status the surviving edge carries. In a signed multigraph the two
parallel edges would instead form an unbalanced $2$-cycle, and $\beta$
would stay~$0$.
\end{example}

%=============================================================
\appendix
\section{Formalisation index}\label{app:formal-index}
%=============================================================

The principal named theorems, propositions, corollaries, and
lemmas of the main text are paired below with corresponding
Lean~4 declarations in the
\texttt{connection\_laplacian\_lean} sandbox. (A handful of
subsidiary lemmas used only in intermediate proofs---e.g.\ the
deck-transformation Lemma~\ref{lem:deck}, the cover-degree
Lemma~\ref{lem:cover-degree}, and the fiber-subset/separation
Lemmas~\ref{lem:fiber-subset}, \ref{lem:sep-if-balanced},
\ref{lem:merge-if-unbalanced}---are implicitly witnessed inside
the proofs of theorems listed below and are not tabulated
separately.) The table below
pairs them explicitly. The production source audit forbids
\texttt{sorry}, \texttt{admit}, \texttt{native\_decide} and local axiom
declarations. The separate CI axiom audit selects $25$ declarations
($18$ before the five conditional graph-transfer results; the two
latest, added on 2026-10-18, are
\path{numBalancedComponents_monotone_remove_nonbridge} and
\path{trace_laplacian_flat}), requiring
each requested output to contain no axioms outside
$\{\texttt{propext},\, \texttt{Classical.choice},\, \texttt{Quot.sound}\}$.
This selected audit does not print every helper or every table row.
Comparator replay covers seven historical and five later cycle statements
in two separate runs; the evidence map records their exact scope. The file
paths are relative to
\path{connection_laplacian_lean/ConnectionLaplacian/}.

{\footnotesize
\renewcommand{\arraystretch}{0.95}
\setlength{\LTpre}{0.6\baselineskip}
\setlength{\LTpost}{0.4\baselineskip}
\begin{longtable}{@{}p{3.2cm}p{6.4cm}p{4.8cm}@{}}
\toprule
Paper statement & Lean declaration & Source file \\
\midrule
\endfirsthead
\multicolumn{3}{@{}l}{\emph{Formalisation index (continued)}} \\[0.4em]
\toprule
Paper statement & Lean declaration & Source file \\
\midrule
\endhead
Eq.~\eqref{eq:connection-laplacian}, \S\ref{sec:prelim} (data) &
  \path{ConnGraph}, \path{laplacian} & \path{Basic.lean} \\
Thm.~\ref{thm:scalar-ker} &
  \path{scalarLaplacian_kernel_dim} & \path{KernelDim.lean} \\
Thm.~\ref{thm:decomp} (direct sum) &
  \path{laplacian_decomposes} & \path{KernelDim.lean} \\
Thm.~\ref{thm:decomp} (ker dim) &
  \path{laplacian_kernel_dim_decomposes} & \path{L8_Recognition.lean} \\
Thm.~\ref{thm:cover-splits} &
  \path{scalarLap_cover_splits} & \path{L5_Cover.lean} \\
Def.~\ref{def:balanced} &
  \path{isBalanced} & \path{L6_Cohomology.lean} \\
Thm.~\ref{thm:fiber-card} &
  \path{componentProj_fiber_card} & \path{L6_Cohomology.lean} \\
Thm.~\ref{thm:signed-kernel} &
  \path{signedLaplacian_kernel_dim_general} & \path{L8_Recognition.lean} \\
Thm.~\ref{thm:connection-ker} &
  \path{connectionLaplacian_kernel_dim_general} & \path{L8_Recognition.lean} \\
Thm.~\ref{thm:strict} &
  \path{mobius_kernel_strict_iff_general} & \path{L8_Recognition.lean} \\
Prop.~\ref{prop:traces} (sc) &
  \path{trace_scalarLaplacian} & \path{L9_Bounds.lean} \\
Prop.~\ref{prop:traces} (sg) &
  \path{trace_signedLaplacianMobius} & \path{L9_Bounds.lean} \\
Prop.~\ref{prop:kernel-ineq} (mono) &
  \path{signed_kernel_le_scalar_kernel} & \path{L9_Bounds.lean} \\
Prop.~\ref{prop:kernel-ineq} (drop~$=\#\comp-\beta$) &
  \path{kernel_drop_eq_unbalanced} & \path{L9_Bounds.lean} \\
Prop.~\ref{prop:kernel-ineq} (drop~$\le\#\comp$) &
  \path{kernel_drop_le_numComponents} & \path{L9_Bounds.lean} \\
Lem.~\ref{lem:signed-psd} &
  \path{signedLaplacianMobius_posSemidef} & \path{L13_PSD.lean} \\
Thm.~\ref{thm:cover-charpoly} &
  \path{cover_charpoly_eq_scalar_times_mobius} & \path{L10_CoverCharpoly.lean} \\
Cor.~\ref{cor:mult-pointwise} &
  \multicolumn{2}{p{11.2cm}}{\emph{corollary of} \path{cover_charpoly_eq_scalar_times_mobius}} \\
Thm.~\ref{thm:tree-balanced} (balance) &
  \path{tree_isBalanced_of_isTree} & \path{L11_Trees.lean} \\
\quad ($\beta=1$) &
  \path{numBalancedComponents_of_isTree} & \path{L11_Trees.lean} \\
\quad (ker dim) &
  \path{connectionLaplacian_kernel_dim_tree_mobius} & \path{L11_Trees.lean} \\
\quad (gap zero) &
  \path{tree_kernel_gap_zero} & \path{L11_Trees.lean} \\
Cor.~\ref{cor:forest-star-path} &
  \multicolumn{2}{p{11.2cm}}{\emph{paths and stars specialise the tree theorem; the forest case is not a named Lean theorem}} \\
Thm.~\ref{thm:walk-sum} &
  \path{isBalanced_iff_closedWalk_wrap_even} & \path{L12_WalkH1.lean} \\
Rem.~\ref{rem:cycle-spectrum-lean} (per-mode, flat) &
  \path{scalarCycle_eigenvalue} & \path{CycleSpectrum.lean} \\
Rem.~\ref{rem:cycle-spectrum-lean} (per-mode, signed) &
  \path{signedCycle_eigenvalue} & \path{CycleSpectrum.lean} \\
Thm.~\ref{thm:flat-cycle} (charpoly) &
  \path{scalarCycle_charpoly_real} & \path{CycleMultiset.lean} \\
Thm.~\ref{thm:flat-cycle} (root multiset) &
  \path{scalarCycle_roots_real} & \path{CycleMultiset.lean} \\
Thm.~\ref{thm:mobius-cycle} (charpoly) &
  \path{signedCycle_charpoly_real} & \path{CycleMultiset.lean} \\
Thm.~\ref{thm:mobius-cycle} (root multiset) &
  \path{signedCycle_roots_real} & \path{CycleMultiset.lean} \\
\quad (graph-conditional transfer) &
  \path{mobius_connection_roots_of_cycle_reindex} & \path{CycleGraphTransfer.lean} \\
Cor.~\ref{cor:cycle-ew} (weak, conditional; Rem.~\ref{rem:cycle-ew-lean}) &
  \path{cycle_isBalanced_iff_even_wrap_weak} & \path{L14_CycleEw.lean} \\
Thm.~\ref{thm:bridge-monotone} &
  \path{numBalancedComponents_monotone_remove_nonbridge} & \path{L15_BridgeMonotone.lean} \\
\quad (historical, unused non-wrap hypothesis) &
  \path{numBalancedComponents_monotone_remove_nonwrap_nonbridge} & \path{L15_BridgeMonotone.lean} \\
Rem.~\ref{rem:direct-bundle-charpoly} (direct charpoly) &
  \path{mobius_charpoly_eq_scalar_times_signed} & \path{L16_SpectrumUnion.lean} \\
Rem.~\ref{rem:direct-bundle-charpoly} (spec union) &
  \path{mobius_charpoly_roots_eq_union} & \path{L16_SpectrumUnion.lean} \\
Rem.~\ref{rem:direct-bundle-charpoly} (shifted det) &
  \path{shiftedDet_factorises} & \path{L17_TracesAndLipschitz.lean} \\
Prop.~\ref{prop:traces} ($\tr L_{\mathrm{flat}}$) &
  \path{trace_laplacian_flat} & \path{L17_TracesAndLipschitz.lean} \\
Prop.~\ref{prop:traces} ($\tr L_{\mathrm{Mob}}$) &
  \path{trace_laplacian_mobius} & \path{L17_TracesAndLipschitz.lean} \\
Prop.~\ref{prop:traces2} ($\tr(\cdot^2)$) &
  \path{trace_sq_laplacian_decomposes} & \path{L17_TracesAndLipschitz.lean} \\
Prop.~\ref{prop:traces2} (Frobenius) &
  \path{frobenius_laplacian_decomposes} & \path{L17_TracesAndLipschitz.lean} \\
Prop.~\ref{prop:traces2} (polarisation) &
  \path{trace_mul_scalar_signed_eq} & \path{L17_TracesAndLipschitz.lean} \\
\bottomrule
\end{longtable}
}
\noindent{\footnotesize (File paths: \texttt{KernelDim.lean} abbreviates \texttt{KernelDimension.lean}.)\par}

\paragraph{Reproducibility.} The complete Lean and Python sources
live at
\url{https://github.com/jesusvilela/connection\_laplacian\_lean}
(concept DOI
\href{https://doi.org/10.5281/zenodo.19695396}{10.5281/zenodo.19695396},
which resolves to the latest archived release). Each archived release is
a snapshot of the repository at its tag. Release v.0.0.5 (2026-10-15;
version DOI
\href{https://doi.org/10.5281/zenodo.23401896}{10.5281/zenodo.23401896})
predates the full cycle-spectrum proofs and their comparator replay;
\path{.github/release-notes/} lists what each later release adds.
Release \href{https://github.com/jesusvilela/connection_laplacian_lean/releases/tag/v.0.0.6}{v.0.0.6}
(18 October 2026; commit \texttt{58fe64b}) is the historical archived
verification baseline. This manuscript also incorporates editorial and
explanatory corrections made on the original repository's \texttt{main}
branch through commit \texttt{ae64b5e} (2 November 2026). These
subsequent corrections should not be mistaken for changes to the
archived release's proof artifacts. The Lean 4.11.0 formalization remains
pinned; the newer Mathlib port is separate research work.
From the project root,
\begin{quote}
\verb|lake build|
\end{quote}
builds the pinned development (Mathlib~v4.11.0 +
\texttt{ConnectionLaplacian}). Invoking \verb|#print axioms| on a
listed name reports its axiom dependencies; it does not regenerate
the statement-to-file correspondence table above. Continuous
fuzz-sweeps now span five rounds of the discovery swarm. The R3/R4
baseline exhausts $176{,}169$ connection-graph configurations
($n\le 5$ exhaustive; $n\in\{6,7,8\}$ wrap-subset / random-graph);
R5 extends this to a $456{,}950$-configuration sweep at $n\le 7$
targeting the cover-charpoly and kernel-dimension identities; R6
Stage-2 \texttt{FUZZER-A} (\path{findings/round6/stage2_fuzzer_A/})
certifies the M6 multiset-union identity at $1.5\cdot 10^{-15}$
relative precision on $3{,}727$ iso-configurations at $n=6$ plus a
random $n=7$ sample; R6 Stage-6 \texttt{FUZZER-B}
(\path{findings/round6/stage6_fuzzer_B/}) cross-checks the
shifted-determinant, trace-square, Frobenius-norm and
cross-polarisation identities of L17 at $n=7$ ($300$ graphs,
$14{,}011$ probes, zero counterexamples). Across all rounds, the
only non-integer numerical deviations are $20$ out of $24{,}971$
configurations at $n=8$ that show a $10^{-3}$-order relative error
in evaluating $\operatorname{charpoly}(\widetilde L^{\mathrm{cov}})$
through the companion matrix (attributable to condition-number
growth, bounded by standard float-polynomial perturbation theory;
max deviation $7.3\cdot 10^{-3}$). The underlying Lean identity
\path{cover_charpoly_eq_scalar_times_mobius} is an exact
statement over $\ZZ[\lambda]$ and is unaffected. Fuzzer scripts and
JSON outputs live under
\texttt{findings/round\{3,4,5,6\}/}.

\paragraph{Counter-claims are also machine-shadowed.} Each
counter-example in \S\ref{sec:counter} (Examples~\ref{ex:naive-eq},
\ref{ex:bridge-wrap}, \ref{ex:cross-merge}, \ref{ex:contraction})
is emitted by the \texttt{NEGATOR} / \texttt{NEGATOR-FUZZY} passes
of the discovery swarm; the generating Python scripts live under
\path{findings/round3/negator/} and
\path{findings/round4/negator_fuzzy/} and can be re-run for any
$n\le 5$ (and $n=6$ with a wrap-subset cap) to regenerate the
counter-witnesses from scratch.

\begin{thebibliography}{99}

\bibitem{HararyCartwright}
F.~Harary.
\emph{On the notion of balance of a signed graph}.
Michigan Math.\ J.\ \textbf{2} (1953/54), 143--146.

\bibitem{Zaslavsky82}
T.~Zaslavsky.
\emph{Signed graphs}.
Discrete Appl.\ Math.\ \textbf{4} (1982), 47--74.

\bibitem{ZaslavskyMatrices}
T.~Zaslavsky.
\emph{Matrices in the Theory of Signed Simple Graphs}.
\href{https://arxiv.org/abs/1303.3083}{arXiv:1303.3083}, 2013,
Section~IV.D, Lemma~IV.2.

\bibitem{Chung}
F.~R.~K.~Chung.
\emph{Spectral Graph Theory},
CBMS Regional Conference Series in Mathematics~\textbf{92},
American Mathematical Society, Providence, 1997.

\bibitem{BiluLinial}
Y.~Bilu and N.~Linial.
\emph{Lifts, discrepancy and nearly optimal spectral gap}.
Combinatorica \textbf{26} (2006), 495--519.
Preprint: \emph{Constructing expander graphs by 2-lifts and discrepancy
vs.\ spectral gap},
\href{https://arxiv.org/abs/math/0312022}{arXiv:math/0312022}.

\bibitem{DiazDevriendtLambiotte}
F.~Diaz-Diaz, K.~Devriendt and R.~Lambiotte.
\emph{Gremban expansion for signed networks: algebraic and combinatorial
foundations for community--faction detection}.
\href{https://arxiv.org/abs/2509.14193}{arXiv:2509.14193}, 2025.

\bibitem{Gremban}
K.~D.~Gremban.
\emph{Combinatorial Preconditioners for Sparse, Symmetric, Diagonally
Dominant Linear Systems}.
PhD thesis, Carnegie Mellon University, 1996.
Technical report CMU-CS-96-123.

\bibitem{SpielmanTeng}
D.~A.~Spielman and S.-H.~Teng.
\emph{Nearly-linear time algorithms for preconditioning and solving
symmetric, diagonally dominant linear systems}.
\href{https://arxiv.org/abs/cs/0607105}{arXiv:cs/0607105}.

\bibitem{Mathlib}
The Mathlib Community.
\emph{The Lean Mathematical Library}.
In: \emph{CPP~2020 Proceedings}, 367--381, 2020.

\bibitem{Lean4}
L.~de~Moura and S.~Ullrich.
\emph{The Lean~4 theorem prover and programming language}.
In: \emph{CADE~28 Proceedings}, LNCS~12699, 625--635, 2021.

\end{thebibliography}

\end{document}