Fock · section of the QIQT-H book

QIQTH.Fock.FreeFieldHFlux

← all sections · ← CyclicWitness · Localization →

Fock · entries 231–235 of 1000

Lemma 231 (hasDerivAt_modularEnergy_of_boost_pos).  source ↗

Modular energy = boost energy, in the +2π convention (sign-flipped copy of hasDerivAt_modularEnergy_of_boost). Given the BW identification modUnitary S = boostUnitary(+2π·), the modular-energy derivative of ξ equals its boost-energy derivative.

(∀(t:R)(u:(Lp C 2 vol)),(Δ S t) u=(U (2⋅π⋅t)) u)→∀(ξ:(Lp C 2 vol))(c:C),(λt↦⟨ξ,(U (2⋅π⋅t)) ξ⟩)′(0)=c→(λt↦⟨ξ,(Δ S t) ξ⟩)′(0)=c(\forall (t : \mathbb{R}) (u : (\mathrm{Lp}\,\mathbb{C}\,2\,\mathrm{vol})), (\href{/browser/qiqth-standardsubspacemodularflow#d-qiqth-standardsubspacemodular-modunitary}{\Delta}\,S\,t)\,u = (\href{/browser/qiqth-fock-oneparticle#d-qiqth-fock-oneparticle-boostunitary}{U}\,(2 \cdot \pi \cdot t))\,u) \to \forall (\xi : (\mathrm{Lp}\,\mathbb{C}\,2\,\mathrm{vol})) (c : \mathbb{C}), ({\lambda t \mapsto \langle {\xi},{(\href{/browser/qiqth-fock-oneparticle#d-qiqth-fock-oneparticle-boostunitary}{U}\,(2 \cdot \pi \cdot t))\,\xi}\rangle})'({0})={c} \to ({\lambda t \mapsto \langle {\xi},{(\href{/browser/qiqth-standardsubspacemodularflow#d-qiqth-standardsubspacemodular-modunitary}{\Delta}\,S\,t)\,\xi}\rangle})'({0})={c}

Proof. Immediate from the definitions. □\square

Used by freeField_modularEnergy_eq_boostCharge.

Lemma 232 (freeField_modularEnergy_eq_boostCharge).  source ↗

The free-field modular-energy = stress-flux derivative, BW supplied internally (Phase 2). For the nice-wedge standard subspace S and ANY mode ξ, given the boost-charge derivative HasDerivAt (t ↦ ⟨ξ, boostUnitary(2πt) ξ⟩) c 0, the modular-energy derivative HasDerivAt (t ↦ ⟨ξ, modUnitary S t ξ⟩) c 0 holds — with the Bisognano–Wichmann identification modUnitary S = boostUnitary(+2π·) supplied internally and axiom-free by oneParticleBW_niceWedge_unconditional (no labelled hUniq/hStrip, no sign mismatch).

(λt↦⟨ξ,(U (2⋅π⋅t)) ξ⟩)′(0)=c→(λt↦⟨ξ,(Δ (K m ⋯ ⋯ ) t) ξ⟩)′(0)=c({\lambda t \mapsto \langle {\xi},{(\href{/browser/qiqth-fock-oneparticle#d-qiqth-fock-oneparticle-boostunitary}{U}\,(2 \cdot \pi \cdot t))\,\xi}\rangle})'({0})={c} \to ({\lambda t \mapsto \langle {\xi},{(\href{/browser/qiqth-standardsubspacemodularflow#d-qiqth-standardsubspacemodular-modunitary}{\Delta}\,(\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgestandardsubspace}{\mathcal{K}}\,m\,\cdots \,\cdots )\,t)\,\xi}\rangle})'({0})={c}

Proof. By oneParticleBW_niceWedge_unconditional, hasDerivAt_modularEnergy_of_boost_pos. □\square

Used by freeField_oneParticle_hFlux.

Lemma 233 (hasDerivAt_inner_boostUnitary_imaginary_pos).  source ↗

The +2π boost-charge derivative (purely imaginary), by the t → −t reflection of the −2π hasDerivAt_inner_boostUnitary_imaginary. Because ⟪ξ, boostUnitary(2πt) ξ⟫ = ⟪ξ, boostUnitary(−2π(−t)) ξ⟫, the +2π correlation is the −2π one precomposed with negation, so its derivative is the negative: d/dt ⟪ξ, boostUnitary(2π t) ξ⟫|₀ = i·((−(2π·∫ conj(f)·f')).im). Reuses the hard dominated-convergence proof of the −2π lemma — no re-derivation. Axiom-free.

Integrable f vol→(∀(x:R),(f)′(x)=f′ x)→AEStronglyMeasurable f′ vol→∀(B:R),(∀(x:R),∥f′ x∥≤B)→(λt↦⟨toLp f hf2,(U (2⋅π⋅t)) (toLp f hf2)⟩)′(0)=i⋅(−(2⋅π⋅∫(θ:R),(starRingEnd C) (f θ)⋅f′ θ)).im\mathrm{Integrable}\,f\,\mathrm{vol} \to (\forall (x : \mathbb{R}), ({f})'({x})={f^{\prime}\,x}) \to \mathrm{AEStronglyMeasurable}\,f^{\prime}\,\mathrm{vol} \to \forall (B : \mathbb{R}), (\forall (x : \mathbb{R}), \|f^{\prime}\,x\| \le B) \to ({\lambda t \mapsto \langle {\mathrm{toLp}\,f\,\mathrm{hf2}},{(\href{/browser/qiqth-fock-oneparticle#d-qiqth-fock-oneparticle-boostunitary}{U}\,(2 \cdot \pi \cdot t))\,(\mathrm{toLp}\,f\,\mathrm{hf2})}\rangle})'({0})={i \cdot (-(2 \cdot \pi \cdot \int (\theta : \mathbb{R}), (\mathrm{starRingEnd}\,\mathbb{C})\,(f\,\theta) \cdot f^{\prime}\,\theta)).\mathrm{im}}

Proof. By hasDerivAt_inner_boostUnitary_imaginary. □\square

Used by freeField_oneParticle_hFlux.

Theorem 234 (freeField_oneParticle_hFlux).  source ↗

The free-field one-particle hFlux, FULLY ASSEMBLED in the satisfiable +2π convention. For any smooth wedge state ξ = f.toLp and the nice-wedge standard subspace S, the modular-energy derivative is i·(2π/ℏ)·T_kk: HasDerivAt (t ↦ ⟪ξ, modUnitary S t ξ⟫) (i·(2π/ℏ·T_kk)) 0, with EVERYTHING operator/analytic discharged axiom-free — the Bisognano–Wichmann identification (oneParticleBW_niceWedge_unconditional) and the boost-charge derivative (hasDerivAt_inner_boostUnitary_imaginary_pos) are both supplied internally. The ONLY labelled input is the single scalar physics identification hTkk : (2π/ℏ)·T_kk = (−(2π·∫ conj(f)·f')).im (the conserved boost Killing charge = stress-tensor flux, in the +2π orientation). …

Integrable f vol→(∀(x:R),(f)′(x)=f′ x)→AEStronglyMeasurable f′ vol→∀(B:R),(∀(x:R),∥f′ x∥≤B)→∀(ℏTkk:R),2⋅π/ℏ⋅Tkk=(−(2⋅π⋅∫(θ:R),(starRingEnd C) (f θ)⋅f′ θ)).im→(λt↦⟨toLp f hf2,(Δ (K m ⋯ ⋯ ) t) (toLp f hf2)⟩)′(0)=i⋅(2⋅π/ℏ⋅Tkk)\mathrm{Integrable}\,f\,\mathrm{vol} \to (\forall (x : \mathbb{R}), ({f})'({x})={f^{\prime}\,x}) \to \mathrm{AEStronglyMeasurable}\,f^{\prime}\,\mathrm{vol} \to \forall (B : \mathbb{R}), (\forall (x : \mathbb{R}), \|f^{\prime}\,x\| \le B) \to \forall (\hbar T_{kk} : \mathbb{R}), 2 \cdot \pi / \hbar \cdot T_{kk} = (-(2 \cdot \pi \cdot \int (\theta : \mathbb{R}), (\mathrm{starRingEnd}\,\mathbb{C})\,(f\,\theta) \cdot f^{\prime}\,\theta)).\mathrm{im} \to ({\lambda t \mapsto \langle {\mathrm{toLp}\,f\,\mathrm{hf2}},{(\href{/browser/qiqth-standardsubspacemodularflow#d-qiqth-standardsubspacemodular-modunitary}{\Delta}\,(\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgestandardsubspace}{\mathcal{K}}\,m\,\cdots \,\cdots )\,t)\,(\mathrm{toLp}\,f\,\mathrm{hf2})}\rangle})'({0})={i \cdot (2 \cdot \pi / \hbar \cdot T_{kk})}

Proof. By freeField_modularEnergy_eq_boostCharge, hasDerivAt_inner_boostUnitary_imaginary_pos, boostUnitary. □\square

Used by freeField_component_hFlux, qiqt_gr_freefield_localized.

Theorem 235 (freeField_component_hFlux).  source ↗

The free-field per-generator flux equation kd = (2π/ℏ)·T_kk (the +2π/nice-wedge analog of component_hFlux_of_wedgeKMS_complete). For the nice-wedge standard subspace S and smooth wedge state ξ = f.toLp, given (i) hbridge — that the abstract per-generator modular-energy coefficient kd IS the derivative of t ↦ ⟪ξ, modUnitary S t ξ⟫ — and (ii) hTkk — the localization identification of the horizon stress component T_kk with the mode’s rapidity stress flux — derivative uniqueness pins kd = (2π/ℏ)·T_kk. …

Integrable f vol→(∀(x:R),(f)′(x)=f′ x)→AEStronglyMeasurable f′ vol→∀(B:R),(∀(x:R),∥f′ x∥≤B)→∀(ℏkdTkk:R),2⋅π/ℏ⋅Tkk=(−(2⋅π⋅∫(θ:R),(starRingEnd C) (f θ)⋅f′ θ)).im→(λt↦⟨toLp f hf2,(Δ (K m ⋯ ⋯ ) t) (toLp f hf2)⟩)′(0)=i⋅kd→kd=2⋅π/ℏ⋅Tkk\mathrm{Integrable}\,f\,\mathrm{vol} \to (\forall (x : \mathbb{R}), ({f})'({x})={f^{\prime}\,x}) \to \mathrm{AEStronglyMeasurable}\,f^{\prime}\,\mathrm{vol} \to \forall (B : \mathbb{R}), (\forall (x : \mathbb{R}), \|f^{\prime}\,x\| \le B) \to \forall (\hbar \mathrm{kd} T_{kk} : \mathbb{R}), 2 \cdot \pi / \hbar \cdot T_{kk} = (-(2 \cdot \pi \cdot \int (\theta : \mathbb{R}), (\mathrm{starRingEnd}\,\mathbb{C})\,(f\,\theta) \cdot f^{\prime}\,\theta)).\mathrm{im} \to ({\lambda t \mapsto \langle {\mathrm{toLp}\,f\,\mathrm{hf2}},{(\href{/browser/qiqth-standardsubspacemodularflow#d-qiqth-standardsubspacemodular-modunitary}{\Delta}\,(\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgestandardsubspace}{\mathcal{K}}\,m\,\cdots \,\cdots )\,t)\,(\mathrm{toLp}\,f\,\mathrm{hf2})}\rangle})'({0})={i \cdot \mathrm{kd}} \to \mathrm{kd} = 2 \cdot \pi / \hbar \cdot T_{kk}

Proof. By freeField_oneParticle_hFlux. □\square

Used by freeField_kd_conclusion.

← all sections · ← CyclicWitness · Localization →