E_base_pos
plain-language theorem explainer
The lemma establishes positivity of the base energy on the φ-ladder. Applied physicists modeling RS-coherent photobiomodulation devices cite it to confirm all ladder energies remain positive. The proof is a one-line term applying mul_pos to the positivity of phi raised to -5 and the eV-to-joule conversion factor.
Claim. Let $E_0 = phi^{-5} times the electronvolt-to-joule conversion factor. Then $0 < E_0$.
background
The Photobiomodulation Device module defines the φ-energy ladder by E(n) = E_base · φ^n, with E_base as the recognition coherence quantum φ^{-5} eV converted to joules. This supports therapeutic wavelengths such as rung 6 at approximately 1.618 eV near 766 nm. The definition of E_base is phi ^ (-5) * eV_to_J, and the upstream lemma eV_to_J_pos states 0 < eV_to_J by norm_num.
proof idea
This is a one-line wrapper that applies mul_pos to Real.rpow_pos_of_pos phi_pos _ (positivity of any real power of phi) and eV_to_J_pos.
why it matters
The result feeds phi_energy_rung_pos, which lifts positivity to every rung via mul_pos E_base_pos (Real.rpow_pos_of_pos phi_pos n). It anchors the φ-ladder construction in the applied module, consistent with the eight-tick octave and recognition coherence quantum from the forcing chain. No open scaffolding questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.