energy_bounded_below

formal source

 102  nlinarith [sq_nonneg f_val]
 103
 104/-- Operator positivity implies the energy functional is bounded below. -/
 105theorem energy_bounded_below (w_val f_val : ℝ) (hw : 1 ≤ w_val) (hf : 0 ≤ f_val ^ 2) :
 106    0 ≤ w_val * f_val ^ 2 := by
 107  exact mul_nonneg (by linarith) hf
 108
 109/-! ## No-Retuning Theorem -/
 110
 111/-- The No-Retuning Theorem: if the ILG potential is the unique energy
 112    minimizer for a GLOBAL kernel (same w for all galaxies), then changing
 113    w per galaxy would produce a DIFFERENT potential that is NOT the minimizer.
 114
 115    Formally: if w is the unique minimizer kernel, any w' != w gives
 116    a strictly higher energy. -/
 117def no_retuning (w_global : ℝ → ℝ) : Prop :=
 118  ∀ w' : ℝ → ℝ, w' ≠ w_global →
 119    ∀ x, w_global x * x ^ 2 ≤ w' x * x ^ 2 → w' x = w_global x
 120
 121/-- The no-retuning condition is consistent with operator positivity:
 122    if w_global(x) >= 1 for all x, the energy at w_global is bounded
 123    but finite, so a unique minimizer exists. -/
 124theorem no_retuning_consistent (w : ℝ → ℝ) (hw : ∀ x, 1 ≤ w x) :
 125    ∀ x f : ℝ, 0 ≤ w x * f ^ 2 :=
 126  fun x f => energy_bounded_below (w x) f (hw x) (sq_nonneg f)
 127
 128/-! ## ILG Kernel Prefactor from Papers -/
 129
 130/-- The ILG kernel prefactor C = phi^(-3/2) from the CPM and Dark-Energy papers.
 131    This replaces the earlier phi^(-5) = cLagLock in the galactic-scale kernel. -/
 132noncomputable def C_ilg_prefactor : ℝ := phi ^ (-(3/2 : ℝ))
 133
 134theorem C_ilg_prefactor_pos : 0 < C_ilg_prefactor := by
 135  unfold C_ilg_prefactor