SemiconductorType
plain-language theorem explainer
SemiconductorType enumerates the five canonical semiconductor configurations in the Recognition Science model, each aligned to a distinct slot on the phi-ladder for band-gap placement. Solid-state physicists using configDim = 5 cite the enumeration when classifying intrinsic, doped, compensated, and degenerate cases. The declaration is a direct inductive definition that derives Fintype to support immediate cardinality and decidability results.
Claim. The type of semiconductor configurations consists of five elements: intrinsic, n-type doped, p-type doped, compensated, and degenerate. These label the distinct band structures admitted when configDim equals 5.
background
The module Semiconductor Band Structure from configDim treats band-gap energies as lying on the phi-ladder, with the number of admissible types fixed by configDim D = 5. The five types are intrinsic (undoped lattice), n-type doped (excess electrons), p-type doped (excess holes), compensated (balanced donor-acceptor), and degenerate (Fermi level inside a band). No upstream lemmas are required; the definition stands alone before the certificate that records the phi-ratio and positivity properties.
proof idea
The declaration is an inductive definition that introduces the five constructors and derives DecidableEq, Repr, BEq, and Fintype in a single line.
why it matters
SemiconductorType supplies the carrier type for SemiconductorCert, which asserts Fintype.card SemiconductorType = 5 together with the phi-ratio bandGap(k+1)/bandGap k = phi and strict positivity of every gap. It therefore anchors the solid-state sector of the Recognition Science framework at the point where configDim meets the phi-ladder, directly supporting the five-type classification required by the B15 depth.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.