  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.