totalJcost
plain-language theorem explainer
The definition computes the aggregate J-cost of a discrete vorticity field by summing the per-site J-costs of amplitudes normalized to the field's root-mean-square scale. Researchers deriving monotonicity bounds or Hamiltonian generators for discrete Navier-Stokes models cite this when passing from local recognition costs to global energy-like quantities. The construction is a direct one-line composition of the total summation operator with the J-cost function applied pointwise to the normalized amplitudes.
Claim. Let $f : [N] → ℝ$ be a discrete vorticity field on $N$ sites. Let rms$(f)$ denote its root-mean-square value. The total J-cost is defined by $∑_{i=1}^N J(|f_i| / $rms$(f))$, where $J(x) = (x + x^{-1})/2 - 1$ is the recognition cost function.
background
The DiscreteVorticity module supplies exact bookkeeping objects for finite vorticity fields on a lattice window: the total sum, root-mean-square scale, pointwise normalized amplitudes, and the three contribution fields (transport, viscous, stretching) that decompose the J-cost derivative. The local setting isolates these algebraic identities so that the hard PDE inequalities can be attached later. Upstream, the same totalJcost pattern appears in HamiltonianEmergence as the sum of per-bond J-costs on small-deviation states and in JCostGeometry as the sum of J-costs over neighbor ratios; both treat J-cost as the derived cost of a multiplicative recognizer.
proof idea
One-line wrapper that applies the total summation operator to the J-cost of each normalized amplitude. The normalizedAmplitude sibling supplies the pointwise ratio |f_i| / rms(f), after which the outer total folds the J-cost function across the finite index set.
why it matters
This definition supplies the global scalar that feeds the quadratic-emergence theorems in HamiltonianEmergence, including totalJcost_approx_quadratic and the hypothesis H_HamiltonianIsGenerator that the recognition operator generates a self-adjoint Hamiltonian in the small-deviation limit. It closes the bookkeeping step required by the J-cost monotonicity program and sits between the T5 J-uniqueness identity and the later discrete Navier-Stokes evolution identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.