lambda_PBM_approx
The declaration proves the Recognition Science photobiomodulation wavelength lies within 5 nm of 766 nm. Device physicists specifying phi-ladder coherent sources cite this bound for the red/near-IR therapeutic window. The tactic proof unfolds the wavelength definition, applies positivity of hc and the division-bounds lemma on the 1.61-1.62 eV energy interval, then closes the gap with norm_num checks and linarith.
claim$|hc/E - 766×10^{-9}| < 5×10^{-9}$ where $E$ is the photon energy at rung 6 of the phi-ladder (satisfying $1.61$ eV $< E < 1.62$ eV) and $h$, $c$ are the Planck constant and speed of light.
background
The PhotobiomodulationDevice module defines the phi-energy ladder by $E(n) = E_base · phi^n$ with $E_base = phi^{-5}$ eV. Rung 6 therefore supplies the therapeutic energy $E_PBM$ between 1.61 eV and 1.62 eV. The wavelength is introduced as the noncomputable definition lambda_PBM = planck_h * speed_of_light / E_PBM, using the exact CODATA values for h and c together with the exact eV-to-joule conversion.
proof idea
The proof unfolds lambda_PBM, forms the positivity fact h_hc_pos via mul_pos on the two positive constants, then applies the upstream lemma div_bounds_of_E_PBM to obtain the reciprocal bounds on the wavelength. Two norm_num facts establish the reference inequalities 761 nm < hc/(1.62 eV) and hc/(1.61 eV) < 771 nm. Transitivity with lt_trans yields 761 nm < lambda_PBM < 771 nm, from which abs_lt.mpr and linarith deliver the stated 5 nm tolerance.
why it matters in Recognition Science
This pins the concrete 766 nm value for rung 6 of the phi-ladder, directly supporting the device specification and the 8-beat modulation pattern that enforces eight-tick neutrality. It supplies the wavelength used in brainwave-entrainment calculations and closes the approximation step required by the RS-coherent light-therapy framework. No downstream uses are recorded, leaving open integration with HealingRate bounds.
scope and limits
- Does not derive the 1.61-1.62 eV energy interval from the phi-ladder axioms.
- Does not address material dispersion or non-ideal refractive effects.
- Does not establish clinical efficacy or safety margins for the device.
- Does not compute an exact wavelength; only the 5 nm tolerance is shown.
formal statement (Lean)
165theorem lambda_PBM_approx : abs (lambda_PBM - 766e-9) < 5e-9 := by
proof body
Tactic-mode proof.
166 unfold lambda_PBM
167 have h_hc_pos : 0 < planck_h * speed_of_light :=
168 mul_pos planck_h_pos speed_of_light_pos
169 have ⟨h_lower, h_upper⟩ := div_bounds_of_E_PBM h_hc_pos
170 have h_lo_ref :
171 (761e-9 : ℝ) < planck_h * speed_of_light / (1.62 * eV_to_J) := by
172 norm_num [planck_h, speed_of_light, eV_to_J]
173 have h_hi_ref :
174 planck_h * speed_of_light / (1.61 * eV_to_J) < (771e-9 : ℝ) := by
175 norm_num [planck_h, speed_of_light, eV_to_J]
176 have h_gt := lt_trans h_lo_ref h_lower
177 have h_lt := lt_trans h_upper h_hi_ref
178 exact abs_lt.mpr ⟨by linarith, by linarith⟩
179
180/-! ## Section 3: 8-Beat Modulation Pattern
181
182The RS-coherent modulation pattern is derived from a superposition of
183DFT modes: s(k) = cos(kπ/4) + (1/φ)·cos(kπ/2).
184
185Using the identities 1/φ = φ - 1 and standard cosine values:
186- s(0) = 1 + 1/φ = φ
187- s(1) = √2/2
188- s(2) = 0 - 1/φ = 1 - φ
189- s(3) = -√2/2
190- s(4) = -1 + 1/φ = φ - 2
191- s(5) = -√2/2
192- s(6) = 0 - 1/φ = 1 - φ
193- s(7) = √2/2
194
195The φ terms and √2/2 terms each cancel pairwise,
196giving Σ s(k) = 0 — exact 8-window neutrality. -/
197
198/-- The RS-coherent 8-beat modulation pattern values.
199 Derived from s(k) = cos(kπ/4) + (1/φ)·cos(kπ/2). -/