operatorPairBudget_nonneg
plain-language theorem explainer
For any incompressible Navier-Stokes operator on a finite lattice with N sites, the associated pair budget is non-negative. Discrete fluid modelers in the Recognition Science setting cite this to guarantee budget positivity when constructing operators from core velocity data. The proof is a one-line wrapper that unfolds the budget definition and invokes the indexed non-negativity theorem on the extracted pair event.
Claim. Let $N$ be a natural number and let $ns$ be an incompressible Navier-Stokes operator on a lattice with $N$ sites (including a divergence-free velocity field, positive grid spacing $h$, and positive viscosity). Then the pair budget $B(ns)$ satisfies $0 ≤ B(ns)$.
background
The IncompressibleNSOperator structure extends EvolutionIdentity and carries a three-direction LatticeTopology, grid spacing $h > 0$, viscosity $ν > 0$, a state, a divergence-free velocity field, and a transport flux; the six earlier free fields for pair amplitude and stretch are now derived from the core flow. The operatorPairBudget function is defined to equal the indexed pair budget of the pair event attached to the operator, where pairEventAt extracts amplitude and stretch factor (with their positivity) at each site. This construction appears in the module that supplies concrete discrete incompressible Navier-Stokes operators whose pair-budget fields are built rather than postulated.
proof idea
The proof unfolds the definition of operatorPairBudget, reducing it to indexedPairBudget applied to pairEventAt ns, then applies the upstream theorem indexedPairBudget_nonneg directly to that event function.
why it matters
The result closes the non-negativity requirement for the pair budget inside the constructed IncompressibleNSOperator, ensuring the DerivedEstimates layer remains physically consistent when pair data are generated from the velocity gradient and Laplacian. It supports the broader discrete Navier-Stokes surface in the Recognition Science framework by inheriting positivity from the indexed pair budget theorem. No downstream uses are recorded yet, but the lemma is a prerequisite for any later energy or absorption estimates that rely on the operator surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.