Graph theory and algorithms
Periodic Signings of C_n(1,2): An Exact Band Edge and Short-Period Classification
Abstract
We study spectral-radius optimization for periodic real signings of the 4-regular circulants C_n(1,2). After gauging all step-1 edges positive, a period-8 triangle-flux pattern produces an explicit 8 × 8 Hermitian Bloch symbol. Its upper band edge occurs at phase z = 1, and the associated infinite operator and every finite quotient C_(8q)(1,2) have the same spectral radius, where t₀ is the largest root displayed below:
√t₀ = 2.7936044933…, t₀⁴ − 16t₀³ + 76t₀² − 96t₀ + 16 = 0.
The proof uses an exact Bloch determinant, rational Sturm certificates, and monotonicity on the full unit-circle phase interval. Independently, a symmetry-reduced certificate classifies all triangle-flux patterns of fundamental period at most 16: the period-8 pattern is the unique norm minimizer up to rotation, reflection, and global flux complement. As an application, its radius is strictly below Suvagiya's proposed twisted-class value for every n = 8q ≥ 32, disproving the corresponding signed-circulant minimum conjecture on an infinite arithmetic progression. All decisive comparisons and classification witnesses are exact; floating-point linear algebra is used only for discovery and stress testing.
Contribution
Uses exact spectral certificates to study a period-eight signing and classify short-period minimizers.
Formalization scope
formalized with stated exclusionsWhat Lean checks
The period-8 flux word and signed circulant adjacency, exact rational sum-of-squares certificates for |vᵀAv| ≤ (1397/500)|v|², the eigenvalue bound, strict comparison with the proposed twisted-class value for n ≥ 32, and the bundled disproof. Supporting results include the Bloch symbol, determinant expansion, and all-phase algebraic band-edge certificate.
What it does not check
The identification of the common spectral radius with √t₀ in both directions, the infinite operator and direct integral, Sturm’s theorem, and the exhaustive short-period classification (Theorem 4.1) are not formalized. The abstract describes the archived manuscript; the scope above describes the later pinned companion.
This scope is reconciled with the hosted manuscript and pinned project README. The mathematical statements and assumptions in the source determine what the formalization establishes; manuscript revisions may clarify the interpretation of the same proof artifact.
- Source commit
9437c5e5ba09d6ba95285eaac4532414a84923e1- Toolchain
leanprover/lean4:v4.30.0
Reproduce the formalization
git clone https://github.com/lennrt/palomar-formalizations.git cd palomar-formalizations git checkout 9437c5e5ba09d6ba95285eaac4532414a84923e1 cd zenodo-21892995/palomar lake exe cache get lake build
See the project README for the complete setup, dependencies, and selected declarations.
Citation & version
Lennart Rudolph. (2026). Periodic Signings of C_n(1,2): An Exact Band Edge and Short-Period Classification. v1.0.0. Zenodo. https://doi.org/10.5281/zenodo.21892995.
View and copy BibTeX
- Hosted manuscript
- v1.0.0 ·
- Version DOI
- 10.5281/zenodo.21892995
- All versions DOI
- 10.5281/zenodo.21892994
- Manuscript license
- Creative Commons Attribution 4.0 International
Manuscript file integrity
SHA-256 of this exact hosted PDF:
54505655186fdd68de915213a6b6bc4be75274984cb595ca4d067df6691b220a