smul
plain-language theorem explainer
Scalar multiplication equips spacetime scalar fields with pointwise scaling by reals, allowing linear combinations inside integrals and convexity arguments. Researchers in continuum fluid limits and action functionals cite it when rescaling fields for Duhamel kernels or J-cost inequalities. The definition constructs the output field by direct pointwise multiplication on the underlying ψ function.
Claim. For real $c$ and scalar field $φ$ with evaluation map $ψ_φ : (Fin 4 → ℝ) → ℝ$, the scaled field $c · φ$ satisfies $(c · φ)(x) = c · ψ_φ(x)$ at every spacetime point $x$.
background
ScalarField is the structure that assigns a real value to each point in 4-dimensional spacetime via the component ψ : (Fin 4 → ℝ) → ℝ. The module supplies the algebraic operations needed to treat these fields as a vector space over ℝ, supporting relativistic models and their passage to continuum limits.
proof idea
One-line structural definition that builds a new ScalarField whose ψ component is the pointwise product c * φ.ψ. No lemmas or tactics are applied; the body directly records the scaled function.
why it matters
The definition supplies the scaling operation required by downstream results on J-cost convexity and Duhamel remainders in 2D fluid limits. It closes the algebraic interface for scalar fields that appears in action functionals and forcing terms, feeding lemmas such as Jcost_convex_combination and the various nsDuhamel identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.