pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.ClassicalBridge.Fluids.Discrete

show as:
view Lean formalization →

This module supplies type definitions and parameters for discretizing incompressible Navier-Stokes within Recognition Science. Researchers constructing the RS-classical fluid bridge cite it to fix dimension, viscosity, and model structure before stating simulation relations. It consists entirely of declarations for NSParams, TimeStep, DiscretizationKind, DiscreteModel, and EnergyFunctional.

claimThe module introduces $NSParams$ as a pair (spatial dimension, viscosity coefficient) for incompressible Navier-Stokes, together with $DiscreteModel$ (discrete state evolution) and $EnergyFunctional$ (associated energy).

background

The module resides in ClassicalBridge.Fluids and supplies the discrete layer that the RS-Navier-Stokes interface later consumes. Its central object NSParams records the dimension and viscosity needed to specialize the incompressible equations. Sibling declarations introduce TimeStep, DiscretizationKind, DiscreteModel, and EnergyFunctional as the concrete carriers for discrete evolution and energy.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The declarations feed directly into the RS ↔ Navier–Stokes Bridge interface, which requires a discrete NS approximation (DiscreteModel), an LNAL spatial semantics, and a simulation statement relating the two. By fixing NSParams and the model skeleton, the module closes the first item on the Bridge specification.

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)