def definition def or abbrev

`totalStretching`

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

formal statement (Lean)

  64def totalStretching {siteCount : ℕ} (c : ContributionFields siteCount) : ℝ :=

Definition body.

  65  total c.stretching
  66
  67/-- Data recording an exact J-cost derivative split. -/

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

core_stretching_absorbed in IndisputableMonolith.NavierStokes.DiscreteNSOperator decl_use
totalStretching_le_operatorPairBudget in IndisputableMonolith.NavierStokes.DiscreteNSOperator decl_use
dJdt_eq_viscous_plus_stretching in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use
dJdt_nonpos_of_transport_cancel_and_absorption in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use
EvolutionIdentity in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use
stretching_term_nonneg in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use
stretching_absorbed_by_viscosity in IndisputableMonolith.NavierStokes.JcostMonotonicity decl_use

Lean names referenced from this declaration's body.

cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
ContributionFields in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use
total in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use
total in IndisputableMonolith.NumberTheory.RiemannHypothesis.ErrorBudget decl_use