core_stretching_absorbed

formal source

 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 : ℝ
 218  ν : ℝ
 219  h_pos : 0 < h
 220  ν_pos : 0 < ν
 221  state : State siteCount
 222  velocity : VectorField siteCount
 223  divergence_free : ∀ x : Fin siteCount, divergence topology h velocity x = 0
 224  transportFlux : ScalarField siteCount
 225  transportPerm : Equiv.Perm (Fin siteCount)