module module high

`IndisputableMonolith.NavierStokes.DiscreteNSOperator`

The DiscreteNSOperator module defines the concrete discrete operators for the incompressible Navier-Stokes equations on the RS lattice, including forward and backward differences, Laplacians, divergence, advection, and conservative transport fields. Researchers in discrete fluid regularity and J-cost monotonicity cite it as the algebraic surface for exact transport cancellation and stretching bounds. It supplies only definitions with no proofs, enabling downstream bookkeeping in the NavierStokes domain.

claimThe discrete NS operator is assembled from forwardDiff, backwardDiff, scalarLaplacian, vectorLaplacian, divergence, advection, and conservativeTransportField on ScalarField and VectorField over LatticeTopology, with the property that total_conservativeTransportField_zero holds identically.

background

This module sits in the NavierStokes domain and imports DiscreteVorticity for finite vorticity fields, total/RMS amplitudes, and transport/viscous/stretching contributions, plus StretchingPairs for RCL pair events and finite pair budgets. It introduces Axis, ScalarField, VectorField, LatticeTopology together with the difference operators forwardDiff and backwardDiff, the Laplacians, divergence, advection, and the conservative transport field whose total vanishes. These objects furnish the exact algebraic surface for the discrete incompressible NS evolution.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the concrete discrete NS operator surface that feeds JcostMonotonicity (transport cancellation and RCL-bounded stretching), DiscreteMaximumPrinciple (self-improving sub-Kolmogorov condition), and VortexStretching (viscous-dissipation estimates). It closes the definition layer for the lattice regularity program referenced in the published papers P1-P3.

scope and limits

Does not contain any theorems or proofs.
Does not address continuous limits or convergence to the PDE.
Does not include numerical implementation or boundary conditions beyond LatticeTopology.
Does not cover compressible or non-incompressible variants.

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.NavierStokes.DiscreteMaximumPrinciple module_import
IndisputableMonolith.NavierStokes.JcostMonotonicity module_import
IndisputableMonolith.NavierStokes.VortexStretching module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.NavierStokes.DiscreteVorticity module_import
IndisputableMonolith.NavierStokes.StretchingPairs module_import

declarations in this module (33)

abbrev Axis L34
abbrev ScalarField L36
abbrev VectorField L38
structure LatticeTopology L40
def forwardDiff L44
def backwardDiff L48
def scalarLaplacian L52
def vectorLaplacian L56
def divergence L60
def advection L64
def conservativeTransportField L68
theorem total_conservativeTransportField_zero L73
def velocityGradientMag L86
structure CoreNSOperator L96
theorem core_transport_zero L132
def corePairAmplitude L142
theorem corePairAmplitude_pos L146
def corePairStretchFactor L151
theorem corePairStretchFactor_pos L155
def corePairEvent L161
theorem core_stretching_le_pair_budget L170
def coreOperatorPairBudget L178
theorem coreOperatorPairBudget_nonneg L181
theorem core_pair_budget_absorbed L187
theorem core_stretching_absorbed L195
theorem core_dJdt_nonpos L205
structure IncompressibleNSOperator L215
def pairEventAt L270
def operatorPairBudget L277
theorem operator_transport_zero L280
theorem operatorPairBudget_nonneg L287
theorem totalStretching_le_operatorPairBudget L293
theorem operatorPairBudget_absorbed_by_viscosity L301