planck_h_pos
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 in Recognition Science
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.
scope and limits
- Does not derive the Planck constant from Recognition Science axioms.
- Does not address effective or running values of h in modified theories.
- Does not guarantee positivity for other imported constants without separate lemmas.
Lean usage
have h_hc_pos : 0 < planck_h * speed_of_light := mul_pos planck_h_pos speed_of_light_posformal statement (Lean)
56lemma planck_h_pos : 0 < planck_h := by norm_num [planck_h]