unconditional_gradient_bound
plain-language theorem explainer
On the RS lattice with finite initial velocity gradients, the discrete Navier-Stokes evolution keeps the gradient bounded by nu over h squared at every time step. Researchers in lattice-based fluid regularity and discrete PDE analysis would cite this to drop the sub-Kolmogorov condition as an external assumption. The proof is a one-line wrapper that applies the sub-Kolmogorov propagation lemma to the initial bound and the nonincreasing property.
Claim. Let $g: ℕ → ℝ$ be a sequence of velocity gradients on the lattice, with viscosity $ν > 0$ and spacing $h > 0$. Assume the initial datum satisfies $g(0) ≤ ν/h²$ and the sequence is nonincreasing: $g(n+1) ≤ g(n)$ for all $n$. Then $g(n) ≤ ν/h²$ for every $n$.
background
This declaration belongs to the module on the Discrete Maximum Principle and Self-Improving Sub-Kolmogorov Condition for the discrete Navier-Stokes operator on the RS lattice. The sub-Kolmogorov condition is the gradient bound $g_n ≤ ν/h²$, which guarantees stability of the discrete evolution; the module shows this bound is self-improving once it holds at the initial step. The initial bound follows from finite energy on any finite lattice, so no external hypothesis remains.
proof idea
The proof is a one-line wrapper that applies the subK_propagation lemma to the supplied initial bound and the nonincreasing assumption, which together force the bound to hold at every later step.
why it matters
This result removes the sub-Kolmogorov condition as an external hypothesis, making the lattice regularity theorem fully unconditional. It feeds directly into the master_lattice_regularity theorem and the unconditional J-cost monotonicity statements in the same module. In the Recognition Science framework it supports the discrete evolution on the phi-ladder lattice and aligns with the self-improving properties under the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.