  29def pressure (W : Kernel) (k a ρ δ : ℝ) : ℝ := ρ * (W k a) * δ
  30
  31/- Effective source via pressure display: 4π G a^2 p. -/
  32def effectiveSource_pressure (P : Phys) (W : Kernel) (k a ρ δ : ℝ) : ℝ :=
  33  4 * Real.pi * P.G * (a ^ 2) * pressure W k a ρ δ
  34
  35/- Algebraic equivalence (display-only): identical right-hand sides. -/
  36theorem source_equiv (P : Phys) (W : Kernel) (k a ρ δ : ℝ) :
  37  effectiveSource P W k a ρ δ = effectiveSource_pressure P W k a ρ δ := rfl
  38
  39end PressureForm
  40end ILG
  41end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.