one_step_factor_le_one
plain-language theorem explainer
The theorem shows that the multiplicative factor for the gradient maximum after one discrete Navier-Stokes step is at most one whenever the sub-Kolmogorov condition holds. Lattice fluid dynamicists cite it when closing the discrete maximum principle on the Recognition Science lattice. The term proof obtains a non-positive difference from the advection-dominance lemma and finishes with linear arithmetic on the positive time step.
Claim. Let data record one-step Navier-Stokes parameters on the lattice with positive time increment dt, advection bound A, and viscous rate nu. Under the sub-Kolmogorov condition, 1 + dt · (A - nu) ≤ 1.
background
The module proves that the sub-Kolmogorov condition improves itself under discrete Navier-Stokes evolution on the RS lattice, removing it as an external hypothesis. OneStepData packages viscosity nu > 0, lattice spacing h > 0, time step dt > 0, current gradient maximum, and advection bound; the sub-Kolmogorov hypothesis encodes that advection is dominated by viscosity via the advection_dominated_by_viscosity lemma. The local setting follows the module's description of a self-improving discrete maximum principle that yields unconditional lattice regularity.
proof idea
Term-mode proof. Invoke advection_dominated_by_viscosity under the sub-Kolmogorov hypothesis to obtain advectionBound - viscousRate ≤ 0 via sub_nonpos.mpr. Apply linarith together with dt_pos.le to conclude the factor is at most one.
why it matters
The result supplies the contraction factor used by gradient_nonincreasing to show the gradient maximum is non-increasing. It closes the self-improving sub-Kolmogorov property, making the discrete maximum principle unconditional on the RS lattice. The module references 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.