pith. sign in
def

blackBodyRadiationDeepCert

definition
show as:

Why this theorem is linked from Combined Diffusion-Relaxation MRI to Assess Muscle Microstructure and Composition unclear

Pith linked this Lean declaration because the review connected a specific passage in the paper to this theorem. The relation tag says how strong that connection is; it is not a generic placeholder.

Simulations recover fv with r=0.95, RMSE=0.03; T2t 31-36 ms, T2v 66-86 ms

Relation between the paper passage and the cited Recognition theorem.

module
IndisputableMonolith.Foundation.BlackBodyRadiationDeep
domain
Foundation
line
50 · github
papers citing
30 papers (below)

plain-language theorem explainer

This definition constructs the master certificate BlackBodyRadiationDeepCert that packages the zero J-cost conditions for Wien's law and the Stefan-Boltzmann law with the positivity of J-cost for all positive ratios away from unity. Researchers deriving thermodynamic radiation laws from the Recognition Science J-cost framework cite it as the central bundling structure. The construction is a direct record definition that populates the three fields from the prior zero-cost theorems and the off-match positivity result.

Claim. The black-body radiation deep certificate is the structure whose Wien field asserts $J(1)=0$, whose Stefan-Boltzmann field asserts $J(1)=0$, and whose off-match field asserts $∀x>0, x≠1 → J(x)>0$, where $J$ denotes the J-cost function on positive reals.

background

In the Recognition Science setting, J-cost quantifies deviation from the self-similar fixed point on thermal ratios, with zero cost precisely at the matched configuration. The module establishes that Wien's displacement law, the Stefan-Boltzmann law, and the Planck distribution each correspond to a J-cost reading that vanishes or stays positive exactly when the ratio equals one. The structure BlackBodyRadiationDeepCert collects these three properties into a single certificate. Upstream results supply the individual facts: wien_zero_cost and stefan_boltzmann_zero_cost each reduce to Jcost_unit0, while off_match_positive applies Jcost_pos_of_ne_one to any positive ratio not equal to one.

proof idea

The definition is a direct record constructor. It assigns the wien_zero field to wien_zero_cost, the sb_zero field to stefan_boltzmann_zero_cost, and the off_match field to off_match_positive. No further tactics or reductions are required.

why it matters

This certificate is the master bundling object for the three black-body laws derived from J-cost. It is consumed by the downstream theorem blackBodyRadiationDeepCert_inhabited to witness that the certificate type is nonempty. Within the framework it confirms that the canonical radiation laws arise as zero-cost configurations under the Recognition Composition Law, completing the structural theorem for thermal radiation.

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

papers checked against this theorem (showing 30 of 30)