PressureEquivalence

formal source

  79
  80    This equivalence means ILG is NOT a modification of GR's field equations
  81    but rather a modification of the SOURCE SIDE only. -/
  82structure PressureEquivalence where
  83  w_kernel : ℝ → ℝ
  84  rho_b : ℝ → ℝ
  85  delta_b : ℝ → ℝ
  86  effective_pressure : ℝ → ℝ
  87  equiv : ∀ x, effective_pressure x = w_kernel x * rho_b x * delta_b x
  88
  89/-- Any ILG kernel with w >= 1 defines a valid pressure equivalence. -/
  90theorem pressure_equiv_from_w (w rho delta : ℝ → ℝ) :
  91    ∃ p : ℝ → ℝ, ∀ x, p x = w x * rho x * delta x :=
  92  ⟨fun x => w x * rho x * delta x, fun _ => rfl⟩
  93
  94/-! ## Operator Positivity -/
  95
  96/-- The ILG weight operator is positive: if w(x) >= 1 for all x,
  97    then <f, w*f> >= ||f||^2 (in L^2 inner product sense).
  98
  99    We formalize this pointwise: w(x) * f(x)^2 >= f(x)^2. -/
 100theorem operator_positivity_pointwise (w_val f_val : ℝ) (hw : 1 ≤ w_val) :
 101    f_val ^ 2 ≤ w_val * f_val ^ 2 := by
 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