pith. machine review for the scientific record. sign in
def definition def or abbrev high

total

show as:
view Lean formalization →

This definition supplies the exact sum of a scalar field over a finite lattice window of sites. Discrete fluid and vorticity modelers in Recognition Science cite it when decomposing J-cost changes into transport, viscous, and stretching contributions. It is realized as a direct finite summation with no auxiliary lemmas or reductions.

claimFor a scalar field $f$ on a finite set of $N$ lattice sites, the total amplitude is defined by the sum $T(f) = ∑_{i=1}^N f(i)$.

background

The Discrete Vorticity module supplies exact bookkeeping primitives for finite vorticity fields on a lattice window. These primitives include totals, RMS values, and normalized amplitudes that later decompose the derivative of J-cost into transport, viscous, and stretching pieces. The module deliberately isolates this surface from the hard PDE inequalities so that monotonicity lemmas can be added incrementally.

proof idea

The definition is a direct summation over the finite index set. No lemmas are invoked; the body is the primitive sum operator applied to the field values.

why it matters in Recognition Science

The total supplies the amplitude primitive consumed by energy-conservation certificates and Noether theorems in the Action layer, including space-translation invariance implying momentum conservation and the total-energy definition along Newtonian trajectories. It thereby anchors the discrete bookkeeping required for J-cost minimization, which rests on the convex J-function, the eight-tick local dynamics, and the phi-ladder structure derived from the Recognition functional equation.

scope and limits

formal statement (Lean)

  32def total {siteCount : ℕ} (f : Fin siteCount → ℝ) : ℝ :=

proof body

Definition body.

  33  ∑ i : Fin siteCount, f i
  34
  35/-- RMS square of a scalar field. -/

used by (40)

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

… and 10 more

depends on (6)

Lean names referenced from this declaration's body.