PressureDropFromVorticity
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the proxy formula from the ILG action.
- Does not specify any concrete fluid model or constitutive relation.
- Does not assign numerical values to $p_0$ or $c_ω$.
- Does not prove existence of a solution to the Navier-Stokes equations.
Lean usage
lemma pressure_eq_proxy (P : PressureParams) [H : PressureDropFromVorticity P] (S : MediumState) : H.pressure S = pressureProxy P S := H.pressure_eq Sformal statement (Lean)
54class PressureDropFromVorticity (P : PressureParams) where
55 pressure : MediumState → ℝ
56 pressure_eq : ∀ S, pressure S = pressureProxy P S
57
58/-- Convenience lemma: once the hypothesis holds, we can rewrite pressure to the proxy. -/