module module high

`IndisputableMonolith.NavierStokes.DiscreteNSOperator`

DiscreteNSOperator defines the concrete discrete incompressible Navier-Stokes operator on the RS lattice, packaging finite-difference primitives and the full evolution surface. Researchers on the J-cost monotonicity program cite it to obtain an explicit operator against which transport cancellation and RCL pair budgets are measured. The module is purely definitional and assembles its objects from the imported DiscreteVorticity and StretchingPairs bookkeeping.

claimThe module supplies the discrete NS operator together with its auxiliary fields, including the maximum absolute forward difference $M = max |Δ^+ u|$ taken over all velocity components and lattice directions.

background

The module operates inside the Recognition Science lattice setting for discrete Navier-Stokes. It imports DiscreteVorticity, whose doc states it packages finite vorticity fields on a lattice window together with total, RMS and normalized amplitudes plus transport/viscous/stretching contribution fields. It also imports StretchingPairs, whose doc isolates paired stretching/compression events and the exact Recognition Composition Law balance for such pairs. Local definitions include Axis, ScalarField, VectorField, LatticeTopology, forwardDiff, backwardDiff, scalarLaplacian, vectorLaplacian, divergence, advection and conservativeTransportField.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the concrete operator surface required by JcostMonotonicity (which derives transport cancellation from conservative incompressible flux and bounds the stretching term by the operator's own RCL pair budget) and by DiscreteMaximumPrinciple (which proves the sub-Kolmogorov condition is self-improving). It also feeds VortexStretching, which closes the three analytic gaps using the cited papers P1-P3.

scope and limits

Does not contain any theorems or proofs.
Does not derive monotonicity or regularity statements.
Does not treat the continuous Navier-Stokes equations or their limits.
Does not incorporate boundary conditions or external forcing terms.

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