constant
plain-language theorem explainer
The constant definition constructs a scalar field that returns the fixed real value c at every point of four-dimensional spacetime. Modelers of uniform backgrounds in relativistic actions or conservation laws cite this construction when building constant solutions. The definition is a direct structural assignment to the ψ component of the ScalarField record.
Claim. A constant scalar field of value $c$ is the map $xmapsto c$ on spacetime points, i.e., the function $ψ:(Fin 4→ℝ)→ℝ$ given by $ψ(·)≡c$.
background
A scalar field assigns a real value to each spacetime point and is formalized as the structure ScalarField whose single field is the function ψ:(Fin 4→ℝ)→ℝ. The module states that scalar fields supply the basic objects for relativistic field theories and action principles. Upstream ScalarField abbreviations appear in the Navier-Stokes and Geometry modules, supplying consistent notation for discrete and tensorial settings.
proof idea
This is a direct definition that populates the ψ component of the ScalarField structure with the constant function returning c.
why it matters
The definition supplies the constant scalar field required by downstream theorems on energy conservation, geodesic equations, and cost-rate Euler-Lagrange conditions. It supports the Recognition framework's use of scalar fields inside action functionals and Noether symmetries that recover conservation laws. The construction closes a basic interface used across the Action and Hamiltonian modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.