modes_span_distinct_bands

formal source

 285  constructor <;> nlinarith [phi_gt_onePointSixOne, phi_lt_onePointSixTwo]
 286
 287/-- The three device modes span distinct, non-overlapping frequency ranges. -/
 288theorem modes_span_distinct_bands :
 289    phi ^ 3 < phi ^ 5 ∧ phi ^ 5 < phi ^ 8 := by
 290  constructor
 291  · linarith [phi_cubed_bounds.2, phi_fifth_bounds.1]
 292  · linarith [phi_fifth_bounds.2, phi_eighth_in_gamma_band.1]
 293
 294/-! ## Section 5: Device Specification
 295
 296The complete RS-coherent PBM device specification.
 297All parameters derive from φ with zero free parameters. -/
 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