phi_energy_rung_pos
plain-language theorem explainer
The lemma shows that the φ-energy rung function returns strictly positive values for every real rung index n. Device modelers in RS photobiomodulation would cite it to confirm all ladder energies remain physical. The proof is a one-line term that multiplies the already-established positivity of E_base by the positivity of φ raised to n.
Claim. For every real number $n$, $E_0 · φ^n > 0$, where $E_0$ denotes the base energy of the φ-ladder and $φ$ is the golden ratio.
background
The Applied.PhotobiomodulationDevice module defines the φ-energy ladder via the noncomputable function phi_energy_rung n := E_base * phi ^ n. This maps any real rung index to photon energy in joules and sits inside the larger RS treatment of coherent light therapy. The upstream lemma E_base_pos establishes 0 < E_base by multiplying Real.rpow_pos_of_pos phi_pos _ with eV_to_J_pos, while the sibling definition scale k := phi ^ k supplies the same exponential building block used elsewhere in cosmology.
proof idea
The proof is a one-line term that applies mul_pos directly to E_base_pos and Real.rpow_pos_of_pos phi_pos n.
why it matters
The result anchors positivity throughout the φ-energy ladder used for therapeutic wavelength selection (rung 6 yields φ eV ≈ 766 nm) and 8-beat modulation neutrality in the module. It supports the device specification RS_Biophase_Light_Device_Spec.tex and the broader Recognition Science φ-ladder (T5–T6) together with the eight-tick octave. No downstream theorems yet depend on it, leaving the positivity fact available for future energy and frequency calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.