QiqtToGR · section of the QIQT-H book

QIQTH.QiqtToGR

← all sections · ← QiqtGrThermo · Raychaudhuri →

QiqtToGR · entries 560–563 of 1000

Lemma 560 (hFocus_of_raychaudhuri). source ↗

The hFocus input DERIVED from the machine-checked Raychaudhuri equation — only the area↔θ modelling identification remains. hFocus (input #3 of qiqt_gr_from_wedge_kms) demands that the area first-variation rate ad equals the contracted Ricci R_kk = BL(Ric) v. Given the equilibrium condition hequil (the shear–expansion quadratic vanishes — a stationary/bifurcation horizon, Jacobson’s setup) and the single modelling identification harea (the abstract area rate is minus the congruence expansion rate −V^ν∂_νθ), raychaudhuri_focusing_at_equilibrium derives ad = R_kk. …

(\forall (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}}) (a b : \mathrm{Fin}\,4), g_{{a}{b}}({y}) = g_{{b}{a}}({y})) \to \forall (V : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}} \to \mathrm{Fin}\,4 \to \mathbb{R}), (\forall (\mu : \mathrm{Fin}\,4), ({\lambda y \mapsto V\,y\,\mu})\in C^{\infty}) \to (\forall (a b c : \mathrm{Fin}\,4), ({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{a}}_{{b}{c}}({y})}})\in C^{\infty}) \to (\forall (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}}) (\mu : \mathrm{Fin}\,4), \sum_{\nu} V\,y\,\nu \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-covderivvec}{(\nabla {V})_{{\nu}}{}^{{\mu}}({y})} = 0) \to \forall (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}}), \sum_{\mu} \sum_{\nu} \href{/browser/qiqth-curvature#d-qiqth-curvature-covderivvec}{(\nabla {V})_{{\mu}}{}^{{\nu}}({x})} \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-covderivvec}{(\nabla {V})_{{\nu}}{}^{{\mu}}({x})} = 0 \to \forall (\mathrm{ad} : \mathbb{R}), \mathrm{ad} = -\sum_{\nu} V\,x\,\nu \cdot \partial_{{\nu}}({\lambda y \mapsto \href{/browser/qiqth-raychaudhuri#d-qiqth-curvature-expansion}{\theta({y})}})({x}) \to \mathrm{ad} = ({\lambda i j \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-ricci}{R_{{i}{j}}({x})}})({V\,x},{V\,x})

Proof. By raychaudhuri_focusing_at_equilibrium. $\square$

Used by qiqt_gr_freefield_localized'.

Lemma 561 (bl_pernull_of_modular). source ↗

The pointwise per-null premise from the derived modular relation + cited AQFT/geometry. From δ⟨K⟩ = η δA (hModular, DERIVED) together with the cited boost-flux (hFlux, Bisognano–Wichmann) and Raychaudhuri focusing (hFocus), with a = 2π/(ℏη), the heat tensor a·T − Ric vanishes on the null vector v: BL(a·T − Ric) v = 0. This is exactly Jacobson’s pernull premise for the direction v.

\hbar \ne 0 \to \eta \ne 0 \to a = 2 \cdot \pi / (\hbar \cdot \eta) \to k^{\prime} = \eta \cdot a^{\prime} \to k^{\prime} = 2 \cdot \pi / \hbar \cdot \href{/browser/qiqth-einsteinequationofstate#d-qiqth-einsteineos-bl}{({T})({v},{v})} \to a^{\prime} = \href{/browser/qiqth-einsteinequationofstate#d-qiqth-einsteineos-bl}{({\mathrm{Ric}})({v},{v})} \to \href{/browser/qiqth-einsteinequationofstate#d-qiqth-einsteineos-bl}{({\lambda i j \mapsto a \cdot T\,i\,j - \mathrm{Ric}\,i\,j})({v},{v})} = 0

Proof. By BL_smul_sub. $\square$

Used by bl_pernull_of_qiqt.

Lemma 562 (bl_pernull_of_qiqt). source ↗

The per-null premise DERIVED from QIQT-H content + the two cited inputs. Composes differential_area_law_of_relEntropy (QIQT-H ⇒ δ⟨K⟩ = η δA) with bl_pernull_of_modular, so the only non-derived inputs are the labelled cited physics (hFlux, hFocus). …

\hbar \ne 0 \to \eta \ne 0 \to a = 2 \cdot \pi / (\hbar \cdot \eta) \to ({S})'({0})={s^{\prime}} \to ({\mathrm{KE}})'({0})={k^{\prime}} \to ({A})'({0})={a^{\prime}} \to (\text{for }t\text{ near }0,\; S\,t \le \eta \cdot A\,t) \to S\,0 = \eta \cdot A\,0 \to (\forall (t : \mathbb{R}), 0 \le \mathrm{KE}\,t - S\,t) \to \mathrm{KE}\,0 - S\,0 = 0 \to k^{\prime} = 2 \cdot \pi / \hbar \cdot \href{/browser/qiqth-einsteinequationofstate#d-qiqth-einsteineos-bl}{({T})({v},{v})} \to a^{\prime} = \href{/browser/qiqth-einsteinequationofstate#d-qiqth-einsteineos-bl}{({\mathrm{Ric}})({v},{v})} \to \href{/browser/qiqth-einsteinequationofstate#d-qiqth-einsteineos-bl}{({\lambda i j \mapsto a \cdot T\,i\,j - \mathrm{Ric}\,i\,j})({v},{v})} = 0

Proof. By differential_area_law_of_relEntropy, bl_pernull_of_modular. $\square$

Used by qiqt_bekenstein_gives_gr.

Theorem 563 (qiqt_bekenstein_gives_gr). source ↗

THE END-TO-END THEOREM — QIQT-H + (cited Bisognano–Wichmann & Raychaudhuri) ⇒ the Einstein field equations. Assembles the whole chain into one theorem. Along each local null generator (x, v) (with v metric-null), QIQT-H’s content — the capacity bound S ≤ η·A (shannon_le_log_card), saturation at the reference (shannon_uniform_eq_log_card), and relative-entropy positivity (Klein, relEntropy_nonneg) — DERIVES the differential area law / modular relation, which with the two cited inputs (hFlux = Bisognano–Wichmann boost flux, hFocus = Raychaudhuri focusing) gives Jacobson’s per-null premise; jacobson_einstein_equation_of_state then yields a·T = G + Λ·g with genuine Einstein tensor and constant Λ. …

(\forall (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}}) (a b : \mathrm{Fin}\,4), g_{{a}{b}}({y}) = g_{{b}{a}}({y})) \to (\forall (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}}) (a b : \mathrm{Fin}\,4), g^{{a}{b}}({y}) = g^{{b}{a}}({y})) \to (\forall (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}}) (a b : \mathrm{Fin}\,4), \sum_{\sigma} g_{{a}{\sigma}}({y}) \cdot g^{{\sigma}{b}}({y}) = \delta_{ab}) \to (\forall (a b : \mathrm{Fin}\,4), ({\lambda y \mapsto g_{{a}{b}}({y})})\in C^{\infty}) \to (\forall (a b : \mathrm{Fin}\,4), ({\lambda y \mapsto g^{{a}{b}}({y})})\in C^{\infty}) \to \forall (T : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}} \to \mathrm{Fin}\,4 \to \mathrm{Fin}\,4 \to \mathbb{R}) (\eta \hbar a : \mathbb{R}), \hbar \ne 0 \to \eta \ne 0 \to a = 2 \cdot \pi / (\hbar \cdot \eta) \to (\forall (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}}) (a^{\prime} b : \mathrm{Fin}\,4), T_{{a^{\prime}}{b}}({x}) = T_{{b}{a^{\prime}}}({x})) \to \forall (P \mathrm{Pinv} : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}} \to \mathrm{Fin}\,4 \to \mathrm{Fin}\,4 \to \mathbb{R}), (\forall (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}}) (i j : \mathrm{Fin}\,4), \sum_{k} P_{{i}{k}}({x}) \cdot (P^{-1})_{{k}{j}}({x}) = \delta_{ij}) \to (\forall (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}}) (i j : \mathrm{Fin}\,4), \sum_{k} (P^{-1})_{{i}{k}}({x}) \cdot P_{{k}{j}}({x}) = \delta_{ij}) \to (\forall (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}}) (i j : \mathrm{Fin}\,4), g_{{i}{j}}({x}) = \sum_{k} \sum_{l} P_{{k}{i}}({x}) \cdot \href{/browser/qiqth-einsteinequationofstate#d-qiqth-einsteineos-gm}{\eta_{{k}{l}}} \cdot P_{{l}{j}}({x})) \to \forall (S \mathrm{KE} A : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}} \to (\mathrm{Fin}\,4 \to \mathbb{R}) \to \mathbb{R} \to \mathbb{R}) (\mathrm{sd} \mathrm{kd} \mathrm{ad} : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}} \to (\mathrm{Fin}\,4 \to \mathbb{R}) \to \mathbb{R}), (\forall (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}}) (v : \mathrm{Fin}\,4 \to \mathbb{R}), \href{/browser/qiqth-einsteinequationofstate#d-qiqth-einsteineos-bl}{({g\,x})({v},{v})} = 0 \to ({S\,x\,v})'({0})={\dot{S}({x},{v})}) \to (\forall (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}}) (v : \mathrm{Fin}\,4 \to \mathbb{R}), \href{/browser/qiqth-einsteinequationofstate#d-qiqth-einsteineos-bl}{({g\,x})({v},{v})} = 0 \to ({\mathrm{KE}\,x\,v})'({0})={\dot{K}({x},{v})}) \to (\forall (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}}) (v : \mathrm{Fin}\,4 \to \mathbb{R}), \href{/browser/qiqth-einsteinequationofstate#d-qiqth-einsteineos-bl}{({g\,x})({v},{v})} = 0 \to ({A\,x\,v})'({0})={\dot{A}({x},{v})}) \to (\forall (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}}) (v : \mathrm{Fin}\,4 \to \mathbb{R}), \href{/browser/qiqth-einsteinequationofstate#d-qiqth-einsteineos-bl}{({g\,x})({v},{v})} = 0 \to \text{for }t\text{ near }0,\; S({x},{v},{t}) \le \eta \cdot A({x},{v},{t})) \to (\forall (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}}) (v : \mathrm{Fin}\,4 \to \mathbb{R}), \href{/browser/qiqth-einsteinequationofstate#d-qiqth-einsteineos-bl}{({g\,x})({v},{v})} = 0 \to S({x},{v},{0}) = \eta \cdot A({x},{v},{0})) \to (\forall (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}}) (v : \mathrm{Fin}\,4 \to \mathbb{R}), \href{/browser/qiqth-einsteinequationofstate#d-qiqth-einsteineos-bl}{({g\,x})({v},{v})} = 0 \to \forall (t : \mathbb{R}), 0 \le \mathrm{KE}({x},{v},{t}) - S({x},{v},{t})) \to (\forall (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}}) (v : \mathrm{Fin}\,4 \to \mathbb{R}), \href{/browser/qiqth-einsteinequationofstate#d-qiqth-einsteineos-bl}{({g\,x})({v},{v})} = 0 \to \mathrm{KE}({x},{v},{0}) - S({x},{v},{0}) = 0) \to (\forall (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}}) (v : \mathrm{Fin}\,4 \to \mathbb{R}), \href{/browser/qiqth-einsteinequationofstate#d-qiqth-einsteineos-bl}{({g\,x})({v},{v})} = 0 \to \dot{K}({x},{v}) = 2 \cdot \pi / \hbar \cdot \href{/browser/qiqth-einsteinequationofstate#d-qiqth-einsteineos-bl}{({T\,x})({v},{v})}) \to (\forall (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}}) (v : \mathrm{Fin}\,4 \to \mathbb{R}), \href{/browser/qiqth-einsteinequationofstate#d-qiqth-einsteineos-bl}{({g\,x})({v},{v})} = 0 \to \dot{A}({x},{v}) = ({\lambda i j \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-ricci}{R_{{i}{j}}({x})}})({v},{v})) \to (\forall (f : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}} \to \mathbb{R}), (\forall (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}}) (a^{\prime} b : \mathrm{Fin}\,4), a \cdot T_{{a^{\prime}}{b}}({y}) = \href{/browser/qiqth-curvature#d-qiqth-curvature-ricci}{R_{{a^{\prime}}{b}}({y})} + f\,y \cdot g_{{a^{\prime}}{b}}({y})) \to (\forall (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}}) (\rho : \mathrm{Fin}\,4), \href{/browser/qiqth-curvature#d-qiqth-curvature-pdiffat}{\mathrm{PdiffAt}}\,f\,\rho\,x) \wedge \mathrm{Differentiable}\,\mathbb{R}\,\lambda y \mapsto f\,y + 1/2 \cdot \href{/browser/qiqth-curvature#d-qiqth-curvature-scalarcurv}{R({y})}) \to (\forall (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}}) (\nu : \mathrm{Fin}\,4), \href{/browser/qiqth-einsteinfieldequation#d-qiqth-curvature-div02}{(\nabla\!\cdot {\lambda y a^{\prime} b \mapsto a \cdot T_{{a^{\prime}}{b}}({y})})_{{\nu}}({x})} = 0) \to \exists \Lambda, \forall (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}}) (\mu \nu : \mathrm{Fin}\,4), a \cdot T_{{\mu}{\nu}}({x}) = \href{/browser/qiqth-curvature#d-qiqth-curvature-einsteintensor}{G_{{\mu}{\nu}}({x})} + \Lambda \cdot g_{{\mu}{\nu}}({x})

Proof. By christoffel_contDiff, christoffel, jacobson_einstein_equation_of_state, bl_pernull_of_qiqt, ricci_symm. $\square$

Used by qiqt_gr_from_wedge_kms_complete, qiqt_gr_from_flux_complete.

← all sections · ← QiqtGrThermo · Raychaudhuri →