wien_zero_cost
plain-language theorem explainer
The theorem establishes that J-cost vanishes at the unit ratio, anchoring the zero-cost condition for Wien's displacement law in the Recognition Science derivation of black-body radiation. Researchers verifying thermal spectra from recognition cost would cite it to confirm matched configurations incur no penalty. The proof reduces directly to the unit lemma for Jcost via a one-line term application.
Claim. $J_ {cost}(1) = 0$, where $J_{cost}(x) = (x-1)^2/(2x)$ for positive ratios $x$.
background
Jcost is the cost function on positive ratios given by the squared expression $J(x) = (x-1)^2/(2x)$, which is nonnegative and zero only at $x=1$. This module derives the three canonical black-body laws as zero J-cost statements on thermal ratios, with the local setting being a structural theorem (zero sorry, zero axiom) that bundles Wien, Stefan-Boltzmann, and Planck results from the Recognition Composition Law. It depends on the upstream lemma Jcost_unit0, which states Jcost(1) = 0 by direct simplification of the squared-ratio form.
proof idea
The proof is a one-line term wrapper that applies the lemma Jcost_unit0 from the Cost module. That lemma itself reduces by simp on the definition of Jcost.
why it matters
This zero-cost result supplies the wien_zero field of the master certificate blackBodyRadiationDeepCert, which bundles the three black-body statements. It fills the Wien component of the structural theorem for black-body radiation from J-cost, aligning with the Recognition Science forcing chain where matched configurations have vanishing cost at the self-similar fixed point. It closes the anchor for the displacement law without touching open questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 4 of 4)
-
Metal-rich sub-Neptunes can separate water from hydrogen
"the adiabatic temperature gradient governing the temperature as a function of depth in the convective envelope becomes shallower at higher metallicities"
-
Rubidium atoms measure blackbody temperature to 1 percent
"the transition rate is Ωij = ... = ω³ij / (3ϵ0 ℏ π c³) |⟨i|d|j⟩|² 1/(e^{ℏωij/kBT}−1)"
-
Spintronic Poisson bolometer achieves 35 mK NEDT at room temperature
"absorptance exceeding 60% across the LWIR spectrum, matching the peak of room-temperature blackbody radiation"
-
Particle bath induces negative differential heat flow in linear chain
"J = 4 γ_L γ_R k² / m (D0 − D1 + …) (T_L − T_R) with γ_L ∼ T_L^{-2} implying J ∼ T_L^{-1} as T_L → ∞"