EinsteinEquationOfState · section of the QIQT-H book

QIQTH.EinsteinEquationOfState

← all sections · ← EffectGleason · EinsteinFieldEquation →

EinsteinEquationOfState · entries 77–82 of 1000

Definition 77 (gm).  source ↗

Minkowski metric (−,+,+,+) on Fin 4, as a function of two indices.

ηij  :=  if i=j then if i=0 then −1 else 1 else 0\href{/browser/qiqth-einsteinequationofstate#d-qiqth-einsteineos-gm}{\eta_{{i}{j}}} \;:=\; \text{if }i = j\text{ then }\text{if }i = 0\text{ then }-1\text{ else }1\text{ else }0

Used by symmTensor_eq_smul_metric_of_null, symmTensor_eq_smul_metric_of_null_general, crux_of_pernull, jacobson_einstein_equation_of_state, ppFrame_cong, qiqt_gr_freefield_complete, qiqt_gr_freefield_complete_covCong, qiqt_gr_explicit_kg, and 10 more.

Definition 78 (QF).  source ↗

The quadratic form of a symmetric tensor C evaluated on a 4-vector (x0,x1,x2,x3) — i.e. ∑_{μν} C_{μν} x^μ x^ν, written out using C i j = C j i.

Used by symmTensor_eq_smul_metric_of_null, QF_eq_BL, symmTensor_eq_smul_metric_of_null_general.

Lemma 79 (symmTensor_eq_smul_metric_of_null).  source ↗

The algebraic crux of Jacobson’s derivation. A symmetric tensor C whose quadratic form vanishes on the entire null cone of Minkowski space (every (x0,x1,x2,x3) with −x0²+x1²+x2²+x3² = 0) is a scalar multiple of the metric: C = c • g. This is the step that turns the per-null-direction Clausius relation into a genuine tensor field equation.

(∀(ij:Fin 4),C i j=C j i)→(∀(x0x1x2x3:R),−x02+x12+x22+x32=0→QF C x0 x1 x2 x3=0)→∃c,∀(ij:Fin 4),C i j=c⋅ηij(\forall (i j : \mathrm{Fin}\,4), C\,i\,j = C\,j\,i) \to (\forall (x_{0} x_{1} x_{2} x_{3} : \mathbb{R}), -{x_{0}}^{2} + {x_{1}}^{2} + {x_{2}}^{2} + {x_{3}}^{2} = 0 \to \href{/browser/qiqth-einsteinequationofstate#d-qiqth-einsteineos-qf}{\mathrm{QF}}\,C\,x_{0}\,x_{1}\,x_{2}\,x_{3} = 0) \to \exists c, \forall (i j : \mathrm{Fin}\,4), C\,i\,j = c \cdot \href{/browser/qiqth-einsteinequationofstate#d-qiqth-einsteineos-gm}{\eta_{{i}{j}}}

Proof. Immediate from the definitions. □\square

Used by symmTensor_eq_smul_metric_of_null_general.

Definition 80 (BL).  source ↗

The bilinear form ∑_{ij} C_{ij} v^i v^j of a tensor on a vector — the coordinate-free shape of QF.

(C)(v,v)  :=  ∑i∑jC i j⋅v i⋅v j\href{/browser/qiqth-einsteinequationofstate#d-qiqth-einsteineos-bl}{({C})({v},{v})} \;:=\; \sum_{i} \sum_{j} C\,i\,j \cdot v\,i \cdot v\,j

Used by BL_smul_sub, QF_eq_BL, symmTensor_eq_smul_metric_of_null_general, crux_of_pernull, jacobson_einstein_equation_of_state, qiqt_gr_freefield_complete, qiqt_gr_freefield_complete_covCong, qiqt_gr_explicit_kg, and 19 more.

Lemma 81 (QF_eq_BL).  source ↗

QF is the bilinear form on the explicit 4-vector (for a symmetric tensor).

(∀(ij:Fin 4),C i j=C j i)→∀(x0x1x2x3:R),QF C x0 x1 x2 x3=(C)(![x0,x1,x2,x3],![x0,x1,x2,x3])(\forall (i j : \mathrm{Fin}\,4), C\,i\,j = C\,j\,i) \to \forall (x_{0} x_{1} x_{2} x_{3} : \mathbb{R}), \href{/browser/qiqth-einsteinequationofstate#d-qiqth-einsteineos-qf}{\mathrm{QF}}\,C\,x_{0}\,x_{1}\,x_{2}\,x_{3} = \href{/browser/qiqth-einsteinequationofstate#d-qiqth-einsteineos-bl}{({C})({![x_{0} , x_{1} , x_{2} , x_{3}]},{![x_{0} , x_{1} , x_{2} , x_{3}]})}

Proof. Immediate from the definitions. □\square

Used by symmTensor_eq_smul_metric_of_null_general.

Lemma 82 (symmTensor_eq_smul_metric_of_null_general).  source ↗

The algebraic crux for a GENERAL Lorentzian metric (Phase 3 — the framework bridge). A symmetric tensor C whose bilinear form vanishes on the entire null cone of an arbitrary Lorentzian metric g is a scalar multiple of g. The Lorentzian hypothesis enters as Sylvester’s law of inertia: g is congruent to Minkowski, g = Pᵀ·η·P for an invertible P (hcong with P, Pinv a two-sided inverse). The proof is a congruence reduction to the proven Minkowski case symmTensor_eq_smul_metric_of_null: transform C by Pinv, apply the Minkowski lemma, transform back. This is exactly what upgrades Jacobson’s per-null Clausius relation (stated in each point’s local inertial frame) into the tensor field equation.

(∀(ij:Fin 4),C i j=C j i)→∀(PPinv:Fin 4→Fin 4→R),(∀(ij:Fin 4),∑kP i k⋅Pinv k j=δij)→(∀(ij:Fin 4),∑kPinv i k⋅P k j=δij)→(∀(ij:Fin 4),g i j=∑k∑lP k i⋅ηkl⋅P l j)→(∀(v:Fin 4→R),(g)(v,v)=0→(C)(v,v)=0)→∃c,∀(ij:Fin 4),C i j=c⋅g i j(\forall (i j : \mathrm{Fin}\,4), C\,i\,j = C\,j\,i) \to \forall (P \mathrm{Pinv} : \mathrm{Fin}\,4 \to \mathrm{Fin}\,4 \to \mathbb{R}), (\forall (i j : \mathrm{Fin}\,4), \sum_{k} P\,i\,k \cdot \mathrm{Pinv}\,k\,j = \delta_{ij}) \to (\forall (i j : \mathrm{Fin}\,4), \sum_{k} \mathrm{Pinv}\,i\,k \cdot P\,k\,j = \delta_{ij}) \to (\forall (i j : \mathrm{Fin}\,4), g\,i\,j = \sum_{k} \sum_{l} P\,k\,i \cdot \href{/browser/qiqth-einsteinequationofstate#d-qiqth-einsteineos-gm}{\eta_{{k}{l}}} \cdot P\,l\,j) \to (\forall (v : \mathrm{Fin}\,4 \to \mathbb{R}), \href{/browser/qiqth-einsteinequationofstate#d-qiqth-einsteineos-bl}{({g})({v},{v})} = 0 \to \href{/browser/qiqth-einsteinequationofstate#d-qiqth-einsteineos-bl}{({C})({v},{v})} = 0) \to \exists c, \forall (i j : \mathrm{Fin}\,4), C\,i\,j = c \cdot g\,i\,j

Proof. By QF, symmTensor_eq_smul_metric_of_null, QF_eq_BL. □\square

Used by crux_of_pernull.

← all sections · ← EffectGleason · EinsteinFieldEquation →