  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 17 of 17)

Short-edge abundance tunes laser modal uniformity
unclear · 2512.04811

"we use the well-known Steady-State ab Initio Laser Theory (SALT) equations ... single-pole approximation (SPA-SALT)"
Anisotropic electrons shape black hole eruption signals
unclear · 2512.06803

"We adopt two Gaussian-type prescriptions... G_b(α), G_l(α) with free α_0, σ"
MatterSim predicts Gibbs free energies at near first-principles accuracy
unclear · 2405.04967

"predicts Gibbs free energies... 15 meV/atom resolution for temperatures up to 1000 K"
One image trains text-to-image models for precise lighting control
echoes · 2512.17489

"physics-based illuminant augmentation along with the Planckian locus to create fine-tuning variants under standard illuminants"
Quantum failures recycled to erase data below Landauer heat limit
unclear · 2601.07522

"We demonstrate thermodynamic recycling on IBM’s superconducting quantum processor by using the HHL algorithm... reducing the heat dissipated in erasing syndrome information... below the Landauer limit"
Stars power UV and Hα in little red dots, not the hidden AGN
echoes · 2601.10573

"the envelope radiates as a ∼5000 K blackbody... UV-to-Hα luminosity ratios are remarkably consistent with young starburst galaxies"
THz spectroscopy maps doping levels from 10^15 to 10^20 cm^{-3}
unclear · 2602.21094

"accessible range ... 10^15 cm^{-3} to 10^20 cm^{-3} ... dependencies on material, doping type, and sample thickness"
UB4-UBC composite raises uranium density with oxidation resistance
unclear · 2603.04824

"oxidation onset temperatures of approximately 400 °C for the UB4–UBC composite and 550 °C for the UB4 sample"
Two PI formulas give minimum settling time for any second-order plant
echoes · 2604.21294

"Ms = 2/√3 ≈ 1.155 ... independent of Kp, T1 and T2"
ML sampling matches MoS2 Raman spectra to experiment at varying temperatures
echoes · 2604.02538

"Our results demonstrate excellent agreement with experimental measurements; notably, the calculated temperature trends in frequencies and linewidths align with empirical observations."
Intermittency forms connected conduits boosting mobility in porous media
unclear · 2605.11991

"the computed pressure-gradient-capillary-number relationship (∇P-Ca) recovers both the linear Darcy and the sub-linear intermittent scaling regimes"
Joint diffusion and relaxation MRI removes echo-time bias in muscle scans
unclear · 2605.09091

"Simulations recover fv with r=0.95, RMSE=0.03; T2t 31-36 ms, T2v 66-86 ms"
Black hole phase transitions peak at maximum entropy production
unclear · 2604.05785

"G(r;T,P) = r/2 (1 + 8/3 π P r² + Q²/r²) − π T r²"
Symmetry test spots ladder structures from atoms to black holes
refines · 2604.06249

"Applications to the quantum harmonic oscillator and dynamical tidal response of Kerr black holes"
Black hole shadows depend on monopoles, charge and spin
unclear · 2604.14213

"the differential energy emission rate takes the form d²E(ω)/dω dt = 2π³ R_s² ω³ / (e^{ω/T_H} – 1)"
Tsallis entropy yields Van der Waals black hole transitions
unclear · 2605.02429

"S_{q,BH} = k_B/(1−q) [ (1 + 3(1−q) A_h/l_P^2) exp(−11(1−q)A_h / [4 l_P^2 (1+3(1−q)A_h/l_P^2)]) − 1 ] ... reduces to S_BH in q→1 limit"
One model unifies magnetization loss and spin transport in ferromagnets
unclear · 2605.02483

"j = A' T^0.5 exp{−B' T^−0.5} — structurally analogous to Efros–Shklovskii law"