  39theorem stefan_boltzmann_zero_cost : Jcost 1 = 0 := Jcost_unit0
  40
  41/-- Off matched: J-cost > 0. -/
  42theorem off_match_positive (x : ℝ) (hx : 0 < x) (hne : x ≠ 1) : 0 < Jcost x :=
  43  Jcost_pos_of_ne_one hx hne
  44
  45structure BlackBodyRadiationDeepCert where
  46  wien_zero : Jcost 1 = 0
  47  sb_zero : Jcost 1 = 0
  48  off_match : ∀ x : ℝ, 0 < x → x ≠ 1 → 0 < Jcost x
  49
  50noncomputable def blackBodyRadiationDeepCert : BlackBodyRadiationDeepCert where
  51  wien_zero := wien_zero_cost
  52  sb_zero := stefan_boltzmann_zero_cost
  53  off_match := off_match_positive
  54
  55theorem blackBodyRadiationDeepCert_inhabited : Nonempty BlackBodyRadiationDeepCert :=
  56  ⟨blackBodyRadiationDeepCert⟩
  57
  58end
  59end BlackBodyRadiationDeep
  60end Foundation
  61end IndisputableMonolith

papers checked against this theorem (showing 3 of 3)

Mulliken charges yield accurate polariton spectra
unclear · 2512.03277

"However, the same approach may not be suitable to be used for studying cavity modification of energy transport or chemical dynamics as this approximation leads to spurious heating of the light-matter hybrid system."
Rubidium atoms measure blackbody temperature to 1 percent
echoes · 2512.08668

"in the limit t→∞, n1 = Ω/(Γ+2Ω) = e^{-ℏω/kBT}/(1+e^{-ℏω/kBT})"
Non-Markovian master equation gains exact memory integral
unclear · 2605.03197

"S(ω+ω_0) = Re[1/(4λ_0) + 1/(8λ_+) + 1/(8λ_-)] ... the familiar Mollow triplet acquires a frequency-dependent linewidth that encodes the memory of the bath"