master_lattice_regularity
plain-language theorem explainer
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.
Claim. Let $(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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.