pith. sign in
module module high

IndisputableMonolith.ClassicalBridge.Fluids.Discrete

show as:
view Lean formalization →

This module defines the discrete parameters and model types for incompressible Navier-Stokes in the Recognition Science setting. It supplies NSParams for dimension and viscosity together with DiscreteModel, TimeStep, DiscretizationKind and EnergyFunctional. These objects are consumed by the Bridge module that outlines the full RS-to-NS interface. The module contains only definitions and imports Mathlib.

claimThe module introduces $NSParams$ (dimension and viscosity pair), $DiscreteModel$ (discrete state evolution for incompressible flow), $EnergyFunctional$, $TimeStep$ and $DiscretizationKind$.

background

The module resides in the ClassicalBridge.Fluids namespace and supplies the discrete approximation side of the Navier-Stokes bridge. NSParams encodes the spatial dimension together with the viscosity coefficient for incompressible flow. Sibling declarations define TimeStep for temporal stepping, DiscretizationKind for spatial schemes, DiscreteModel as the core evolution operator, and EnergyFunctional as the associated energy norm. The module imports only Mathlib and introduces no Recognition Science axioms.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies DiscreteModel and NSParams that the Bridge module requires for its RS ↔ Navier–Stokes interface specification. It therefore populates the first item in the four-point list given in the Bridge doc-comment: a discrete NS approximation.

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)