PressureParams
plain-language theorem explainer
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ω.
Claim. Let 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.