pith. machine review for the scientific record. sign in
def definition def or abbrev high

eval

show as:
view Lean formalization →

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.

claimFor 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  15noncomputable def eval (φ : ScalarField) (x : Fin 4 → ℝ) : ℝ := φ.ψ x

proof body

Definition body.

  16
  17/-- Constant scalar field. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (4)

Lean names referenced from this declaration's body.