Add initial condensed matter directory structure

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

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

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

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

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

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

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

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