blackBodyRadiationDeepCert_inhabited
plain-language theorem explainer
The theorem establishes that a certificate structure for the three black-body radiation laws derived from J-cost is non-empty. Researchers deriving thermal radiation from Recognition Science would cite it to confirm simultaneous satisfaction of the Wien, Stefan-Boltzmann, and Planck relations. The proof is a direct term that supplies the explicit certificate assembled from the zero-cost and positivity lemmas.
Claim. There exists a structure $C$ such that $J(1)=0$ holds for both the Wien displacement condition and the Stefan-Boltzmann intensity condition, while $J(x)>0$ for every positive real $x$ distinct from 1, where $J$ is the J-cost function on thermal ratios.
background
The Black-Body Radiation from J-Cost module treats the J-cost function as a measure of deviation from matched thermal ratios in Recognition Science. The structure BlackBodyRadiationDeepCert collects three properties: J-cost vanishes at the Wien peak (wavelength-temperature product equals the Wien constant), vanishes at the Stefan-Boltzmann intensity, and remains strictly positive for all positive arguments away from the matched point $x=1$. This module presents the three canonical radiation laws as simultaneous J-cost readings.
proof idea
The proof is a term-mode wrapper that directly inhabits the type by supplying the pre-built certificate blackBodyRadiationDeepCert. That certificate is assembled from the upstream lemmas that establish zero J-cost at the Wien and Stefan-Boltzmann points together with the positivity result off the matched ratio.
why it matters
The declaration closes the structural theorem for black-body radiation by confirming the certificate is inhabited, thereby validating the Wien, Stefan-Boltzmann, and Planck laws as zero J-cost configurations inside the Recognition Science framework. It supports the derivation of thermal physics from the J-function and Recognition Composition Law without introducing new axioms. The module reports zero sorrys, so no open scaffolding remains at this level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.