HelicityProxy
plain-language theorem explainer
A lightweight structure supplying a single real-valued placeholder for helicity in discrete medium states. Researchers extending LNAL fluid models would reference it when adding auxiliary tracking slots to vorticity-based interfaces. The definition is a direct structure declaration with no lemmas or computation.
Claim. A helicity proxy consists of a structure with one field $value : ℝ$ that serves as a placeholder for helicity in a medium state.
background
The Flight.Medium module supplies a minimal discrete scaffold for medium states via vorticity proxies, without claiming a continuum Navier-Stokes model. The file is intentionally decoupled from LNAL invariants during their modernization. HelicityProxy provides the stubbed field referenced in LNAL fluids comments for auxiliary helicity tracking.
proof idea
Direct structure definition that introduces the real-valued field with no applied lemmas or tactics.
why it matters
The structure feeds the MediumStateH wrapper that attaches the proxy to a base MediumState. It closes a gap in the discrete Flight scaffold, permitting downstream refinement of helicity without committing to the full LNAL modernization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.