subK_preserved
plain-language theorem explainer
Analysts of discrete fluid equations cite this result to show that the sub-Kolmogorov bound on the gradient maximum survives a single time step of the lattice Navier-Stokes evolution under the stated update inequality. The theorem removes one external hypothesis from the regularity induction on the RS lattice. Its term proof applies the gradient-nonincreasing property and order transitivity after parameter rewriting.
Claim. Let $data$ be a one-step datum with positive viscosity $nu$, lattice spacing $h$, time step $dt$, nonnegative gradient maximum $G$, and advection bound $A$. Suppose the sub-Kolmogorov condition holds for $data$. Let $G'$ satisfy $G' ≤ G · (1 + dt · (A - nu/h²)). Let $data'$ be a one-step datum with the same viscous rate $nu/h²$ and gradient maximum $G'$. Then $data'$ satisfies the sub-Kolmogorov condition.
background
OneStepData packages the parameters for a single discrete Navier-Stokes time step on a finite lattice: positive viscosity $nu$, spacing $h$, time step $dt$, current gradient maximum, and advection bound. The sub-Kolmogorov condition is the predicate on this datum that the module shows is self-improving. The module documentation states: 'This module proves that the sub-Kolmogorov condition is self-improving under the discrete Navier--Stokes evolution on the RS lattice, eliminating it as an external hypothesis and making the lattice regularity result fully unconditional.'
proof idea
The proof is a one-line term-mode wrapper. It unfolds the subKolmogorov predicate on the new datum, rewrites the gradient maximum and viscous rate via the supplied equalities, then applies the gradient_nonincreasing lemma to obtain the bound on the updated maximum and composes it with the original hypothesis via le_trans.
why it matters
This supplies the one-step preservation needed for the inductive propagation of the sub-Kolmogorov condition over arbitrary time steps, removing it as an external hypothesis in the lattice regularity theorem. It advances the discrete maximum principle for Navier-Stokes on the RS lattice and aligns with the self-improving regularity developed in the module. The surrounding documentation references the spectral gap from Proposition III.1 in Thapa & Washburn (GCIC, J. Math. Phys. 2026).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.