off_peak_positive
plain-language theorem explainer
The result establishes that the recognition cost J(r) is strictly positive for any positive energy ratio r not equal to one. Physicists deriving blackbody spectra within the Recognition Science framework cite it to confirm that non-equilibrium photon modes carry positive cost. The proof is a direct one-line application of the general J-cost positivity lemma to the off-peak hypotheses.
Claim. For any real number $r > 0$ with $r ≠ 1$, the J-cost function satisfies $0 < J(r)$.
background
In the Recognition Science treatment of blackbody radiation, each photon mode is assigned a J-cost based on the energy ratio $r = hν/kT$. The J-cost vanishes at equilibrium ($r=1$, the Rayleigh-Jeans regime) and is positive for all other positive ratios. The upstream lemma states that J(x) > 0 whenever x > 0 and x ≠ 1; it follows from expressing the cost as a square divided by a positive term. The module uses this to partition the spectrum into five regions whose boundaries are set by the sign changes of J.
proof idea
This is a one-line wrapper that applies the lemma Jcost_pos_of_ne_one to the supplied hypotheses on r.
why it matters
It supplies the off-peak positivity field to the BlackBodyRadiationCert definition, which also records the five spectral regions and the Rayleigh-Jeans equilibrium point. This component supports the larger claim that the Planck distribution follows from the J-cost structure, consistent with the Recognition Science forcing chain that fixes D=3 and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.