pith. sign in
theorem

stefan_boltzmann_zero_cost

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

plain-language theorem explainer

The theorem establishes that J-cost vanishes at the unit ratio, encoding the Stefan-Boltzmann law at zero cost for matched thermal configurations. Researchers deriving black-body radiation laws inside the Recognition Science framework cite this result to confirm the zero-cost condition for j* = σ T^4. The proof is a direct term application of the Jcost_unit0 lemma.

Claim. The J-cost of the unit ratio vanishes: $J(1) = 0$, where $J(x) = (x-1)^2/(2x)$ is the cost induced by the multiplicative recognizer on positive ratios.

background

J-cost is the non-negative function J(x) = (x-1)^2/(2x) that vanishes only at x=1; it is the derived cost of the comparator inside a multiplicative recognizer. The BlackBodyRadiationDeep module applies this cost to thermal ratios to recover the classical radiation laws as zero-cost statements. The upstream Jcost_unit0 lemma states that Jcost(1) = 0 by direct simplification of the definition.

proof idea

The proof is a one-line wrapper that applies the Jcost_unit0 lemma from the Cost module.

why it matters

This supplies the sb_zero field inside the master certificate blackBodyRadiationDeepCert that bundles the three black-body laws. It completes the structural claim that the Stefan-Boltzmann relation corresponds to a matched configuration of vanishing J-cost, consistent with the Recognition Composition Law. The module certifies the Wien, Stefan-Boltzmann and Planck laws from J-cost with no additional axioms.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.

papers checked against this theorem (showing 5 of 5)