`core_dJdt_nonpos`

proved

show as: view math explainer →

module: IndisputableMonolith.NavierStokes.DiscreteNSOperator
domain: NavierStokes
line: 205 · 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 205.

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

formal source

 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)
 226  transport_def :
 227    contributions.transport = conservativeTransportField transportFlux transportPerm
 228  viscous_def :
 229    contributions.viscous = fun x => ν * scalarLaplacian topology h state.omega x
 230  pairAmplitude : Fin siteCount → ℝ
 231  pairStretchFactor : Fin siteCount → ℝ
 232  pairAmplitude_pos : ∀ i : Fin siteCount, 0 < pairAmplitude i
 233  pairStretchFactor_pos : ∀ i : Fin siteCount, 0 < pairStretchFactor i
 234  stretching_le_pair_budget :
 235    ∀ i : Fin siteCount,

papers checked against this theorem

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