theorem proved term proof

`total_viscous_nonpos`

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

formal statement (Lean)

  42theorem total_viscous_nonpos {siteCount : ℕ}
  43    (viscousField : Fin siteCount → ℝ)
  44    (pointwise_nonpos : ∀ i : Fin siteCount, viscousField i ≤ 0) :
  45    total viscousField ≤ 0 := by

proof body

Term-mode proof.

  46  unfold total
  47  exact Finset.sum_nonpos (fun i _ => pointwise_nonpos i)
  48
  49/-! ## Gap 2: Sub-Kolmogorov Viscous Domination (PROVED)
  50
  51Pure real arithmetic: if mu * h^2 <= nu then mu <= nu / h^2. -/
  52

depends on (3)

Lean names referenced from this declaration's body.

mu in IndisputableMonolith.Cost.Ndim.Projector decl_use
total in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use
total in IndisputableMonolith.NumberTheory.RiemannHypothesis.ErrorBudget decl_use