field_squared
This definition supplies the pointwise square of a scalar field value at a spacetime point for insertion into potential terms. A researcher building relativistic scalar actions would cite it to express the quadratic contribution in the Lagrangian density. The definition is realized by a direct projection onto the field's evaluation map followed by squaring.
claimLet $φ$ be a scalar field with evaluation map $ψ : (ℝ^4) → ℝ$. The squared field at spacetime point $x ∈ ℝ^4$ is defined by $φ²(x) := [ψ(x)]²$.
background
A scalar field is formalized here as a structure containing a single function ψ that assigns a real number to each point in 4-dimensional spacetime, represented as Fin 4 → ℝ. The module opens by stating that a scalar field assigns a real value to each spacetime point. Upstream abbrevs in the Navier-Stokes and Geometry modules supply dimensionally different versions of the same concept, while the local structure specializes it to the relativistic 4D setting.
proof idea
The definition is a one-line wrapper that projects the ψ component of the input structure at the given point and squares the resulting real value.
why it matters in Recognition Science
It supplies the quadratic term required by the potential action integral defined downstream, which assembles (m²/2) times the integral of this squared field against the volume element. The same file immediately uses it to prove non-negativity. In the Recognition framework this quadratic form enters the mass term on the phi-ladder and the action principles that recover D = 3 and the eight-tick octave.
scope and limits
- Does not define the full action integral or Lagrangian.
- Does not impose any dynamics or equation of motion on the field.
- Does not reference the J-cost function or phi-ladder.
- Does not extend to vector or tensor fields.
formal statement (Lean)
90noncomputable def field_squared (φ : ScalarField) (x : Fin 4 → ℝ) : ℝ :=
proof body
Definition body.
91 (φ.ψ x) ^ 2
92