smul_zero
plain-language theorem explainer
Scalar multiplication by zero annihilates any scalar field, returning the zero field at every spacetime point. Researchers modeling field dynamics in Recognition Science cite this when reducing expressions involving zero coefficients in relativistic equations. The proof is a direct simplification using the definitions of field evaluation and scalar multiplication.
Claim. For any scalar field $φ$ (a map from spacetime points in $ℝ^4$ to $ℝ$), the evaluation of the zero-scaled field satisfies $∀ x, eval(smul 0 φ) x = 0$.
background
A scalar field assigns a real value to each spacetime point via the structure $ψ : (Fin 4 → ℝ) → ℝ$. The eval function extracts this value at a point, while smul implements componentwise multiplication by a real scalar. This module develops the basic algebraic operations on such fields for relativistic applications in Recognition Science.
proof idea
The proof introduces the arbitrary point x and applies simplification on the definitions of eval and smul, reducing the left-hand side directly to the constant zero.
why it matters
This lemma supplies a basic annihilation property for the scalar field algebra, supporting simplifications in field equations within the relativity module. It aligns with the framework's spacetime setup (Fin 4 for 3+1 dimensions) and the eight-tick dynamics from upstream PhiForcingDerived and SpectralEmergence structures. No downstream uses appear yet, leaving it as foundational scaffolding for later field manipulations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.