ratioInRange

formal source

 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
 135/-- Distance-independent healing study protocol -/
 136structure HealingProtocol where
 137  /-- Number of healer-patient pairs -/
 138  n_pairs : ℕ := 50
 139  /-- Distances to test (meters) -/
 140  distances : List ℝ := [1, 10, 100, 1000, 10000]
 141  /-- Blinding: healer knows when sending, patient does not -/
 142  double_blind_patient : Bool := true
 143  /-- Outcome measures -/
 144  outcomes : List String := ["subjective_wellbeing", "HRV_coherence", "EEG_phase_locking"]
 145
 146/-- Healing coherence transfer prediction -/
 147structure HealingPrediction where
 148  /-- Predicted increase in patient coherence (effect size d) -/
 149  effect_size : ℝ := 0.5
 150  /-- Effect should NOT decay with distance -/
 151  distance_independent : Bool := true
 152  /-- Minimum phase locking value (PLV) increase -/
 153  min_plv_increase : ℝ := 0.1
 154
 155/-- Data from a single healing trial -/
 156structure HealingTrialData where
 157  distance : ℝ
 158  effect_size : ℝ
 159  plv_change : ℝ
 160