totalPairBudget_nonneg
plain-language theorem explainer
Non-negativity of the summed RCL budgets over any finite collection of paired stretching events follows by induction on list length. Discrete Navier-Stokes modelers cite this when verifying that total J-cost remains non-decreasing under sequences of stretching operations. The argument reduces the claim to the single-event case via additivity of summation and the already-proved non-negativity for individual PairEvent structures.
Claim. For every finite list of paired stretching events, the sum of their individual RCL budgets satisfies $0 ≤ ∑_{ev ∈ events} pairEventBudget(ev)$.
background
PairEvent is a structure consisting of a positive real amplitude and a positive real stretchFactor. The totalPairBudget function maps a list of such events to the sum of their individual pairEventBudget values. This module isolates the algebraic core of the J-cost monotonicity program for discrete stretching and compression events in a PDE-free setting suitable for reuse in discrete Navier-Stokes operators.
proof idea
The proof proceeds by induction on the list of events. The nil case follows immediately from the definition of totalPairBudget as the sum over an empty list, which is zero. The cons case applies simplification to reduce to the sum of the head budget and the tail sum, then invokes add_nonneg together with the single-event non-negativity theorem and the induction hypothesis.
why it matters
This result supplies the non-negativity foundation for the total RCL pair budget in the stretching-pairs module, which supports the broader J-cost monotonicity program in Recognition Science. It directly implements the Recognition Composition Law balance for finite families of events without invoking continuous PDE machinery. No downstream theorems are listed, indicating it serves as a terminal algebraic fact within the discrete stretching layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.