WedgeKMSToGR · section of the QIQT-H book

QIQTH.WedgeKMSToGR

WedgeKMSToGR · entries 997–1000 of 1000

Definition 997 (WedgeKMSFlux_complete). source ↗

The wedge KMS property with the genuine, non-vacuous KMS condition. Identical to WedgeKMSFlux except the bundled opaque hUniq (the KMS-uniqueness implication) and the trivially-satisfiable StripKMS are replaced by the single genuine RvD Definition 3.4 predicate StripKMSrvd V 𝒦_W — from which the BW identification modUnitary = boostUnitary is DERIVED (oneParticleBW_wedge_complete, via the RvD Theorem 3.8 discharge oneParticleBW_complete). So the wedge KMS input is now exactly: standardness of the wedge subspace, V = boostUnitary(−2π·), the genuine KMS condition, the boost-charge = stress-flux identity, and the localization identity — with NO assumed uniqueness implication.

Used by qiqt_gr_explicit_kg, hFlux_of_wedgeKMS_complete, qiqt_gr_from_wedge_kms_complete.

Lemma 998 (hFlux_of_wedgeKMS_complete). source ↗

hFlux derived from the genuine wedge KMS property (via component_hFlux_of_wedgeKMS_complete): kd = (2π/ℏ)·T_kk per null generator, with the BW identification machine-checked from StripKMSrvd.

\href{/browser/qiqth-wedgekmstogr#d-qiqth-wedgekmstogr-wedgekmsflux-complete}{\mathrm{WedgeKMSFlux\_complete}}\,g\,T\,\mathrm{kd}\,\hbar \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})}

Proof. By boostUnitary, wedgeGenSet, StripKMSrvd, component_hFlux_of_wedgeKMS_complete, modUnitary. $\square$

Used by qiqt_gr_from_wedge_kms_complete.

Lemma 999 (qiqt_gr_from_wedge_kms_complete). source ↗

THE GOAL THEOREM, with KMS-uniqueness DERIVED. Einstein’s equations from QIQT-H’s capacity postulate + Klein positivity, modulo the three labelled physics inputs — but now the wedge KMS input is the GENUINE, non-vacuous WedgeKMSFlux_complete (using StripKMSrvd, RvD Def 3.4), with the Bisognano–Wichmann KMS-uniqueness no longer an assumed bundled implication but DERIVED from the machine-checked RvD Theorem 3.8 (oneParticleBW_complete). This is qiqt_gr_from_wedge_kms with its one remaining modular-theory assumption (the old opaque hUniq + vacuous StripKMS) replaced by a theorem.

(\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 (\mathrm{Sf} \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 ({\mathrm{Sf}\,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,\; \mathrm{Sf}\,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 \mathrm{Sf}\,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}) - \mathrm{Sf}\,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}) - \mathrm{Sf}\,x\,v\,0 = 0) \to \href{/browser/qiqth-wedgekmstogr#d-qiqth-wedgekmstogr-wedgekmsflux-complete}{\mathrm{WedgeKMSFlux\_complete}}\,g\,T\,\mathrm{kd}\,\hbar \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 qiqt_bekenstein_gives_gr, hFlux_of_wedgeKMS_complete. $\square$

Used by qiqt_gr_explicit_kg.

Theorem 1000 (qiqt_gr_from_flux_complete). source ↗

THE GOAL THEOREM, taking the per-generator flux EQUATION directly. Identical to qiqt_gr_from_wedge_kms_complete, but the modular input is the bare conclusion hflux : kd x v = (2π/ℏ)·BL(T x)v per null generator — exactly what qiqt_bekenstein_gives_gr consumes — instead of the WedgeKMSFlux_complete (−2π/wedgeGenSet) bundle. This is the convention-agnostic GR entry point: the bundle supplies hflux via hFlux_of_wedgeKMS_complete, and the free-field +2π route supplies it via freeField_component_hFlux — both land here. Axiom-free, no sorry.

(\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 (\mathrm{Sf} \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 ({\mathrm{Sf}\,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,\; \mathrm{Sf}\,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 \mathrm{Sf}\,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}) - \mathrm{Sf}\,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}) - \mathrm{Sf}\,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 qiqt_bekenstein_gives_gr. $\square$

Used by qiqt_gr_freefield.

← all sections · ← ValueSelection