From e23c909b0d64fa83342fdba72fda1fabc1696bad Mon Sep 17 00:00:00 2001 From: Wahaj Ayub Date: Mon, 10 Aug 2026 12:12:40 -0700 Subject: [PATCH] Add initial condensed matter directory structure Co-authored-by: OpenAI GPT-5.6 Pro --- Physlib.lean | 6 ++++ Physlib/CondensedMatter/BandTheory/Basic.lean | 18 +++++++++++ Physlib/CondensedMatter/Basic.lean | 30 ++++++++++++------- Physlib/CondensedMatter/Crystal/Basic.lean | 17 +++++++++++ .../CondensedMatter/LatticeModels/Basic.lean | 18 +++++++++++ Physlib/CondensedMatter/ManyBody/Basic.lean | 17 +++++++++++ Physlib/CondensedMatter/Response/Basic.lean | 17 +++++++++++ Physlib/CondensedMatter/Topology/Basic.lean | 19 ++++++++++++ 8 files changed, 131 insertions(+), 11 deletions(-) create mode 100644 Physlib/CondensedMatter/BandTheory/Basic.lean create mode 100644 Physlib/CondensedMatter/Crystal/Basic.lean create mode 100644 Physlib/CondensedMatter/LatticeModels/Basic.lean create mode 100644 Physlib/CondensedMatter/ManyBody/Basic.lean create mode 100644 Physlib/CondensedMatter/Response/Basic.lean create mode 100644 Physlib/CondensedMatter/Topology/Basic.lean diff --git a/Physlib.lean b/Physlib.lean index 5d704d893..983891a6f 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -28,9 +28,15 @@ public import Physlib.ClassicalMechanics.Scattering.RigidSphere public import Physlib.ClassicalMechanics.Vibrations.LinearTriatomic public import Physlib.ClassicalMechanics.WaveEquation.Basic public import Physlib.ClassicalMechanics.WaveEquation.HarmonicWave +public import Physlib.CondensedMatter.BandTheory.Basic public import Physlib.CondensedMatter.Basic +public import Physlib.CondensedMatter.Crystal.Basic +public import Physlib.CondensedMatter.LatticeModels.Basic +public import Physlib.CondensedMatter.ManyBody.Basic +public import Physlib.CondensedMatter.Response.Basic public import Physlib.CondensedMatter.Thermoelectric.Basic public import Physlib.CondensedMatter.TightBindingChain.Basic +public import Physlib.CondensedMatter.Topology.Basic public import Physlib.Cosmology.Basic public import Physlib.Cosmology.FLRW.Basic public import Physlib.Cosmology.FLRW.ConformalTime diff --git a/Physlib/CondensedMatter/BandTheory/Basic.lean b/Physlib/CondensedMatter/BandTheory/Basic.lean new file mode 100644 index 000000000..19bcd9c42 --- /dev/null +++ b/Physlib/CondensedMatter/BandTheory/Basic.lean @@ -0,0 +1,18 @@ +/- +Copyright (c) 2026 Wahaj Ayub. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Wahaj Ayub +-/ +module + +/-! + +# A. Band theory + +This module provides a home for the theory of Bloch Hamiltonians and states, band projectors, +energy bands and gaps, and band geometry. Generic quantum-mechanical infrastructure should be +reused from Physlib rather than redefined here. + +-/ + +@[expose] public section diff --git a/Physlib/CondensedMatter/Basic.lean b/Physlib/CondensedMatter/Basic.lean index 837df4a87..19957a492 100644 --- a/Physlib/CondensedMatter/Basic.lean +++ b/Physlib/CondensedMatter/Basic.lean @@ -7,17 +7,25 @@ module /-! -# Condensed Matter +# A. Condensed matter -This directory is currently a place holder. -Please feel free to contribute! +Condensed matter physics studies the collective behavior of matter, from crystalline structure +and lattice models to interacting phases, topology, and material response. -Some directories which are NOT currently place holders are: -- Mathematics -- Meta -- Particles -- QFT -- Quantum Mechanics -- Relativity +## A.1. Scope --/@[expose] public section +- `Crystal` covers crystal structures, reciprocal-space descriptions, symmetries, and dynamics. +- `LatticeModels` covers Hamiltonian models whose degrees of freedom live on lattices. +- `BandTheory` covers Bloch descriptions, energy bands, gaps, and band geometry. +- `ManyBody` covers correlations, quasiparticles, Green functions, and interacting matter. +- `Topology` covers topological phases and invariants in condensed matter systems. +- `Response` covers transport and the linear, optical, and nonlinear response of materials. + +## A.2. Existing modules + +Existing condensed-matter modules currently include `TightBindingChain` and `Thermoelectric`. +They remain in their existing locations and have not been reorganized into the scopes above. + +-/ + +@[expose] public section diff --git a/Physlib/CondensedMatter/Crystal/Basic.lean b/Physlib/CondensedMatter/Crystal/Basic.lean new file mode 100644 index 000000000..bce17b51d --- /dev/null +++ b/Physlib/CondensedMatter/Crystal/Basic.lean @@ -0,0 +1,17 @@ +/- +Copyright (c) 2026 Wahaj Ayub. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Wahaj Ayub +-/ +module + +/-! + +# A. Crystals + +This module provides a home for Bravais and reciprocal lattices, unit cells, crystal momentum, +Brillouin zones, crystalline symmetries, and lattice dynamics. + +-/ + +@[expose] public section diff --git a/Physlib/CondensedMatter/LatticeModels/Basic.lean b/Physlib/CondensedMatter/LatticeModels/Basic.lean new file mode 100644 index 000000000..4912efc24 --- /dev/null +++ b/Physlib/CondensedMatter/LatticeModels/Basic.lean @@ -0,0 +1,18 @@ +/- +Copyright (c) 2026 Wahaj Ayub. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Wahaj Ayub +-/ +module + +/-! + +# A. Lattice models + +This module provides a home for hopping Hamiltonians, tight-binding and Hubbard-type models, +and spin lattice models. A future design issue is the relation between real-space lattice +Hamiltonians and momentum-space Bloch Hamiltonians. + +-/ + +@[expose] public section diff --git a/Physlib/CondensedMatter/ManyBody/Basic.lean b/Physlib/CondensedMatter/ManyBody/Basic.lean new file mode 100644 index 000000000..3da1460ed --- /dev/null +++ b/Physlib/CondensedMatter/ManyBody/Basic.lean @@ -0,0 +1,17 @@ +/- +Copyright (c) 2026 Wahaj Ayub. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Wahaj Ayub +-/ +module + +/-! + +# A. Many-body physics + +This module provides a home for correlation functions, quasiparticles, Green functions, +mean-field descriptions, and interacting quantum matter. + +-/ + +@[expose] public section diff --git a/Physlib/CondensedMatter/Response/Basic.lean b/Physlib/CondensedMatter/Response/Basic.lean new file mode 100644 index 000000000..26f3e497e --- /dev/null +++ b/Physlib/CondensedMatter/Response/Basic.lean @@ -0,0 +1,17 @@ +/- +Copyright (c) 2026 Wahaj Ayub. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Wahaj Ayub +-/ +module + +/-! + +# A. Response + +This module provides a home for electrical and thermal transport, linear and thermoelectric +response, optical response, and nonlinear response. + +-/ + +@[expose] public section diff --git a/Physlib/CondensedMatter/Topology/Basic.lean b/Physlib/CondensedMatter/Topology/Basic.lean new file mode 100644 index 000000000..05e2a0eef --- /dev/null +++ b/Physlib/CondensedMatter/Topology/Basic.lean @@ -0,0 +1,19 @@ +/- +Copyright (c) 2026 Wahaj Ayub. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Wahaj Ayub +-/ +module + +/-! + +# A. Topological condensed matter + +This module provides a home for topological invariants of bands, Chern and topological +insulators, Weyl and nodal semimetals, topological superconductors, symmetry-protected phases, +and interacting topological phases. It distinguishes local band geometry from global +topological invariants. + +-/ + +@[expose] public section