pith. machine review for the scientific record. sign in
theorem proved term proof

defect_bound_constant_value

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  66theorem defect_bound_constant_value :
  67    defect_bound_constant = 162 / 49 := by

proof body

Term-mode proof.

  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. -/

depends on (19)

Lean names referenced from this declaration's body.