semiconductorPhysicsCert
plain-language theorem explainer
semiconductorPhysicsCert bundles the three numerical facts that define semiconductor physics inside Recognition Science: five device types, two carrier species, and eight crystal symmetries. A materials physicist citing RS derivations would reference this certificate to ground device taxonomy and lattice symmetry counts. The definition assembles the record directly from three decide lemmas that compute the cardinalities and equalities.
Claim. The semiconductor physics certificate asserts that the number of canonical semiconductor devices is five, the number of carrier types equals three minus one, and the number of crystal symmetries equals eight.
background
The module SemiconductorPhysicsFromRS derives semiconductor properties from the Recognition Science dimension D. The structure SemiconductorPhysicsCert collects three relations: the cardinality of SemiconductorDevice equals five, carrierTypes equals three minus one, and crystalSymmetries equals eight. These arise because five device types match configDim D, two carriers match D minus one, and eight symmetries match two to the power D. The upstream theorems semiconductorDeviceCount, carrierTypes_eq_Dminus1, and crystalSymmetries_8 each establish one equality by direct decision.
proof idea
The definition constructs an instance of SemiconductorPhysicsCert by setting the five_devices field to the theorem semiconductorDeviceCount, the two_carriers field to carrierTypes_eq_Dminus1, and the eight_syms field to crystalSymmetries_8. Each supplying theorem is proved by a single decide tactic that evaluates the finite cardinalities and arithmetic equalities.
why it matters
This definition supplies the complete certificate for the semiconductor-physics module, confirming that RS reproduces the standard counts of devices, carriers, and symmetries. It closes the derivation that starts from the forced spatial dimension D in the unified forcing chain and the eight-tick octave. The certificate stands ready for use in higher-level RS materials or device models, although no downstream applications are recorded in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.