core_pair_budget_absorbed
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove existence or uniqueness of solutions to the discrete equations.
- Does not address boundary conditions or external forcing.
- Does not extend the absorption claim to compressible or turbulent regimes.
- Does not supply numerical convergence rates to the continuous Navier-Stokes limit.
Lean usage
have h_budget : coreOperatorPairBudget op ≤ - totalViscous op.contributions := core_pair_budget_absorbed opformal statement (Lean)
187theorem core_pair_budget_absorbed {siteCount : ℕ}
188 (op : CoreNSOperator siteCount) :
189 coreOperatorPairBudget op ≤ - totalViscous op.contributions := by
proof body
Term-mode proof.
190 unfold coreOperatorPairBudget indexedPairBudget total
191 simp only [corePairEvent, pairEventBudget, corePairAmplitude, corePairStretchFactor]
192 exact op.viscous_absorbs
193
194/-- Stretching is absorbed by viscosity via the derived pair budget. -/