Kernel Dimension of the Z/2 Connection Laplacian on a Finite Simple Graph (A Formalisation in Lean 4 / Mathlib v4.11.0)
Source: hexagonmath.org/abs/2611.00061v1
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/hexagon/2611.00061
curl -X POST /api/v1/records/hexagon/2611.00061/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/hexagon/2611.00061/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'