partialDeriv_v2 — Recognition explainer

formal statement (Lean)

  25noncomputable def partialDeriv_v2 (_psi : RRF) (_μ : Fin 4) (_x : Fin 4 → ℝ) : ℝ := 0

proof body

Definition body.

  26
  27/-- Placeholder metric determinant accessor. -/

used by (34)

From the project-wide theorem graph. These declarations reference this one in their body.

HamiltonianDensity in IndisputableMonolith.Foundation.Hamiltonian decl_use
StressEnergyTensor in IndisputableMonolith.Foundation.Hamiltonian decl_use
deriv_add_lin in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use
differentiableAt_coordRay_partialDeriv_v2_radialInv in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use
laplacian_smul in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use
partialDeriv_v2 in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use
partialDeriv_v2_const in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use
partialDeriv_v2_mul in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use
partialDeriv_v2_radialInv in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use
partialDeriv_v2_smul in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use
partialDeriv_v2_spatialNormSq in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use
partialDeriv_v2_spatialRadius in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use
partialDeriv_v2_x_sq in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use
secondDeriv in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use
secondDeriv_radialInv in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use
secondDeriv_smul in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use
secondDeriv_smul_local in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use
C2DischargeCert in IndisputableMonolith.Relativity.Calculus.RadialDerivativesProofs decl_use
differentiableAt_coordRay_partialDeriv_v2_radialInv_proved in IndisputableMonolith.Relativity.Calculus.RadialDerivativesProofs decl_use
partialDeriv_v2_radialInv_proved in IndisputableMonolith.Relativity.Calculus.RadialDerivativesProofs decl_use
partialDeriv_v2_spatialRadius_proved in IndisputableMonolith.Relativity.Calculus.RadialDerivativesProofs decl_use
secondDeriv_radialInv_proved in IndisputableMonolith.Relativity.Calculus.RadialDerivativesProofs decl_use
cov_deriv_1_2 in IndisputableMonolith.Relativity.Geometry.CovariantDerivative decl_use
christoffel in IndisputableMonolith.Relativity.Geometry.Curvature decl_use
eta_deriv_zero in IndisputableMonolith.Relativity.Geometry.Curvature decl_use
minkowski_riemann_zero in IndisputableMonolith.Relativity.Geometry.Curvature decl_use
riemann_tensor in IndisputableMonolith.Relativity.Geometry.Curvature decl_use
connection_uniqueness_lowered in IndisputableMonolith.Relativity.Geometry.LeviCivitaTheorem decl_use
cov_deriv_metric in IndisputableMonolith.Relativity.Geometry.LeviCivitaTheorem decl_use
FundamentalTheoremUniqueness in IndisputableMonolith.Relativity.Geometry.LeviCivitaTheorem decl_use

… and 4 more

depends on (2)

Lean names referenced from this declaration's body.

RRF in IndisputableMonolith.Foundation.Hamiltonian decl_use
partialDeriv_v2 in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use