ILG_falsified

formal source

  50def tight_threshold : ℝ := 3.0
  51
  52/-- ILG is falsified if median chi2/dof exceeds the generous threshold. -/
  53def ILG_falsified (median_chi2_dof : ℝ) : Prop :=
  54  generous_threshold < median_chi2_dof
  55
  56/-- The RS-specific prediction is refuted if median > tight threshold. -/
  57def RS_prediction_refuted (median_chi2_dof : ℝ) : Prop :=
  58  tight_threshold < median_chi2_dof
  59
  60/-- If the median is below the generous threshold, ILG PASSES. -/
  61def ILG_passes (median_chi2_dof : ℝ) : Prop :=
  62  median_chi2_dof ≤ generous_threshold
  63
  64/-- The falsification criterion is decidable (for any real number). -/
  65theorem falsification_decidable (x : ℝ) :
  66    ILG_falsified x ∨ ILG_passes x := by
  67  unfold ILG_falsified ILG_passes generous_threshold
  68  exact le_or_gt x 5.0 |>.elim (Or.inr) (Or.inl)
  69
  70/-! ## RS Parameter Lock -/
  71
  72/-- The alpha parameter is locked to alphaLock ≈ 0.191. -/
  73noncomputable def alpha_locked : ℝ := alphaLock
  74
  75/-- The mass-to-light ratio is locked to phi ≈ 1.618. -/
  76noncomputable def upsilon_locked : ℝ := phi
  77
  78/-- The lag coupling is locked to phi^(-5) ≈ 0.090. -/
  79noncomputable def clag_locked : ℝ := cLagLock
  80
  81/-- All three parameters are derived from phi (zero free parameters). -/
  82theorem parameters_from_phi :
  83    alpha_locked = (1 - 1/phi) / 2 ∧