div_bounds_of_E_PBM
plain-language theorem explainer
The lemma transfers the interval bounds on photobiomodulation energy E_PBM to reversed inequalities for the quotient K/E_PBM whenever the numerator K is positive. Wavelength calculations in photobiomodulation device proofs cite this helper to bound lambda_PBM. The proof unpacks E_PBM_bounds, establishes positivity of the endpoint multipliers, applies the reciprocal inequality one_div_lt_one_div_of_lt twice, then scales both sides by the positive K via mul_lt_mul_of_pos_left before simplifying the divisions.
Claim. For any positive real $K$, if $1.61 eV_to_J < E_{PBM} < 1.62 eV_to_J$ where $E_{PBM} = phi eV_to_J$, then $K/(1.62 eV_to_J) < K/E_{PBM} < K/(1.61 eV_to_J)$.
background
The Applied.PhotobiomodulationDevice module formalizes a Recognition Science device whose photon energies follow the phi-ladder E(n) = E_base phi^n with E_base = phi^{-5} eV. E_PBM is defined as the rung-6 value phi eV_to_J, which the module doc places near 1.618 eV and links to the red/near-IR therapeutic window. E_PBM_bounds supplies the concrete interval (1.61, 1.62) times eV_to_J while E_PBM_pos and eV_to_J_pos guarantee positivity; K is the dimensionless bridge ratio from Constants.
proof idea
The term proof first obtains h_lower and h_upper from E_PBM_bounds. It builds positivity of 1.62 eV_to_J and 1.61 eV_to_J via mul_pos with eV_to_J_pos. Two applications of one_div_lt_one_div_of_lt produce the reciprocal inequalities; each is then multiplied on the left by the positive K using mul_lt_mul_of_pos_left. Final simpa rewrites the divisions as products of inverses and reorders factors.
why it matters
The lemma is invoked directly by lambda_PBM_in_therapeutic_window and lambda_PBM_approx to bound hc/E_PBM inside the 750-780 nm window and the tighter 766 nm approximation. It therefore closes the computational link between the phi-ladder rung-6 energy and observable therapeutic wavelengths, consistent with the eight-tick octave neutrality constraint stated in the module doc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.