pith. sign in
module module high

IndisputableMonolith.NavierStokes.FRCBridge

show as:
view Lean formalization →

The FRCBridge module defines finite-volume vorticity profiles on RS lattices, packaging siteCount, omegaMax, omegaRms, and finiteVolumeControl to enforce norm equivalence via sqrt(siteCount) scaling of RMS values. Researchers studying discrete approximations to Navier-Stokes regularity would cite these structures to control pointwise amplitudes on finite windows. The module imports the phi-ladder cutoff from PhiLadderCutoff and assembles supporting lemmas on normalized ratios and J-cost bounds to bridge lattice data to the energy cascade.

claimA finite-volume vorticity profile on an RS lattice consists of a natural number $N$ (siteCount), scales $omega_{max}$ and $omega_{rms}$, and a control datum ensuring that the pointwise supremum of the vorticity satisfies $||omega||_infty leq sqrt(N) cdot omega_{rms}$.

background

This module sits inside the Navier-Stokes regularity program that uses the phi-ladder as an ultraviolet cutoff on the RS discrete lattice. The central object is the finite-volume vorticity profile, whose fields record the number of active sites in a finite window together with the maximum and root-mean-square vorticity scales. The finiteVolumeControl field supplies the norm-equivalence relation that replaces the usual Sobolev embedding on the continuum: pointwise amplitude is controlled by sqrt(siteCount) times the RMS scale. The imported PhiLadderCutoff module supplies the algebraic core that terminates the energy cascade once these lattice quantities are bounded.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

FRCBridge supplies the lattice-specific vorticity profile that feeds the main results on Navier-Stokes regularity from the phi-ladder cutoff. Its definitions enable the subsequent lemmas (normalizedRatio_pos, finiteVolume_Jcost_bound, frc_holds_on_RS_lattice) that close the discrete energy estimates. The structure directly supports the combinatorial argument that the phi-ladder terminates the cascade on the RS lattice, as outlined in the parent PhiLadderCutoff module.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (17)