indexedPairBudget
plain-language theorem explainer
indexedPairBudget sums the J-cost budgets of paired stretching events across a finite lattice of sites. Discrete Navier-Stokes modelers cite it when aggregating stretching contributions for comparison against viscous dissipation. The definition is a direct composition of the total summation operator with the per-event budget map.
Claim. For $n : ℕ$ and a map $e : Fin n → PairEvent$, the indexed pair budget is the sum $∑_{i} pairEventBudget(e(i))$, where each pairEventBudget extracts the J-cost change from the amplitude and stretchFactor of the event at site $i$.
background
The module isolates algebraic relations for paired stretching and compression events to support J-cost monotonicity in discrete Navier-Stokes. A PairEvent is a structure with positive amplitude and stretchFactor. pairEventBudget computes the pairwiseStretchingChange for one event. The total operator from DiscreteVorticity sums any scalar field over the finite index set Fin siteCount.
proof idea
One-line wrapper that applies the total summation from DiscreteVorticity to the function mapping each site to pairEventBudget of the corresponding PairEvent.
why it matters
This supplies the lattice-summed pair budget for coreOperatorPairBudget in DiscreteNSOperator, which feeds the absorption theorems core_pair_budget_absorbed and core_stretching_absorbed. It advances the RCL-based monotonicity program by providing an indexed sum of stretching budgets that viscosity can bound, connecting directly to the Recognition Composition Law balance for pairs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.