deriv_constant
plain-language theorem explainer
The directional derivative of any constant scalar field vanishes at every spacetime point and in every coordinate direction. Researchers deriving field equations or Lagrangians in the Recognition Science treatment of relativity cite this fact to drop gradient terms involving constant backgrounds. The proof is a one-line wrapper that unfolds the definitions of directional_deriv and constant then applies numerical normalization.
Claim. For any real constant $c$, direction index $μ ∈ {0,1,2,3}$, and spacetime point $x$, the directional derivative of the constant scalar field of value $c$ in direction $μ$ at $x$ is zero.
background
A scalar field assigns a real value to each spacetime point. The module defines the constant scalar field, directional derivative, and basic algebraic operations on fields. Upstream structures supply the J-cost and phi-forcing context in which these field operations sit inside the larger Recognition Science forcing chain.
proof idea
The proof is a one-line wrapper that applies the definitions of directional_deriv and constant, followed by norm_num to reduce the resulting expression to zero.
why it matters
This lemma supplies the elementary vanishing property required whenever constant scalar backgrounds appear in Recognition Science field models. It aligns with the framework's T5 J-uniqueness and T8 D=3 landmarks by ensuring derivative operators act only on non-constant degrees of freedom. No downstream theorems are listed, so the result functions as a foundational building block rather than a direct input to a parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.