module module high

`IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D`

This module defines the infinite Fourier coefficient state for 2D velocity fields on the torus, extending the finite Galerkin truncation to the continuum limit. It supplies the M5 packaging step in the 2D fluids pipeline. Researchers assembling the full regularity composition would cite it. The module consists entirely of definitions and algebraic lemmas with no analytic estimates.

claimThe type $FourierState2D$ of full (infinite) Fourier coefficient states for divergence-free 2D velocity fields on the torus $𝕋²$, equipped with coefficient extraction $coeffAt$, zero-extension $extendByZero$ from finite truncations, and the associated linear structure and divergence-free constraint.

background

The module sits in the ClassicalBridge.Fluids hierarchy and imports Galerkin2D (finite Fourier-mode truncation of 2D incompressible Navier–Stokes on the torus, supplying discrete state space and inviscid energy identity) and CPM2D (instantiation of the CPM core that packages required analytic inequalities into explicit Hypothesis structures). It introduces the infinite extension of those finite states. The local setting is the 2D incompressible case on $𝕋²$ with no appeal to the Recognition Science forcing chain or phi-ladder.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

This module supplies the continuum-limit packaging (M5) required by the top-level composition theorem in Regularity2D, which assembles Galerkin2D (M1) + LNAL + CPM (M4) + this step into an abstract “continuum solution exists” conclusion. It closes the finite-to-infinite bridge without proving the analytic estimates themselves.

scope and limits

Does not prove any analytic inequalities for the continuum limit.
Does not discharge Hypothesis structures imported from CPM2D.
Does not address 3D flows or compressible cases.
Does not connect to the J-uniqueness or phi fixed-point machinery.
Does not establish existence or regularity of actual solutions.

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