theorem proved term proof

`operator_transport_zero`

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

formal statement (Lean)

 280theorem operator_transport_zero {siteCount : ℕ}
 281    (ns : IncompressibleNSOperator siteCount) :
 282    totalTransport ns.contributions = 0 := by

proof body

Term-mode proof.

 283  unfold totalTransport
 284  rw [ns.transport_def]
 285  exact total_conservativeTransportField_zero _ _
 286

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

dJcost_dt_nonpos_of_operator in IndisputableMonolith.NavierStokes.JcostMonotonicity decl_use

depends on (3)

Lean names referenced from this declaration's body.

IncompressibleNSOperator in IndisputableMonolith.NavierStokes.DiscreteNSOperator decl_use
total_conservativeTransportField_zero in IndisputableMonolith.NavierStokes.DiscreteNSOperator decl_use
totalTransport in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use