IndisputableMonolith.NavierStokes.DiscreteMaximumPrinciple
This module defines OneStepData for a single discrete time step of incompressible Navier-Stokes on a finite 3D lattice and proves a collection of monotonicity and bound lemmas that together establish a discrete maximum principle. Lattice fluid modelers and Recognition Science researchers would cite it when discretizing NS evolution while preserving J-cost structure. The argument is built from direct algebraic properties of the imported discrete operators plus vortex-stretching estimates.
claimLet OneStepData record a velocity field $u$ on the finite three-direction lattice together with the associated pressure and time-step parameters. The module proves $J(u_{n+1})leq J(u_n)$, gradient nonincreasing, and unconditional bounds on the discrete Laplacian under the CoreNSOperator evolution.
background
The module sits inside the NavierStokes domain and imports the finite-lattice topology, discrete differential operators, and CoreNSOperator from DiscreteNSOperator. That upstream module supplies the concrete derivations of pair-budget and viscous-absorption fields directly from the velocity gradient and Laplacian. VortexStretching supplies the three analytic gap closures drawn from the cited papers on finite-volume rigidity and reciprocal-cost uniqueness.
proof idea
This is a definition-and-lemma module. It first declares the OneStepData record, then proves the listed monotonicity statements (advection_dominated_by_viscosity, gradient_nonincreasing, Jcost_nonincreasing, etc.) by algebraic reduction on the discrete advection and diffusion terms, invoking the vortex-stretching estimates for the absorption bounds.
why it matters in Recognition Science
The lemmas supply the discrete maximum principle that supports master_lattice_regularity and unconditional_Jcost_monotonicity inside the same module. These results close the lattice-regularity step needed for the Recognition Science treatment of Navier-Stokes, linking the J-cost monotonicity (T5) to the eight-tick octave and three-dimensional lattice structure.
scope and limits
- Does not address the continuous-space limit of the lattice discretization.
- Does not treat external forcing or non-periodic boundaries.
- Does not prove global existence of discrete solutions, only evolution properties.
- Does not quantify convergence rates to the continuous NS equations.
depends on (2)
declarations in this module (10)
-
structure
OneStepData -
theorem
advection_dominated_by_viscosity -
theorem
one_step_factor_le_one -
theorem
gradient_nonincreasing -
theorem
subK_preserved -
theorem
subK_propagation -
theorem
unconditional_gradient_bound -
theorem
unconditional_Jcost_monotonicity -
theorem
Jcost_nonincreasing -
theorem
master_lattice_regularity