gradient_nonincreasing
plain-language theorem explainer
Gradient maxima remain non-increasing across one discrete Navier-Stokes step on the lattice whenever the sub-Kolmogorov condition holds. Researchers proving unconditional regularity for lattice NS would invoke this bound. The argument reduces to applying the factor lemma and chaining inequalities via le_trans.
Claim. For one-step data $data$ on the discrete Navier-Stokes lattice with sub-Kolmogorov condition holding, if $newGradMax ≤ data.gradMax ⋅ (1 + data.dt ⋅ (data.advectionBound - data.viscousRate))$, then $newGradMax ≤ data.gradMax$.
background
OneStepData collects the inputs for a single time step in the discrete Navier-Stokes model: positive viscosity nu, mesh size h, time increment dt, current max gradient, and an advection bound. The sub-Kolmogorov condition is the key hypothesis ensuring the discrete operator respects a maximum principle. The module develops the discrete maximum principle to show self-improvement of the sub-Kolmogorov condition under RS lattice evolution, removing it as an external assumption for regularity results. Upstream, it relies on the cellular automata step definition and arithmetic transitivity lemmas to handle the discrete updates.
proof idea
Term proof. First obtain the factor bound via one_step_factor_le_one data hsubK. Then apply le_trans to the hypothesis h_update and the inequality from mul_le_of_le_one_right using gradMax_nonneg and the factor ≤ 1.
why it matters
Directly used by subK_preserved to establish preservation of the sub-Kolmogorov condition. This advances the module's aim of unconditional lattice regularity for discrete NS, referencing the spectral gap in Thapa & Washburn GCIC 2026. It supports the broader Recognition Science program by securing gradient control on the lattice without external hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.