ILG_passes

formal source

  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 ∧
  84    upsilon_locked = phi ∧
  85    clag_locked = phi ^ (-(5 : ℝ)) := by
  86  unfold alpha_locked upsilon_locked clag_locked alphaLock cLagLock
  87  exact ⟨rfl, rfl, rfl⟩
  88
  89/-- The number of per-galaxy free parameters is exactly zero. -/
  90def per_galaxy_free_parameters : ℕ := 0
  91