lambda_PBM_in_therapeutic_window
The wavelength lambda_PBM derived from the phi-energy ladder at rung 6 satisfies 750 nm < lambda_PBM < 780 nm. Modelers of RS-coherent photobiomodulation devices cite this result to place the device output inside the red/near-IR therapeutic band. The proof unfolds the wavelength definition, invokes a division-bounds lemma on E_PBM, and closes the two inequalities by direct numerical comparison.
claim$750 < 10^9 lambda < 780$ where $lambda = hc / E$ and $E = phi * 1.602176634 * 10^{-19}$ J.
background
The module formalizes an RS-coherent photobiomodulation device whose photon energy follows the phi-ladder E(n) = E_base * phi^n. E_PBM is defined as phi * eV_to_J, the energy at rung 6. lambda_PBM is then hc / E_PBM with h and c the standard constants. The upstream lemma div_bounds_of_E_PBM states that for any positive K the quotient K / E_PBM lies strictly between K / (1.62 eV_to_J) and K / (1.61 eV_to_J).
proof idea
Unfold lambda_PBM. Establish positivity of planck_h * speed_of_light by mul_pos. Apply div_bounds_of_E_PBM to obtain the sandwich. Use constructor to split the conjunction, then two calc blocks that compare the explicit numerical bounds 750e-9 and 780e-9 via norm_num.
why it matters in Recognition Science
The result anchors the therapeutic wavelength inside the module's phi-ladder construction and supplies the wavelength field of the downstream rs_device definition. It realizes the explicit prediction that rung 6 yields approximately 766 nm, consistent with the eight-tick octave and the alpha-band constants of the Recognition Science framework.
scope and limits
- Does not prove clinical efficacy or biological mechanism.
- Does not derive the phi ladder or the value of phi from more primitive axioms.
- Does not treat modulation pattern or entrainment frequencies.
- Does not supply wavelength error bars narrower than the 750-780 nm interval.
formal statement (Lean)
149theorem lambda_PBM_in_therapeutic_window :
150 750e-9 < lambda_PBM ∧ lambda_PBM < 780e-9 := by
proof body
Tactic-mode proof.
151 unfold lambda_PBM
152 have h_hc_pos : 0 < planck_h * speed_of_light :=
153 mul_pos planck_h_pos speed_of_light_pos
154 have ⟨h_lower, h_upper⟩ := div_bounds_of_E_PBM h_hc_pos
155 constructor
156 · calc (750e-9 : ℝ)
157 < planck_h * speed_of_light / (1.62 * eV_to_J) := by
158 norm_num [planck_h, speed_of_light, eV_to_J]
159 _ < planck_h * speed_of_light / E_PBM := h_lower
160 · calc planck_h * speed_of_light / E_PBM
161 < planck_h * speed_of_light / (1.61 * eV_to_J) := h_upper
162 _ < (780e-9 : ℝ) := by norm_num [planck_h, speed_of_light, eV_to_J]
163
164/-- Tighter approximation: λ_PBM ≈ 766 nm (within ±5 nm). -/