eV_to_J_pos
plain-language theorem explainer
The lemma asserts that the electron-volt to joule conversion constant is strictly positive. Device-modeling code in the photobiomodulation module cites it to guarantee that all φ-ladder photon energies remain positive. The proof is a one-line norm_num reduction on the explicit decimal definition of the constant.
Claim. The electron-volt to joule conversion constant is positive: $0 < 1.602176634 × 10^{-19}$.
background
The module formalizes RS-coherent light therapy via the φ-energy ladder, where E_base = φ^{-5} × (eV-to-J conversion) supplies the recognition coherence quantum in joules. The conversion itself is the exact factor 1.602176634 × 10^{-19}. Module documentation states that rung 6 yields E(6) = φ eV ≈ 1.618 eV, mapping to the therapeutic red/near-IR window, and that the 8-beat modulation satisfies 8-window neutrality.
proof idea
One-line term proof that applies norm_num to the definition of the conversion factor.
why it matters
The result is invoked by E_base_pos, E_PBM_pos, E_PBM_bounds, and div_bounds_of_E_PBM to keep all energies positive. It supports the module claim that rung-6 photons lie inside the (1.61, 1.62) eV therapeutic window and closes the positivity interface needed for 8-tick neutrality and brainwave entrainment statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.