pith. sign in
theorem

wien_zero_cost

proved
show as:
module
IndisputableMonolith.Foundation.BlackBodyRadiationDeep
domain
Foundation
line
36 · github
papers citing
8 papers (below)

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 8 of 8)