L_cov

formal source

  78noncomputable def L_coupling (_g : Metric) (_ψ : RefreshField) (p : ILGParams) : ℝ := p.cLag * p.alpha
  79
  80/-- Covariant scalar Lagrangian (toy): L_cov = L_kin − L_mass + L_pot + L_coupling. -/
  81noncomputable def L_cov (g : Metric) (ψ : RefreshField) (p : ILGParams) : ℝ :=
  82  L_kin g ψ p - L_mass g ψ p + L_pot g ψ p + L_coupling g ψ p
  83
  84/-- Covariant total action using L_cov: S_cov = S_EH + ∫ L_cov (toy: scalar sum). -/
  85noncomputable def S_total_cov (g : Metric) (ψ : RefreshField) (p : ILGParams) : ℝ :=
  86  S_EH g + L_cov g ψ p
  87
  88/-- GR-limit for S_total_cov (α=0, C_lag=0). -/
  89theorem gr_limit_cov (g : Metric) (ψ : RefreshField) :
  90  S_total_cov g ψ { alpha := 0, cLag := 0 } = S_EH g := by
  91  unfold S_total_cov L_cov L_kin L_mass L_pot L_coupling
  92  simp
  93
  94/-- Convenience total action using bundled params. -/
  95noncomputable def S_total (g : Metric) (ψ : RefreshField) (p : ILGParams) : ℝ :=
  96  S_EH g + PsiAction g ψ p.cLag p.alpha
  97
  98/-- ψ-sector action using bundled parameters. -/
  99noncomputable def PsiActionP (g : Metric) (ψ : RefreshField) (p : ILGParams) : ℝ :=
 100  PsiKinetic g ψ p.alpha + PsiPotential g ψ p.cLag
 101
 102/-! Euler-Lagrange predicates moved to ILG/Variation.lean (now use real equations).
 103    EL_g and EL_psi now defined in Variation.lean with actual PDEs. -/
 104
 105/-- Consolidated bands schema for observables (scaffold). -/
 106structure Bands where
 107  κ_ppn : ℝ
 108  κ_lensing : ℝ
 109  κ_gw : ℝ
 110  h_ppn : 0 ≤ κ_ppn
 111  h_lensing : 0 ≤ κ_lensing