pressure_eq_proxy
plain-language theorem explainer
The lemma equates the pressure field defined by a vorticity-coupling hypothesis to its explicit proxy formula under the given parameters. Fluid dynamicists modeling pressure drops from local vorticity would invoke it to simplify calculations once the hypothesis is assumed. The proof is a direct application of the defining equality in the PressureDropFromVorticity class.
Claim. Let $P$ be parameters with baseline pressure $p_0$ and nonnegative coupling $c_ω$. Let $H$ be the hypothesis that operational pressure equals the proxy. For any medium state $S$, the pressure under $H$ equals $p_0 - c_ω · |ω(S)|^2$.
background
The Flight Pressure module separates a mathematical proxy definition from any physical claim that it matches measured pressure. PressureParams is a structure holding baseline pressure $p_0$ and coupling coefficient $c_ω ≥ 0$. The proxy itself is the display model $p = p_0 - c_ω · |ω|^2$, computed from the signed log-vorticity magnitude at the center of a MediumState. MediumState is a minimal local configuration consisting of a center vorticity voxel plus a list of neighbor voxels. PressureDropFromVorticity is the class interface supplying an operational pressure function together with the equality that it matches the proxy for every state.
proof idea
This is a one-line wrapper that applies the pressure_eq field of the PressureDropFromVorticity hypothesis instance to the given medium state S.
why it matters
This convenience lemma sits in the pressure layer of the flight model, enabling direct substitution of the proxy once the vorticity-to-pressure hypothesis is adopted. It prepares the ground for replacing the interface with a stronger bridge theorem under a chosen fluid model, as noted in the module documentation. No downstream uses are recorded yet, but it supports simplification in any proof involving pressure drops in vortical flows.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.