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

IndisputableMonolith.ClassicalBridge.Fluids.CPM2D

show as:
view Lean formalization →

The module supplies the CPM instantiation for the 2D Galerkin truncation of incompressible Navier-Stokes. It defines the discrete state at truncation level N together with defectMass, energyGap, and test functionals that satisfy the generic A/B/C inequalities. Workers on the Recognition fluids pipeline cite it to connect the finite model to the abstract existence theorem. The content is definitional with direct algebraic checks on the squared norms.

claimThe module defines the discrete state space $S_N$ for the truncated 2D Fourier modes on the torus and the functionals $d$, $e$, $t$ such that the projection-defect inequality, coercivity factorization (energy gap controls defect), and aggregation principle hold.

background

The Coercive Projection Method (CPM) provides a generic, domain-agnostic framework in three parts: A projection-defect inequality, B coercivity factorization where the energy gap controls the defect, and C aggregation principle from local tests to membership. This module instantiates the framework for 2D incompressible Navier-Stokes using the finite-dimensional Galerkin model, which represents truncated Fourier modes as a Finset with the basic algebraic energy identity for the inviscid case. The state type is the discrete 2D Galerkin state at truncation level N, equipped with functionals including defectMass, orthoMass, energyGap, and tests, verified through norm-squared identities.

proof idea

This is a definition module, no proofs. It introduces the State type, Functionals, and Hypothesis, then defines model, bridge, constantsOne, functionalsNormSq, hypothesisNormSq, and bridgeNormSq that discharge the CPM requirements via direct algebraic verification of the squared-norm hypotheses.

why it matters in Recognition Science

This module provides the concrete CPM bridge required by the 2D fluids pipeline. It feeds the ContinuumLimit2D and Regularity2D modules, which compose it with the Galerkin model and LNAL encoding to reach an abstract continuum solution existence result. It realizes the M4 step in the milestone sequence for passing from discrete approximations to the continuum limit.

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)