theorem
proved
rs_pattern_phi_components_neutral
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Applied.PhotobiomodulationDevice on GitHub at line 243.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
240theorem rs_pattern_peak : rs_pattern ⟨0, by omega⟩ = phi := rfl
241
242/-- The φ-indexed entries (k = 0, 2, 4, 6) independently sum to zero. -/
243theorem rs_pattern_phi_components_neutral :
244 rs_pattern ⟨0, by omega⟩ + rs_pattern ⟨2, by omega⟩ +
245 rs_pattern ⟨4, by omega⟩ + rs_pattern ⟨6, by omega⟩ = 0 := by
246 simp only [rs_pattern]
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).