brillouinKPoints
plain-language theorem explainer
The definition sets the number of k-points sampling the first Brillouin zone of a cubic lattice to exactly 8. Solid-state physicists using the Recognition Science framework cite it when mapping the eight vertices of the Q₃ cube to discrete momentum points in three dimensions. The assignment is a direct equating of the natural number 2 raised to the power 3 with no lemmas or tactics required.
Claim. The number of k-points in the first Brillouin zone of a cubic lattice is defined by $N_k := 2^3$.
background
The module treats solid-state physics as five canonical phenomena (band structure, phonons, magnetism, superconductivity, topology) corresponding to configDim D = 5. In this setting the crystal lattice is identified with the 8-vertex cube Q₃ whose first Brillouin zone is sampled at its eight symmetry-equivalent points. The definition therefore records the relation 8 k-points = 2^D that follows from the spatial dimension count.
proof idea
This is a direct definition that equates the constant to the result of natural-number exponentiation 2^3. No lemmas are applied and the body contains no tactics.
why it matters
The definition supplies the concrete integer required by the downstream SolidStatePhysicsCert structure, which pairs it with the count of five phenomena. It realizes the module statement that 8 k-points = 2^D, thereby connecting the cubic lattice to the eight-tick octave and D = 3 in the forcing chain. The companion theorem brillouinKPoints_8 later confirms the equality by decision.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.