emBandCount
plain-language theorem explainer
The Recognition Science electromagnetic spectrum model asserts exactly five bands. Modelers of spectral classification in the phi-ladder framework cite this to anchor the discrete band count at configDim D equals 5. The proof applies the decide tactic directly to the Fintype instance derived from the five-constructor inductive type.
Claim. The set of electromagnetic bands has cardinality 5, consisting of the radio, microwave, infrared, visible, and ultraviolet-X-gamma bands.
background
In the Electromagnetic Spectrum from Phi-Ladder module the EM spectrum is partitioned into bands each spanning approximately one phi-decade in frequency, with the total spanning about 24 orders of magnitude. The module states that five canonical bands correspond to configDim D = 5, with visible-light bandwidth ratio lying between phi and phi squared. The inductive type EMBand enumerates the bands as radio, microwave, infrared, visible, uvXGamma and derives Fintype, DecidableEq, and related instances to support cardinality and equality computations.
proof idea
The proof is a one-line wrapper that invokes the decide tactic. This tactic computes Fintype.card by enumerating the five constructors of the EMBand inductive type and confirms the result equals 5.
why it matters
This theorem supplies the five_bands field inside the emSpectrumCert definition, which certifies the overall electromagnetic spectrum properties including the phi ratio and carrier band. It realizes the module claim that five bands equal configDim D = 5 and aligns with the phi-ladder structure in Recognition Science where spectral divisions follow self-similar scaling from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.