EMSpectrumCert
plain-language theorem explainer
The EMSpectrumCert structure packages three assertions: the electromagnetic band set has cardinality five, successive frequencies form a geometric sequence with common ratio phi, and the cortical carrier frequency lies in the open interval (8,9). Physicists constructing Recognition Science models of the spectrum would cite this certificate when linking the five phi-decades to the configuration dimension D=5. The declaration is a plain structure definition with no proof obligations or computational content.
Claim. A certificate structure asserting that the electromagnetic band set has cardinality 5, that consecutive frequencies satisfy the ratio equal to the golden ratio, and that the cortical carrier frequency $5phi$ satisfies $8 < 5phi < 9$.
background
The module treats the electromagnetic spectrum as five phi-decades, with each band spanning one geometric step in frequency. The inductive type enumerates the bands radio, microwave, infrared, visible, and uvXGamma. Frequency of index k is defined as phi to the power k, while the cortical carrier is defined as five times phi, asserted to lie between 8 and 9 Hz as the fundamental biological resonance.
proof idea
This is a structure definition that directly encodes the three required properties as fields. No tactics or lemmas are applied; the declaration simply packages the cardinality statement for the band type, the universal quantification over the frequency ratio, and the inequality for the carrier.
why it matters
This structure is instantiated by the emSpectrumCert definition in the same module. It formalizes the module claim that the spectrum comprises five phi-decades with the 5 phi Hz carrier linking to biological resonances. In the Recognition Science framework it realizes the five-band decomposition predicted by configuration dimension D=5 and the phi-ladder scaling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.