pith. sign in
module module high

IndisputableMonolith.Physics.BlackBodyRadiationFromJCost

show as:
view Lean formalization →

The module derives black-body radiation properties from the J-cost function. It defines spectral regions and certifies the Rayleigh-Jeans equilibrium where the cost vanishes exactly when hν equals kT. The structure consists of successive definitions for regions, counts, equilibrium points, off-peak positivity, and an overall radiation certificate.

claimThe Rayleigh-Jeans equilibrium is the condition $J(hν/kT)=0$ at the ratio $hν/kT=1$, extended by positive off-peak cost and a certificate for black-body spectra.

background

The J-cost is the functional imported from the Cost module and obeying the Recognition Composition Law J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y). Spectral regions are partitions of the frequency axis on which the cost exhibits definite sign or monotonicity behavior. The module works in the Recognition Science setting where constants are expressed in phi-native units and radiation laws are recovered from the uniqueness property of J.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the radiation-law foundation that feeds into larger physics derivations in Recognition Science. It anchors the classical limit of the forcing chain by realizing the J-uniqueness step as the equilibrium condition for thermal spectra.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)