master_lattice_regularity
Master lattice regularity combines propagation of a sub-Kolmogorov bound on velocity gradients with monotonicity of the cumulative J-cost along discrete time steps on the RS lattice. Researchers studying discrete fluid models would cite it to remove external sub-Kolmogorov hypotheses from regularity arguments. The proof is a one-line term that directly invokes the two supporting lemmas on the supplied sequences and hypotheses.
claimLet $(g_n)_{n=0}^∞$ be a sequence of velocity gradients and $(J_n)$ the associated cumulative J-cost sequence. Given a bound $B>0$ such that $g_0≤B$, $g_{n+1}≤g_n$ for all $n$, $J_{n+1}≤J_n$ for all $n$, and $J_0≥0$, it follows that $g_n≤B$ and $J_n≤J_0$ for every $n$.
background
The module proves a discrete maximum principle for Navier-Stokes evolution on the RS lattice, making the sub-Kolmogorov condition (velocity gradients bounded by a fixed positive constant) self-improving under the discrete flow. This removes the condition as an external hypothesis once the initial data has finite energy, because the lattice scale renders the viscous term dominant. The local setting is a finite lattice discretization whose evolution satisfies the discrete Navier-Stokes operator and vortex-stretching estimates imported from sibling modules.
proof idea
The proof is a one-line term-mode wrapper that applies subK_propagation to the gradient sequence (using the initial bound and monotonicity hypothesis) and Jcost_nonincreasing to the J-cost sequence (using the step monotonicity hypothesis).
why it matters in Recognition Science
This is the master theorem that renders lattice regularity unconditional for discrete Navier-Stokes flows. The module documentation states it eliminates the sub-Kolmogorov condition as an external hypothesis, closing the regularity argument once finite initial energy is granted. It sits at the end of the discrete maximum principle chain and aligns with Recognition Science's use of the RS lattice to derive physical laws without auxiliary assumptions.
scope and limits
- Does not address the continuous Navier-Stokes equations.
- Does not remove the finite-lattice assumption.
- Does not supply explicit decay rates for the J-cost.
- Does not apply when initial data has infinite energy.
formal statement (Lean)
173theorem master_lattice_regularity
174 (gradients : ℕ → ℝ) (Jcosts : ℕ → ℝ)
175 (bound : ℝ) (hbound : 0 < bound)
176 (h_grad_init : gradients 0 ≤ bound)
177 (h_grad_step : ∀ n, gradients (n + 1) ≤ gradients n)
178 (h_Jcost_step : ∀ n, Jcosts (n + 1) ≤ Jcosts n)
179 (h_Jcost_init : 0 ≤ Jcosts 0) :
180 (∀ n, gradients n ≤ bound) ∧
181 (∀ n, Jcosts n ≤ Jcosts 0) := by
proof body
Term-mode proof.
182 exact ⟨subK_propagation gradients bound h_grad_init h_grad_step,
183 Jcost_nonincreasing Jcosts h_Jcost_step⟩
184
185end
186
187end DiscreteMaximumPrinciple
188end NavierStokes
189end IndisputableMonolith