PsiActionP

formal source

  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
 112  h_gw : 0 ≤ κ_gw
 113
 114/-- Map ILG parameters to a bands schema (toy: proportional to |C_lag·α|). -/
 115noncomputable def bandsFromParams (p : ILGParams) : Bands :=
 116  let κ := |p.cLag * p.alpha|
 117  { κ_ppn := κ, κ_lensing := κ, κ_gw := κ
 118  , h_ppn := by exact abs_nonneg _
 119  , h_lensing := by exact abs_nonneg _
 120  , h_gw := by exact abs_nonneg _ }
 121
 122/-! Symbolic Einstein equations moved to Variation/Einstein.lean.
 123    VacuumEinstein now defined with real G_μν = 0. -/
 124
 125/-- Bundle the action inputs `(g, ψ)` for convenience in downstream modules. -/
 126abbrev ActionInputs := Metric × RefreshField
 127
 128/-- Apply total action on bundled inputs. -/
 129noncomputable def S_on (inp : ActionInputs) (p : ILGParams) : ℝ :=