phi_eighth_in_gamma_band
plain-language theorem explainer
The eighth power of the golden ratio satisfies 30 < φ^8 < 100 and therefore sits inside the gamma EEG band. Device specifications in Recognition Science cite the result to fix the gamma mode at φ^8 Hz. The proof rewrites φ^8 via its Fibonacci closed form and finishes with linear arithmetic on the interval bounds 1.61 < φ < 1.62.
Claim. $30 < φ^8 ∧ φ^8 < 100$, where $φ = (1 + √5)/2$ is the golden ratio.
background
The Applied.PhotobiomodulationDevice module constructs an RS-coherent light therapy device whose frequencies follow the φ-ladder. Theta, alpha, and gamma modes are assigned φ^3, φ^5, and φ^8 Hz respectively so that each lands in a distinct EEG band. The upstream lemma phi_eighth_eq supplies the identity φ^8 = 21φ + 13 (Fibonacci recurrence), while phi_gt_onePointSixOne and phi_lt_onePointSixTwo give the tight numerical bounds 1.61 < φ < 1.62 that turn the target interval check into an immediate arithmetic verification.
proof idea
The term proof first rewrites the goal with phi_eighth_eq to obtain an expression linear in φ. It then splits the conjunction and applies nlinarith to each conjunct, feeding in the two bounding lemmas on φ.
why it matters
This theorem supplies the gamma frequency for the canonical rs_device definition and is invoked inside modes_span_distinct_bands to separate the three device modes into non-overlapping bands. It realizes the brainwave entrainment step of the module, linking the eight-tick octave to the observed gamma range (30–100 Hz) associated with cross-modal binding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.