constant_eval
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not apply to non-constant scalar fields.
- Does not address derivatives or field equations.
- Does not incorporate spacetime curvature.
- Does not assign physical units or link to constants such as phi.
formal statement (Lean)
20theorem constant_eval (c : ℝ) (x : Fin 4 → ℝ) :
21 eval (constant c) x = c := rfl
proof body
Term-mode proof.
22
23/-- Zero scalar field. -/