EMBand
plain-language theorem explainer
The inductive definition enumerates the five canonical electromagnetic bands in the Recognition Science phi-ladder model of the spectrum. A physicist deriving frequency ratios or carrier frequencies from the phi-ladder would reference this type when establishing band counts or spectral properties. It is introduced as a simple inductive enumeration deriving decidable equality and finiteness.
Claim. The electromagnetic spectrum is partitioned into five bands: radio, microwave, infrared, visible, and ultraviolet plus X-ray plus gamma, denoted as an inductive type with these constructors.
background
In the Recognition Science framework the electromagnetic spectrum is modeled via the phi-ladder, with each spectral band spanning approximately one phi-decade: ν_k = ν_0 × φ^k. The module sets five canonical bands (radio, microwave, infrared, visible, UV+X+gamma) equal to configDim D = 5, a coarser partition than the usual seven. This choice is checked against the visible-light bandwidth ratio ≈ φ² ≈ 2.618, matching the observed 700 nm / 400 nm interval, and supports the prediction of a 5φ Hz carrier linked to biological resonances.
proof idea
The declaration is an inductive definition that lists the five bands explicitly, equipped with deriving clauses for DecidableEq, Repr, BEq and Fintype.
why it matters
This definition supplies the foundational enumeration for the five-band structure required by the phi-ladder treatment of the electromagnetic spectrum. It is used directly by emBandCount to prove Fintype.card EMBand = 5 and by EMSpectrumCert to certify the phi_ratio property together with the corticalCarrier bounds. It fills the A1 SM Depth section of the Recognition Science framework, aligning the spectral partition with the overall phi-ladder scaling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.