IndisputableMonolith.ClassicalBridge.Fluids.Discrete

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace ClassicalBridge
   5namespace Fluids
   6
   7/-!
   8# Fluids Bridge: Discrete model interface
   9
  10This file deliberately does **not** pick a discretization yet (Galerkin vs grid).
  11It defines the minimal interface we need for a discrete Navier–Stokes approximation
  12that we can later relate to:
  13
  14- an LNAL spatial execution semantics, and
  15- a CPM instantiation (defect/energy/tests).
  16
  17Downstream files should introduce concrete models (e.g. Galerkin on `𝕋^2` first).
  18-/
  19
  20/-- Parameters for incompressible Navier–Stokes (dimension + viscosity). -/
  21structure NSParams where
  22  /-- Spatial dimension (use 2 first, then lift to 3). -/
  23  d : ℕ := 3
  24  /-- Kinematic viscosity. -/
  25  ν : ℝ := 1
  26
  27/-- Validity predicate for parameters (keep proofs out of the structure to avoid hidden coercions). -/
  28def NSParams.Valid (p : NSParams) : Prop :=
  29  0 < p.ν ∧ 2 ≤ p.d
  30
  31/-- A discrete time step (Δt > 0). -/
  32structure TimeStep where
  33  Δt : ℝ := 1
  34
  35def TimeStep.Valid (h : TimeStep) : Prop := 0 < h.Δt
  36
  37/-- High-level choice of discretization family. -/
  38inductive DiscretizationKind where
  39  | spectralGalerkin
  40  | finiteDifference
  41deriving DecidableEq
  42
  43/-- A discrete dynamical model intended to approximate NS. -/
  44structure DiscreteModel where
  45  /-- State type (e.g. truncated Fourier coefficients). -/
  46  State : Type
  47  /-- Tag: Galerkin vs grid, etc. -/
  48  kind : DiscretizationKind
  49  /-- One (discrete) time step of the model. -/
  50  step : NSParams → TimeStep → State → State
  51
  52/-- Optional energy functional on the discrete state (used for a priori bounds). -/
  53structure EnergyFunctional (D : DiscreteModel) where
  54  E : D.State → ℝ
  55
  56end Fluids
  57end ClassicalBridge
  58end IndisputableMonolith
  59