E_PBM_bounds
plain-language theorem explainer
The lemma shows the photobiomodulation energy lies strictly between 1.61 and 1.62 times the electron-volt conversion factor. Engineers specifying RS-coherent light therapy devices cite it to locate the operating point at rung 6 of the phi-energy ladder inside the red/near-IR window. The proof is a term that applies the positive-multiplication inequality twice to the supplied bounds on phi.
Claim. $1.61$ times the electron-volt-to-joules conversion factor is strictly less than the photobiomodulation energy, and the photobiomodulation energy is strictly less than $1.62$ times the same conversion factor, where the photobiomodulation energy equals phi times the conversion factor.
background
The module sets up a photobiomodulation device on the phi-energy ladder. The base energy is defined as phi to the power of negative five times the electron-volt conversion (the recognition coherence quantum in joules). The photobiomodulation energy is defined as phi times the same conversion, placing the device at rung 6 and yielding phi electron volts, or roughly 1.618 eV and wavelength near 766 nm inside the 600-850 nm therapeutic band. The 8-beat modulation pattern is required to satisfy the neutrality constraint that prevents recognition strain accumulation.
proof idea
Term proof that builds the conjunction by two applications of mul_lt_mul_of_pos_right. The first uses the lemma phi greater than 1.61 together with the positivity of the electron-volt conversion; the second uses phi less than 1.62 with the same positivity fact.
why it matters
The bound is invoked by the downstream division-bounds helper that propagates the interval to any positive numerator. It supplies the concrete numerical check that rung 6 of the phi-energy ladder lands inside the clinically relevant window, consistent with the eight-tick octave and D=3 spatial setting of the Recognition Science framework. No open scaffolding questions are closed by this lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.