pith. sign in
module module moderate

IndisputableMonolith.NavierStokes.FRCBridge

show as:
view Lean formalization →

The FRCBridge module defines finite-volume vorticity profiles on RS lattices, packaging siteCount, omegaMax, omegaRms, and the finiteVolumeControl bound that equates pointwise and RMS norms via sqrt(siteCount). Researchers extending the phi-ladder cutoff to discrete Navier-Stokes would cite these structures to control energy cascades on finite windows. The module is a collection of definitions and elementary lemmas on normalized ratios and J-cost bounds.

claimA finite-volume vorticity profile consists of siteCount : \mathbb{N}, \omega_{\max}, \omega_{\mathrm{rms}} : \mathbb{R}, and finiteVolumeControl witnessing \| \omega \|_{\infty} \le \sqrt{\mathrm{siteCount}} \, \omega_{\mathrm{rms}} on an RS lattice.

background

This module belongs to the Navier-Stokes domain and imports PhiLadderCutoff, whose doc states it formalizes the algebraic and combinatorial core of the argument that the φ-ladder provides an ultraviolet cutoff terminating the Navier-Stokes energy cascade on the RS discrete lattice.

FiniteVolumeProfile is the central object: siteCount counts active lattice sites in the finite window, omegaMax and omegaRms package the relevant scales, and finiteVolumeControl supplies the norm-equivalence input that pointwise amplitude is controlled by sqrt(siteCount) times the RMS scale.

Sibling definitions supply normalizedRatio (with positivity, lower and upper bounds) together with Jcost_le_self_of_one_le and finiteVolume_Jcost_bound that prepare the lattice FRC statements.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the discrete-lattice bridge required by the phi-ladder cutoff argument for Navier-Stokes regularity. It feeds the main results listed in PhiLadderCutoff on ultraviolet termination of the energy cascade. It touches the T7 eight-tick octave and D=3 spatial dimensions by discretizing the RS lattice while leaving the continuous limit and full time-dependent regularity open.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (17)