core_pair_budget_absorbed
plain-language theorem explainer
The theorem establishes that the derived pair budget of a core discrete Navier-Stokes operator is bounded above by the negative total viscous contribution on the lattice. Researchers deriving energy balances for incompressible flows in Recognition Science or discrete fluid models would cite this when closing absorption properties from core data. The proof is a direct term reduction that unfolds the budget definitions and invokes the operator's viscous absorption field.
Claim. Let $op$ be a core Navier-Stokes operator on a lattice with $N$ sites. The derived pair budget satisfies $pairBudget(op) ≤ -totalViscous(op.contributions)$.
background
The module constructs a concrete discrete incompressible Navier-Stokes operator on a finite three-direction lattice. CoreNSOperator supplies the physical data: lattice topology, spacing $h$, viscosity $ν$, divergence-free velocity field, and transport flux, but carries no pair-budget or absorption fields. Those quantities are derived from the velocity gradient and Laplacian via the CoreNSOperator structure, which extends EvolutionIdentity. The local setting replaces previously free data (pair amplitude, stretch factor, absorption hypotheses) with explicit constructions from the core flow.
proof idea
The term proof unfolds coreOperatorPairBudget and indexedPairBudget, then simplifies using the core pair event, pair event budget, core pair amplitude, and core pair stretch factor definitions. It concludes by applying the viscous_absorbs field carried by the operator.
why it matters
This supplies the absorption inequality required by the downstream theorem core_stretching_absorbed, which bounds total stretching by the negative viscous term. It completes the derivation layer that turns the bare CoreNSOperator into the full IncompressibleNSOperator whose pair-budget fields are constructed rather than assumed, advancing the discrete NS surface in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.