coreOperatorPairBudget_nonneg
plain-language theorem explainer
The declaration proves non-negativity of the total derived pair budget for any core discrete incompressible Navier-Stokes operator on a finite lattice. Researchers constructing lattice discretizations of incompressible flows cite it to confirm that the pair-budget term stays non-negative once extracted from physical core data. The proof is a direct term application of the indexed pair budget non-negativity result to the core pair event.
Claim. Let $n$ be a natural number and let $op$ be a structure holding the physical data of a discrete incompressible lattice flow on $n$ sites, including lattice topology, positive spacing $h$, positive viscosity $ν$, a divergence-free velocity field, and transport flux. Then the total derived pair budget extracted from $op$ satisfies $0 ≤$ total derived pair budget of $op$.
background
The module defines a concrete discrete incompressible Navier-Stokes operator surface on a finite three-direction lattice. CoreNSOperator supplies only the physical inputs: topology, spacing $h>0$, viscosity $ν>0$, state, velocity field with vanishing divergence at every site, and transport flux. Pair budgets and absorption fields are derived downstream via corePairEvent and coreOperatorPairBudget rather than supplied as free data.
proof idea
The proof is a term proof consisting of a single direct application of indexedPairBudget_nonneg to the pair event obtained via corePairEvent from the operator. No further reductions or tactics appear.
why it matters
This result guarantees that the pair budget derived from the core operator remains non-negative, enabling the DerivedEstimates layer that supplies the six fields previously treated as free data. It supports construction of the full IncompressibleNSOperator whose pair-budget fields are now built from the core. The placement aligns with the requirement that derived quantities in the discrete model stay non-negative, consistent with the module's shift from assumed to constructed budgets.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.