Project overview

lattice-system is a Lean 4 and mathlib formalization of lattice models. Its primary abstraction is a graph: finite lattices are graph instances, while infinite graphs remain available for the thermodynamic and continuum limits.

Browse the project

Formalization catalogue — browse by source or topic and find the complete interim catalogue.
Formalization-status publication — stable human/machine paths, generation architecture, and reproduction.
Current roadmap — active direction and the authoritative tracking Issues.
Limitations and documented axioms — current trust boundaries and deferred mathematical infrastructure.
Historical records — cumulative implementation history and deleted proof routes.
Mathematical proof guide — statements, motivation, and proof sketches.
Refactoring conventions

Formalization-status authority during migration

The complete hand-maintained catalogue under formalization/legacy/ is the interim authority for formalization status and capstone identification. The version 1 data contract and its JSON catalogue are a non-authoritative prototype. Issue #5228 alone performs the structured-data cutover after full migration and audit. Do not combine the prototype and legacy pages into competing ledgers.

Present coverage

The present implementation covers finite-volume classical and quantum spin systems, fermions and Hubbard-model infrastructure, and reusable finite matrix-analysis foundations. Infinite-volume, thermodynamic-limit, and continuum-limit work remains a central long-term goal rather than an excluded topic. The limitations page explains the policy for documented axioms; complete declaration-level axiom occurrences remain in the interim legacy catalogue until #5228.

API documentation generation with doc-gen4 remains disabled because its former CI job was prohibitively slow. Formalization-status publication is a separate project tracked by #5229.

Project resources

Former index fragments

Every former section fragment remains an explicit landing-page stub. Each stub links to the section’s new purpose-specific home.

Design axis: graphs, not lattices

Refactoring conventions and review criteria

Deleted routes: what this index used to document

Appendix A: status and axiomatization policy

Formalized theorems

Single-site Pauli operators

Spin-1/2 operators (Tasaki §2.1)

Spin-1/2 rotation operators (Tasaki §2.1 eq. (2.1.26))

3D rotation matrices R^(α)_θ (general θ, Tasaki §2.1 eq. (2.1.11))

Z₂ × Z₂ representation (Tasaki §2.1 eqs. (2.1.27)-(2.1.34))

3D rotation matrices R^(α)_π (Tasaki §2.1 eq. (2.1.28))

Pauli-basis decomposition (Tasaki §2.1 Problem 2.1.a, S = 1/2)

Polynomial-basis decomposition for S = 1 (Tasaki §2.1 Problem 2.1.a, S = 1)

S = 1 matrix representations (Tasaki §2.1 eq. (2.1.9))

Spin-S operators (general S ≥ 0, parameterised by N = 2S : ℕ)

Basis states and raising/lowering (Tasaki §2.1)

Basis states and raising/lowering for S = 1 (Tasaki §2.1)

Time-reversal map for S = 1/2 (Tasaki §2.3)

Multi-body operator space (abstract lattice)

Generic matrix-analysis helpers (Math/MatrixAnalysis/)

Horsch–von der Linden low-lying states (Tasaki §3.4, Theorem 3.1)

Bose–Einstein condensation of hard-core bosons (Tasaki §5.1–§5.2)

Antiferromagnetic Heisenberg chains and the Haldane conjecture (Tasaki §6.1)

The AKLT model (Tasaki §7.1)

Total spin operator (Tasaki §2.2 eq. (2.2.7), (2.2.8))

Two-site spin inner product (Tasaki §2.2 eq. (2.2.16))

One-dimensional open-chain quantum Ising

Testing infrastructure

Gibbs state (Tasaki §3.3)

Heisenberg chain (Tasaki §3.5)

Perron-Frobenius theorem (Math/PerronFrobenius.lean, Math/PerronFrobeniusPrimitive.lean, Math/CollatzWielandt.lean, Math/PerronFrobeniusMain.lean)

Spin-S Marshall–Lieb–Mattis on the magnetization sector (Tasaki §2.5 Theorem 2.2 generic S, sector form)

Spin-S saturated ferromagnetic state (Tasaki §2.4 generalised)

Single-mode fermion (P2 skeleton)

Multi-mode fermion via Jordan–Wigner (P2 backbone)

Fock space representation and Slater determinants (Tasaki §9.2.3)

Hubbard spin symmetry — full SU(2) invariance (Tasaki §9.3.3)

Hubbard all-up-spin state and saturated ferromagnetism (Tasaki §11.1.1)

Hubbard hard-core subspace (Tasaki §11.2)

Hubbard hard-core projection (Tasaki §11.2)

Hubbard one-hole hard-core basis states (Tasaki §11.2)

Jordan–Wigner string action on basis states (Tasaki §11.2 infrastructure)

Span of the one-hole hard-core sector (Tasaki §11.2, footnote 8)

Hole-filling hop configuration (Tasaki §11.2, eq. (11.2.4) spatial content)

Degenerate perturbation theory: second-order effective Hamiltonian (Tasaki §10.1, Lemma 10.1)

Lieb’s theorem for the attractive Hubbard model (Tasaki §10.2.1, Theorems 10.2 & 10.3)

Spin-reflection-positivity foundation for Lieb’s theorem (Tasaki §10.2.1, PR1 toward discharging Theorem 10.2)

Lieb’s theorem for the repulsive Hubbard model at half-filling (Tasaki §10.2.2, Theorem 10.4)

Kubo–Kishi finite-temperature susceptibility bound (Tasaki §10.2.5, Theorem 10.11, AXIOM)

Hubbard effective Hamiltonian on the hard-core sector (Tasaki §11.2)

Tasaki ordered-creation basis (Tasaki §11.2, eq. (11.2.3))

Uniform-sign hole-filling action (Tasaki §11.2, eq. (11.2.4))

Effective-Hamiltonian matrix element (Tasaki §11.2, eq. (11.2.5))

Cauchy–Schwarz energy bound (Tasaki §11.2, eq. (11.2.9))

SU(2) symmetry of the effective Hamiltonian (Tasaki §11.2)

Weak Nagaoka spin multiplet (Tasaki §11.2.1, Theorem 11.5 core)

Nagaoka’s theorem on a magnetization sector (Tasaki §11.2.2, Theorem 11.7 / Lemma 11.9)

General flat-band ground states: the annihilation peel behind eq. (11.3.46) (Tasaki §11.3.4)

Continuum-limit roadmap

Open items / axioms

~~TODO (P1d’’’) — Problem 2.1.a for general S ≥ 1~~ DONE

~~TODO — Tasaki Problem 2.2.c (SU(2) non-invariance / averaged state)~~ DONE

Tasaki §2.5 antiferromagnetic status (issues #240, #412)

TODO — remove remaining 7 per-theorem linter suppressions (issue #377)