eta_deriv_zero
plain-language theorem explainer
The Minkowski metric tensor is independent of position, so every coordinate derivative vanishes identically. Workers deriving curvature tensors or Christoffel symbols in flat spacetime cite this fact to simplify all subsequent expressions to zero. The proof is a one-line wrapper that invokes the constant-function derivative lemma after unfolding the metric definition to confirm constancy.
Claim. $∂_κ η_{μν}(x) = 0$ for all indices $μ,ν,κ ∈ {0,1,2,3}$ and all $x ∈ ℝ^4$, where $η$ denotes the Minkowski metric bilinear form with components $η_{00}=-1$, $η_{ii}=1$ for $i=1,2,3$ and all off-diagonal entries zero.
background
The operator partialDeriv_v2 reduces the directional derivative $∂_μ f(x)$ to the ordinary derivative of $f$ composed with the coordinate ray along the $μ$-th axis. The metric eta is the constant bilinear form that returns $-1$ on the time-time slot, $+1$ on the three spatial diagonal slots, and zero otherwise. This lemma lives in the module that constructs Christoffel symbols directly from an arbitrary metric tensor. It rests on the upstream fact that the derivative of any constant function is identically zero.
proof idea
The proof applies the lemma partialDeriv_v2_const, supplying the constant value eta x (fun _ => 0) (fun i => if i.val = 0 then μ else ν). It then unfolds the definition of eta to obtain a constant expression independent of the dummy variable y and closes with reflexivity.
why it matters
The result is invoked inside minkowski_christoffel_zero_proper to conclude that all Christoffel symbols of the Minkowski metric vanish. In the Recognition Science setting this confirms that the flat metric produces zero curvature, consistent with the eight-tick octave and the emergence of D=3 spatial dimensions from the forcing chain. It supplies the base case needed before curvature tensors are computed for non-flat metrics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.