OneStepData
plain-language theorem explainer
OneStepData bundles viscosity, lattice spacing, time step, gradient maximum, and advection bound for one discrete Navier-Stokes step on the RS lattice. Analysts of discrete maximum principles cite the record to state the sub-Kolmogorov hypothesis. It is realized as a structure definition that directly defines the viscous contraction rate as nu over h squared and the comparison predicate gradMax less than or equal to that rate.
Claim. A record containing positive reals $nu$ (viscosity), $h$ (lattice spacing), $dt$ (time step), $gradMax$ (maximum gradient), and advection bound $A$ with $0 le A le gradMax$, together with the derived viscous rate $nu/h^2$ and the predicate $gradMax le nu/h^2$.
background
The module develops a discrete maximum principle for the Navier-Stokes system on the Recognition Science lattice. It shows that the sub-Kolmogorov condition is self-improving under the discrete evolution, removing the need for an external hypothesis and yielding unconditional gradient bounds. OneStepData packages the inputs for a single time step: positive viscosity $nu$, spacing $h$, time increment $dt$, the current gradient maximum, and an upper bound on the discrete advection term. The viscous rate is defined as $nu/h^2$, matching the standard discrete Laplacian scaling. Upstream, the advection operator is the lattice sum over axes of velocity times forward difference, while the viscous rate reuses the definition from the vortex stretching module.
proof idea
The declaration is a structure definition. viscousRate is introduced by the direct quotient data.nu / data.h ^ 2. subKolmogorov is the inequality data.gradMax le data.viscousRate. The positivity theorem for the rate applies the division-positivity lemma to the two positivity hypotheses on nu and h.
why it matters
This record supplies the common hypotheses for the four downstream theorems proving advection domination by viscosity, the one-step contraction factor at most one, nonincreasing gradient maximum, and preservation of the sub-Kolmogorov condition. These steps close the self-improving loop for the discrete maximum principle, supporting the unconditional lattice regularity result. It aligns with the forcing-chain landmarks by ensuring bounded gradients on the three-dimensional lattice under the eight-tick octave dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.