def definition def or abbrev

`corePairStretchFactor`

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

formal statement (Lean)

 151def corePairStretchFactor {siteCount : ℕ} (op : CoreNSOperator siteCount)
 152    (i : Fin siteCount) : ℝ :=

Definition body.

 153  1 + op.dt * velocityGradientMag op.topology op.h op.velocity i
 154

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

core_pair_budget_absorbed in IndisputableMonolith.NavierStokes.DiscreteNSOperator decl_use
corePairEvent in IndisputableMonolith.NavierStokes.DiscreteNSOperator decl_use
corePairStretchFactor_pos in IndisputableMonolith.NavierStokes.DiscreteNSOperator decl_use
core_stretching_le_pair_budget in IndisputableMonolith.NavierStokes.DiscreteNSOperator decl_use
IncompressibleNSOperator in IndisputableMonolith.NavierStokes.DiscreteNSOperator decl_use

Lean names referenced from this declaration's body.

CoreNSOperator in IndisputableMonolith.NavierStokes.DiscreteNSOperator decl_use
velocityGradientMag in IndisputableMonolith.NavierStokes.DiscreteNSOperator decl_use