IndisputableMonolith.Physics.SemiconductorBandStructureFromConfigDim
This module defines semiconductor types, band gaps, and certification predicates derived from configuration dimension in Recognition Science. It builds directly on the RS time quantum imported from Constants. Condensed-matter researchers applying the framework to materials would reference these objects. The module contains only definitions and no proofs.
claimSemiconductorType is an enumeration; bandGap and bandGap_ratio map configuration dimension to energy gaps $E_g$; SemiconductorCert is the predicate certifying valid band-gap ratios.
background
The module imports the RS time quantum τ₀ = 1 tick from Constants. It introduces SemiconductorType, semiconductorType_count, bandGap, bandGap_ratio, bandGap_pos, SemiconductorCert, and semiconductorCert as the core objects for band-structure derivation from configuration dimension. The local setting is the physics domain of Recognition Science, where all quantities are expressed in RS-native units.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the semiconductor band-structure layer that later physics results can cite; no parent theorems are listed in the used-by graph yet.
scope and limits
- Does not contain any theorems or proofs.
- Does not import modules beyond Mathlib and Constants.
- Does not define numerical values for band gaps.
- Does not connect to the J-cost or phi-ladder machinery.