planck_h
plain-language theorem explainer
The definition supplies the Planck constant as the numerical value 6.62607015 × 10^{-34} in joule-seconds from CODATA 2024. Device modelers computing wavelengths on the φ-energy ladder for photobiomodulation cite this constant when forming λ = h c / E. The binding is a direct constant assignment with no reduction steps or lemmas.
Claim. The Planck constant is defined by the assignment $h = 6.62607015 × 10^{-34}$ (J·s).
background
The Photobiomodulation Device module instantiates constants to support the φ-energy ladder E(n) = E_base · φ^n. Rung 6 yields E ≈ φ eV, which converts to wavelength λ ≈ 766 nm inside the 600–850 nm therapeutic band. The module documentation states that this wavelength aligns with clinical evidence for red/near-IR efficacy and that the 8-beat modulation satisfies Σ s(k) = 0 for neutrality under the eight-tick constraint.
proof idea
Direct numerical assignment of the CODATA 2024 value. No lemmas or tactics are invoked; the definition serves as a base constant referenced by lambda_PBM and its bounding theorems.
why it matters
This constant anchors the wavelength formulas lambda_PBM, lambda_PBM_approx, and lambda_PBM_in_therapeutic_window. It supplies the h factor required to map the φ-ladder energies (E(6) = φ eV) onto observable wavelengths inside the therapeutic window. The placement connects the applied device model to the Recognition Science landmarks of the eight-tick octave and the φ-ladder mass/energy scaling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.