partialDeriv_v2
plain-language theorem explainer
partialDeriv_v2 supplies a zero-valued placeholder for the directional derivative of the recognition reality field. It is cited in constructions of the Hamiltonian density and stress-energy tensor inside the Recognition Hamiltonian Formalism. The definition is a direct constant assignment that ignores its three arguments.
Claim. Define the placeholder operator by setting the directional derivative to zero: for recognition field function type RRF, index μ in Fin 4, and point x in Fin 4 → ℝ, let ∂_μ ψ(x) := 0.
background
The module sets up the Recognition Hamiltonian Formalism whose objective is to derive the Hamiltonian H_rec for the Recognition Reality Field and prove energy conservation from time-translation symmetry. RRF is the local non-sealed interface abbrev RRF := (Fin 4 → ℝ) → ℝ. The upstream partialDeriv_v2 from Relativity.Calculus.Derivatives supplies the actual definition ∂_μ f(x) := deriv (fun t => f (coordRay x μ t)) 0.
proof idea
The definition is a direct constant assignment returning 0, independent of the recognition field, coordinate index, and evaluation point.
why it matters
It is used by HamiltonianDensity (which sets the density proportional to (∂_0 ψ)^2 plus gradient terms) and StressEnergyTensor (which builds the bilinear form from products of partialDeriv_v2 terms). The placeholder fills the interface required by the Recognition Hamiltonian Formalism module while the actual derivative computation remains in the calculus layer. It touches the scaffold closure needed to connect the Hamiltonian to the J-cost and phi-ladder structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.