QiqtGrCovCong · section of the QIQT-H book

QIQTH.QiqtGrCovCong

← all sections · ← QiqtGrComplete · QiqtGrExplicitKG →

QiqtGrCovCong · entries 547–547 of 1000

Lemma 547 (qiqt_gr_freefield_complete_covCong). source ↗

The maximally-discharged QIQT→GR capstone with the Raychaudhuri congruence premises reduced to one condition. Identical to qiqt_gr_freefield_complete, but the geodesic premise hWgeo and the equilibrium premise hWequil are replaced by the single condition hcov (the congruence W x v is covariantly constant), from which both are derived (raychaudhuri_setup_of_covConst). Together with the localization (T3-3-C3) and entropy (T3-1) discharges, the only surviving labelled inputs are the genuine physics floor (hbound/hcap/hK/hS/hA = H2/FQ + realization), the matter EOM hKG, the covariant-constancy condition hcov (the geometric setup, satisfiable e.g. …

(\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 (\varphi : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}} \to \mathbb{R}) (m \eta \hbar a : \mathbb{R}), \hbar \ne 0 \to 0 < \hbar \to \eta \ne 0 \to a = 2 \cdot \pi / (\hbar \cdot \eta) \to ({\varphi})\in C^{\infty} \to (\forall (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}}), \href{/browser/qiqth-kgstressconservation#d-qiqth-curvature-boxfield}{(\Box {\varphi})({x})} = {m}^{2} \cdot \varphi\,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 (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} : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}} \to (\mathrm{Fin}\,4 \to \mathbb{R}) \to \mathbb{R}) (p : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}} \to (\mathrm{Fin}\,4 \to \mathbb{R}) \to \mathbb{R} \to \iota \to \mathbb{R}), (\forall (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}}) (v : \mathrm{Fin}\,4 \to \mathbb{R}) (t : \mathbb{R}) (r : \iota), 0 \le p\,x\,v\,t\,r) \to (\forall (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}}) (v : \mathrm{Fin}\,4 \to \mathbb{R}) (t : \mathbb{R}), \sum_{r} p\,x\,v\,t\,r = 1) \to (\forall (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}}) (v : \mathrm{Fin}\,4 \to \mathbb{R}), p\,x\,v\,0 = \lambda x \mapsto {((\#\,\iota))}^{-1}) \to (\forall (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}}) (v : \mathrm{Fin}\,4 \to \mathbb{R}), \eta \cdot A({x},{v},{0}) = \log\,(\#\,\iota)) \to \forall (W : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}} \to (\mathrm{Fin}\,4 \to \mathbb{R}) \to \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}} \to \mathrm{Fin}\,4 \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 W\,x\,v\,x = v) \to (\forall (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}}) (v : \mathrm{Fin}\,4 \to \mathbb{R}) (\mu : \mathrm{Fin}\,4), ({\lambda y \mapsto W\,x\,v\,y\,\mu})\in C^{\infty}) \to (\forall (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}}) (v : \mathrm{Fin}\,4 \to \mathbb{R}) (a b : \mathrm{Fin}\,4) (y : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}}), \href{/browser/qiqth-curvature#d-qiqth-curvature-covderivvec}{(\nabla {W\,x\,v})_{{a}}{}^{{b}}({y})} = 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 ({\lambda t \mapsto \href{/browser/qiqth-branchledger#d-qiqth-branchledger-shannon}{S({p\,x\,v\,t})}})'({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 ({\lambda t \mapsto \href{/browser/qiqth-branchledger#d-qiqth-branchledger-shannon}{S({p\,x\,v\,t})} + \href{/browser/qiqth-relentpositivity#d-qiqth-relentpositivity-kl}{D_{\mathrm{KL}}({p\,x\,v\,t}\,\|\,{p\,x\,v\,0})}})'({0})={2 \cdot \pi / \hbar \cdot ({\href{/browser/qiqth-kgstressconservation#d-qiqth-curvature-kgstress}{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 ({A\,x\,v})'({0})={-\sum_{\nu} W\,x\,v\,x\,\nu \cdot \partial_{{\nu}}({\lambda y \mapsto \href{/browser/qiqth-raychaudhuri#d-qiqth-curvature-expansion}{\theta({y})}})({x})}) \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,\; \href{/browser/qiqth-branchledger#d-qiqth-branchledger-shannon}{S({p\,x\,v\,t})} \le \eta \cdot A({x},{v},{t})) \to \forall (\mathrm{mw} : \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}), 0 < \mathrm{mw}\,x\,v) \to \exists \Lambda, \forall (x : \href{/browser/qiqth-curvature#d-qiqth-curvature-point}{M^{{4}}}) (\mu \nu : \mathrm{Fin}\,4), a \cdot \href{/browser/qiqth-kgstressconservation#d-qiqth-curvature-kgstress}{T({x})\,\mu\,\nu} = \href{/browser/qiqth-curvature#d-qiqth-curvature-einsteintensor}{G_{{\mu}{\nu}}({x})} + \Lambda \cdot g_{{\mu}{\nu}}({x})

Proof. By qiqt_gr_freefield_complete, raychaudhuri_setup_of_covConst. $\square$

Used by qiqt_gr_ppwave.

← all sections · ← QiqtGrComplete · QiqtGrExplicitKG →