pith. sign in
theorem

off_match_positive

proved
show as:
module
IndisputableMonolith.Foundation.BlackBodyRadiationDeep
domain
Foundation
line
42 · github
papers citing
4 papers (below)

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)