operatorPairBudget
plain-language theorem explainer
The definition computes the total pair budget for an incompressible Navier-Stokes operator on a finite lattice by summing pair-event budgets extracted site by site. Discrete fluid-dynamics researchers in the Recognition Science setting cite it when proving non-negativity or viscous absorption of the budget. The implementation is a direct one-line wrapper applying the indexed summation to the site-wise events.
Claim. Let $ns$ be an incompressible Navier-Stokes operator on a lattice with $N$ sites. The operator pair budget equals the sum over all sites $i$ of the pair-event budget $B(e_i)$, where each $e_i$ is the pair event constructed from the amplitude and stretch factor at site $i$.
background
The module constructs a concrete discrete incompressible Navier-Stokes operator surface on a finite three-direction lattice. IncompressibleNSOperator extends EvolutionIdentity with lattice topology, positive step size $h$, positive viscosity $ν$, a divergence-free velocity field, and transport flux; the six previously free pair-budget fields are now derived from the core flow data. pairEventAt extracts a PairEvent record at each site from the operator's pairAmplitude and pairStretchFactor. indexedPairBudget sums the individual pairEventBudget values over the finite set of sites.
proof idea
One-line wrapper that applies indexedPairBudget to the function pairEventAt ns.
why it matters
The definition supplies the concrete pair budget consumed by the three immediate downstream theorems: operatorPairBudget_nonneg, totalStretching_le_operatorPairBudget, and operatorPairBudget_absorbed_by_viscosity. It belongs to the DerivedEstimates layer that replaces assumed pair-budget data with quantities constructed from the core velocity gradient and Laplacian, thereby completing the passage from CoreNSOperator to the full IncompressibleNSOperator surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.