structure definition def or abbrev

`ContributionFields`

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

formal statement (Lean)

  52structure ContributionFields (siteCount : ℕ) where
  53  transport : Fin siteCount → ℝ
  54  viscous : Fin siteCount → ℝ
  55  stretching : Fin siteCount → ℝ
  56
  57/-- Total contributions of the three pieces. -/

used by (8)

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

EvolutionIdentity in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use
stretching_term_nonneg in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use
totalStretching in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use
totalTransport in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use
totalViscous in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use
transport_term_cancels in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use
viscous_term_dissipative in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use
zero_transport_cancels in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use

depends on (5)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use