Raychaudhuri · section of the QIQT-H book
QIQTH.Raychaudhuri
← all sections · ← QiqtToGR · RaychaudhuriCongruence →
Raychaudhuri · entries 564–574 of 1000
Definition 564 (covDeriv2Vec). source ↗
Second covariant derivative of a vector field, ∇_μ ∇_ν V^ρ. Treating W^ρ_ν := ∇_ν V^ρ (= covDerivVec) as a (1,1) tensor: ∇_μ W^ρ_ν = ∂_μ W^ρ_ν + Γ^ρ_{μσ} W^σ_ν − Γ^σ_{μν} W^ρ_σ.
Used by ricci_identity, ricci_identity_contracted, covDeriv2Vec_trace, raychaudhuri_focusing, geodesic_leibniz, raychaudhuri_geodesic.
Lemma 565 (pd_covDerivVec). source ↗
The partial derivative of ∇_ν V^ρ, expanded via the product rule: ∂_μ(∇_ν V^ρ) = ∂_μ∂_ν V^ρ + Σ_σ (∂_μ Γ^ρ_{νσ}) V^σ + Σ_σ Γ^ρ_{νσ} ∂_μ V^σ.
(∀(μ:Finn),(λy↦Vyμ)∈C∞)→(∀(abc:Finn),(λy↦Γbca(y))∈C∞)→∀(μνρ:Finn)(x:Mn),∂μ(λy↦(∇V)νρ(y))(x)=∂μ(λy↦∂ν(λz↦Vzρ)(y))(x)+σ∑(∂μ(λy↦Γνσρ(y))(x)⋅Vxσ+Γνσρ(x)⋅∂μ(λy↦Vyσ)(x))
Proof. By PdiffAt, pd_add, PdiffAt_of_contDiff, mul, PdiffAt_sum, pd_sum, pd_mul, PdiffAt_pd. □
Used by ricci_identity.
Lemma 566 (ricci_identity). source ↗
The Ricci identity — the commutator of covariant derivatives is the Riemann curvature: (∇_μ ∇_ν − ∇_ν ∇_μ) V^ρ = R^ρ_{σμν} V^σ. The geometric heart of Raychaudhuri focusing.
(∀(y:Mn)(ab:Finn),gab(y)=gba(y))→∀(V:Mn→Finn→R),(∀(μ:Finn),(λy↦Vyμ)∈C∞)→(∀(abc:Finn),(λy↦Γbca(y))∈C∞)→∀(μνρ:Finn)(x:Mn),∇2ggiVμνρx−∇2ggiVνμρx=σ∑Riemggiρσμνx⋅Vxσ
Proof. By pd, pd_comm, christoffel_symm, covDerivVec, pd_covDerivVec. □
Used by ricci_identity_contracted.
Lemma 567 (ricci_identity_contracted). source ↗
The contracted Ricci identity — tracing the commutator on the upper index (ρ = μ, summed) turns the Riemann tensor into the Ricci tensor: ∑_μ (∇_μ∇_ν − ∇_ν∇_μ) V^μ = R_{σν} V^σ. This is exactly the step that introduces the R_{μν} focusing term into the expansion evolution.
(∀(y:Mn)(ab:Finn),gab(y)=gba(y))→∀(V:Mn→Finn→R),(∀(μ:Finn),(λy↦Vyμ)∈C∞)→(∀(abc:Finn),(λy↦Γbca(y))∈C∞)→∀(ν:Finn)(x:Mn),μ∑(∇2ggiVμνμx−∇2ggiVνμμx)=σ∑Rσν(x)⋅Vxσ
Proof. By riemann, ricci_identity. □
Used by raychaudhuri_focusing.
Definition 568 (expansion). source ↗
The expansion θ = ∇_μ V^μ — the covariant divergence of a vector field.
expansionnggiVx:=μ∑(∇V)μμ(x)
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_freefield_thermo, and 8 more.
Lemma 569 (covDeriv2Vec_trace). source ↗
Covariant derivative commutes with contraction (the geodesic-direction Γ terms cancel by torsion-freeness): the trace ∑_μ ∇_ν ∇_μ V^μ is just the ordinary derivative of the expansion, ∂_ν θ. This is what turns ∇_ν(∇_μ V^μ) into ∂_ν θ in the Raychaudhuri derivation.
(∀(μ:Finn),(λy↦Vyμ)∈C∞)→(∀(abc:Finn),(λy↦Γbca(y))∈C∞)→∀(ν:Finn)(x:Mn),μ∑∇2ggiVνμμx=∂ν(λy↦θ(y))(x)
Proof. By PdiffAt, PdiffAt_of_contDiff, mul, add, PdiffAt_sum, pd_sum, PdiffAt_pd, covDerivVec. □
Used by raychaudhuri_focusing.
Lemma 570 (raychaudhuri_focusing). source ↗
The Raychaudhuri focusing equation. Contracting the (contracted) Ricci identity with V gives the evolution of the expansion θ along V, with the Ricci focusing term −R_{σν}V^σV^ν made explicit:
V^ν ∂_ν θ = Σ_{μν} V^ν ∇_μ∇_ν V^μ − R_{σν} V^σ V^ν.
This is Jacobson’s focusing step (the geometry of his front half). For a geodesic V (V^σ∇_σV^μ=0) the first right-hand term equals −(∇_μV^ν)(∇_νV^μ) (the −½θ²−σ² shear part); that geodesic simplification is the remaining (Leibniz) polish. Holds for any vector field.
(∀(y:Mn)(ab:Finn),gab(y)=gba(y))→∀(V:Mn→Finn→R),(∀(μ:Finn),(λy↦Vyμ)∈C∞)→(∀(abc:Finn),(λy↦Γbca(y))∈C∞)→∀(x:Mn),ν∑Vxν⋅∂ν(λy↦θ(y))(x)=ν∑μ∑Vxν⋅∇2ggiVμνμx−ν∑σ∑Rσν(x)⋅Vxσ⋅Vxν
Proof. By ricci_identity_contracted, covDeriv2Vec_trace. □
Used by raychaudhuri_geodesic.
Lemma 571 (geodesic_divergence_leibniz). source ↗
Partial-Leibniz of the geodesic acceleration. For a geodesic vector field V (Σ_ν V^ν ∇_ν V^μ = 0 as a field), the divergence of the acceleration vanishes, expanded by the product rule: Σ_ν (∂_μ V^ν · ∇_ν V^μ + V^ν · ∂_μ(∇_ν V^μ)) = 0. The step that lets Σ V^ν∇_μ∇_νV^μ be rewritten as −(∇_μV^ν)(∇_νV^μ) (the −½θ²−σ² shear part).
(∀(μ:Finn),(λy↦Vyμ)∈C∞)→(∀(abc:Finn),(λy↦Γbca(y))∈C∞)→(∀(y:Mn)(μ:Finn),ν∑Vyν⋅(∇V)νμ(y)=0)→∀(μ:Finn)(x:Mn),ν∑(∂μ(λy↦Vyν)(x)⋅(∇V)νμ(x)+Vxν⋅∂μ(λy↦(∇V)νμ(y))(x))=0
Proof. By PdiffAt, pd_const, PdiffAt_of_contDiff, mul, add, PdiffAt_sum, pd_sum, pd_mul, PdiffAt_pd. □
Used by geodesic_leibniz.
Lemma 572 (geodesic_leibniz). source ↗
Geodesic Leibniz identity. For a geodesic field V, the Raychaudhuri second-derivative term is the shear/expansion quadratic: Σ_{νμ} V^ν ∇_μ∇_ν V^μ = − Σ_{μν} (∇_μ V^ν)(∇_ν V^μ).
(∀(y:Mn)(ab:Finn),gab(y)=gba(y))→∀(V:Mn→Finn→R),(∀(μ:Finn),(λy↦Vyμ)∈C∞)→(∀(abc:Finn),(λy↦Γbca(y))∈C∞)→(∀(y:Mn)(μ:Finn),ν∑Vyν⋅(∇V)νμ(y)=0)→∀(x:Mn),ν∑μ∑Vxν⋅∇2ggiVμνμx=−μ∑ν∑(∇V)μν(x)⋅(∇V)νμ(x)
Proof. By pd, geodesic_divergence_leibniz. □
Used by raychaudhuri_geodesic.
Lemma 573 (raychaudhuri_geodesic). source ↗
The Raychaudhuri equation (geodesic congruence), in Jacobson’s exact form:
V^ν ∂_ν θ = − (∇_μ V^ν)(∇_ν V^μ) − R_{σν} V^σ V^ν.
The expansion θ of a geodesic congruence focuses, driven by the shear/expansion quadratic −(∇V)(∇V) (Jacobson’s −½θ²−σ², the term he neglects near a stationary horizon) and the Ricci focusing term −R(V,V) (the term he uses). Assembled from raychaudhuri_focusing and geodesic_leibniz. The full geometry of Jacobson’s front half is now machine-checked, axiom-free.
(∀(y:Mn)(ab:Finn),gab(y)=gba(y))→∀(V:Mn→Finn→R),(∀(μ:Finn),(λy↦Vyμ)∈C∞)→(∀(abc:Finn),(λy↦Γbca(y))∈C∞)→(∀(y:Mn)(μ:Finn),ν∑Vyν⋅(∇V)νμ(y)=0)→∀(x:Mn),ν∑Vxν⋅∂ν(λy↦θ(y))(x)=−μ∑ν∑(∇V)μν(x)⋅(∇V)νμ(x)−ν∑σ∑Rσν(x)⋅Vxσ⋅Vxν
Proof. By covDeriv2Vec, raychaudhuri_focusing, geodesic_leibniz. □
Used by raychaudhuri_focusing_at_equilibrium.
Lemma 574 (raychaudhuri_focusing_at_equilibrium). source ↗
Leading-order Raychaudhuri focusing at equilibrium — the geometric content of Jacobson’s hFocus. At a moment of local equilibrium (a stationary/bifurcation horizon, where the shear–expansion quadratic (∇_μV^ν)(∇_νV^μ) vanishes — θ = σ = ω = 0, the condition Jacobson imposes), the Raychaudhuri equation collapses to pure Ricci focusing:
V^ν ∂_ν θ = − R_{σν} V^σ V^ν (i.e. …
(∀(y:Mn)(ab:Finn),gab(y)=gba(y))→∀(V:Mn→Finn→R),(∀(μ:Finn),(λy↦Vyμ)∈C∞)→(∀(abc:Finn),(λy↦Γbca(y))∈C∞)→(∀(y:Mn)(μ:Finn),ν∑Vyν⋅(∇V)νμ(y)=0)→∀(x:Mn),μ∑ν∑(∇V)μν(x)⋅(∇V)νμ(x)=0→ν∑Vxν⋅∂ν(λy↦θ(y))(x)=−ν∑σ∑Rσν(x)⋅Vxσ⋅Vxν
Proof. By raychaudhuri_geodesic. □
Used by hFocus_of_raychaudhuri.
← all sections · ← QiqtToGR · RaychaudhuriCongruence →