spectralRegionCount
plain-language theorem explainer
The theorem establishes that the Recognition Science blackbody model partitions the spectrum into exactly five regions. Physicists deriving Planck distributions from the J-cost functional would cite this to fix the discrete band count before computing equilibria. The proof is a one-line decision procedure that enumerates the constructors of the SpectralRegion inductive type.
Claim. The finite type of spectral regions has cardinality five: $ |SpectralRegion| = 5 $, where the regions are radio, infrared, visible, ultraviolet, and x-ray.
background
In the BlackBodyRadiationFromJCost module the electromagnetic spectrum is partitioned into five discrete regions by the inductive type SpectralRegion whose constructors are radio, infrared, visible, ultraviolet, and xray. This partition is identified with configuration dimension D = 5 in the Recognition Science framework, as stated in the module documentation on blackbody radiation from J-cost.
proof idea
The proof is a one-line term that applies the decide tactic to the decidable Fintype instance automatically derived for the SpectralRegion inductive type, yielding cardinality five directly.
why it matters
This result supplies the five_regions component of the blackBodyRadiationCert definition that certifies the structural properties of blackbody radiation in RS terms. It realizes the module claim that five spectral regions equal configDim D = 5 and sits downstream of the equilibrium theorem Jcost(1) = 0 that anchors the Rayleigh-Jeans limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.