Reference: Kittel Ch.1-3, Ashcroft & Mermin Ch.4-5, International Tables for Crystallography Vol. A, MIT 8.231
- L1-L7: Complete
- L8: Partial+ (2/5 advanced topics: Ewald summation, Madelung constant)
- L9: Partial (documented, not implemented)
| Level | Name | Status | Key Items |
|---|---|---|---|
| L1 | Definitions | ✅ Complete | 14 Bravais lattices, 7 crystal systems, reciprocal lattice, Miller indices, structure factor, HS k-points |
| L2 | Core Concepts | ✅ Complete | Translational symmetry, sphere packing, extinction rules, crystallographic restriction theorem |
| L3 | Math Structures | ✅ Complete | Vector/matrix algebra, Rodrigues rotation, metric tensor, group representation |
| L4 | Fundamental Laws | ✅ Complete | Bragg's law, Laue condition, structure factor formula, Ewald summation |
| L5 | Algorithms | ✅ Complete | Lattice construction, d-spacing, WS cell, BZ reduction, XRD generation |
| L6 | Canonical Systems | ✅ Complete | SC/BCC/FCC/HCP/Diamond/NaCl/CsCl/ZnS/Perovskite/Fluorite/Graphite/Graphene |
| L7 | Applications | ✅ Complete | Powder XRD simulation, crystal ID, materials database (28 entries) |
| L8 | Advanced | ✅ Partial+ | Ewald summation, Madelung constant |
| L9 | Frontiers | ✅ Partial | Time crystals, ML prediction (documented) |
Line count: include/ (514) + src/ (5236) = 5750 lines ≥ 3000 ✅
| Definition | C struct / enum | Lean 4 |
|---|---|---|
| Bravais lattice (14 types) | bravais_lattice_t, bravais_lattice_type_t |
inductive BravaisLattice |
| Crystal system (7 types) | crystal_system_t |
inductive CrystalSystem |
| Reciprocal lattice | reciprocal_lattice_t |
(dual relation) |
| Miller indices | miller_indices_t |
structure MillerIndices |
| Structure factor | complex_double_t (S(G)) |
(formula) |
| Brillouin zone | brillouin_zone_t |
(WS cell of RL) |
| Wigner-Seitz cell | (geometric constructor) |
(Voronoi cell) |
| Symmetry operation | symmetry_op_t |
inductive SymmetryOpType |
| Point group (32 types) | point_group_t |
inductive PointGroup |
| Space group (230) | space_group_t (24 entries) |
structure SpaceGroup |
| Theorem | Formula | Implementation |
|---|---|---|
| Bragg's law | nλ = 2d sin θ | bragg_angle(), bragg_d_spacing() |
| Laue condition | Δk = G, G ∈ RL | laue_condition_check() |
| Structure factor | S(G) = Σ f_j e^{-iG·r_j} | structure_factor() |
| FCC extinction | S=0 unless all h,k,l same parity | structure_factor_fcc() |
| BCC extinction | S=0 unless h+k+l even | structure_factor_bcc() |
| Madelung energy | U = -α z⁺z⁻e²/4πε₀r₀ | madelung_constant_ewald() |
| Kepler conjecture | η_max = π/√18 ≈ 0.7405 | packing_fraction_fcc() |
| Crystallographic restriction | Only n=1,2,3,4,6 | isCrystallographicRotation (Lean) |
| Algorithm | Complexity | Function |
|---|---|---|
| Lattice construction (6 params) | O(1) | bravais_lattice_create() |
| Reciprocal lattice computation | O(1) | reciprocal_lattice() |
| d-spacing (all 7 systems) | O(1) | d_spacing_*() |
| Ewald summation | O(N³) | madelung_constant_ewald() |
| Wigner-Seitz cell (2D/3D) | O(N²) | wigner_seitz_construct_*() |
| BZ reduction (k-folding) | O(N) | brillouin_zone_reduce() |
| Ewald sphere search | O(N³) | ewald_sphere_intersections() |
| XRD pattern generation | O(N³) | xrd_pattern_create() |
| Structure factor (general) | O(N_atoms) | structure_factor() |
| Structure | Lattice | Basis | Implementation |
|---|---|---|---|
| SC (Po) | cP | 1 atom | PROTOTYPE_SC |
| BCC (Fe) | cI | 1 atom | PROTOTYPE_BCC |
| FCC (Cu) | cF | 1 atom | PROTOTYPE_FCC |
| HCP (Mg) | hP | 2 atoms | PROTOTYPE_HCP |
| Diamond (C) | cF | 2 atoms | PROTOTYPE_DIAMOND |
| NaCl | cF | 2 atoms | PROTOTYPE_NACL |
| CsCl | cP | 2 atoms | PROTOTYPE_CSCL |
| ZnS (zincblende) | cF | 2 atoms | PROTOTYPE_ZINCBLENDE |
| ZnS (wurtzite) | hP | 4 atoms | PROTOTYPE_WURTZITE |
| Perovskite (BaTiO₃) | cP | 5 atoms | PROTOTYPE_PEROVSKITE |
| Fluorite (CaF₂) | cF | 3 atoms | PROTOTYPE_FLUORITE |
| Graphite | hP | 4 atoms | PROTOTYPE_GRAPHITE |
| Graphene | hP | 2 atoms | PROTOTYPE_GRAPHENE |
| School | Course | Topics Covered |
|---|---|---|
| MIT | 8.231 Physics of Solids | Bravais lattices, reciprocal lattice, structure factor, BZ |
| Stanford | PHYSICS 370 CM | Crystal symmetry, XRD, reciprocal space |
| Berkeley | PHYS 231 Solid State | Lattice structures, diffraction, packing |
| Caltech | Ph 205 Solid State | Crystal lattices, reciprocal lattice |
| Princeton | PHY 525 CM | Bravais classification, BZ, WS cells |
| Cambridge | Part II Theo Phys | Crystal structure, symmetry, Madelung |
| Oxford | CMT Graduate | Group theory, reciprocal lattice, XRD |
| ETH | 402-0891 CM | Crystal symmetry, reciprocal space |
| Tokyo | 量子力学 · 統計力学 | Crystal fundamentals, Madelung sum |
cd mini-crystal-structure/
make test # Compile and run 61 assertion tests
make examples # Build 4 end-to-end examples
./examples/ex1_sc_bcc_fcc # SC, BCC, FCC comparison
./examples/ex2_nacl_xrd # NaCl powder XRD pattern
./examples/ex3_bravais_all # All 14 Bravais lattices
./examples/ex4_brillouin_zone # Brillouin zones for cubic lattices
make clean # Remove build artifactsmini-crystal-structure/
├── Makefile
├── README.md
├── include/
│ └── crystal_types.h (491 lines, all type definitions + API)
├── src/
│ ├── vec3_mat3.c (vector & matrix algebra, Rodrigues formula)
│ ├── bravais_lattice.c (14 Bravais lattices, 7 crystal systems)
│ ├── reciprocal_lattice.c (reciprocal lattice, duality)
│ ├── miller_indices.c (Miller indices, d-spacing all systems)
│ ├── bragg_law.c (Bragg's law, Laue condition, Ewald sphere)
│ ├── structure_factor.c (S(G), form factors, extinction rules)
│ ├── symmetry.c (symmetry ops, 32 point groups, 24 space groups)
│ ├── packing_fraction.c (η, z, d_nn for all canonical structures)
│ ├── brillouin_zone.c (BZ construction, k-point paths)
│ ├── wigner_seitz.c (WS cell 2D/3D, Voronoi)
│ ├── madlung_constant.c (Madelung direct + Ewald summation)
│ ├── xrd_pattern.c (powder XRD simulation)
│ ├── crystal_structure.c (13 archetypes, density, identification)
│ └── crystal_structure.lean (Lean 4 formalization, ~30 theorems)
├── tests/
│ └── test_crystal.c (61 assertion-based tests, all passing)
├── examples/
│ ├── ex1_sc_bcc_fcc.c (cubic lattices comparison)
│ ├── ex2_nacl_xrd.c (NaCl powder XRD pattern)
│ ├── ex3_bravais_all.c (all 14 Bravais lattices)
│ └── ex4_brillouin_zone.c (Brillouin zones, k-path conventions)
├── docs/
│ ├── cheatsheet.md
│ ├── knowledge-graph.md (L1-L9 coverage table)
│ ├── coverage-report.md (detailed assessment)
│ ├── gap-report.md (missing items + priorities)
│ ├── course-alignment.md (9-school mapping)
│ └── course-tree.md (prerequisites + postrequisites)
├── demos/
├── benches/
└── notebooks/
| Text | Author | Year | Key Chapters |
|---|---|---|---|
| Introduction to Solid State Physics | Kittel | 2004 | Ch.1-3, 9 |
| Solid State Physics | Ashcroft & Mermin | 1976 | Ch.4-5, 8-9 |
| International Tables for Crystallography | IUCr | Vol. A-C | All |
| Elements of X-ray Diffraction | Cullity & Stock | 2014 | Ch.2-5 |
| Space Groups for Solid State Scientists | Burns & Glazer | 2013 | Ch.1-5 |
| Group Theory: Application to Condensed Matter | Dresselhaus | 2007 | Ch.2 |