pith. sign in
structure

BlackBodyRadiationDeepCert

definition
show as:
module
IndisputableMonolith.Foundation.BlackBodyRadiationDeep
domain
Foundation
line
45 · github
papers citing
9 papers (below)

plain-language theorem explainer

BlackBodyRadiationDeepCert packages the J-cost zero at ratio 1 for both Wien and Stefan-Boltzmann laws with strict positivity off that point to certify the Planck distribution form. A researcher deriving thermal spectra from the J functional equation cites this record to confirm that the three canonical laws emerge as J-cost readings on matched thermal ratios. The declaration is a pure structure definition that introduces the record type with no proof obligations or computational content.

Claim. The structure certifying black-body radiation consists of the fields $J(1)=0$ (Wien zero-cost), $J(1)=0$ (Stefan-Boltzmann zero-cost), and $J(x)>0$ for all $x>0$ with $x≠1$ (off-match positivity).

background

The J-cost function is the Recognition Science cost measure defined by the composition law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ with explicit form $J(x)=(x+x^{-1})/2-1$. This module recovers the three black-body laws by reading J-cost on thermal ratios, with zero cost at the matched point (ratio 1) and positivity elsewhere. The module doc states that each law is already proved individually as a J-cost reading and that BlackBodyRadiationDeepCert is the master certificate bundling all three.

proof idea

The declaration is a structure definition with no proof body. It introduces the record type whose three fields are later supplied by the downstream lemmas wien_zero_cost, stefan_boltzmann_zero_cost, and off_match_positive.

why it matters

This structure collects the J-cost derivations of the Wien, Stefan-Boltzmann, and Planck laws, directly supplying the fields for blackBodyRadiationDeepCert and the nonemptiness result blackBodyRadiationDeepCert_inhabited. It completes the structural theorem for black-body radiation from J-cost, consistent with J-uniqueness in the forcing chain. The module status records it as a structural theorem with zero axioms.

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

papers checked against this theorem (showing 9 of 9)