field_squared_nonneg
The squared value of any scalar field at a spacetime point is non-negative. Relativists modeling scalar potentials or energy densities cite this when enforcing positivity constraints on observables. The proof is a one-line term wrapper that unfolds the field_squared definition and applies the standard sq_nonneg fact from the reals.
claimFor any scalar field $φ$ and point $x$ in four-dimensional spacetime, $(φ(x))^2 ≥ 0$.
background
ScalarField is the structure whose single field ψ maps each spacetime point (Fin 4 → ℝ) to a real number. The auxiliary definition field_squared simply returns the square of that value at the chosen point. The module treats scalar fields as the simplest relativistic objects, importing the same type abbreviation from both the geometry tensor layer and the discrete Navier-Stokes operator.
proof idea
The term proof first calls simp with the field_squared definition, which replaces the goal by (φ.ψ x)^2. It then applies the Mathlib lemma sq_nonneg directly to the resulting real number.
why it matters in Recognition Science
The result supplies the elementary non-negativity needed for any later construction of energy densities or stability criteria built from scalar fields. It closes the most basic positivity requirement inside the scalar sector of the relativity module, consistent with the framework demand that squared quantities remain non-negative before further forcing-chain steps are applied.
scope and limits
- Does not address vector or tensor fields.
- Does not treat complex-valued scalars.
- Does not derive bounds stricter than zero.
- Does not involve derivatives or field equations.
formal statement (Lean)
93theorem field_squared_nonneg (φ : ScalarField) (x : Fin 4 → ℝ) :
94 field_squared φ x ≥ 0 := by
proof body
Term-mode proof.
95 simp [field_squared]
96 exact sq_nonneg _
97
98end Fields
99end Relativity
100end IndisputableMonolith