brillouinKPoints
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the k-point count from the phi-ladder or J-cost.
- Does not treat non-cubic lattices or dimensions other than three.
- Does not compute band gaps, dispersion relations, or dynamical quantities.
Lean usage
theorem brillouinKPoints_8 : brillouinKPoints = 8 := by decideformal statement (Lean)
30def brillouinKPoints : ℕ := 2 ^ 3