planck_h_pos
plain-language theorem explainer
planck_h_pos establishes that the Planck constant is strictly positive. Applied researchers deriving therapeutic wavelengths from the phi-energy ladder in photobiomodulation models cite it to justify positivity when multiplying by speed of light and dividing by photon energy. The proof is a direct numerical reduction via the norm_num tactic on the constant definition.
Claim. $0 < h$, where $h = 6.62607015 × 10^{-34}$ denotes the Planck constant in joule-seconds.
background
The Photobiomodulation Device module formalizes RS-coherent light therapy via the phi-energy ladder E(n) = E_base · φ^n, with rung 6 yielding photon energy near 1.618 eV and wavelength near 766 nm inside the 600-850 nm therapeutic band. Planck's constant enters the wavelength formula λ = hc / E. The upstream definition supplies the CODATA 2024 value for planck_h.
proof idea
The proof is a one-line wrapper that applies the norm_num tactic to the explicit positive numerical definition of planck_h.
why it matters
This lemma supplies the positivity fact required by the three downstream results lambda_PBM_pos, lambda_PBM_in_therapeutic_window, and lambda_PBM_approx that place the PBM wavelength inside the 750-780 nm window. It supports the module's applied calculations that combine the phi-ladder with the eight-tick neutrality pattern while using the empirical Planck value rather than the RS-native hbar = phi^{-5}.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.