rayleighJeans_equilibrium
plain-language theorem explainer
The theorem establishes that the J-cost vanishes exactly at unit ratio, marking the Rayleigh-Jeans equilibrium where photon energy equals thermal energy. Researchers deriving blackbody spectra from recognition costs would cite this as the zero-cost point in the distribution. The proof reduces directly to the unit lemma for the J-cost function via term application.
Claim. In the Recognition Science framework, the J-cost function satisfies $J(1) = 0$, where the argument 1 denotes the ratio $hν / kT$.
background
In this module the blackbody spectrum is obtained from the J-cost of photon modes, with each mode assigned energy ratio $x = hν / kT$. The cost function is $J(x) = (x-1)^2 / (2x)$, which is the squared-ratio form of the J-uniqueness expression from the forcing chain. Equilibrium holds when this cost is zero, at $x=1$ (i.e., $hν = kT$). The module states that five spectral regions arise from configDim $D=5$ and that the full Planck distribution follows from the structural claim that $J(hν/kT)$ determines the spectrum shape.
proof idea
The proof is a one-line wrapper that applies the Jcost_unit0 lemma from the Cost module. That lemma itself simplifies the definition of Jcost at argument 1 to obtain the zero result.
why it matters
This supplies the Rayleigh-Jeans equilibrium field to the BlackBodyRadiationCert definition, which also records the count of five spectral regions and off-peak positivity. It completes the equilibrium step in the J-cost derivation of blackbody radiation, directly instantiating the J-uniqueness property (T5) at the thermal point. The parent structure is the blackBodyRadiationCert that certifies the spectral properties for the Recognition Science treatment of Planck's law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.