pith. machine review for the scientific record. sign in
structure

EEGProtocol

definition
show as:
view math explainer →
module
IndisputableMonolith.Experiments.Protocols
domain
Experiments
line
36 · github
papers citing
none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Experiments.Protocols on GitHub at line 36.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  33/-! ## EEG Frequency Predictions -/
  34
  35/-- A complete EEG experimental protocol -/
  36structure EEGProtocol where
  37  /-- Sample size for each group -/
  38  n_subjects : ℕ := 30
  39  /-- Recording duration in seconds -/
  40  duration_sec : ℕ := 600  -- 10 minutes
  41  /-- Sampling rate in Hz -/
  42  sampling_rate : ℕ := 256
  43  /-- Frequency resolution in Hz -/
  44  freq_resolution : ℝ := 0.1
  45  /-- Electrode positions (10-20 system) -/
  46  electrodes : List String := ["Fz", "Cz", "Pz", "O1", "O2"]
  47
  48/-- Predicted EEG peaks with confidence intervals -/
  49structure EEGPrediction where
  50  /-- The mode index n in φ^n -/
  51  mode_index : ℤ
  52  /-- Central frequency (φ^n Hz) -/
  53  center_freq : ℝ
  54  /-- Expected peak width (Hz) -/
  55  bandwidth : ℝ := 0.2
  56  /-- Minimum peak amplitude (μV²/Hz) -/
  57  min_amplitude : ℝ
  58  /-- Confidence level for detection -/
  59  confidence : ℝ := 0.95
  60
  61/-- The set of predicted EEG frequencies -/
  62noncomputable def eegPredictions : List EEGPrediction :=
  63  [⟨-2, φ^(-2 : ℤ), 0.2, 0.5, 0.95⟩,   -- ~0.38 Hz (infra-slow)
  64   ⟨-1, φ^(-1 : ℤ), 0.2, 0.5, 0.95⟩,   -- ~0.62 Hz (delta-low)
  65   ⟨0, 1, 0.2, 1.0, 0.95⟩,              -- 1.00 Hz (delta-high)
  66   ⟨1, φ, 0.2, 1.0, 0.95⟩,              -- ~1.62 Hz (delta-theta)