phi_fifth_in_alpha_band
plain-language theorem explainer
The theorem confirms that the golden ratio to the fifth power lies strictly between 8 and 13, placing the associated frequency inside the alpha EEG band. Device designers working in the Recognition Science framework cite the result to fix the default modulation rate for relaxed wakefulness and healing coherence. The proof is a term-mode wrapper that splits the conjunction and applies linear arithmetic to the tighter bounds supplied by the constants module.
Claim. The golden ratio to the fifth power satisfies $8 < phi^5 < 13$.
background
The PhotobiomodulationDevice module develops Recognition Science foundations for a light therapy device aligned with the phi-ladder. Energy levels follow E(n) = E_base · phi^n, and frequencies phi^n Hz are matched to EEG bands for entrainment, with the alpha band (8-13 Hz) selected as the default for optimal healing coherence. This result depends on the upstream lemma phi_fifth_bounds, which states that phi^5 lies between 10.7 and 11.3, with the explicit note that phi^5 = 5 phi + 3 ≈ 11.090.
proof idea
The term proof begins with constructor to split the conjunction into two inequalities. Each side is then discharged by linarith applied to the corresponding component of phi_fifth_bounds.
why it matters
The declaration supports the rs_device definition, the canonical RS-coherent PBM device that sets alpha_freq_Hz to phi^5. It supplies the brainwave entrainment justification for the device specification and aligns with the eight-tick octave structure in the forcing chain. The module documentation identifies this frequency as the recommended default modulation for relaxed wakefulness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.