PressureDropFromVorticity
plain-language theorem explainer
PressureDropFromVorticity supplies a hypothesis interface asserting that operational pressure on a medium state equals the vorticity-magnitude proxy. Fluid modelers cite it when separating a display formula from measured pressure. The declaration is a class definition that packages the equality as instance fields rather than a derived theorem.
Claim. Let $P=(p_0,c_ω)$ be parameters with $c_ω≥0$. A hypothesis interface asserts the existence of a pressure map such that for every medium state $S$ the operational pressure equals $p_0-c_ω|ω(S)|^2$.
background
The Flight Pressure module separates a mathematical proxy from a physical hypothesis. PressureParams is the structure holding baseline pressure $p_0$ and nonnegative coupling coefficient $c_ω$. pressureProxy is the explicit display formula $p_0-c_ω(ωMag S)^2$, where ωMag extracts the signed log-vorticity magnitude from the center voxel of a MediumState. MediumState itself is the minimal patch consisting of a center VorticityVoxel plus its neighborhood list, mirroring the LNAL VM evolution step.
proof idea
This is a class definition with an empty proof body. It directly declares the two fields pressure and pressure_eq; the latter is the universal quantification that equates the operational pressure to the proxy for every medium state.
why it matters
The interface is the immediate parent of the convenience lemma pressure_eq_proxy, which rewrites any occurrence of the operational pressure to the proxy once an instance is supplied. It implements the module's stated separation between the always-available proxy and the physical hypothesis that must later be replaced by a stronger bridge theorem under a chosen fluid model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.