PressureParams
PressureParams bundles a baseline pressure p0 and nonnegative coupling coefficient cω to define a vorticity-based pressure proxy p = p0 - cω |ω|^2. Researchers building fluid display models in Recognition Science cite it to isolate mathematical proxies before attaching physical hypotheses. The definition is a plain structure declaration that records the three fields and enforces only the inequality on cω.
claimLet the pressure parameters consist of a baseline pressure $p_0$ and coupling coefficient $c_ω$ satisfying $c_ω ≥ 0$. The associated proxy pressure is then given by $p = p_0 - c_ω |ω|^2$, where this equality is not asserted to match operational pressure until a separate hypothesis instance is supplied.
background
The Flight.Pressure module introduces a pressure proxy to model drops driven by vorticity magnitude while keeping the mathematical expression separate from any claim of physical equivalence. The proxy formula uses the vorticity magnitude omegaMag drawn from a MediumState, and the module documentation states that the proxy remains available independently of any fluid model. PressureDropFromVorticity supplies the later hypothesis interface that equates operational pressure to this proxy under an instance.
proof idea
The declaration is a structure definition that directly introduces the three fields p0, cω and the nonnegativity constraint hcω. No lemmas or tactics are invoked; the object simply packages the parameters for use by pressureProxy and the PressureDropFromVorticity class.
why it matters in Recognition Science
PressureParams anchors the display-model side of the pressure layer and is referenced by pressureProxy and the PressureDropFromVorticity hypothesis interface. It supports the module's explicit separation of proxy from physical assertion, which later feeds into fluid-model bridges such as those constructed from CPM2D. The structure therefore occupies the position where Recognition Science keeps mathematical scaffolding distinct from empirical or axiomatic commitments.
scope and limits
- Does not assert that the proxy equals measured pressure.
- Does not fix units or scaling conventions for p0 or cω.
- Does not embed any specific fluid-model equations beyond the vorticity term.
- Does not supply default values or a solver for the parameters.
formal statement (Lean)
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-/