partialDeriv_v2
plain-language theorem explainer
partialDeriv_v2 supplies a zero-valued placeholder for the directional derivative of the recognition reality field (RRF) at coordinate index mu and point x. Developers assembling the recognition Hamiltonian density and stress-energy tensor cite it while the full derivative rules remain external. The definition is a direct constant assignment that lets downstream expressions reference the operator without immediate differentiability obligations.
Claim. Let ψ be a recognition field of type (ℝ⁴ → ℝ). The partial derivative ∂_μ ψ(x) is defined to return the constant value 0 for every field, index μ ∈ Fin 4, and point x.
background
The module develops the Hamiltonian formalism for the Recognition Reality Field (RRF), an abbrev for maps (Fin 4 → ℝ) → ℝ. Its stated objective is to obtain energy conservation from time-translation symmetry of the ledger. The upstream partialDeriv_v2 in Relativity.Calculus.Derivatives supplies the concrete operator ∂_μ f(x) := deriv (fun t ↦ f (coordRay x μ t)) 0, while the local version here acts as a scaffold.
proof idea
The definition is a one-line wrapper that directly returns the constant 0, independent of the input field, index, or point. No lemmas are applied; the body is a literal constant assignment.
why it matters
It is referenced by HamiltonianDensity (which writes the density as ½(∂₀ψ)² + …) and StressEnergyTensor (which builds bilinear components from products of partialDeriv_v2 terms). These feed the module goal of proving energy conservation from time-translation invariance. The placeholder touches the integration step between the RRF scaffold and the full directional-derivative calculus imported from Derivatives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.