pith. sign in
module module high

IndisputableMonolith.ClassicalBridge.Fluids.CPM2D

show as:
view Lean formalization →

CPM2D instantiates the Coercive Projection Method for the 2D Galerkin truncation of incompressible Navier-Stokes on the torus. It supplies the discrete state type at truncation level N, the concrete functionals, and the hypothesis that the A/B/C conditions hold. Pipeline workers cite this as the M4 bridge between the discrete model and the continuum limit. The module consists entirely of definitions and hypotheses.

claimThe discrete 2D Galerkin state space $S_N$ at truncation level $N$, the associated CPM functionals (defectMass, orthoMass, energyGap), and the hypothesis that these satisfy the generic projection-defect, coercivity, and aggregation conditions.

background

This module belongs to the ClassicalBridge.Fluids domain and imports the domain-agnostic CPM interface, the 2D Galerkin model, and the Law of Existence core. Galerkin2D introduces a finite-dimensional Fourier-mode truncated model for 2D incompressible Navier-Stokes on the torus whose goal is a concrete discrete state space and the basic algebraic energy identity for the inviscid case. LawOfExistence supplies the generic A/B/C structure: A is the projection-defect inequality, B is the coercivity factorization in which the energy gap controls the defect, and C is the aggregation principle that local tests imply membership.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

CPM2D supplies the CPM instantiation (M4) that the 2D pipeline requires. It feeds ContinuumLimit2D (M5), which packages finite-dimensional Galerkin approximations into a continuum limit object, and Regularity2D (M6), whose top-level composition theorem states that Galerkin2D (M1) plus LNAL encoding plus one-step simulation plus CPM instantiation (M4) plus continuum limit packaging (M5) yields an abstract continuum solution. The module therefore closes the discrete-to-continuous step for 2D fluids.

scope and limits

used by (2)

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

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (9)