lambda_PBM_approx
plain-language theorem explainer
The theorem shows the photobiomodulation wavelength derived from the phi-energy ladder at rung 6 lies inside a 5 nm window around 766 nm. Device physicists specifying RS-coherent light sources would cite the result for wavelength selection. The proof unfolds the wavelength definition, invokes division bounds on the energy interval, checks reference inequalities by direct computation, and closes with linear arithmetic on the absolute value.
Claim. $|hc/E - 766 nm| < 5 nm$, where $E$ is the photon energy at rung 6 of the phi-ladder ($E = 1.618$ eV) and $h$, $c$ are the Planck constant and speed of light.
background
The module defines the phi-energy ladder via $E(n) = E_{base} · phi^n$, with $E_{base} = phi^{-5}$ eV from the BIOPHASE scale. Rung 6 therefore yields $E = phi$ eV, which converts to wavelength by $lambda = hc/E$. The auxiliary definition $E_{PBM}$ is the numerical interval (1.61, 1.62) eV that brackets this value. The lemma div_bounds_of_E_PBM states that for any positive numerator $K$, the inequalities $K/(1.62 eV_to_J) < K/E_{PBM} < K/(1.61 eV_to_J)$ hold, transferring energy bounds directly to wavelength bounds.
proof idea
The tactic proof first unfolds lambda_PBM to $hc/E_{PBM}$. It obtains positivity of the product $hc$ from the two positivity lemmas. It then applies div_bounds_of_E_PBM to produce the two-sided bound on the wavelength. Two norm_num blocks verify the concrete reference inequalities 761 nm < hc/(1.62 eV_to_J) and hc/(1.61 eV_to_J) < 771 nm. Transitivity chains these with the bounds lemma, after which abs_lt.mpr together with linarith finishes the absolute-value claim.
why it matters
The result supplies the concrete wavelength anchor for the RS-coherent PBM device described in the module doc-comment, confirming that rung 6 lands inside the clinically relevant 600-850 nm window. It directly supports the eight-tick octave neutrality constraint mentioned in the same module. No downstream theorems are recorded yet, so the declaration currently functions as a terminal numerical check rather than an intermediate lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.