deriv_smul
plain-language theorem explainer
The declaration establishes linearity of directional derivatives under constant scaling for scalar fields on spacetime. Researchers deriving equations of motion or stress-energy tensors in Recognition Science relativity would invoke this when factoring constants out of derivatives. The proof proceeds by direct simplification of the definitions followed by ring normalization.
Claim. For a real scalar $c$, a scalar field assigning a real value to each spacetime point, a direction index $mu$ in Fin 4, and a point $x$ in $mathbb{R}^4$, the directional derivative of the scaled field $c$ times the scalar field in direction $mu$ at $x$ equals $c$ times the directional derivative of the original field in direction $mu$ at $x$.
background
ScalarField is defined as a structure whose sole component is a function from spacetime points (Fin 4 to real numbers) to real numbers. The module sets the local setting as scalar fields in spacetime for relativistic field theory. Upstream results supply structures from PhiForcingDerived on J-cost and from SpectralEmergence on gauge content and particle generations that embed this algebraic property in the broader Recognition Science framework.
proof idea
The proof is a term-mode proof that applies simp only on the definitions of directional_deriv and smul, then invokes ring to verify the resulting algebraic identity.
why it matters
This supplies a basic linearity property for scalar field operations in the Relativity.Fields.Scalar module. It supports manipulations within the Recognition Science forcing chain from T0 to T8 without new hypotheses. No direct parent theorems appear in the used_by edges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.