zero
plain-language theorem explainer
Zero scalar field is the constant function returning the value zero at every spacetime point. It supplies the additive identity for the vector space of scalar fields in the relativity module. The definition is a direct one-line instantiation of the constant field constructor with argument zero.
Claim. The zero scalar field is the map $p : (Fin 4 → ℝ) → ℝ$ given by $p(x) = 0$ for every spacetime point $x$.
background
In this module a scalar field is a structure whose sole field is a function ψ that assigns a real number to each spacetime point, where points are represented as maps from Fin 4 to ℝ. The constant scalar field constructor fixes ψ to return the same real value c at every point. The zero definition simply supplies the special case c = 0, yielding the neutral element under the addition operation defined on scalar fields.
proof idea
One-line wrapper that applies the constant constructor to the real number zero.
why it matters
This definition supplies the zero element required for the vector-space operations on scalar fields (addition and scalar multiplication) listed among the sibling declarations. It completes the basic algebraic structure without adding hypotheses or depending on geometry beyond the point representation. No downstream theorems are recorded, indicating it functions as a foundational building block rather than a derived result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.