`NSParams`

definition

show as: view math explainer →

module: IndisputableMonolith.ClassicalBridge.Fluids.Discrete
domain: ClassicalBridge
line: 21 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.ClassicalBridge.Fluids.Discrete on GitHub at line 21.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.