`coreOperatorPairBudget`

definition

show as: view math explainer →

module: IndisputableMonolith.NavierStokes.DiscreteNSOperator
domain: NavierStokes
line: 178 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NavierStokes.DiscreteNSOperator on GitHub at line 178.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 175  exact op.stretching_bound i
 176
 177/-- Total derived pair budget from the core. -/
 178def coreOperatorPairBudget {siteCount : ℕ} (op : CoreNSOperator siteCount) : ℝ :=
 179  indexedPairBudget (corePairEvent op)
 180
 181theorem coreOperatorPairBudget_nonneg {siteCount : ℕ}
 182    (op : CoreNSOperator siteCount) :
 183    0 ≤ coreOperatorPairBudget op :=
 184  indexedPairBudget_nonneg (corePairEvent op)
 185
 186/-- The derived pair budget is absorbed by viscosity. -/
 187theorem core_pair_budget_absorbed {siteCount : ℕ}
 188    (op : CoreNSOperator siteCount) :
 189    coreOperatorPairBudget op ≤ - totalViscous op.contributions := by
 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. -/
 195theorem core_stretching_absorbed {siteCount : ℕ}
 196    (op : CoreNSOperator siteCount) :
 197    totalStretching op.contributions ≤ - totalViscous op.contributions := by
 198  have hle : totalStretching op.contributions ≤ coreOperatorPairBudget op := by
 199    unfold totalStretching total coreOperatorPairBudget indexedPairBudget
 200    exact Finset.sum_le_sum (fun i _ =>
 201      by simpa [corePairEvent, pairEventBudget] using core_stretching_le_pair_budget op i)
 202  exact le_trans hle (core_pair_budget_absorbed op)
 203
 204/-- J-cost monotonicity from the core operator alone. -/
 205theorem core_dJdt_nonpos {siteCount : ℕ}
 206    (op : CoreNSOperator siteCount) :
 207    op.dJdt ≤ 0 :=
 208  dJdt_nonpos_of_transport_cancel_and_absorption op.toEvolutionIdentity

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.