no_retuning_consistent

formal source

 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
 136  exact Real.rpow_pos_of_pos phi_pos _
 137
 138/-- The ILG alpha exponent: alpha = (1 - 1/phi) / 2 = alphaLock. -/
 139theorem ilg_alpha_is_alphaLock : alphaLock = (1 - 1/phi) / 2 := rfl
 140
 141/-! ## Certificate -/
 142
 143structure CoerciveProjectionCert where
 144  coercivity_positive : (0 : ℚ) < c_coercive
 145  net_above_one : (1 : ℚ) < K_net
 146  operator_positive : ∀ w f : ℝ, 1 ≤ w → 0 ≤ w * f ^ 2
 147  prefactor_positive : 0 < C_ilg_prefactor
 148
 149theorem coercive_projection_cert : CoerciveProjectionCert where
 150  coercivity_positive := c_coercive_pos
 151  net_above_one := K_net_gt_one
 152  operator_positive := fun w f hw => energy_bounded_below w f hw (sq_nonneg f)
 153  prefactor_positive := C_ilg_prefactor_pos
 154