RSLatticeFRC
plain-language theorem explainer
RSLatticeFRC packages the strong finite recognition cost bound for any finite-volume vorticity profile on an RS lattice by requiring the J-cost of the normalized vorticity ratio to lie at most at the square root of the site count. Workers on conditional-completion routes for Navier-Stokes regularity cite it to supply the lattice-side FRC hypothesis that feeds the injection-damping and direction-constancy steps. The definition is a direct packaging of the inequality that follows from the finite-volume control axiom already present in the profile
Claim. Let $s$ be a finite-volume vorticity profile with site count $N$, maximum vorticity amplitude $ω_{max}$, and root-mean-square amplitude $ω_{rms}$. Then $J(ω_{max}/ω_{rms}) ≤ √N$, where $J$ denotes the J-cost function.
background
FiniteVolumeProfile is the structure that records a vorticity profile on a finite RS lattice window. Its fields include a positive natural siteCount, positive reals omegaMax and omegaRms (with omegaRms ≤ omegaMax), and the finiteVolumeControl axiom omegaMax ≤ √(siteCount) · omegaRms. This axiom encodes the norm-equivalence that holds on any finite lattice: pointwise amplitudes are controlled by the RMS scale multiplied by the square root of the number of sites. normalizedRatio simply extracts the ratio omegaMax / omegaRms from such a profile.
proof idea
The declaration is a direct definition that assembles the inequality Jcost (normalizedRatio s) ≤ √(s.siteCount) into a named Prop. No lemmas are applied; the body is the inequality itself, which is well-typed once the profile structure supplies the necessary fields.
why it matters
RSLatticeFRC supplies the strong lattice FRC predicate that FRCBridgeCert quantifies over all profiles and that lattice_regular_via_direction_constancy uses to instantiate the conditional completion route. It thereby closes the logical bridge from the lattice φ-ladder cutoff to the abstract FRC → regularity chain in the Navier-Stokes paper. The definition touches the open question of extending the bound beyond finite windows but completes the finite-volume case required by the conditional route.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.