lattice-system

Complete interim formalization catalogue

Interim authority. These pages are a lossless partition of the former docs/index.md theorem catalogue. They remain authoritative for formalization status and capstone identification until Issue #5228 performs the audited structured-data cutover. The version 1 JSON records are still a non-authoritative prototype.

The partition is source-neutral where the old heading mixed Tasaki results, external references, and project-original infrastructure. No item was reclassified during this mechanical move. Each original catalogue data row occurs in exactly one chunk; repeated table headers are presentation only.

Formalized theorems

The catalogue below includes proved results, conditional results, and documented axioms as recorded, with zero sorry. Full mathematical statements and proof sketches are in tex/proof-guide.tex.

The formalization-status data contract and its representative version 1 catalogue are available for review. The catalogue is a non-authoritative prototype until the governance cutover tracked by issue #5228; this page remains the current formalization-status and capstone authority during migration.

Catalogue groups

Spin foundations and Tasaki Chapter 2

• 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/)
• Total spin operator (Tasaki §2.2 eq. (2.2.7), (2.2.8)) — part 1 of 5
• Total spin operator (Tasaki §2.2 eq. (2.2.7), (2.2.8)) — part 2 of 5
• Total spin operator (Tasaki §2.2 eq. (2.2.7), (2.2.8)) — part 3 of 5
• Total spin operator (Tasaki §2.2 eq. (2.2.7), (2.2.8)) — part 4 of 5
• Total spin operator (Tasaki §2.2 eq. (2.2.7), (2.2.8)) — part 5 of 5
• Two-site spin inner product (Tasaki §2.2 eq. (2.2.16))
• Spin-S Marshall–Lieb–Mattis on the magnetization sector (Tasaki §2.5 Theorem 2.2 generic S, sector form) — part 1 of 4
• Spin-S Marshall–Lieb–Mattis on the magnetization sector (Tasaki §2.5 Theorem 2.2 generic S, sector form) — part 2 of 4
• Spin-S Marshall–Lieb–Mattis on the magnetization sector (Tasaki §2.5 Theorem 2.2 generic S, sector form) — part 3 of 4
• Spin-S Marshall–Lieb–Mattis on the magnetization sector (Tasaki §2.5 Theorem 2.2 generic S, sector form) — part 4 of 4
• Spin-S saturated ferromagnetic state (Tasaki §2.4 generalised) — part 1 of 2
• Spin-S saturated ferromagnetic state (Tasaki §2.4 generalised) — part 2 of 2

Spin models, Chapters 3–7, and spectral tools

• Horsch–von der Linden low-lying states (Tasaki §3.4, Theorem 3.1) — part 1 of 2
• Horsch–von der Linden low-lying states (Tasaki §3.4, Theorem 3.1) — part 2 of 2
• 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)
• One-dimensional open-chain quantum Ising
• Gibbs state (Tasaki §3.3)
• Heisenberg chain (Tasaki §3.5) — part 1 of 2
• Heisenberg chain (Tasaki §3.5) — part 2 of 2
• Perron-Frobenius theorem (Math/PerronFrobenius.lean, Math/PerronFrobeniusPrimitive.lean, Math/CollatzWielandt.lean, Math/PerronFrobeniusMain.lean)

Project infrastructure

• Testing infrastructure

Fermions and Hubbard models

• Single-mode fermion (P2 skeleton)
• Multi-mode fermion via Jordan–Wigner (P2 backbone) — part 1 of 4
• Multi-mode fermion via Jordan–Wigner (P2 backbone) — part 2 of 4
• Multi-mode fermion via Jordan–Wigner (P2 backbone) — part 3 of 4
• Multi-mode fermion via Jordan–Wigner (P2 backbone) — part 4 of 4