pith. sign in
module module moderate

IndisputableMonolith.ClassicalBridge.Fluids.Discrete

show as:
view Lean formalization →

This module supplies type definitions and parameters for a discrete approximation to incompressible Navier-Stokes within Recognition Science. Researchers constructing the RS-to-classical-fluids bridge cite it for the DiscreteModel layer. It consists entirely of parameter and structure definitions with no theorems or proofs.

claim$NSParams := (d, ν)$ with $d ∈ ℕ$ the spatial dimension and $ν > 0$ the viscosity; $DiscreteModel$ encodes the time-stepped state evolution under a chosen $DiscretizationKind$ and $EnergyFunctional$.

background

The ClassicalBridge.Fluids.Discrete module sits inside the larger ClassicalBridge domain and introduces the discrete layer needed for Navier-Stokes. Its sibling definitions are NSParams (dimension plus viscosity), TimeStep, DiscretizationKind, DiscreteModel (the core state object), and EnergyFunctional. These supply the concrete objects referenced by the downstream Bridge interface.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the DiscreteModel required by the RS ↔ Navier–Stokes Bridge interface. That interface lists four required pieces: a discrete NS approximation, LNAL spatial semantics, a simulation statement, and a CPM instantiation; this module provides the first piece.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

declarations in this module (5)