 298
 299/-- RS-coherent photobiomodulation device specification.
 300    Every field is derived from the golden ratio φ. -/
 301structure PBMDeviceSpec where
 302  /-- Operating wavelength (meters) -/
 303  wavelength_m : ℝ
 304  /-- Window-neutral modulation pattern -/
 305  modulation_pattern : WindowNeutralPattern
 306  /-- Theta mode frequency (Hz) -/
 307  theta_freq_Hz : ℝ
 308  /-- Alpha mode frequency (Hz) -/
 309  alpha_freq_Hz : ℝ
 310  /-- Gamma mode frequency (Hz) -/
 311  gamma_freq_Hz : ℝ
 312  /-- Ticks per modulation cycle -/
 313  ticks_per_cycle : ℕ
 314
 315  wavelength_pos : 0 < wavelength_m
 316  wavelength_therapeutic : 750e-9 < wavelength_m ∧ wavelength_m < 780e-9
 317  ticks_is_eight : ticks_per_cycle = 8
 318  theta_in_band : 4 < theta_freq_Hz ∧ theta_freq_Hz < 8
 319  alpha_in_band : 8 < alpha_freq_Hz ∧ alpha_freq_Hz < 13
 320  gamma_in_band : 30 < gamma_freq_Hz ∧ gamma_freq_Hz < 100
 321  modes_ordered : theta_freq_Hz < alpha_freq_Hz ∧ alpha_freq_Hz < gamma_freq_Hz
 322
 323/-- The canonical RS-coherent PBM device.
 324    All parameters are derived from φ with zero free parameters. -/
 325noncomputable def rs_device : PBMDeviceSpec := {
 326  wavelength_m := lambda_PBM
 327  modulation_pattern := rs_neutral_pattern
 328  theta_freq_Hz := phi ^ 3
 329  alpha_freq_Hz := phi ^ 5
 330  gamma_freq_Hz := phi ^ 8
 331  ticks_per_cycle := 8

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.