pith. sign in
module module high

IndisputableMonolith.ClassicalBridge.Fluids.CPM

show as:
view Lean formalization →

The module supplies a CPM instantiation for a particular state type in the classical fluids bridge. Researchers building the discrete Navier-Stokes approximation cite it to satisfy the CPM requirement inside the RS-NS bridge specification. The module directly applies the generic A/B/C structure imported from LawOfExistence without adding new proofs.

claimCPM instantiation for state type $S$ implementing the projection-defect inequality, coercivity factorization, and aggregation principle.

background

The upstream LawOfExistence module supplies a generic formalization of the Coercive Projection Method (CPM) in three parts: A: Projection-Defect inequality; B: Coercivity factorization (energy gap controls defect); C: Aggregation principle (local tests imply membership). This module instantiates those parts for a fluids-specific state type. The classical bridge context requires such an instantiation to connect Recognition Science to discrete Navier-Stokes approximations.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

This module supplies the CPM instantiation required by the RS ↔ Navier–Stokes Bridge interface and is imported by the CPM2D module for the 2D Galerkin model. It fills the role of packaging the core CPM structures for downstream discrete model simulations in the fluids domain.

scope and limits

used by (2)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (1)