constant_eval
plain-language theorem explainer
Constant scalar fields evaluate to their fixed value at every spacetime point. Researchers modeling uniform potentials in relativistic settings cite this for verifying field definitions. The proof is a one-line reflexivity that follows directly from the definitions of constant and eval.
Claim. For any real number $c$ and spacetime point $x : Fin 4 → ℝ$, the evaluation of the constant scalar field with value $c$ at $x$ equals $c$.
background
A scalar field assigns a real value to each spacetime point. The constant scalar field is the structure whose underlying function ψ returns the fixed real c at every input. Evaluation of a scalar field φ at x is the direct application of φ.ψ to x.
proof idea
The proof is a term-mode reflexivity (rfl). It unfolds the definition of constant to the constant function and the definition of eval to function application, matching the right-hand side c identically.
why it matters
This supplies the basic evaluation property for constant fields inside the relativity scalar module. It ensures uniform fields behave as expected before introducing derivatives or dynamics. No downstream theorems are listed yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.