heatFactor
plain-language theorem explainer
heatFactor supplies the explicit Fourier multiplier exp(-ν |k|² t) that damps each mode in the linear Stokes evolution for the 2D continuum limit. Analysts constructing mild solutions or Duhamel integrals from Galerkin truncations cite it to obtain kernel bounds and dominated-convergence hypotheses. It is realized as a direct one-line definition that multiplies viscosity, squared wavenumber, and time inside the real exponential.
Claim. For viscosity ν ∈ ℝ, time t ∈ ℝ and wave vector k ∈ ℤ × ℤ, the heat factor is defined by exp(-ν |k|² t), where |k|² = k₁² + k₂².
background
The ContinuumLimit2D module constructs a Lean-checkable pipeline from finite Galerkin truncations to an infinite Fourier coefficient state, keeping compactness and identification steps as explicit hypotheses. Within this setting heatFactor supplies the modewise multiplier for the linear heat/Stokes part of the evolution. Mode2 is the type ℤ × ℤ of integer wave vectors; kSq extracts the squared Euclidean norm |k|² = k₁² + k₂², which appears directly in the exponent because the Fourier Laplacian multiplies coefficients by -|k|².
proof idea
The definition is a one-line wrapper that applies the real exponential to the product of negative viscosity, the squared wavenumber returned by kSq, and the time argument.
why it matters
heatFactor is the central linear kernel object invoked by thirty-one downstream declarations, among them abs_heatFactor_le_one, duhamelKernelIntegral, duhamelRemainderOfGalerkin and the dominated-convergence structures. It supplies the explicit damping factor required for the variation-of-constants formula that converts the forced Galerkin ODE into an integral identity, exactly as needed for the M5 milestone pipeline from discrete to continuum Navier-Stokes. In the Recognition framework it anchors the classical-bridge step that prepares dominated-convergence arguments for the fluid limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.