PressureParams

formal source

  33`p0` is a baseline (ambient) pressure in the chosen display units.
  34`cω` is a coupling coefficient (nonnegative).
  35-/
  36structure PressureParams where
  37  p0  : ℝ
  38  cω  : ℝ
  39  hcω : 0 ≤ cω
  40
  41/-- Pressure proxy (display model): `p = p0 - cω · |ω|^2`.
  42
  43This is *not* asserted to equal physical pressure until we supply a
  44`PressureDropFromVorticity` instance.
  45-/
  46noncomputable def pressureProxy (P : PressureParams) (S : MediumState) : ℝ :=
  47  P.p0 - P.cω * (omegaMag S) ^ 2
  48
  49/-- Hypothesis interface: the operational pressure equals the proxy.
  50
  51This should eventually be replaced by a stronger bridge theorem under a
  52chosen fluid model.
  53-/
  54class PressureDropFromVorticity (P : PressureParams) where
  55  pressure : MediumState → ℝ
  56  pressure_eq : ∀ S, pressure S = pressureProxy P S
  57
  58/-- Convenience lemma: once the hypothesis holds, we can rewrite pressure to the proxy. -/
  59lemma pressure_eq_proxy (P : PressureParams) [H : PressureDropFromVorticity P] (S : MediumState) :
  60    H.pressure S = pressureProxy P S :=
  61  H.pressure_eq S
  62
  63end Pressure
  64end Flight
  65end IndisputableMonolith
  66