totalStretching_le_operatorPairBudget
plain-language theorem explainer
The inequality bounds the summed stretching contributions of a discrete incompressible Navier-Stokes operator by its derived pair-event budget on a finite lattice. Researchers working on discrete fluid models or Recognition Science embeddings of Navier-Stokes would cite this bound when verifying energy dissipation. The proof is a direct unfolding of the total and budget sums followed by a pointwise comparison at each lattice site.
Claim. For an incompressible Navier-Stokes operator $ns$ on a finite lattice with $N$ sites, the total stretching sum over the contribution fields satisfies $totalStretching(ns.contributions) ≤ operatorPairBudget(ns)$, where the right-hand side is the sum of pair-event budgets derived from the operator's per-site amplitudes and stretch factors.
background
The module defines a concrete discrete incompressible Navier-Stokes operator surface on a finite three-direction lattice. IncompressibleNSOperator extends EvolutionIdentity and carries lattice topology, spacing $h$, viscosity $ν$, divergence-free velocity, and transport flux; pair budgets are now constructed from the core flow data via DerivedEstimates rather than assumed as free data. totalStretching sums the stretching scalar field over all sites, while operatorPairBudget applies indexedPairBudget to the lattice of pair events, each recording amplitude and stretchFactor at a site.
proof idea
The term proof unfolds totalStretching, total, operatorPairBudget, and indexedPairBudget to expose the underlying finite sums. It then invokes Finset.sum_le_sum to reduce the global comparison to a sitewise inequality, which is discharged by the per-site stretching_le_pair_budget lemma after simplification with pairEventAt and pairEventBudget.
why it matters
This bound is the direct antecedent of stretching_absorbed_by_viscosity in the JcostMonotonicity module, which concludes that lattice stretching is absorbed by the viscous budget via le_trans. It supplies the missing link that lets the discrete NS operator close its energy estimate using the RCL-derived pair budgets. In the Recognition framework it supports absorption of stretching into viscosity for the eight-tick lattice model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.