off_match_positive
Why this theorem is linked from Atomic and molecular systems for radiation thermometry echoes
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.
in the limit t→∞, n1 = Ω/(Γ+2Ω) = e^{-ℏω/kBT}/(1+e^{-ℏω/kBT})
ECHOES: this paper passage has the same mathematical shape or conceptual pattern as the Recognition theorem, but is not a direct formal dependency.
plain-language theorem explainer
Off-match positivity of J-cost is established for any positive real away from unity. Black-body radiation derivations in Recognition Science cite this result when confirming the Planck law holds with positive J-cost off the matched thermal ratio. The argument is a direct one-line wrapper that invokes the core positivity lemma for J-cost.
Claim. For any real number $x > 0$ with $x ≠ 1$, the J-cost satisfies $0 < Jcost(x)$.
background
The module derives the three canonical black-body laws (Wien, Stefan-Boltzmann, Planck) as J-cost readings on thermal ratios. J-cost is the function that vanishes exactly at matched configurations and is positive elsewhere; its core positivity property is supplied by the upstream lemma Jcost_pos_of_ne_one, which rewrites Jcost as a square over a positive denominator and concludes strict positivity for $x > 0$, $x ≠ 1$. The local setting is the structural theorem that bundles these laws into a single master certificate without axioms or sorrys.
proof idea
One-line wrapper that applies Jcost_pos_of_ne_one.
why it matters
This supplies the off_match field of blackBodyRadiationDeepCert, the master certificate that records wien_zero_cost, stefan_boltzmann_zero_cost and off_match_positive as the three J-cost readings. It closes the positivity requirement for the Planck law inside the module's structural theorem. The result sits inside the Recognition Science derivation of black-body radiation from the single functional equation via J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 4 of 4)
-
Normalized Transformer sets new keypoint matching records
"hyperspherical loss... penalizes whenever two different keypoints are aligned... applied after each normalized transformer layer"
-
Mulliken charges yield accurate polariton spectra
"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
"in the limit t→∞, n1 = Ω/(Γ+2Ω) = e^{-ℏω/kBT}/(1+e^{-ℏω/kBT})"
-
Non-Markovian master equation gains exact memory integral
"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"