module module high

`IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D`

ContinuumLimit2D supplies the infinite Fourier coefficient state for 2D velocity fields on the torus, extending the finite Galerkin truncation to the full continuum. Fluid dynamicists working on 2D Navier-Stokes regularity in the Recognition framework would cite it when moving from discrete models to continuous limits. The module achieves this by importing Galerkin2D and CPM2D to define the state space and related operators without embedding analytic proofs.

claimLet $FourierState2D$ be the space of all Fourier coefficients for a divergence-free 2D velocity field on the torus $𝕋²$, with $coeffAt$ extracting coefficients, $extendByZero$ the natural extension from finite truncations, and $IsDivergenceFree$ the constraint that the field remains incompressible.

background

This module belongs to the ClassicalBridge.Fluids section of the Recognition Science pipeline. It imports Galerkin2D, which introduces a finite-dimensional Fourier-mode truncated model for 2D incompressible Navier-Stokes on the torus, and CPM2D, which instantiates the CPM core for that model. The CPM2D doc states: 'the nontrivial analytic inequalities needed for a real fluids proof are not proved here. Instead, we package them explicitly in a ...Hypothesis structure.'

proof idea

This is a definition module, no proofs. It defines FourierState2D together with the sibling operations coeffAt, extendByZero, divConstraint and IsDivergenceFree by lifting the finite structures of Galerkin2D to infinite series while preserving the algebraic relations already established in the imported modules.

why it matters in Recognition Science

The module supplies the continuum-limit packaging (M5) required by Regularity2D (M6). The downstream doc describes Regularity2D as the top-level composition theorem: 'Galerkin2D (M1) + LNAL encoding/semantics (M2) + one-step simulation (M3) + CPM instantiation (M4) + continuum limit packaging (M5) ⇒ an abstract “continuum solution exists” conclusion.' It therefore closes the finite-to-infinite step in the 2D fluids chain.

scope and limits

Does not prove the analytic inequalities for the continuum limit; these remain packaged as hypotheses in CPM2D.
Does not establish existence of actual continuum solutions; that conclusion is assembled only in Regularity2D.
Does not treat 3D flows or compressible fluids; the construction is restricted to 2D incompressible fields on the torus.

used by (1)

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

IndisputableMonolith.ClassicalBridge.Fluids.Regularity2D module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.ClassicalBridge.Fluids.CPM2D module_import
IndisputableMonolith.ClassicalBridge.Fluids.Galerkin2D module_import

declarations in this module (61)

abbrev FourierState2D L37
def coeffAt L46
def extendByZero L55
lemma coeffAt_add L67
lemma coeffAt_smul L74
lemma extendByZero_add L81
lemma extendByZero_smul L88
lemma extendByZero_neg L95
def extendByZeroLinear L102
def extendByZeroCLM L114
def divConstraint L127
def IsDivergenceFree L131
def IsDivergenceFreeTraj L135
lemma divConstraint_continuous L138
def heatFactor L160
def IsStokesMildTraj L164
def IsStokesODETraj L175
def IsNSDuhamelTraj L194
theorem stokesODE L200
lemma extendByZero_laplacianCoeff L285
lemma hasDerivAt_extendByZero_apply L294
theorem galerkinNS_hasDerivAt_extendByZero_mode L309
def duhamelRemainderOfGalerkin L344
theorem galerkinNS_hasDerivAt_duhamelRemainder_mode L351
theorem duhamelRemainderOfGalerkin_integratingFactor L431
theorem duhamelRemainderOfGalerkin_kernel L527
def duhamelKernelIntegral L655
structure DuhamelKernelDominatedConvergenceAt L660
structure ForcingDominatedConvergenceAt L688
lemma abs_heatFactor_le_one L706
def duhamelKernelDominatedConvergenceAt_of_forcing L746
theorem tendsto_duhamelKernelIntegral_of_dominated_convergence L801
theorem galerkin_duhamelKernel_identity L831
lemma norm_extendByZero_le L863
structure UniformBoundsHypothesis L938
def galerkinForcing L971
structure GalerkinForcingDominatedConvergenceHypothesis L983
def forcingDCTAt L1008
theorem aestronglyMeasurable_galerkinForcing_mode_of_continuous L1023
def of_convectionNormBound L1055
def of_convectionNormBound_of_continuous L1112
structure ConvergenceHypothesis L1133
theorem coeff_bound_of_uniformBounds L1144
theorem divConstraint_eq_zero_of_forall L1173
theorem divFree_of_forall L1201
theorem stokesMild_of_forall L1209
theorem nsDuhamel_of_forall L1240
theorem nsDuhamel_of_forall_kernelIntegral L1285
theorem nsDuhamel_of_forall_kernelIntegral_of_forcing L1308
structure IdentificationHypothesis L1380
def trivial L1389
def coeffBound L1400
def divFreeCoeffBound L1412
def stokesMildCoeffBound L1429
def nsDuhamelCoeffBound L1451
def nsDuhamelCoeffBound_kernelIntegral L1471
def nsDuhamelCoeffBound_kernelIntegral_of_forcing L1492
def nsDuhamelCoeffBound_galerkinKernel L1517
def nsDuhamelCoeffBound_galerkinKernel_of_forcing L1554
def nsDuhamelCoeffBound_galerkinKernel_of_forcingHyp L1593
theorem continuum_limit_exists L1621