CoreNSOperator
plain-language theorem explainer
CoreNSOperator assembles the minimal physical data for an incompressible discrete Navier-Stokes flow on a finite lattice: a topology, positive mesh and viscosity parameters, a divergence-free velocity, conservative transport flux, and explicit bounds on stretching costs via J-cost differences together with viscous absorption of pair budgets. Researchers deriving monotonicity of J-cost or pair budgets in discrete fluid models cite this structure as the base carrier before any derived estimates. The declaration is a direct structure extension of
Claim. A structure on $N$ sites consisting of a lattice topology, positive scalars $h,ν,dt$, a Galerkin state with vorticity field $ω$, a divergence-free velocity field $u$, a scalar transport flux and site permutation such that the transport contribution equals the conservative difference field, the viscous contribution equals $ν$ times the scalar Laplacian of $ω$, a positive RMS scale $ω_{rms}$ with normalized $|ω_i|/ω_{rms}>0$, non-negative velocity gradient magnitudes, and two inequalities: the local stretching contribution at each site is bounded above by the sum of two J-cost terms minus twice the base J-cost, while the total pairwise stretching change is bounded above by the negative of the total viscous contribution.
background
LatticeTopology supplies the plus and minus neighbor maps for each of three axes on the finite site set. VectorField and ScalarField are the obvious function types from sites to axis-indexed reals and to reals. State is the discrete 2D Galerkin state carrying the vorticity field $ω$. The module constructs a finite three-direction lattice topology together with discrete differential operators and then defines CoreNSOperator to carry only the physical flow data; pair-budget and absorption fields are derived in a subsequent layer rather than supplied as free data.
proof idea
The declaration is a structure definition that directly lists the required fields, extends EvolutionIdentity, and records the transport and viscous assignments plus the two bounding inequalities as field data.
why it matters
CoreNSOperator supplies the physical input from which corePairAmplitude, coreOperatorPairBudget, core_pair_budget_absorbed and core_dJdt_nonpos are obtained by direct substitution. It therefore closes the gap between raw lattice flow data and the J-cost monotonicity statements required by the Recognition Science treatment of discrete fluids. The construction realizes the module goal of replacing previously free pair-budget hypotheses with quantities built from velocity gradients and Laplacians.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.