`ModeRatioProtocol`

definition

show as: view math explainer →

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

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

 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 -/
 120  confidence : ℝ := 0.95
 121
 122/-- The predicted mode ratios for each state -/
 123def modeRatioPredictions : List ModeRatioPrediction :=
 124  [⟨.flow, 1.5, 3.0, 0.95⟩,        -- High M2/M4 in flow
 125   ⟨.analytical, 0.3, 0.8, 0.95⟩,  -- Low M2/M4 in analytical
 126   ⟨.meditation, 0.9, 1.1, 0.95⟩,  -- Balanced in meditation
 127   ⟨.baseline, 0.8, 1.2, 0.90⟩]    -- Variable at baseline
 128
 129/-- Check if measured ratio falls in predicted range -/
 130noncomputable def ratioInRange (pred : ModeRatioPrediction) (measured : ℝ) : Bool :=
 131  pred.ratio_low ≤ measured && measured ≤ pred.ratio_high
 132
 133/-! ## Healing Study Predictions -/
 134

papers checked against this theorem

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