theorem
proved
solidStatePhenomenonCount
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.SolidStatePhysicsFromRS on GitHub at line 27.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
24 | bandStructure | phonons | magnetism | superconductivity | topology
25 deriving DecidableEq, Repr, BEq, Fintype
26
27theorem solidStatePhenomenonCount : Fintype.card SolidStatePhenomenon = 5 := by decide
28
29/-- 8 k-points in Brillouin zone = 2^3. -/
30def brillouinKPoints : ℕ := 2 ^ 3
31theorem brillouinKPoints_8 : brillouinKPoints = 8 := by decide
32
33noncomputable def bandGap (k : ℕ) : ℝ := phi ^ k
34
35structure SolidStatePhysicsCert where
36 five_phenomena : Fintype.card SolidStatePhenomenon = 5
37 eight_kpoints : brillouinKPoints = 8
38
39def solidStatePhysicsCert : SolidStatePhysicsCert where
40 five_phenomena := solidStatePhenomenonCount
41 eight_kpoints := brillouinKPoints_8
42
43end IndisputableMonolith.Physics.SolidStatePhysicsFromRS