SemiconductorPhysicsCert
plain-language theorem explainer
This structure definition bundles three numerical identities that connect semiconductor device taxonomy to the Recognition Science dimension D=3. A solid-state physicist deriving materials properties from the forcing chain would cite it to confirm that five device types, two carrier species, and eight crystal symmetries follow directly from T8 without extra parameters. The declaration is introduced by direct structure definition, with each field populated by sibling computations of cardinalities and equalities.
Claim. The structure certifying semiconductor physics from RS asserts that the set of canonical devices has cardinality 5, the number of carrier types equals $D-1=2$, and the number of crystal symmetry operations equals $2^D=8$.
background
In the Recognition Science framework, semiconductor physics is derived from the dimension D=3 fixed by the eight-tick octave in the forcing chain (T8). The module introduces an inductive type with five constructors (diode, BJT, MOSFET, JFET, IGBT) whose Fintype cardinality supplies the device count. Carrier types are defined as the constant 2, matching D-1, while crystal symmetries are defined as 2^3=8 to match zincblende operations. Upstream results supply the constants carrierTypes := 2 and crystalSymmetries := 2^3, anchoring the certification to the dimension count.
proof idea
This declaration is a structure definition that packages three equalities. It relies on the inductive definition of the device type to obtain Fintype.card = 5, the definition of carrierTypes as 2 (which equals 3-1), and the definition of crystalSymmetries as 8. No tactics are applied; the structure simply records the identities for downstream instantiation.
why it matters
This structure supplies the type for the downstream semiconductorPhysicsCert definition, which populates it via lemmas computing the device count, the D-1 carrier equality, and the 2^D symmetry count. It directly encodes the module claim that five device types equal configDim D=5, two carriers equal D-1, and eight symmetries equal 2^D, linking T8 to concrete device taxonomy and the phi-ladder band-gap approximation. It closes a narrow bridge from abstract forcing to materials physics with no remaining scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.