defect_bound_constant_value

formal source

  63    The constant M * K_net * C_proj controls the stability of the energy minimizer. -/
  64def defect_bound_constant : ℚ := K_net * C_proj
  65
  66theorem defect_bound_constant_value :
  67    defect_bound_constant = 162 / 49 := by
  68  unfold defect_bound_constant K_net C_proj; norm_num
  69
  70/-! ## Pressure Equivalence -/
  71
  72/-- The ILG modified Poisson equation is EQUIVALENT to the standard Poisson
  73    equation with an effective pressure source:
  74
  75    ILG:      nabla^2 Phi = 4*pi*G * a^2 * (w * rho_b * delta_b)
  76    Standard: nabla^2 Phi = 4*pi*G * a^2 * p
  77
  78    where p = w * rho_b * delta_b is the "effective pressure."
  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,