bandGap
plain-language theorem explainer
bandGap(k) assigns the k-th energy level on the phi-ladder to phi^k in RS-native units. Solid-state physicists working from the Recognition Science derivation of band structure cite it when scaling semiconductor gaps from the self-similar fixed point. The declaration is a direct one-line assignment with no lemmas or reduction steps.
Claim. The band gap at rung $k$ equals $phi^k$.
background
Recognition Science generates discrete scales on the phi-ladder, where phi is the self-similar fixed point forced at T6. The module derives five solid-state phenomena from configDim D=5, modeling the crystal lattice as the 8-vertex cube Q3 and placing eight k-points in the first Brillouin zone via 2^D=8. Band gaps are stated as Delta E = phi^k times hbar omega, here normalized to the pure power.
proof idea
This is a direct definition that assigns bandGap k to the expression phi raised to k. No upstream lemmas are invoked; the body is an abbreviation matching the identical declaration in SemiconductorBandStructureFromConfigDim.
why it matters
The definition supplies the expression required by SemiconductorCert, bandGap_pos, and bandGap_ratio in the semiconductor module. It realizes the phi-ladder contribution to the five phenomena listed in the module doc-comment and connects to the T5 J-uniqueness and T7 eight-tick octave steps of the forcing chain. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.