`isEEGFalsified`

definition

show as: view math explainer →

module: IndisputableMonolith.Experiments.Protocols
domain: Experiments
line: 89 · 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 89.

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

formal source

  86  (|f - φ^(3 : ℤ)| < tolerance)
  87
  88/-- The EEG prediction is falsified if too few peaks match -/
  89def isEEGFalsified (data : EEGFalsification) : Prop :=
  90  (data.measured_peaks.filter (matchesPhiPeak · data.tolerance)).length < data.min_matches
  91
  92/-! ## Mode Ratio Predictions -/
  93
  94/-- Consciousness state classification -/
  95inductive ConsciousnessState
  96  | baseline
  97  | flow
  98  | analytical
  99  | meditation
 100  | sleep
 101  deriving DecidableEq, Repr
 102
 103/-- M2/M4 ratio measurement protocol -/
 104structure ModeRatioProtocol where
 105  /-- States to measure -/
 106  states : List ConsciousnessState := [.baseline, .flow, .analytical, .meditation]
 107  /-- Number of trials per state -/
 108  trials_per_state : ℕ := 20
 109  /-- Measurement modality -/
 110  modality : String := "EEG_coherence"
 111
 112/-- Predictions for mode ratios by state -/
 113structure ModeRatioPrediction where
 114  state : ConsciousnessState
 115  /-- Expected M2/M4 ratio range (low bound) -/
 116  ratio_low : ℝ
 117  /-- Expected M2/M4 ratio range (high bound) -/
 118  ratio_high : ℝ
 119  /-- Prediction confidence -/

papers checked against this theorem

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