subK_propagation
plain-language theorem explainer
Sub-Kolmogorov bounds on velocity gradients propagate forward under the discrete Navier-Stokes evolution on the RS lattice. Discrete regularity analysts cite the result to close the self-improving property and remove external hypotheses. The argument is a direct induction on the time index that applies order transitivity at each successor step.
Claim. Let $(g_n)_{n=0}^∞$ be a sequence of real numbers and let $B ∈ ℝ$. If $g_0 ≤ B$ and $g_{n+1} ≤ g_n$ for every natural number $n$, then $g_n ≤ B$ for all $n$.
background
The module proves that the sub-Kolmogorov condition is self-improving under discrete Navier-Stokes evolution on the RS lattice, making lattice regularity unconditional. The sub-Kolmogorov condition is the requirement that the velocity gradient stays below the viscous scale $ν/h²$ at every time step. The local setting is a finite lattice with finite-energy initial data, where the discrete maximum principle ensures viscous contraction dominates advection when the bound holds.
proof idea
The proof is a direct induction on the time index n. The base case at zero applies the initial bound hypothesis. The successor case invokes the step hypothesis to obtain the bound at k+1 from the bound at k, then combines it with the inductive hypothesis via order transitivity.
why it matters
This supplies the propagation step for unconditional_gradient_bound, which in turn feeds master_lattice_regularity. By eliminating the external sub-Kolmogorov hypothesis, it renders the discrete Navier-Stokes regularity result fully unconditional on the finite RS lattice. The module cites Proposition III.1 of Thapa & Washburn on strong convexity and spectral gap for the torus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.