pd as a directional fderiv: ∂ᵢ g (x) = Dg(x)[eᵢ] for g differentiable at x. The bridge from the coordinate partial derivative to the Fréchet derivative (chain rule through update).

\mathrm{DifferentiableAt}\,\mathbb{R}\,g\,x \to \href{/browser/qiqth-curvature#d-qiqth-curvature-pd}{\partial_{{i}}({g})({x})} = (\mathrm{fderiv}\,\mathbb{R}\,g\,x)\,(\mathrm{single}\,i\,1)

Proof. Immediate from the definitions. $\square$

Used by contDiff_pd, pd_pd_eq, PdiffAt_pd, second_bianchi_deriv_part, const_of_pd_zero.

Lemma 30 (pd_pd_eq). source ↗

A mixed second partial equals the second Fréchet derivative bilinear form on the basis vectors.

({f})\in C^{\infty} \to \partial_{{i}}({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-pd}{\partial_{{j}}({f})({y})}})({x}) = ((\mathrm{fderiv}\,\mathbb{R}\,(\mathrm{fderiv}\,\mathbb{R}\,f)\,x)\,(\mathrm{single}\,i\,1))\,(\mathrm{single}\,j\,1)

Proof. By pd_eq_fderiv. $\square$

Used by pd_comm.

Lemma 31 (pd_comm). source ↗

Schwarz: mixed partial derivatives commute ∂ᵢ∂ⱼ f = ∂ⱼ∂ᵢ f for smooth f. The analytic keystone for the second Bianchi identity.

({f})\in C^{\infty} \to \partial_{{i}}({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-pd}{\partial_{{j}}({f})({y})}})({x}) = \partial_{{j}}({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-pd}{\partial_{{i}}({f})({y})}})({x})

Proof. By pd_pd_eq. $\square$

Used by second_bianchi_deriv_part, lowered_riemann_antisymm, hessGrad_partial_eq, ricci_identity.

Lemma 32 (PdiffAt_pd). source ↗

The partial derivative ∂_d f of a smooth field is itself partially differentiable in any direction (f ∈ C^∞ ⇒ ∂_d f ∈ C^∞ ⇒ differentiable).

({f})\in C^{\infty} \to \forall (d e : \mathrm{Fin}\,n) (z : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}), \href{/browser/qiqth-curvature#d-qiqth-curvature-pdiffat}{\mathrm{PdiffAt}}\,(\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-pd}{\partial_{{d}}({f})({y})})\,e\,z

Proof. By pd_eq_fderiv. $\square$

Used by second_bianchi, PdiffAt_riemann, kg_conserv_of_contDiff, pd_covDerivVec, covDeriv2Vec_trace, geodesic_divergence_leibniz.

Definition 33 (christoffel). source ↗

Christoffel symbols Γ^μ_{νρ} = ½ g^{μα}(∂_ν g_{αρ} + ∂_ρ g_{αν} − ∂_α g_{νρ}).

Used by christoffel_contDiff, riemann_contDiff, christoffel_symm, riemann, riemann_antisymm, covDerivVec, covDeriv02, covDeriv20, and 53 more.

Lemma 34 (christoffel_symm). source ↗

Christoffel symbols are symmetric in their lower indices (torsion-freeness), for a symmetric metric. Immediate from the definition — no analytic input.

(\forall (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}) (a b : \mathrm{Fin}\,n), g_{{a}{b}}({y}) = g_{{b}{a}}({y})) \to \forall (\mu \nu \rho : \mathrm{Fin}\,n) (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}), \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\mu}}_{{\nu}{\rho}}({x})} = \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\mu}}_{{\rho}{\nu}}({x})}

Proof. By pd. $\square$

Used by riemann_first_bianchi, bianchi_extra_terms, hHessGrad_eq, ricci_identity.

Definition 35 (riemann). source ↗

Riemann curvature tensor (type (1,3)), R^ρ_{σμν} = ∂_μ Γ^ρ_{νσ} − ∂_ν Γ^ρ_{μσ} + Σ_λ (Γ^ρ_{μλ} Γ^λ_{νσ} − Γ^ρ_{νλ} Γ^λ_{μσ}).

Used by riemann_contDiff, ricci_contDiff, riemann_antisymm, ricci, riemann_first_bianchi, bianchi_extra_terms, covDerivRiem, second_bianchi, and 14 more.

Lemma 36 (riemann_antisymm). source ↗

Riemann is antisymmetric in its last two indices: R^ρ_{σμν} = −R^ρ_{σνμ}. Immediate from the definition (the derivative pair and the quadratic sum each negate under μ ↔ ν).

\href{/browser/qiqth-curvature#d-qiqth-curvature-riemann}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\rho\,\sigma\,\mu\,\nu\,x = -\href{/browser/qiqth-curvature#d-qiqth-curvature-riemann}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\rho\,\sigma\,\nu\,\mu\,x

Proof. By pd, christoffel. $\square$

Used by bianchi_extra_terms, covDerivRiem_antisymm, lowered_riemann_pair_symm.

Definition 37 (ricci). source ↗

Ricci tensor R_{σν} = R^μ_{σμν} (contraction on the first and third indices).

\mathrm{ricci}\,n\,g\,\mathrm{gi}\,\sigma\,\nu\,x \;:=\; \sum_{\mu} \href{/browser/qiqth-curvature#d-qiqth-curvature-riemann}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\mu\,\sigma\,\mu\,\nu\,x

Used by ricci_contDiff, scalarCurv_contDiff, scalarCurv, einsteinTensor, covDerivRiem_contract, covDerivRiem_contract', second_bianchi_contracted, lowered_riemann_gi_trace, and 24 more.

Definition 38 (scalarCurv). source ↗

Scalar curvature R = g^{σν} R_{σν}.

\mathrm{scalarCurv}\,n\,g\,\mathrm{gi}\,x \;:=\; \sum_{\sigma} \sum_{\nu} g^{{\sigma}{\nu}}({x}) \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-ricci}{R_{{\sigma}{\nu}}({x})}

Used by scalarCurv_contDiff, einsteinTensor, gi_trace_covDeriv_ricci, twice_contracted_bianchi, einstein_field_equation_real, einstein_field_equation_real_global, jacobson_einstein_equation_of_state, hreg_kg, and 5 more.

Definition 39 (einsteinTensor). source ↗

Einstein tensor G_{σν} = R_{σν} − ½ R g_{σν}.

\mathrm{einsteinTensor}\,n\,g\,\mathrm{gi}\,\sigma\,\nu\,x \;:=\; \href{/browser/qiqth-curvature#d-qiqth-curvature-ricci}{R_{{\sigma}{\nu}}({x})} - 1/2 \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-scalarcurv}{R({x})} \cdot g_{{\sigma}{\nu}}({x})

Used by einstein_field_equation_real, einstein_field_equation_real_global, jacobson_einstein_equation_of_state, qiqt_gr_freefield_complete, qiqt_gr_freefield_complete_covCong, qiqt_gr_explicit_kg, qiqt_gr_freefield, qiqt_gr_freefield_localized, and 10 more.

Definition 40 (covDerivVec). source ↗

Covariant derivative of a vector field V^μ: ∇_ν V^μ = ∂_ν V^μ + Γ^μ_{νσ} V^σ.

\mathrm{covDerivVec}\,n\,g\,\mathrm{gi}\,V\,\nu\,\mu\,x \;:=\; \href{/browser/qiqth-curvature#d-qiqth-curvature-pd}{\partial_{{\nu}}({\lambda y \mapsto V\,y\,\mu})({x})} + \sum_{\sigma} \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\mu}}_{{\nu}{\sigma}}({x})} \cdot V\,x\,\sigma

Used by qiqt_gr_freefield_complete, qiqt_gr_freefield_complete_covCong, qiqt_gr_freefield_localized', qiqt_gr_freefield_nullEnergy, qiqt_gr_freefield_geom, qiqt_gr_freefield_gaussian, qiqt_gr_ppwave, qiqt_gr_ppwave_showcase, and 15 more.

Definition 41 (covDeriv02). source ↗

Covariant derivative of a (0,2) tensor T_{μρ}: ∇_ν T_{μρ} = ∂_ν T_{μρ} − Γ^σ_{νμ} T_{σρ} − Γ^σ_{νρ} T_{μσ}.

Used by metric_compat, covDerivRiem_contract, covDerivRiem_contract', second_bianchi_contracted, inv_metric_compat, lowered_riemann_eq, lowered_riemann_antisymm, gi_trace_covDeriv_ricci, and 9 more.

Definition 42 (covDeriv20). source ↗

Covariant derivative of a (2,0) tensor T^{μρ}: ∇_ν T^{μρ} = ∂_ν T^{μρ} + Γ^μ_{νκ} T^{κρ} + Γ^ρ_{νκ} T^{μκ}.

Used by inv_metric_compat, gi_trace_covDeriv_ricci, gi_trace_covDerivRiem, gi_trace_covDerivRiem_ricci.

Lemma 43 (inv_contract). source ↗

Inverse-metric contraction. For gi a right-inverse of the (symmetric) metric g at x, lowering an upper index then contracting returns the original: ∑σ g_{σν} (∑α g^{σα} w_α) = w_ν.

(\forall (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}) (a b : \mathrm{Fin}\,n), g_{{a}{b}}({y}) = g_{{b}{a}}({y})) \to \forall (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}), (\forall (a b : \mathrm{Fin}\,n), \sum_{\sigma} g_{{a}{\sigma}}({x}) \cdot g^{{\sigma}{b}}({x}) = \delta_{ab}) \to \forall (\nu : \mathrm{Fin}\,n) (w : \mathrm{Fin}\,n \to \mathbb{R}), \sum_{\sigma} g_{{\sigma}{\nu}}({x}) \cdot \sum_{\alpha} g^{{\sigma}{\alpha}}({x}) \cdot w\,\alpha = w\,\nu

Proof. Immediate from the definitions. $\square$

Used by christoffel_lower.

Lemma 44 (christoffel_lower). source ↗

Lowered Christoffel symbol Γ_{νλμ} = ∑σ g_{σν} Γ^σ_{λμ} = ½(∂_λ g_{νμ} + ∂_μ g_{νλ} − ∂_ν g_{λμ}) — the inverse metric in Γ is cancelled by the lowering, via inv_contract.

(\forall (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}) (a b : \mathrm{Fin}\,n), g_{{a}{b}}({y}) = g_{{b}{a}}({y})) \to \forall (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}), (\forall (a b : \mathrm{Fin}\,n), \sum_{\sigma} g_{{a}{\sigma}}({x}) \cdot g^{{\sigma}{b}}({x}) = \delta_{ab}) \to \forall (\nu \lambda \mathrm{mu} : \mathrm{Fin}\,n), \sum_{\sigma} g_{{\sigma}{\nu}}({x}) \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\sigma}}_{{\lambda}{\mathrm{mu}}}({x})} = 1/2 \cdot (\href{/browser/qiqth-curvature#d-qiqth-curvature-pd}{\partial_{{\lambda}}({\lambda y \mapsto g_{{\nu}{\mathrm{mu}}}({y})})({x})} + \href{/browser/qiqth-curvature#d-qiqth-curvature-pd}{\partial_{{\mathrm{mu}}}({\lambda y \mapsto g_{{\nu}{\lambda}}({y})})({x})} - \href{/browser/qiqth-curvature#d-qiqth-curvature-pd}{\partial_{{\nu}}({\lambda y \mapsto g_{{\lambda}{\mathrm{mu}}}({y})})({x})})

Proof. By inv_contract. $\square$

Used by metric_compat.

Lemma 45 (metric_compat). source ↗

Metric compatibility ∇_λ g_{μν} = 0 — the defining property of the Levi-Civita connection, now a THEOREM from the Christoffel definition (via christoffel_lower) + metric symmetry. (Needs only that gi is the inverse and g is symmetric — no smoothness, since ∇g is algebraic in the ∂g.)

(\forall (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}) (a b : \mathrm{Fin}\,n), g_{{a}{b}}({y}) = g_{{b}{a}}({y})) \to \forall (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}), (\forall (a b : \mathrm{Fin}\,n), \sum_{\sigma} g_{{a}{\sigma}}({x}) \cdot g^{{\sigma}{b}}({x}) = \delta_{ab}) \to \forall (\lambda \mathrm{mu} \nu : \mathrm{Fin}\,n), \href{/browser/qiqth-curvature#d-qiqth-curvature-covderiv02}{\nabla^{2}}\,g\,\mathrm{gi}\,g\,\lambda\,\mathrm{mu}\,\nu\,x = 0

Proof. By pd, christoffel, christoffel_lower. $\square$

Used by inv_metric_compat, lowered_riemann_eq, lowered_riemann_antisymm, div02_scalar_metric, pd_g_eq.

Lemma 46 (riemann_first_bianchi). source ↗

First Bianchi identity (the algebraic/cyclic one): R^ρ_{σμν} + R^ρ_{μνσ} + R^ρ_{νσμ} = 0, for the torsion-free (Levi-Civita) connection. Purely algebraic — the derivative terms cancel pairwise by Christoffel lower-symmetry (no Schwarz / mixed partials needed), and the quadratic ΓΓ sums cancel termwise.

(\forall (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}) (a b : \mathrm{Fin}\,n), g_{{a}{b}}({y}) = g_{{b}{a}}({y})) \to \forall (\rho \sigma \mu \nu : \mathrm{Fin}\,n) (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}), \href{/browser/qiqth-curvature#d-qiqth-curvature-riemann}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\rho\,\sigma\,\mu\,\nu\,x + \href{/browser/qiqth-curvature#d-qiqth-curvature-riemann}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\rho\,\mu\,\nu\,\sigma\,x + \href{/browser/qiqth-curvature#d-qiqth-curvature-riemann}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\rho\,\nu\,\sigma\,\mu\,x = 0

Proof. By pd, christoffel, christoffel_symm. $\square$

Used by lowered_riemann_pair_symm.

Definition 47 (riemannLin). source ↗

The derivative (“principal”) part of the Riemann tensor — ∂_μ Γ^ρ_{νσ} − ∂_ν Γ^ρ_{μσ}, the part of R^ρ_{σμν} linear in ∂Γ (the ΓΓ part dropped).

\mathrm{Riem}\,n\,g\,\mathrm{gi}\,\rho\,\sigma\,\mu\,\nu\,x \;:=\; \partial_{{\mu}}({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\rho}}_{{\nu}{\sigma}}({y})}})({x}) - \partial_{{\nu}}({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\rho}}_{{\mu}{\sigma}}({y})}})({x})

Used by second_bianchi_deriv_part, bianchi_dGamma, second_bianchi.

Lemma 48 (second_bianchi_deriv_part). source ↗

The derivative part of the second Bianchi cyclic sum vanishes — ∂_λ Rlin^ρ_{σμν} + ∂_μ Rlin^ρ_{σνλ} + ∂_ν Rlin^ρ_{σλμ} = 0 for smooth Christoffel symbols. This is the part of the second Bianchi identity that the SCHWARZ keystone (pd_comm) handles: the six second-derivative ∂∂Γ terms cancel in pairs once mixed partials commute. (The full second Bianchi additionally needs the ΓΓ / Γ·R terms to cancel via the first Bianchi + Christoffel symmetry — the long general-coordinate remainder; see note 51.)

(\forall (a b c : \mathrm{Fin}\,n), ({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{a}}_{{b}{c}}({y})}})\in C^{\infty}) \to \partial_{{\lambda}}({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-riemannlin}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\rho\,\sigma\,\mathrm{mu}\,\nu\,y})({x}) + \partial_{{\mathrm{mu}}}({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-riemannlin}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\rho\,\sigma\,\nu\,\lambda\,y})({x}) + \partial_{{\nu}}({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-riemannlin}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\rho\,\sigma\,\lambda\,\mathrm{mu}\,y})({x}) = 0

Proof. By PdiffAt, pd_sub, pd_eq_fderiv, pd_comm. $\square$

Used by second_bianchi.

Lemma 49 (bianchi_extra_terms). source ↗

The “extra” lower-index connection terms cancel under the cyclic sum. ∇R (as a (1,3) tensor) has four Γ·R terms; the curvature-2-form DF=0 proof needs only the two acting on the ρ,σ matrix indices. The other two (acting on the antisymmetric form indices μ,ν) cancel cyclically, by Christoffel symmetry + Riemann antisymmetry — reducing the second Bianchi to the clean matrix-form DF=0.

(\forall (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}) (a b : \mathrm{Fin}\,n), g_{{a}{b}}({y}) = g_{{b}{a}}({y})) \to \forall (\rho \sigma \lambda \mathrm{mu} \nu : \mathrm{Fin}\,n) (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}), \sum_{\kappa} \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\kappa}}_{{\lambda}{\mathrm{mu}}}({x})} \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-riemann}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\rho\,\sigma\,\kappa\,\nu\,x + \sum_{\kappa} \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\kappa}}_{{\lambda}{\nu}}({x})} \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-riemann}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\rho\,\sigma\,\mathrm{mu}\,\kappa\,x + \sum_{\kappa} \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\kappa}}_{{\mathrm{mu}}{\nu}}({x})} \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-riemann}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\rho\,\sigma\,\kappa\,\lambda\,x + \sum_{\kappa} \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\kappa}}_{{\mathrm{mu}}{\lambda}}({x})} \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-riemann}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\rho\,\sigma\,\nu\,\kappa\,x + \sum_{\kappa} \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\kappa}}_{{\nu}{\lambda}}({x})} \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-riemann}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\rho\,\sigma\,\kappa\,\mathrm{mu}\,x + \sum_{\kappa} \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\kappa}}_{{\nu}{\mathrm{mu}}}({x})} \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-riemann}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\rho\,\sigma\,\lambda\,\kappa\,x = 0

Proof. By christoffel_symm, riemann_antisymm. $\square$

Used by second_bianchi.

Definition 50 (riemannQuad). source ↗

The quadratic (ΓΓ) part of the Riemann tensor: R^ρ_{σμν}|_quad = ∑_l (Γ^ρ_{μl}Γ^l_{νσ} − Γ^ρ_{νl}Γ^l_{μσ}). As a matrix in the (ρ,σ) indices this is the commutator [Γ_μ, Γ_ν].

Used by bianchi_GGG, pd_riemannQuad, bianchi_dGamma, second_bianchi.

Lemma 51 (bianchi_GGG). source ↗

The ΓΓΓ part of the second Bianchi cyclic sum vanishes — the Jacobi identity. In the matrix-form DF=0, the cubic part is ∑_cyclic [Γ_λ, [Γ_μ, Γ_ν]] = 0 (Jacobi). In components every matrix triple-product appears once with each sign, matched pairwise by a single κ ↔ e swap of the two contracted indices (Finset.sum_comm) — no Christoffel symmetry needed.

\sum_{\kappa} \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\rho}}_{{\lambda}{\kappa}}({x})} \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-riemannquad}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\kappa\,\sigma\,\mathrm{mu}\,\nu\,x - \sum_{\kappa} \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\kappa}}_{{\lambda}{\sigma}}({x})} \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-riemannquad}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\rho\,\kappa\,\mathrm{mu}\,\nu\,x + (\sum_{\kappa} \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\rho}}_{{\mathrm{mu}}{\kappa}}({x})} \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-riemannquad}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\kappa\,\sigma\,\nu\,\lambda\,x - \sum_{\kappa} \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\kappa}}_{{\mathrm{mu}}{\sigma}}({x})} \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-riemannquad}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\rho\,\kappa\,\nu\,\lambda\,x) + (\sum_{\kappa} \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\rho}}_{{\nu}{\kappa}}({x})} \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-riemannquad}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\kappa\,\sigma\,\lambda\,\mathrm{mu}\,x - \sum_{\kappa} \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\kappa}}_{{\nu}{\sigma}}({x})} \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-riemannquad}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\rho\,\kappa\,\lambda\,\mathrm{mu}\,x) = 0

Proof. Immediate from the definitions. $\square$

Used by second_bianchi.

Lemma 52 (pd_riemannQuad). source ↗

Expansion of ∂_λ (R_quad)^ρ_{σμν} via pd_sum + Leibniz: the ∑_l (∂Γ·Γ + Γ·∂Γ) terms.

(\forall (a b c : \mathrm{Fin}\,n), ({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{a}}_{{b}{c}}({y})}})\in C^{\infty}) \to \forall (\lambda \rho \sigma \mu \nu : \mathrm{Fin}\,n) (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}), \partial_{{\lambda}}({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-riemannquad}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\rho\,\sigma\,\mu\,\nu\,y})({x}) = \sum_{l} (\partial_{{\lambda}}({\lambda w \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\rho}}_{{\mu}{l}}({w})}})({x}) \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{l}}_{{\nu}{\sigma}}({x})} + \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\rho}}_{{\mu}{l}}({x})} \cdot \partial_{{\lambda}}({\lambda w \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{l}}_{{\nu}{\sigma}}({w})}})({x}) - \partial_{{\lambda}}({\lambda w \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\rho}}_{{\nu}{l}}({w})}})({x}) \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{l}}_{{\mu}{\sigma}}({x})} - \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\rho}}_{{\nu}{l}}({x})} \cdot \partial_{{\lambda}}({\lambda w \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{l}}_{{\mu}{\sigma}}({w})}})({x}))

Proof. By PdiffAt, pd_sub, PdiffAt_of_contDiff, mul, sub, pd_sum, pd_mul. $\square$

Used by bianchi_dGamma.

Lemma 53 (bianchi_dGamma). source ↗

The ∂Γ·Γ part of the second Bianchi cyclic sum vanishes. The first-derivative-of-Γ terms come from two places — the Leibniz derivative of R_quad (pd_riemannQuad) and the linear part of the Γ·R terms (Γ·R_lin). Under the cyclic sum they cancel as identical sums up to renaming the contracted index (no Christoffel symmetry, no index swap) — closed by ring.

(\forall (a b c : \mathrm{Fin}\,n), ({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{a}}_{{b}{c}}({y})}})\in C^{\infty}) \to \forall (\rho \sigma \lambda \mathrm{mu} \nu : \mathrm{Fin}\,n) (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}), \partial_{{\lambda}}({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-riemannquad}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\rho\,\sigma\,\mathrm{mu}\,\nu\,y})({x}) + \sum_{\kappa} \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\rho}}_{{\lambda}{\kappa}}({x})} \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-riemannlin}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\kappa\,\sigma\,\mathrm{mu}\,\nu\,x - \sum_{\kappa} \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\kappa}}_{{\lambda}{\sigma}}({x})} \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-riemannlin}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\rho\,\kappa\,\mathrm{mu}\,\nu\,x + (\partial_{{\mathrm{mu}}}({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-riemannquad}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\rho\,\sigma\,\nu\,\lambda\,y})({x}) + \sum_{\kappa} \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\rho}}_{{\mathrm{mu}}{\kappa}}({x})} \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-riemannlin}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\kappa\,\sigma\,\nu\,\lambda\,x - \sum_{\kappa} \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\kappa}}_{{\mathrm{mu}}{\sigma}}({x})} \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-riemannlin}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\rho\,\kappa\,\nu\,\lambda\,x) + (\partial_{{\nu}}({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-riemannquad}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\rho\,\sigma\,\lambda\,\mathrm{mu}\,y})({x}) + \sum_{\kappa} \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\rho}}_{{\nu}{\kappa}}({x})} \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-riemannlin}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\kappa\,\sigma\,\lambda\,\mathrm{mu}\,x - \sum_{\kappa} \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\kappa}}_{{\nu}{\sigma}}({x})} \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-riemannlin}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\rho\,\kappa\,\lambda\,\mathrm{mu}\,x) = 0

Proof. By pd_riemannQuad. $\square$

Used by second_bianchi.

Definition 54 (covDerivRiem). source ↗

Covariant derivative of the (1,3) Riemann tensor ∇_λ R^ρ_{σμν} = ∂_λ R^ρ_{σμν} + Γ^ρ_{λκ}R^κ_{σμν} − Γ^κ_{λσ}R^ρ_{κμν} − Γ^κ_{λμ}R^ρ_{σκν} − Γ^κ_{λν}R^ρ_{σμκ}.

Used by second_bianchi, covDerivRiem_contract, covDerivRiem_antisymm, covDerivRiem_contract', second_bianchi_contracted, gi_trace_covDerivRiem, gi_trace_covDerivRiem_ricci, divRiemann_trace_eq, and 1 more.

Lemma 55 (second_bianchi). source ↗

The second Bianchi identity (differential Bianchi): for the Levi-Civita connection of a smooth metric, the cyclic sum of covariant derivatives of the Riemann tensor vanishes, ∇_λ R^ρ_{σμν} + ∇_μ R^ρ_{σνλ} + ∇_ν R^ρ_{σλμ} = 0. Proved by decomposing each ∇R into four pieces — ∂∂Γ (cancels via Schwarz, second_bianchi_deriv_part), ∂Γ·Γ (bianchi_dGamma), the cubic ΓΓΓ/Jacobi part (bianchi_GGG), and the lower-index “extra” terms (bianchi_extra_terms) — each of whose cyclic sum is zero. This is the conservation identity behind ∇^μ G_{μν}=0 (Jacobson’s contracted-Bianchi step). Established mathematics, here machine-checked component-level and axiom-free.

(\forall (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}) (a b : \mathrm{Fin}\,n), g_{{a}{b}}({y}) = g_{{b}{a}}({y})) \to (\forall (a b c : \mathrm{Fin}\,n), ({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{a}}_{{b}{c}}({y})}})\in C^{\infty}) \to \forall (\rho \sigma \lambda \mathrm{mu} \nu : \mathrm{Fin}\,n) (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}), \href{/browser/qiqth-curvature#d-qiqth-curvature-covderivriem}{\nabla\mathrm{Riem}}\,g\,\mathrm{gi}\,\lambda\,\rho\,\sigma\,\mathrm{mu}\,\nu\,x + \href{/browser/qiqth-curvature#d-qiqth-curvature-covderivriem}{\nabla\mathrm{Riem}}\,g\,\mathrm{gi}\,\mathrm{mu}\,\rho\,\sigma\,\nu\,\lambda\,x + \href{/browser/qiqth-curvature#d-qiqth-curvature-covderivriem}{\nabla\mathrm{Riem}}\,g\,\mathrm{gi}\,\nu\,\rho\,\sigma\,\lambda\,\mathrm{mu}\,x = 0

Proof. By pd, PdiffAt, pd_add, PdiffAt_of_contDiff, mul, sub, PdiffAt_sum, PdiffAt_pd, riemann, riemannLin, second_bianchi_deriv_part, bianchi_extra_terms, riemannQuad, bianchi_GGG, bianchi_dGamma. $\square$

Used by second_bianchi_contracted.

Lemma 56 (PdiffAt_riemann). source ↗

R^ρ_{σμν} is partially differentiable in any direction (Γ smooth).

(\forall (a b c : \mathrm{Fin}\,n), ({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{a}}_{{b}{c}}({y})}})\in C^{\infty}) \to \forall (\rho \sigma \mu \nu \lambda : \mathrm{Fin}\,n) (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}), \href{/browser/qiqth-curvature#d-qiqth-curvature-pdiffat}{\mathrm{PdiffAt}}\,(\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-riemann}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\rho\,\sigma\,\mu\,\nu\,y)\,\lambda\,x

Proof. By pd, PdiffAt_of_contDiff, mul, sub, add, PdiffAt_sum, PdiffAt_pd. $\square$

Used by covDerivRiem_contract, covDerivRiem_antisymm, PdiffAt_ricci, gi_trace_covDerivRiem.

Lemma 57 (covDerivRiem_contract). source ↗

The covariant derivative commutes with contraction (the (ρ,μ)-trace giving Ricci): ∑_ρ ∇_λ R^ρ_{σρν} = ∇_λ R_{σν}. The connection corrections for the contracted index pair cancel (Finset.sum_comm), and the remaining two assemble into the (0,2) covariant derivative of Ric. The key step that turns the second Bianchi into the contracted Bianchi ∇^μ G_{μν}=0.

(\forall (a b c : \mathrm{Fin}\,n), ({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{a}}_{{b}{c}}({y})}})\in C^{\infty}) \to \forall (\lambda \sigma \nu : \mathrm{Fin}\,n) (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}), \sum_{\rho} \href{/browser/qiqth-curvature#d-qiqth-curvature-covderivriem}{\nabla\mathrm{Riem}}\,g\,\mathrm{gi}\,\lambda\,\rho\,\sigma\,\rho\,\nu\,x = \href{/browser/qiqth-curvature#d-qiqth-curvature-covderiv02}{\nabla^{2}}\,g\,\mathrm{gi}\,(\lambda y a b \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-ricci}{R_{{a}{b}}({y})})\,\lambda\,\sigma\,\nu\,x

Proof. By pd, pd_sum, riemann, PdiffAt_riemann. $\square$

Used by covDerivRiem_contract', second_bianchi_contracted.

Lemma 58 (covDerivRiem_antisymm). source ↗

∇R inherits Riemann’s antisymmetry in the last two indices: ∇_λ R^ρ_{σμν} + ∇_λ R^ρ_{σνμ} = 0. Each of the five constituent terms pairs off via riemann_antisymm (the ∂∂ term via pd_const_mul).

(\forall (a b c : \mathrm{Fin}\,n), ({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{a}}_{{b}{c}}({y})}})\in C^{\infty}) \to \forall (\lambda \rho \sigma \mu \nu : \mathrm{Fin}\,n) (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}), \href{/browser/qiqth-curvature#d-qiqth-curvature-covderivriem}{\nabla\mathrm{Riem}}\,g\,\mathrm{gi}\,\lambda\,\rho\,\sigma\,\mu\,\nu\,x + \href{/browser/qiqth-curvature#d-qiqth-curvature-covderivriem}{\nabla\mathrm{Riem}}\,g\,\mathrm{gi}\,\lambda\,\rho\,\sigma\,\nu\,\mu\,x = 0

Proof. By pd, pd_const_mul, riemann, riemann_antisymm, PdiffAt_riemann. $\square$

Used by covDerivRiem_contract'.

Lemma 59 (covDerivRiem_contract'). source ↗

The Ricci trace via the other contraction (antisymmetry): ∑_ρ R^ρ_{σμρ} = −R_{σμ}. Helper not needed standalone — folded into the (ρ,ν)-slot contraction below.

(\forall (a b c : \mathrm{Fin}\,n), ({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{a}}_{{b}{c}}({y})}})\in C^{\infty}) \to \forall (\mathrm{dir} \sigma \mu : \mathrm{Fin}\,n) (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}), \sum_{\rho} \href{/browser/qiqth-curvature#d-qiqth-curvature-covderivriem}{\nabla\mathrm{Riem}}\,g\,\mathrm{gi}\,\mathrm{dir}\,\rho\,\sigma\,\mu\,\rho\,x = -\href{/browser/qiqth-curvature#d-qiqth-curvature-covderiv02}{\nabla^{2}}\,g\,\mathrm{gi}\,(\lambda y a b \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-ricci}{R_{{a}{b}}({y})})\,\mathrm{dir}\,\sigma\,\mu\,x

Proof. By covDerivRiem_contract, covDerivRiem_antisymm. $\square$

Used by second_bianchi_contracted.

Lemma 60 (second_bianchi_contracted). source ↗

The once-contracted (second) Bianchi identity ∇_λ R_{σν} − ∇_ν R_{σλ} + ∇_ρ R^ρ_{σνλ} = 0, obtained by tracing the second Bianchi over (ρ,μ) (covDerivRiem_contract/'). The remaining divergence term ∑_ρ ∇_ρ R^ρ_{σνλ} is the Riemann divergence; contracting once more with g^{μν} yields ∇^μ G_{μν}=0. Established mathematics, machine-checked component-level and axiom-free.

(\forall (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}) (a b : \mathrm{Fin}\,n), g_{{a}{b}}({y}) = g_{{b}{a}}({y})) \to (\forall (a b c : \mathrm{Fin}\,n), ({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{a}}_{{b}{c}}({y})}})\in C^{\infty}) \to \forall (\lambda \sigma \nu : \mathrm{Fin}\,n) (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}), \href{/browser/qiqth-curvature#d-qiqth-curvature-covderiv02}{\nabla^{2}}\,g\,\mathrm{gi}\,(\lambda y a b \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-ricci}{R_{{a}{b}}({y})})\,\lambda\,\sigma\,\nu\,x - \href{/browser/qiqth-curvature#d-qiqth-curvature-covderiv02}{\nabla^{2}}\,g\,\mathrm{gi}\,(\lambda y a b \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-ricci}{R_{{a}{b}}({y})})\,\nu\,\sigma\,\lambda\,x + \sum_{\rho} \href{/browser/qiqth-curvature#d-qiqth-curvature-covderivriem}{\nabla\mathrm{Riem}}\,g\,\mathrm{gi}\,\rho\,\rho\,\sigma\,\nu\,\lambda\,x = 0

Proof. By second_bianchi, covDerivRiem_contract, covDerivRiem_contract'. $\square$

Used by twice_contracted_bianchi.

Lemma 61 (inv_metric_compat). source ↗

Inverse-metric covariant constancy ∇_λ g^{μρ} = 0 — the raised-index companion of metric_compat. Derived by differentiating the inverse relation ∑_σ g_{aσ}g^{σb}=δ (so ∑_σ g_{aσ}∂_λ g^{σρ} = −∑_σ (∂_λ g_{aσ})g^{σρ}), substituting ∂g from metric_compat, and cancelling the connection terms; the contraction with g is then removed by invertibility. The tool that lets the metric pass through ∇ in the g^{μν}-contractions of ∇^μ G_{μν}=0.

(\forall (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}) (a b : \mathrm{Fin}\,n), g_{{a}{b}}({y}) = g_{{b}{a}}({y})) \to (\forall (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}) (a b : \mathrm{Fin}\,n), g^{{a}{b}}({y}) = g^{{b}{a}}({y})) \to (\forall (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}) (a b : \mathrm{Fin}\,n), \sum_{\sigma} g_{{a}{\sigma}}({y}) \cdot g^{{\sigma}{b}}({y}) = \delta_{ab}) \to \forall (\lambda : \mathrm{Fin}\,n) (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}), (\forall (a b : \mathrm{Fin}\,n), \href{/browser/qiqth-curvature#d-qiqth-curvature-pdiffat}{\mathrm{PdiffAt}}\,(\lambda y \mapsto g_{{a}{b}}({y}))\,\lambda\,x) \to (\forall (a b : \mathrm{Fin}\,n), \href{/browser/qiqth-curvature#d-qiqth-curvature-pdiffat}{\mathrm{PdiffAt}}\,(\lambda y \mapsto g^{{a}{b}}({y}))\,\lambda\,x) \to \forall (\mu \rho : \mathrm{Fin}\,n), \href{/browser/qiqth-curvature#d-qiqth-curvature-covderiv20}{\nabla^{2}}\,g\,\mathrm{gi}\,\mathrm{gi}\,\lambda\,\mu\,\rho\,x = 0

Proof. By pd, pd_const, mul, pd_sum, pd_mul, christoffel, covDeriv02, metric_compat. $\square$

Used by gi_trace_covDeriv_ricci, gi_trace_covDerivRiem, gi_trace_covDerivRiem_ricci.

Lemma 62 (lowered_riemann_eq). source ↗

Riemann in terms of the metric (lowered first index): g_{ρα} R^α_{σμν} equals ∂_μ Γ_{ρνσ} − ∂_ν Γ_{ρμσ} − Γ^κ_{μρ}Γ_{κνσ} + Γ^κ_{νρ}Γ_{κμσ}, where Γ_{ρνσ}=∑_α g_{ρα}Γ^α_{νσ} is the lowered Christoffel (written here as the contraction g_{ακ} for the connection terms). The g·ΓΓ terms produced by differentiating g (metric_compat) cancel the Riemann ΓΓ terms.

(\forall (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}) (a b : \mathrm{Fin}\,n), g_{{a}{b}}({y}) = g_{{b}{a}}({y})) \to (\forall (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}) (a b : \mathrm{Fin}\,n), \sum_{\sigma} g_{{a}{\sigma}}({y}) \cdot g^{{\sigma}{b}}({y}) = \delta_{ab}) \to (\forall (a b : \mathrm{Fin}\,n), ({\lambda y \mapsto g_{{a}{b}}({y})})\in C^{\infty}) \to (\forall (a b c : \mathrm{Fin}\,n), ({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{a}}_{{b}{c}}({y})}})\in C^{\infty}) \to \forall (\rho \sigma \mu \nu : \mathrm{Fin}\,n) (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}), \sum_{\alpha} g_{{\rho}{\alpha}}({x}) \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-riemann}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\alpha\,\sigma\,\mu\,\nu\,x = \partial_{{\mu}}({\lambda y \mapsto \sum_{\alpha} g_{{\rho}{\alpha}}({y}) \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\alpha}}_{{\nu}{\sigma}}({y})}})({x}) - \partial_{{\nu}}({\lambda y \mapsto \sum_{\alpha} g_{{\rho}{\alpha}}({y}) \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\alpha}}_{{\mu}{\sigma}}({y})}})({x}) - \sum_{\kappa} \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\kappa}}_{{\mu}{\rho}}({x})} \cdot \sum_{\alpha} g_{{\alpha}{\kappa}}({x}) \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\alpha}}_{{\nu}{\sigma}}({x})} + \sum_{\kappa} \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\kappa}}_{{\nu}{\rho}}({x})} \cdot \sum_{\alpha} g_{{\alpha}{\kappa}}({x}) \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\alpha}}_{{\mu}{\sigma}}({x})}

Proof. By PdiffAt_of_contDiff, mul, pd_sum, pd_mul, covDeriv02, metric_compat. $\square$

Used by lowered_riemann_antisymm.

Lemma 63 (lowered_riemann_antisymm). source ↗

First-pair antisymmetry of the lowered Riemann tensor: g_{ρα}R^α_{σμν} + g_{σα}R^α_{ρμν} = 0, i.e. R_{ρσμν}=−R_{σρμν}. From lowered_riemann_eq: the ∂Γ_lower pairs combine (via metric_compat as a function identity) into ∂∂g_{ρσ} and cancel by Schwarz (pd_comm); the ΓΓ pairs cancel by the symmetry of ⟨ab,cd⟩=∑_{κα}g_{ακ}Γ^κ_{ab}Γ^α_{cd} under (ab)↔(cd). The crux of the metric-raising tower (piece B) — required for g^{σν}R^ρ_{σνλ} in ∇^μ G_{μν}=0.

(\forall (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}) (a b : \mathrm{Fin}\,n), g_{{a}{b}}({y}) = g_{{b}{a}}({y})) \to (\forall (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}) (a b : \mathrm{Fin}\,n), \sum_{\sigma} g_{{a}{\sigma}}({y}) \cdot g^{{\sigma}{b}}({y}) = \delta_{ab}) \to (\forall (a b : \mathrm{Fin}\,n), ({\lambda y \mapsto g_{{a}{b}}({y})})\in C^{\infty}) \to (\forall (a b c : \mathrm{Fin}\,n), ({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{a}}_{{b}{c}}({y})}})\in C^{\infty}) \to \forall (\rho \sigma \mu \nu : \mathrm{Fin}\,n) (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}), \sum_{\alpha} g_{{\rho}{\alpha}}({x}) \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-riemann}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\alpha\,\sigma\,\mu\,\nu\,x + \sum_{\alpha} g_{{\sigma}{\alpha}}({x}) \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-riemann}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\alpha\,\rho\,\mu\,\nu\,x = 0

Proof. By pd, PdiffAt, pd_add, PdiffAt_of_contDiff, mul, PdiffAt_sum, pd_comm, covDeriv02, metric_compat, lowered_riemann_eq. $\square$

Used by lowered_riemann_gi_trace, lowered_riemann_pair_symm.

Lemma 64 (lowered_riemann_gi_trace). source ↗

Metric trace of the lowered Riemann tensor → Ricci: ∑_{σν} g^{σν}(g_{βρ}R^ρ_{σνλ}) = −R_{βλ}. The contraction over the first two lower slots, via first-pair antisymmetry (lowered_riemann_antisymm) turns into the contraction over the (1,3)-Ricci slots, and the g^{σν}g_{σρ}=δ collapse reproduces ricci β λ = ∑_ν R^ν_{βνλ}. The core of metric-raising tower piece C (the contraction identity behind g^{σν}R^ρ_{σνλ} in ∇^μ G_{μν}=0).

(\forall (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}) (a b : \mathrm{Fin}\,n), g_{{a}{b}}({y}) = g_{{b}{a}}({y})) \to (\forall (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}) (a b : \mathrm{Fin}\,n), g^{{a}{b}}({y}) = g^{{b}{a}}({y})) \to (\forall (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}) (a b : \mathrm{Fin}\,n), \sum_{\sigma} g_{{a}{\sigma}}({y}) \cdot g^{{\sigma}{b}}({y}) = \delta_{ab}) \to (\forall (a b : \mathrm{Fin}\,n), ({\lambda y \mapsto g_{{a}{b}}({y})})\in C^{\infty}) \to (\forall (a b c : \mathrm{Fin}\,n), ({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{a}}_{{b}{c}}({y})}})\in C^{\infty}) \to \forall (\beta \lambda : \mathrm{Fin}\,n) (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}), \sum_{\sigma} \sum_{\nu} g^{{\sigma}{\nu}}({x}) \cdot \sum_{\rho} g_{{\beta}{\rho}}({x}) \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-riemann}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\rho\,\sigma\,\nu\,\lambda\,x = -\href{/browser/qiqth-curvature#d-qiqth-curvature-ricci}{R_{{\beta}{\lambda}}({x})}

Proof. By lowered_riemann_antisymm. $\square$

Used by ricci_gi_raise.

Lemma 65 (ricci_gi_raise). source ↗

Raised metric trace of Riemann → raised Ricci (metric-raising tower, piece C raised): ∑_{σν} g^{σν} R^ρ_{σνλ} = −∑_β g^{ρβ} Ric_{βλ}. Raises lowered_riemann_gi_trace through the g⁻¹·g = δ inversion.

(\forall (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}) (a b : \mathrm{Fin}\,n), g_{{a}{b}}({y}) = g_{{b}{a}}({y})) \to (\forall (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}) (a b : \mathrm{Fin}\,n), g^{{a}{b}}({y}) = g^{{b}{a}}({y})) \to (\forall (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}) (a b : \mathrm{Fin}\,n), \sum_{\sigma} g_{{a}{\sigma}}({y}) \cdot g^{{\sigma}{b}}({y}) = \delta_{ab}) \to (\forall (a b : \mathrm{Fin}\,n), ({\lambda y \mapsto g_{{a}{b}}({y})})\in C^{\infty}) \to (\forall (a b c : \mathrm{Fin}\,n), ({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{a}}_{{b}{c}}({y})}})\in C^{\infty}) \to \forall (\rho \lambda : \mathrm{Fin}\,n) (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}), \sum_{\sigma} \sum_{\nu} g^{{\sigma}{\nu}}({x}) \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-riemann}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\rho\,\sigma\,\nu\,\lambda\,x = -\sum_{\beta} g^{{\rho}{\beta}}({x}) \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-ricci}{R_{{\beta}{\lambda}}({x})}

Proof. By lowered_riemann_gi_trace. $\square$

Used by gi_trace_covDerivRiem_ricci.

Lemma 66 (PdiffAt_ricci). source ↗

Ric_{σν} is partially differentiable in any direction (Γ smooth).

(\forall (a b c : \mathrm{Fin}\,n), ({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{a}}_{{b}{c}}({y})}})\in C^{\infty}) \to \forall (\sigma \nu \lambda : \mathrm{Fin}\,n) (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}), \href{/browser/qiqth-curvature#d-qiqth-curvature-pdiffat}{\mathrm{PdiffAt}}\,(\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-ricci}{R_{{\sigma}{\nu}}({y})})\,\lambda\,x

Proof. By PdiffAt_sum, riemann, PdiffAt_riemann. $\square$

Used by gi_trace_covDeriv_ricci, gi_trace_covDerivRiem_ricci, einstein_field_equation_real.

Lemma 67 (gi_trace_covDeriv_ricci). source ↗

T1 of the twice-contracted Bianchi — the scalar-curvature derivative: ∑_{σν} g^{σν} ∇_λ Ric_{σν} = ∂_λ R. Product rule on R = ∑g^{σν}Ric_{σν} (pd_sum+pd_mul) plus inv_metric_compat (∂g^{σν} = −Γg−Γg) cancels the connection terms by index swaps.

(\forall (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}) (a b : \mathrm{Fin}\,n), g_{{a}{b}}({y}) = g_{{b}{a}}({y})) \to (\forall (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}) (a b : \mathrm{Fin}\,n), g^{{a}{b}}({y}) = g^{{b}{a}}({y})) \to (\forall (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}) (a b : \mathrm{Fin}\,n), \sum_{\sigma} g_{{a}{\sigma}}({y}) \cdot g^{{\sigma}{b}}({y}) = \delta_{ab}) \to (\forall (a b : \mathrm{Fin}\,n), ({\lambda y \mapsto g_{{a}{b}}({y})})\in C^{\infty}) \to (\forall (a b : \mathrm{Fin}\,n), ({\lambda y \mapsto g^{{a}{b}}({y})})\in C^{\infty}) \to (\forall (a b c : \mathrm{Fin}\,n), ({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{a}}_{{b}{c}}({y})}})\in C^{\infty}) \to \forall (\lambda : \mathrm{Fin}\,n) (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}), \sum_{\sigma} \sum_{\nu} g^{{\sigma}{\nu}}({x}) \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-covderiv02}{\nabla^{2}}\,g\,\mathrm{gi}\,(\lambda y a b \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-ricci}{R_{{a}{b}}({y})})\,\lambda\,\sigma\,\nu\,x = \partial_{{\lambda}}({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-scalarcurv}{R({y})}})({x})

Proof. By PdiffAt, PdiffAt_of_contDiff, mul, PdiffAt_sum, pd_sum, pd_mul, covDeriv20, inv_metric_compat, PdiffAt_ricci. $\square$

Used by twice_contracted_bianchi.

Lemma 68 (gi_trace_covDerivRiem). source ↗

T3 core — contraction commutes with the Riemann divergence: for fixed ρ, ∑_{σν} g^{σν} ∇_ρ R^ρ_{σνλ} equals ∂_ρ S^ρ_λ + Γ^ρ_{ρκ}S^κ_λ − Γ^κ_{ρλ}S^ρ_κ, the (1,1) covariant divergence of S^a_b := ∑_{σν} g^{σν} R^a_{σνb} — the σ,ν connection corrections of covDerivRiem cancel ∂g^{σν} (inv_metric_compat) by the same swaps as T1.

(\forall (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}) (a b : \mathrm{Fin}\,n), g_{{a}{b}}({y}) = g_{{b}{a}}({y})) \to (\forall (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}) (a b : \mathrm{Fin}\,n), g^{{a}{b}}({y}) = g^{{b}{a}}({y})) \to (\forall (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}) (a b : \mathrm{Fin}\,n), \sum_{\sigma} g_{{a}{\sigma}}({y}) \cdot g^{{\sigma}{b}}({y}) = \delta_{ab}) \to (\forall (a b : \mathrm{Fin}\,n), ({\lambda y \mapsto g_{{a}{b}}({y})})\in C^{\infty}) \to (\forall (a b : \mathrm{Fin}\,n), ({\lambda y \mapsto g^{{a}{b}}({y})})\in C^{\infty}) \to (\forall (a b c : \mathrm{Fin}\,n), ({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{a}}_{{b}{c}}({y})}})\in C^{\infty}) \to \forall (\rho \lambda : \mathrm{Fin}\,n) (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}), \sum_{\sigma} \sum_{\nu} g^{{\sigma}{\nu}}({x}) \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-covderivriem}{\nabla\mathrm{Riem}}\,g\,\mathrm{gi}\,\rho\,\rho\,\sigma\,\nu\,\lambda\,x = \partial_{{\rho}}({\lambda y \mapsto \sum_{\sigma} \sum_{\nu} g^{{\sigma}{\nu}}({y}) \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-riemann}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\rho\,\sigma\,\nu\,\lambda\,y})({x}) + \sum_{\sigma} \sum_{\nu} \sum_{\kappa} g^{{\sigma}{\nu}}({x}) \cdot (\href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\rho}}_{{\rho}{\kappa}}({x})} \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-riemann}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\kappa\,\sigma\,\nu\,\lambda\,x) - \sum_{\sigma} \sum_{\nu} \sum_{\kappa} g^{{\sigma}{\nu}}({x}) \cdot (\href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\kappa}}_{{\rho}{\lambda}}({x})} \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-riemann}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\rho\,\sigma\,\nu\,\kappa\,x)

Proof. By PdiffAt, PdiffAt_of_contDiff, mul, PdiffAt_sum, pd_sum, pd_mul, covDeriv20, PdiffAt_riemann, inv_metric_compat. $\square$

Used by gi_trace_covDerivRiem_ricci.

Lemma 69 (gi_trace_covDerivRiem_ricci). source ↗

T3 core with S substituted to −(raised Ricci) (via ricci_gi_raise): for fixed ρ, ∑_{σν} g^{σν} ∇_ρ R^ρ_{σνλ} = −∑_β g^{ρβ}∂_ρ Ric_{βλ} + ∑_{βκ} Γ^β_{ρκ}g^{ρκ}Ric_{βλ} + ∑_{βκ} Γ^κ_{ρλ}g^{ρβ}Ric_{βκ}. The Γ^ρ_{ρκ} terms from ∂g cancel the ∑Γ^ρ_{ρκ}S^κ spectator.

(\forall (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}) (a b : \mathrm{Fin}\,n), g_{{a}{b}}({y}) = g_{{b}{a}}({y})) \to (\forall (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}) (a b : \mathrm{Fin}\,n), g^{{a}{b}}({y}) = g^{{b}{a}}({y})) \to (\forall (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}) (a b : \mathrm{Fin}\,n), \sum_{\sigma} g_{{a}{\sigma}}({y}) \cdot g^{{\sigma}{b}}({y}) = \delta_{ab}) \to (\forall (a b : \mathrm{Fin}\,n), ({\lambda y \mapsto g_{{a}{b}}({y})})\in C^{\infty}) \to (\forall (a b : \mathrm{Fin}\,n), ({\lambda y \mapsto g^{{a}{b}}({y})})\in C^{\infty}) \to (\forall (a b c : \mathrm{Fin}\,n), ({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{a}}_{{b}{c}}({y})}})\in C^{\infty}) \to \forall (\rho \lambda : \mathrm{Fin}\,n) (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}), \sum_{\sigma} \sum_{\nu} g^{{\sigma}{\nu}}({x}) \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-covderivriem}{\nabla\mathrm{Riem}}\,g\,\mathrm{gi}\,\rho\,\rho\,\sigma\,\nu\,\lambda\,x = -\sum_{\beta} g^{{\rho}{\beta}}({x}) \cdot \partial_{{\rho}}({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-ricci}{R_{{\beta}{\lambda}}({y})}})({x}) + \sum_{\beta} \sum_{\kappa} \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\beta}}_{{\rho}{\kappa}}({x})} \cdot g^{{\rho}{\kappa}}({x}) \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-ricci}{R_{{\beta}{\lambda}}({x})} + \sum_{\beta} \sum_{\kappa} \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\kappa}}_{{\rho}{\lambda}}({x})} \cdot g^{{\rho}{\beta}}({x}) \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-ricci}{R_{{\beta}{\kappa}}({x})}

Proof. By PdiffAt, pd_const_mul, PdiffAt_of_contDiff, mul, PdiffAt_sum, pd_sum, pd_mul, riemann, covDeriv20, inv_metric_compat, ricci_gi_raise, PdiffAt_ricci, gi_trace_covDerivRiem. $\square$

Used by divRiemann_trace_eq.

Lemma 70 (const_of_pd_zero). source ↗

A field with vanishing partial derivatives everywhere is constant (on Point n = Fin n → ℝ, which is connected). All ∂ᵢ F = 0 ⇒ fderiv F = 0 (the partials span the differential) ⇒ F is constant by is_const_of_fderiv_eq_zero. Upgrades “covariantly constant at a point” to a genuine constant — e.g. the cosmological constant Λ.

\mathrm{Differentiable}\,\mathbb{R}\,F \to (\forall (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}) (\nu : \mathrm{Fin}\,n), \href{/browser/qiqth-curvature#d-qiqth-curvature-pd}{\partial_{{\nu}}({F})({x})} = 0) \to \forall (x y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{n}}}), F\,x = F\,y

Proof. By pd_eq_fderiv. $\square$

Used by einstein_field_equation_real_global.

← all sections · ← CoreNoCollapse · DifferentialAreaLaw →