planck_h_pos
plain-language theorem explainer
The lemma asserts positivity of the Planck constant in the photobiomodulation formalization. Researchers modeling RS-coherent light therapy cite it when establishing wavelength positivity and therapeutic bounds. The proof is a one-line norm_num reduction on the constant definition.
Claim. $0 < h$ where $h$ is the Planck constant in J·s.
background
The Applied.PhotobiomodulationDevice module develops RS foundations for a PBM device via the φ-energy ladder E(n) = E_base · φ^n and 8-beat modulation. It imports planck_h as the CODATA 2024 value 6.62607015e-34 from Constants. The positivity result supplies the sign condition required for divisions that produce lambda_PBM from h c / E_PBM.
proof idea
One-line wrapper that applies the norm_num tactic to the definition of planck_h.
why it matters
The lemma is invoked by lambda_PBM_pos, lambda_PBM_in_therapeutic_window, and lambda_PBM_approx to confirm the 766 nm wavelength lies inside the 750–780 nm therapeutic window. It links the standard Planck constant to the module's φ-ladder and 8-tick neutrality claims, supporting the RS biophase light device specification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.