pressureProxy
plain-language theorem explainer
The pressure proxy supplies the explicit formula p = p0 - cω |ω|^2 for a display model of pressure in a medium state. Researchers modeling fluid pressure drops in vortical flows cite this before invoking the PressureDropFromVorticity hypothesis. The definition is a direct one-line algebraic expression using the omegaMag conversion from log-vorticity.
Claim. Let $P = (p_0, c_ω)$ with $c_ω ≥ 0$. For a medium state $S$, the pressure proxy is $p_0 - c_ω · |ω(S)|^2$, where $|ω(S)|$ is the positive magnitude obtained by exponentiating the absolute log-vorticity at the center voxel.
background
The Flight Pressure module separates a mathematical proxy definition from a physical hypothesis. PressureParams is a structure holding baseline pressure p0 and nonnegative coupling cω. MediumState consists of a center VorticityVoxel and a list of neighbors. omegaMag converts the signed log-vorticity to a positive magnitude via exponentiation of its absolute value. This proxy is intended for display purposes in flight modeling and connects to the ClassicalBridge.Fluids.CPM2D for fluid models via the Hypothesis bundle that encodes projection defects and energy gaps. The upstream bridge packs the model into CPMBridge for traceability.
proof idea
This is a one-line definition that directly computes P.p0 minus P.cω times the square of omegaMag applied to S.
why it matters
This definition provides the concrete expression that the PressureDropFromVorticity class equates to operational pressure. It fills the display model slot in the Flight Pressure Layer, separating proxy from hypothesis as described in the module documentation. It supports downstream lemmas like pressure_eq_proxy that rewrite pressure to the proxy once the hypothesis holds. In the Recognition framework it interfaces fluid models from the CPM2D bridge to the ILG pressure form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.