add
plain-language theorem explainer
Scalar field addition constructs the pointwise sum of two scalar fields on spacetime. Researchers building algebraic structures for fields in Recognition Science relativity would cite this when forming linear combinations. The definition proceeds by direct construction of the result's ψ component as the sum of the input ψ functions.
Claim. For scalar fields $φ_1$ and $φ_2$, the sum is the scalar field $φ$ defined by $φ.ψ(x) = φ_1.ψ(x) + φ_2.ψ(x)$ for every spacetime point $x : ℝ^4$.
background
A scalar field assigns a real value to each spacetime point. The structure ScalarField packages this as a function ψ from (Fin 4 → ℝ) to ℝ, matching the abbrev ScalarField in DiscreteNSOperator and the identical structure in Geometry.Tensor. The module sets the local setting as scalar fields on 4D spacetime within the relativity treatment.
proof idea
The definition is a direct one-line construction that equips the output with the pointwise sum of the two input ψ functions. No lemmas or tactics are invoked.
why it matters
This definition supplies the additive operation on scalar fields, which is required for the sibling declarations that establish commutativity and related properties. It supports the algebraic layer of field constructions in the Recognition Science relativity module and aligns with the framework's derivation of physics from a single functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.