stretching_term_nonneg
plain-language theorem explainer
Nonnegativity of the total stretching contribution follows from pointwise nonnegativity on the finite lattice. Workers on discrete J-cost estimates in Recognition Science cite it to control signs in the derivative decomposition. The argument is a direct appeal to the sum of nonnegative terms being nonnegative after unfolding the total definition.
Claim. Let $c$ be a contribution field on a lattice window with $N$ sites. If the stretching component of $c$ satisfies $s(i)geq 0$ for every site index $i$, then the sum of the stretching component over all sites is nonnegative.
background
The Discrete Vorticity module packages finite vorticity fields on a lattice window together with totals, RMS amplitudes, and the exact decomposition of the J-cost derivative into transport, viscous, and stretching pieces. ContributionFields is the structure that holds these three maps from the finite index set to the reals. The total function simply sums any scalar field over the sites. The module keeps the bookkeeping surface separate from the hard PDE inequalities so that sign and monotonicity lemmas can be added one at a time.
proof idea
The proof unfolds the definitions of totalStretching and total, reducing the claim to nonnegativity of a finite sum. It then applies the standard lemma that the sum of a pointwise nonnegative function over a finite set is nonnegative, instantiated directly on the given hypothesis for the stretching component.
why it matters
This result supplies a basic sign property required for the J-cost monotonicity program in the discrete vorticity setting. It guarantees that nonnegative stretching contributions cannot decrease the total J-cost inside the derivative identity. The bookkeeping module supports eventual connection to the Recognition Composition Law and the forcing chain steps that lead toward continuous limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.