core_pair_budget_absorbed

formal source

 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
 209    (core_transport_zero op) (core_stretching_absorbed op)
 210
 211/-! ## Legacy IncompressibleNSOperator (now built from CoreNSOperator) -/
 212
 213/-- Full operator surface, now constructible from a `CoreNSOperator`.
 214Retained for backward compatibility with downstream modules. -/
 215structure IncompressibleNSOperator (siteCount : ℕ) extends EvolutionIdentity siteCount where
 216  topology : LatticeTopology siteCount
 217  h : ℝ