LatticeRegularityCertificate
plain-language theorem explainer
LatticeRegularityCertificate packages a regularity certificate obtained by feeding a finite-volume vorticity profile on an RS lattice into an abstract conditional-completion route. Researchers bridging lattice cutoffs to Navier-Stokes regularity claims would cite it to supply the explicit finite recognition-cost bound. The declaration is a structure definition that directly bundles the non-negative bound, the lattice FRC instance, and the route's four successive properties.
Claim. Let $P$ be a finite-volume vorticity profile on an RS lattice (with site count $N$, maximum vorticity scale, and RMS scale satisfying the finite-volume control $M_0(P) = M_1(P) / N^{1/2}$). Let $R$ be a conditional-completion route. A lattice regularity certificate consists of a real number $B$ with $B$ nonnegative, a proof that the recognition cost of the normalized vorticity ratio of $P$ is at most $N^{1/2}$, and proofs that $R$ maps the FRC property of $P$ successively through injection damping, direction constancy, and rigid-rotation veto to regularity.
background
The module closes the logical loop between the lattice φ-ladder cutoff and the conditional-completion route of the Navier-Stokes regularity paper. On a finite RS lattice the normalized vorticity ratio is automatically finite-volume controlled, supplying a finite recognition-cost bound that feeds the abstract route FRC → injection damping → direction constancy → rigid rotation veto → regularity. The PDE-heavy steps remain external; only the logical bridge is formalized here.
proof idea
The declaration is a structure definition. It assembles the required fields by direct reference to the sibling definitions: the non-negative bound and RSLatticeFRC instance come from the finite-volume control on the profile, while the four route properties are supplied by the implication chain inside ConditionalCompletionRoute.
why it matters
This structure instantiates the conditional route on a lattice profile, exactly as described in the module documentation: the lattice FRC theorem is enough to instantiate the conditional route. It supplies the finite recognition-cost bound required by any downstream regularity argument that begins from the RS lattice cutoff. In the Recognition Science framework it realizes the finite-volume control step that connects the φ-ladder to fluid regularity statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.