pairEventBudget_nonneg
plain-language theorem explainer
The non-negativity of the J-cost budget for a single paired stretching event follows by direct appeal to the pairwise stretching non-negativity lemma. Researchers modeling discrete fluid stretching or establishing J-cost monotonicity under the Recognition Composition Law cite this as the base case before summing over lists or indexed families. The proof is a one-line term application of pairwiseStretching_nonneg to the positivity witnesses carried by the event structure.
Claim. Let ev be a paired stretching event whose amplitude and stretch factor are both positive reals. Then the J-cost budget contributed by ev satisfies $0 ≤ B(ev)$, where $B$ denotes the budget function derived from the Recognition Composition Law.
background
The module isolates the algebraic core of the J-cost monotonicity program for discrete stretching: paired events, the exact Recognition Composition Law balance they obey, and finite budgets indexed by lists or lattice sites. PairEvent is the structure that records one such event by an amplitude and a stretchFactor, both required to be strictly positive. The local setting is deliberately PDE-free so that the same definitions can be reused by discrete Navier-Stokes operators without creating abstraction cycles. Upstream structures on J-cost convexity and local eight-tick dynamics supply the surrounding justification that individual budgets must remain non-negative.
proof idea
The proof is a term-mode one-liner that applies the sibling lemma pairwiseStretching_nonneg directly to the amplitude_pos and stretchFactor_pos fields of the input PairEvent.
why it matters
This supplies the base non-negativity step required by the totalPairBudget_nonneg and indexedPairBudget_nonneg theorems that immediately follow in the same module. It advances the J-cost monotonicity program by confirming that each discrete stretching pair contributes a non-negative amount, consistent with the Recognition Composition Law balance and the broader phi-ladder construction. No open scaffolding questions are closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.