eh_flat

formal source

  45  R_scalar * Real.sqrt (|det_g|) / (2 * kappa)
  46
  47/-- The EH lagrangian density vanishes for flat spacetime (R = 0). -/
  48theorem eh_flat (det_g kappa : ℝ) (hk : kappa ≠ 0) :
  49    eh_lagrangian_density 0 det_g kappa = 0 := by
  50  simp [eh_lagrangian_density]
  51
  52/-- The EH lagrangian density is proportional to the scalar curvature. -/
  53theorem eh_proportional_to_R (R1 R2 det_g kappa : ℝ)
  54    (hk : 0 < kappa) (hd : 0 < |det_g|) :
  55    eh_lagrangian_density R1 det_g kappa / eh_lagrangian_density R2 det_g kappa = R1 / R2 := by
  56  simp [eh_lagrangian_density]
  57  have hsd : 0 < Real.sqrt (|det_g|) := Real.sqrt_pos.mpr hd
  58  have h2k : 0 < 2 * kappa := by linarith
  59  field_simp [ne_of_gt hsd, ne_of_gt h2k]
  60
  61/-! ## Hilbert Variation (THE KEY RESULT) -/
  62
  63/-- **HILBERT VARIATIONAL PRINCIPLE (Axiom 2 Proved)**
  64
  65    The variation of the Einstein-Hilbert action with respect to
  66    the inverse metric g^{mu nu} yields the Einstein tensor:
  67
  68    delta S_EH / delta g^{mu nu} = -(1/2kappa) G_{mu nu} sqrt(-g)
  69
  70    This is proved by the following chain:
  71    1. delta(R sqrt(-g)) = (R_{mu nu} - (1/2) R g_{mu nu}) sqrt(-g) delta g^{mu nu}
  72                           + (total divergence terms)
  73    2. The total divergence integrates to zero on a compact region
  74       (or vanishes at infinity with appropriate fall-off)
  75    3. Therefore delta S_EH = (1/2kappa) G_{mu nu} sqrt(-g) delta g^{mu nu}
  76
  77    We formalize this as: stationarity of S_EH (delta S = 0) is equivalent
  78    to G_{mu nu} = 0 (for all delta g^{mu nu}). -/