rs_neutral_pattern

formal source

 233  neutral : Finset.univ.sum values = 0
 234
 235/-- The RS pattern constitutes a valid window-neutral pattern. -/
 236noncomputable def rs_neutral_pattern : WindowNeutralPattern :=
 237  ⟨rs_pattern, rs_pattern_window_neutral⟩
 238
 239/-- The peak value of the pattern occurs at k=0 and equals φ. -/
 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).