indexedPairBudget_nonneg
plain-language theorem explainer
The indexed pair budget over a finite lattice is nonnegative for any assignment of paired stretching events. Discrete Navier-Stokes researchers cite it to guarantee that total J-cost from stretching pairs stays nonnegative before viscosity absorption. The proof is a one-line term wrapper that unfolds the budget to a finite sum and applies the per-event nonnegativity lemma.
Claim. Let $N$ be a natural number and let $e : Fin N → PairEvent$ assign to each lattice site a paired stretching event with positive amplitude and stretch factor. Then $0 ≤ ∑_{i:Fin N} B(e_i)$, where $B$ is the J-cost budget contributed by one such event.
background
The StretchingPairs module isolates the algebraic core of J-cost monotonicity for discrete Navier-Stokes. A PairEvent is a structure carrying a positive real amplitude and a positive real stretch factor; its pairEventBudget extracts the net contribution under the Recognition Composition Law. The indexedPairBudget is defined as the total operator applied to the map sending each site to its individual pairEventBudget, where total is the standard finite sum over the lattice window.
proof idea
The proof is a one-line term-mode wrapper. It unfolds indexedPairBudget to the total sum and invokes Finset.sum_nonneg whose summand is supplied directly by pairEventBudget_nonneg applied to each event.
why it matters
This result is invoked by coreOperatorPairBudget_nonneg and operatorPairBudget_nonneg in DiscreteNSOperator, where it ensures the pair-budget term is absorbed by viscosity. It supplies a concrete nonnegativity instance for the J-cost program inside the Recognition framework, confirming that discrete stretching events produce no negative defect budgets on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.