def definition def or abbrev

`boundaryTerm`

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

formal statement (Lean)

  50noncomputable def boundaryTerm (P : RM2URadialProfile) : ℝ → ℝ :=

Definition body.

  51  fun r => tailFlux P.A P.A' r
  52
  53/-- Convenience: `TailFluxVanish` for a profile. -/

Lean names referenced from this declaration's body.

A in IndisputableMonolith.Foundation.IntegrationGap decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
RM2URadialProfile in IndisputableMonolith.NavierStokes.RM2U.Core decl_use
tailFlux in IndisputableMonolith.NavierStokes.RM2U.Core decl_use
TailFluxVanish in IndisputableMonolith.NavierStokes.RM2U.Core decl_use