coreOperatorPairBudget_nonneg
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove existence of solutions to the discrete equations.
- Does not bound the magnitude of the pair budget.
- Does not address the continuous limit as lattice spacing tends to zero.
- Does not incorporate external forces or boundary conditions.
formal statement (Lean)
181theorem coreOperatorPairBudget_nonneg {siteCount : ℕ}
182 (op : CoreNSOperator siteCount) :
183 0 ≤ coreOperatorPairBudget op :=
proof body
Term-mode proof.
184 indexedPairBudget_nonneg (corePairEvent op)
185
186/-- The derived pair budget is absorbed by viscosity. -/