IndisputableMonolith.Flight.Medium

   1import Mathlib
   2
   3/-!
   4# Flight Medium (Aether / Light Field) — discrete scaffold
   5
   6This file defines a minimal “medium state” interface usable by Flight proofs.
   7
   8At this stage we do **not** claim a continuum Navier–Stokes model; we simply
   9use a discrete vorticity proxy.
  10
  11Note: this is intentionally **decoupled** from `IndisputableMonolith.LNAL` for
  12now because the LNAL invariants subtheory is being actively modernized to the
  13current toolchain/mathlib.
  14-/
  15
  16namespace IndisputableMonolith
  17namespace Flight
  18namespace Medium
  19
  20open scoped Real
  21
  22/-! ## Discrete vorticity proxy -/
  23
  24/-- Local vorticity voxel proxy for Flight.
  25
  26This mirrors the shape of the LNAL `VorticityVoxel` record, but lives in the
  27Flight namespace so Flight can compile independently of the larger VM stack.
  28-/
  29structure VorticityVoxel where
  30  /-- Signed log-vorticity proxy (display units). -/
  31  logVorticity    : ℝ
  32  /-- Stream function proxy (display units). -/
  33  streamFunction  : ℝ := 0
  34  /-- Parity/sign channel (integer lattice). -/
  35  signParity      : Int := 1
  36  /-- Coarse time slice / tick index. -/
  37  timeSlice       : Nat := 0
  38  /-- Discrete velocity mode. -/
  39  velocityMode    : Int := 0
  40  /-- Discrete phase index. -/
  41  vorticityPhase  : Int := 0
  42
  43/-- A minimal medium state: a center voxel plus a neighborhood.
  44
  45This intentionally mirrors the way the LNAL VM would evolve a local patch.
  46-/
  47structure MediumState where
  48  center    : VorticityVoxel
  49  neighbors : List VorticityVoxel
  50
  51/-- Convenience: the signed log-vorticity at the center voxel.
  52
  53`logVorticity` is treated as a φ-quantized proxy for `log |ω|`.
  54-/
  55@[simp] def logVorticity (S : MediumState) : ℝ := S.center.logVorticity
  56
  57/-- Convenience: absolute log-vorticity (magnitude proxy). -/
  58@[simp] def absLogVorticity (S : MediumState) : ℝ := |S.center.logVorticity|
  59
  60/-- A very lightweight “helicity proxy” placeholder.
  61
  62In the LNAL fluids comments, helicity is tracked in an auxiliary slot; the
  63current domain file does not expose it directly, so we provide a stubbed
  64field for downstream refinement.
  65-/
  66structure HelicityProxy where
  67  value : ℝ
  68
  69/-- Attach a helicity proxy to a medium state (display-level wrapper). -/
  70structure MediumStateH where
  71  S : MediumState
  72  H : HelicityProxy
  73
  74end Medium
  75end Flight
  76end IndisputableMonolith
  77
  78