eval
plain-language theorem explainer
The eval definition projects the underlying function from a scalar field structure to return its real value at a given spacetime point. Modelers of scalar fields in relativistic settings or circuit evaluations cite this accessor to obtain field values without additional computation. It is realized as a direct one-line projection from the structure's ψ component.
Claim. For a scalar field $φ$ whose component function is $ψ : (ℝ^4) → ℝ$, the evaluation at a point $x ∈ ℝ^4$ is given by $eval(φ, x) = ψ(x)$.
background
The Relativity.Fields.Scalar module defines a scalar field as a structure that assigns a real value to each point in four-dimensional spacetime via the function ψ : (Fin 4 → ℝ) → ℝ. This matches the module description that a scalar field assigns a real value to each spacetime point. Upstream, the same abstraction appears in Relativity.Geometry.Tensor as the abbreviation (Fin 4 → ℝ) → ℝ and in NavierStokes.DiscreteNSOperator as a finite-site map Fin siteCount → ℝ.
proof idea
The definition is a one-line wrapper that projects the ψ field from the ScalarField structure and applies it directly to the input point x.
why it matters
This accessor supports scalar field usage across the framework and feeds into downstream structures such as BooleanCircuitWithEval and CircuitDecides in Complexity.CircuitLedger as well as status summaries in Constants.Derivation and Constants.RSNativeUnits. It supplies the basic evaluation operation required for field-based models in the relativity sector, consistent with the Recognition Science approach of deriving physical quantities from functional equations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.