semiconductorDeviceCount
plain-language theorem explainer
The theorem establishes that the finite set of canonical semiconductor devices under Recognition Science contains exactly five elements. Device physicists modeling RS-derived electronics would cite this enumeration when classifying configurations against configDim D. The proof is a one-line decision procedure that exhausts the inductive definition of the device type.
Claim. The cardinality of the finite type of semiconductor devices satisfies $|SemiconductorDevice| = 5$, where the devices are the diode, BJT, MOSFET, JFET, and IGBT.
background
The module defines an inductive type SemiconductorDevice with five constructors: diode, bjt, mosfet, jfet, igbt, deriving Fintype. This count is identified with configDim D = 5. The module states that two carrier types equal D minus one and eight crystal symmetries equal two to the power D, with band gaps placed on the phi-ladder. Upstream carrier definitions set frequencies to five phi hertz in related engineering modules, though the cardinality rests directly on the Fintype instance of the inductive type.
proof idea
The proof is a one-line wrapper that invokes the decide tactic to compute the cardinality of the finite inductive type SemiconductorDevice.
why it matters
This result supplies the five_devices field in the SemiconductorPhysicsCert definition, which also incorporates the two-carrier and eight-symmetry relations. It realizes the claim that five device types equal configDim D = 5 within the RS framework, linking to the phi-ladder for band gaps and the eight-tick octave for symmetries. The parent theorem semiconductorPhysicsCert bundles these facts for certification of semiconductor physics derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.