totalPairBudget
plain-language theorem explainer
The total RCL pair budget aggregates the J-cost contributions from each paired stretching event in a finite list. Researchers modeling discrete Navier-Stokes or proving J-cost monotonicity cite this aggregation when summing budgets over families of events. The definition applies list mapping to pairEventBudget followed by summation over the reals.
Claim. For a finite list of paired stretching events $(e_i)$, the total RCL pair budget equals $B = sum_i b(e_i)$, where $b(e)$ denotes the J-cost budget of event $e$.
background
This definition lives in the module on RCL Pair Events for Discrete Stretching, which isolates the algebraic core of the J-cost monotonicity program via paired stretching/compression events and the exact Recognition Composition Law balance. A PairEvent is a structure carrying positive real amplitude and stretchFactor. The pairEventBudget of an event is the value of pairwiseStretchingChange on those fields, which supplies the per-event J-cost contribution. The upstream map from RSNative.Core applies a function to a measurement value while preserving window, protocol, uncertainty and notes; the present definition uses the standard list form of map.
proof idea
One-line definition that maps pairEventBudget over the input list and sums the resulting real numbers.
why it matters
It supplies the aggregation step required by the downstream non-negativity theorem totalPairBudget_nonneg, proved by induction on the list. The construction belongs to the algebraic foundation for finite pair budgets inside the Recognition Science treatment of Navier-Stokes, relying on the Recognition Composition Law and J-cost without any PDE content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.