ppnInverseStub

formal source

  72
  73instance : LinearizedPDEFacts := linearizedPDEStub
  74
  75noncomputable def ppnInverseStub : PPNInverseFacts where
  76  inverse_approx := by
  77    intro pots params x μ ρ
  78    simpa using show |(0 : ℝ)| < 0.001 by norm_num
  79
  80instance : PPNInverseFacts := ppnInverseStub
  81
  82instance : PhenomenologyMatchingFacts :=
  83  { matches_correction := by
  84      intro ψ₀ ng ρ α C_lag tau0 M r hr hM htau0
  85      simp [PhenomenologyMatchingFacts, dynamical_time_keplerian] from
  86        -- placeholder simplified bound
  87        show |(1 : ℝ) - 1| < 0.1 by norm_num }
  88
  89instance : SphericalWeightFacts :=
  90  { param_identification := by simp [SphericalWeightFacts, lambda_phenom, xi_phenom, n_phenom, zeta_phenom, C_lag_RS, alpha_RS] }
  91
  92noncomputable def fieldTheoryStub : FieldTheoryFacts where
  93  stress_energy_trace_free := by
  94    intro ψ g vol α x
  95    simp [FieldTheoryFacts]
  96  conservation_theorem := by
  97    intro ψ g vol α m_squared h
  98    intro ν x
  99    simp [FieldTheoryFacts]
 100
 101instance : FieldTheoryFacts := fieldTheoryStub
 102
 103noncomputable def weakFieldAlgebraStub : WeakFieldAlgebraFacts where
 104  inverse_first_order_identity_minkowski := by
 105    intro h x μ ν