HelicityProxy
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not implement continuum helicity dynamics or Navier-Stokes equations.
- Does not expose direct links to LNAL invariants.
- Does not derive helicity values from spin statistics beyond the placeholder field.
formal statement (Lean)
66structure HelicityProxy where
67 value : ℝ
68
69/-- Attach a helicity proxy to a medium state (display-level wrapper). -/