FiniteVolumeProfile
plain-language theorem explainer
FiniteVolumeProfile packages a positive integer site count N with vorticity scales omega_max and omega_rms under the control inequality omega_max <= sqrt(N) * omega_rms. Authors bridging lattice phi-ladder cutoffs to Navier-Stokes regularity cite the structure to obtain a finite recognition-cost bound on an RS lattice. The declaration is a bare structure definition that directly encodes the finite-volume norm equivalence.
Claim. A finite-volume vorticity profile on an RS lattice consists of a positive integer $N$ (active site count), positive reals $omega_max$ and $omega_rms$ satisfying $omega_rms le omega_max le sqrt(N) cdot omega_rms$.
background
The Lattice FRC Bridge module formalizes the logical link between the lattice phi-ladder cutoff and the conditional-completion route for Navier-Stokes regularity. FiniteVolumeProfile supplies the input type: siteCount counts active lattice sites while omegaMax and omegaRms record the relevant vorticity scales. The finiteVolumeControl field encodes the finite-lattice norm equivalence that pointwise amplitude is bounded by sqrt(siteCount) times the RMS value.
proof idea
FiniteVolumeProfile is introduced as a structure definition whose fields directly assert the positivity, ordering, and finite-volume control conditions. No lemmas or tactics are invoked; the declaration simply packages the required data and inequality.
why it matters
The structure supplies the domain for finiteVolume_Jcost_bound, which proves Jcost(normalizedRatio s) le sqrt(siteCount), and for FRCBridgeCert together with frc_holds_on_RS_lattice and frc_holds_on_RS_lattice_exists. It thereby closes the lattice-to-conditional bridge: lattice FRC implies a finite bound that can be fed into the abstract route FRC to injection_damping to direction_constancy to regularity. The module keeps all PDE steps external.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.