theorem proved term proof

`core_dJdt_nonpos`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 205theorem core_dJdt_nonpos {siteCount : ℕ}
 206    (op : CoreNSOperator siteCount) :
 207    op.dJdt ≤ 0 :=

proof body

Term-mode proof.

 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. -/

depends on (8)

Lean names referenced from this declaration's body.

from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
modules in IndisputableMonolith.Masses.Manifest decl_use
CoreNSOperator in IndisputableMonolith.NavierStokes.DiscreteNSOperator decl_use
core_stretching_absorbed in IndisputableMonolith.NavierStokes.DiscreteNSOperator decl_use
core_transport_zero in IndisputableMonolith.NavierStokes.DiscreteNSOperator decl_use
IncompressibleNSOperator in IndisputableMonolith.NavierStokes.DiscreteNSOperator decl_use
dJdt_nonpos_of_transport_cancel_and_absorption in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use