DopantType
The declaration introduces an inductive type that enumerates five dopant categories for silicon semiconductors under configDim equal to five. Materials physicists classifying impurity effects on carrier density cite this enumeration when building device models. It is realized as a direct inductive construction that derives decidable equality, representation, boolean equality, and finite type structure automatically.
claimThe set of canonical dopant types in silicon semiconductors consists of group-V donors, group-III acceptors, deep-level impurities, compensating impurities, and transition-metal scattering centers.
background
The module treats semiconductor modeling when the configuration dimension equals five, corresponding to silicon-type systems. It enumerates five categories: group-V donors (P, As, Sb), group-III acceptors (B, Al, Ga), deep-level impurities, compensating impurities, and transition-metal scattering centers. These categories classify how impurities modify electrical behavior in the Recognition Science materials layer.
proof idea
The declaration is an inductive definition with five constructors and derives the instances DecidableEq, Repr, BEq, and Fintype automatically with no proof body or lemmas applied.
why it matters in Recognition Science
This definition supplies the type whose cardinality is fixed at five in the downstream theorem dopantType_count and the structure SemiconductorDopantCert. It anchors the materials section to the configDim = 5 case, consistent with the framework's assignment of D = 3 spatial dimensions to material classification. No open questions or scaffolding are indicated.
scope and limits
- Does not assign ionization energies or energy levels to any category.
- Does not derive transport equations or scattering rates.
- Does not connect the types to the J-cost function or phi-ladder.
- Does not specify numerical dopant concentrations or temperature dependence.
formal statement (Lean)
18inductive DopantType where
19 | groupVDonor
20 | groupIIIAcceptor
21 | deepLevel
22 | compensating
23 | transitionMetal
24 deriving DecidableEq, Repr, BEq, Fintype
25