theorem
proved
rs_pattern_sqrt_components_neutral
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Applied.PhotobiomodulationDevice on GitHub at line 250.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
247 ring
248
249/-- The √2/2-indexed entries (k = 1, 3, 5, 7) independently sum to zero. -/
250theorem rs_pattern_sqrt_components_neutral :
251 rs_pattern ⟨1, by omega⟩ + rs_pattern ⟨3, by omega⟩ +
252 rs_pattern ⟨5, by omega⟩ + rs_pattern ⟨7, by omega⟩ = 0 := by
253 simp only [rs_pattern]
254 ring
255
256/-! ## Section 4: Brainwave Entrainment Frequencies
257
258The device modulation frequencies are powers of φ in Hz, which
259fall naturally into known EEG bands:
260- φ³ ≈ 4.24 Hz → theta (4–8 Hz)
261- φ⁵ ≈ 11.09 Hz → alpha (8–13 Hz)
262- φ⁸ ≈ 46.98 Hz → gamma (30–100 Hz)
263
264This is not tuned — it falls out of the φ-ladder structure. -/
265
266/-- φ³ ≈ 4.24 Hz falls in the theta EEG band (4–8 Hz).
267 Theta waves: deep meditation, memory consolidation, healing. -/
268theorem phi_cubed_in_theta_band : 4 < phi ^ 3 ∧ phi ^ 3 < 8 := by
269 constructor
270 · linarith [phi_cubed_bounds.1]
271 · linarith [phi_cubed_bounds.2]
272
273/-- φ⁵ ≈ 11.09 Hz falls in the alpha EEG band (8–13 Hz).
274 Alpha waves: relaxed wakefulness, optimal healing coherence.
275 This is the recommended default device modulation. -/
276theorem phi_fifth_in_alpha_band : 8 < phi ^ 5 ∧ phi ^ 5 < 13 := by
277 constructor
278 · linarith [phi_fifth_bounds.1]
279 · linarith [phi_fifth_bounds.2]
280