IndisputableMonolith.Materials.SemiconductorDopantTypesFromConfigDim

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Semiconductor Dopant Types from configDim — B15 Solid-State Depth
   6
   7Five canonical dopant categories for silicon-type semiconductors
   8(= configDim D = 5):
   9  group-V donor (P, As, Sb), group-III acceptor (B, Al, Ga),
  10  deep-level impurity, compensating, transition-metal scattering
  11  center.
  12
  13Lean status: 0 sorry, 0 axiom.
  14-/
  15
  16namespace IndisputableMonolith.Materials.SemiconductorDopantTypesFromConfigDim
  17
  18inductive DopantType where
  19  | groupVDonor
  20  | groupIIIAcceptor
  21  | deepLevel
  22  | compensating
  23  | transitionMetal
  24  deriving DecidableEq, Repr, BEq, Fintype
  25
  26theorem dopantType_count : Fintype.card DopantType = 5 := by decide
  27
  28structure SemiconductorDopantCert where
  29  five_types : Fintype.card DopantType = 5
  30
  31def semiconductorDopantCert : SemiconductorDopantCert where
  32  five_types := dopantType_count
  33
  34end IndisputableMonolith.Materials.SemiconductorDopantTypesFromConfigDim
  35