LatticeRegularityCertificate
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove any PDE estimates or existence of solutions.
- Does not claim the conditional route applies outside finite RS lattices.
- Does not derive the bound from first principles; it inherits it from finite-volume control.
- Does not address infinite-volume or continuum limits.
formal statement (Lean)
130structure LatticeRegularityCertificate
131 (route : ConditionalCompletionRoute FiniteVolumeProfile)
132 (profile : FiniteVolumeProfile) where
133 frcBound : ℝ
134 frcBound_nonneg : 0 ≤ frcBound
135 frcProof : RSLatticeFRC profile
136 injectionDamping : route.InjectionDamping profile
137 directionConstancy : route.DirectionConstancy profile
138 rigidRotationVeto : route.RigidRotationVeto profile
139 regularity : route.Regularity profile
140
141/-- The lattice FRC theorem is enough to instantiate the conditional route. -/