pith. machine review for the scientific record. sign in
def definition def or abbrev high

heatFactor

show as:
view Lean formalization →

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.

claimFor 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 160noncomputable def heatFactor (ν : ℝ) (t : ℝ) (k : Mode2) : ℝ :=

proof body

Definition body.

 161  Real.exp (-ν * kSq k * t)
 162
 163/-- Mild Stokes/heat solution in Fourier coefficients (modewise, for `t ≥ 0`). -/

used by (31)

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

… and 1 more

depends on (3)

Lean names referenced from this declaration's body.