bandsFromParams

formal source

 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) : ℝ :=
 130  S_total inp.fst inp.snd p
 131
 132/-- Full ILG action: S[g, ψ; C_lag, α] := S_EH[g] + S_ψ[g,ψ]. -/
 133noncomputable def S (g : Metric) (ψ : RefreshField) (C_lag α : ℝ) : ℝ :=
 134  S_EH g + PsiAction g ψ C_lag α
 135
 136/-- GR-limit reduction: when C_lag = 0 and α = 0, the ψ-sector vanishes. -/
 137theorem gr_limit_reduces (g : Metric) (ψ : RefreshField) :
 138  S g ψ 0 0 = S_EH g := by
 139  unfold S PsiAction PsiKinetic PsiPotential
 140  simp [Fields.kinetic_action, Fields.potential_action]
 141
 142/-- GR-limit for bundled parameters (α=0, C_lag=0). -/
 143theorem gr_limit_zero (g : Metric) (ψ : RefreshField) :
 144  S_total g ψ { alpha := 0, cLag := 0 } = S_EH g := by
 145  unfold S_total PsiAction PsiKinetic PsiPotential