add_comm
plain-language theorem explainer
Addition of scalar fields is commutative under pointwise evaluation at spacetime points. Researchers deriving algebraic properties of fields in Recognition Science or cost algebras would cite this to confirm the underlying ring structure before invoking simplifications in larger proofs. The proof is a short tactic sequence that introduces an arbitrary point, unfolds the evaluation and addition definitions, and applies the ring tactic to reduce to commutativity of real addition.
Claim. Let $φ_1, φ_2$ be scalar fields, each a map from spacetime points $x ∈ ℝ^4$ to real numbers. Then for all $x$, eval$(φ_1 + φ_2, x) = $eval$(φ_2 + φ_1, x)$.
background
In this module a scalar field is the structure whose single field ψ maps (Fin 4 → ℝ) to ℝ, i.e., assigns a real value to each point of four-dimensional spacetime. The sibling definition eval φ x := φ.ψ x simply projects this function. Addition is the pointwise operation on these functions, whose explicit form appears among the module siblings.
proof idea
The proof is a short tactic sequence: introduce an arbitrary spacetime point x, simplify using the definitions of eval and add to expose pointwise real addition, then apply the ring tactic which discharges the equality by commutativity of addition on ℝ.
why it matters
This result guarantees that the scalar-field algebra is commutative and is invoked directly by downstream theorems such as costFamily_neg_param (via simp [add_comm]) to establish evenness of the κ-family. It therefore supports the cost algebra and recognition-category constructions that feed into H_dAlembert and the multiplicative d'Alembert equation whose solution is cosh. In the Recognition Science framework it supplies one of the elementary algebraic facts needed for the phi-ring and the functional equations that appear in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.