QIQTH.Fock.OneParticleBW

← all sections · ← OneParticle · SchwartzDecay →

Fock · entries 286–319 of 1000

Lemma 286 (boostUnitary_KrepL2).  source ↗

L² boost-covariance of the localization (GPT-5.5’s first Layer-1 brick, the sign check): boostUnitary a (KrepL2 f) = KrepL2 (boostTest (−a) f). The geometric boost acts on the one-particle wavefunction Krep f ∈ L²(rapidity) exactly as the spacetime boost boostTest (−a) on the test function. This is the engine for boost-invariance of the physically-defined wedge subspace (𝒦 := closure of {KrepL2 f : f real, supp f ⊆ right wedge}). Axiom-free; from Krep_boost + the flow θ ↦ θ + (−a) = θ − a.

Proof. By Krep_boost, flow, mp, unitary_apply, boostFlow. $\square$

Used by inner_boostUnitary_KrepL2, vec_boost, boostUnitary_mapsTo_wedgeGenSet.

Lemma 287 (coeFn_boostUnitary).  source ↗

Pointwise form of the boost action: (boostUnitary a ξ)(θ) = ξ(θ − a) (a.e.). The rapidity boost is the spatial translation θ ↦ θ − a on the one-particle wavefunction. From MPFlow.unitary_apply (the unitary precomposes with the pullback flow θ ↦ θ + (−a)).

Proof. By flow, mp, unitary_apply, boostFlow. $\square$

Used by inner_boostUnitary_toLp, boostUnitary_toLp.

Lemma 288 (boostUnitary_eq_vadd).  source ↗

The boost unitary IS the canonical Lp domain-translation DomAddAct.mk t +ᵥ ξ. boostUnitary t is precomposition with θ ↦ θ + t (the rapidity-translation flow); Mathlib’s DomAddAct action is precomposition with θ ↦ t + θ. They agree by add_comm, identifying the project’s boost group with Mathlib’s continuous domain action — the bridge that makes the boost group’s strong continuity a one-line consequence of Mathlib’s Lp.instContinuousVAddDomAddAct.

Proof. By flow, mp, unitary_apply, boostFlow. $\square$

Used by continuous_boostUnitary_apply.

Lemma 289 (continuous_boostUnitary_apply).  source ↗

Strong continuity of the boost group (vector level): for every one-particle state ξ, the orbit t ↦ boostUnitary t ξ is continuous. This is the genuine strong continuity of the rapidity-translation unitary group — the first brick of the Stone-generator program whose later steps would ground the boost-charge derivative hBoostCharge. Derived from Mathlib’s continuity of the Lp domain action (Lp.instContinuousVAddDomAddAct, valid since Lebesgue measure is translation-invariant, locally finite, inner regular) via the identification boostUnitary_eq_vadd. Axiom-free.

Proof. By boostUnitary_eq_vadd. $\square$

Used by oneParticleBW_niceWedge, oneParticleBW_wedge_complete.

Lemma 290 (inner_boostUnitary_toLp).  source ↗

The boost matrix coefficient as a concrete translation integral. For a one-particle state given by a representative f (ξ = f.toLp), the modular/boost correlation ⟪ξ, boostUnitary s ξ⟫ is the cross-correlation integral ∫ conj(f θ)·f(θ − s) dθ. This is the inner-product-to-integral bridge (L2.inner_def + MemLp.coeFn_toLp + coeFn_boostUnitary, the translation pushed through the measure-preserving shift) that turns the abstract boost correlation into an analyzable integral — the setup on which the boost-charge derivative (Stone generator → hBoostCharge) is computed. Axiom-free.

Proof. By coeFn_boostUnitary. $\square$

Used by hasDerivAt_inner_boostUnitary_wedge.

Lemma 291 (hasDerivAt_inner_boostUnitary_wedge).  source ↗

The boost-charge derivative (the analytic core of hBoostCharge). For a one-particle state ξ = f.toLp with f smooth enough (differentiable with derivative f', with f, |f|² integrable and ‖f'‖ globally bounded — all satisfied by any Schwartz / compactly-supported-C¹ f), the boost correlation t ↦ ⟪ξ, boostUnitary(−2π t) ξ⟫ is differentiable at 0 with derivative 2π·∫ conj(f)·f'. This is the rapidity-momentum expectation 2π⟪ξ, −i∂_θ ξ⟫ — the boost charge — obtained by differentiating the cross-correlation integral under the integral sign (hasDerivAt_integral_of_dominated_loc_of_deriv_le, dominating function 2π·B·|f|). …

Proof. By inner_boostUnitary_toLp. $\square$

Used by hasDerivAt_inner_boostUnitary_imaginary.

Lemma 292 (hasDerivAt_inner_boostUnitary_imaginary).  source ↗

The boost-charge derivative in its physical i·(real) form — hBoostCharge grounded. The boost correlation derivative is purely imaginary: d/dt ⟪ξ, boostUnitary(−2π t) ξ⟫|₀ = i·(boost energy), with boost energy = (2π·∫ conj(f)·f')·(−i) = the real rapidity-momentum expectation. This is exactly the shape of the labelled hBoostCharge input — now DERIVED for any smooth wedge state (modulo only the single physical identification boost energy = (2π/ℏ)·T_kk, the stress tensor). …

Proof. By boostUnitary_zero_apply, hasDerivAt_inner_boostUnitary_wedge. $\square$

Used by hasDerivAt_inner_boostUnitary_imaginary_pos.

Lemma 293 (mapsTo_closure_span).  source ↗

Invariance engine (for the boost-invariance of the wedge standard subspace): a continuous ℝ-linear map L that maps a set W into itself also maps closure (span ℝ W) into itself. Applied with L = boostUnitary a and W = the (boost-closed) wedge generating set, this gives boostUnitary a (𝒦_W) ⊆ 𝒦_W — the boost-invariance the KMS-uniqueness route needs.

Proof. Immediate from the definitions. $\square$

Used by boostUnitary_mapsTo_closure_span.

Lemma 294 (boostUnitary_mapsTo_closure_span).  source ↗

Boost-invariance of a physically-defined wedge subspace. If a set S of one-particle vectors is closed under the boost (boostUnitary a maps S into S — true for S = the KrepL2 of a boost-closed family of wedge test functions, via boostUnitary_KrepL2), then the wedge standard subspace 𝒦_W := closure (span_ℝ S) is boost-invariant: boostUnitary a (𝒦_W) ⊆ 𝒦_W. This is the invariance the GPT-5-pro KMS-uniqueness route consumes (V(a)𝒦 = 𝒦).

Proof. By mapsTo_closure_span. $\square$

Used by boostUnitary_mapsTo_wedgeSubspace.

Definition 295 (rightWedge).  source ↗

The right wedge W_R = {z : z¹ > |z⁰|} in 1+1D Minkowski V = Fin 2 → ℝ (index 0 = time, 1 = space), written in light-cone form z¹ − z⁰ > 0 ∧ z¹ + z⁰ > 0.

Used by lorentzBoost_mapsTo_rightWedge, support_boostTest_subset, wedgeGenSet, boostUnitary_mapsTo_wedgeGenSet.

Lemma 296 (lorentzBoost_mapsTo_rightWedge).  source ↗

The right wedge is boost-invariant: lorentzBoost a maps W_R into itself. In light-cone coordinates z± = z¹ ± z⁰ the boost acts by the positive scalings z⁻ ↦ e^{−a}z⁻, z⁺ ↦ e^{a}z⁺, so positivity of both is preserved. This is why the wedge generating set of test functions is boost-closed, hence 𝒦_W is boost-invariant.

Proof. Immediate from the definitions. $\square$

Used by support_boostTest_subset.

Lemma 297 (lorentzBoost_neg_boost).  source ↗

The boost is invertible: lorentzBoost (−a) ∘ lorentzBoost a = id (cosh²−sinh²=1).

Proof. Immediate from the definitions. $\square$

Used by support_boostTest_subset.

Lemma 298 (support_boostTest_subset).  source ↗

Boost preserves wedge support: if f is supported in the right wedge, so is its boost boostTest a f = f ∘ lorentzBoost a. (From lorentzBoost_mapsTo_rightWedge + the boost inverse.) This makes the wedge generating set {KrepL2 f : supp f ⊆ W_R} boost-closed.

Proof. By lorentzBoost, lorentzBoost_mapsTo_rightWedge, lorentzBoost_neg_boost. $\square$

Used by boostUnitary_mapsTo_wedgeGenSet.

Definition 299 (wedgeGenSet).  source ↗

The wedge generating set: the one-particle vectors KrepL2 f from real, wedge-supported, L² test functions. The physical generators of the wedge standard subspace — defined PURELY from wedge test functions (NOT from modular data), per the anti-circularity discipline.

Used by boostUnitary_mapsTo_wedgeGenSet, boostUnitary_mapsTo_wedgeSubspace, oneParticleBW_wedge_complete, oneParticle_hFlux_complete, component_hFlux_of_wedgeKMS_complete, WedgeKMSFlux_complete, hFlux_of_wedgeKMS_complete.

Lemma 300 (boostUnitary_mapsTo_wedgeGenSet).  source ↗

The wedge generating set is boost-closed: boostUnitary a maps it into itself. For ψ = KrepL2 f, boostUnitary a ψ = KrepL2(boostTest(−a) f) (sign lemma), and boostTest(−a) f is again real, wedge-supported (support_boostTest_subset), and L² (translation of an L² function).

Proof. By V, lorentzBoost, boostTest, Krep, Krep_boost, boostUnitary_KrepL2, rightWedge, support_boostTest_subset. $\square$

Used by boostUnitary_mapsTo_wedgeSubspace.

Lemma 301 (boostUnitary_mapsTo_wedgeSubspace).  source ↗

The wedge standard subspace 𝒦_W := closure (span_ℝ (wedge generators)) is BOOST-INVARIANT: boostUnitary a (𝒦_W) ⊆ 𝒦_W for every rapidity a. This is the V(a)𝒦 = 𝒦 the GPT-5-pro KMS-uniqueness route consumes — now PROVED axiom-free for the physically-defined wedge subspace (assembling the sign lemma + invariance engine + wedge geometry). The remaining inputs of the one-particle BW are the (formalizable) KMS-uniqueness lemma and the single labelled strip/KMS property of boostUnitary on these vectors.

Proof. By boostUnitary_mapsTo_closure_span, boostUnitary_mapsTo_wedgeGenSet. $\square$

Used by oneParticleBW_wedge_complete.

Definition 302 (StripKMSrvd).  source ↗

The CORRECT one-particle KMS condition — Rieffel–Van Daele (1977), Definition 3.4. Faithful to the source (refs/RieffelVanDaele): a strongly-continuous unitary group V satisfies the KMS condition w.r.t. the real subspace K (= 𝒦) iff for every ξ, η ∈ K there is f * bounded and continuous on the closed strip {−1 ≤ Im z ≤ 0}, analytic in the interior (DiffContOnCl on the open strip {−1 < Im < 0} + a uniform bound M), with boundary values * f(t) = ⟪η, V(t) ξ⟫ (bottom edge Im = 0), * f(t−i) = ⟪V(t) ξ, η⟫ (top edge Im = −1, the plain flip). …

Used by stripKMSrvd_boostUnitary, oneParticleBW_niceWedge, stripKMSrvd_real_midline, stripKMSrvd_halfStripReal, h1_of_stripKMSrvd, oneParticleBW_of_comparison, oneParticleBW_of_inputs, oneParticleBW_of_stripKMSrvd_density, and 6 more.

Lemma 303 (stripKMSrvd_real_midline).  source ↗

From RvD Definition 3.4 to the half-strip reality (RvD Proposition 3.5 applied to StripKMSrvd). The plain-flip top-edge value f(t − i) = ⟪V_t ξ, η⟫ of StripKMSrvd is automatically conj(f(t)): by conjugate symmetry ⟪V_t ξ, η⟫ = conj⟪η, V_t ξ⟫, and f(t) = ⟪η, V_t ξ⟫ (the corrected RvD Def 3.4 convention, orbit in the linear slot). So real_on_midline_of_conj_flip (RvD Prop 3.5) upgrades the witness to the half-strip KMS form: a bounded-holomorphic f with real-axis value f(t) = ⟪V_t ξ, η⟫ and f(t − i/2) REAL — exactly the reality input RvD Theorem 3.8 consumes (Δ^{1/2} = J on the standard subspace). This discharges the Prop-3.5 step of the hUniq proof from the labelled StripKMSrvd, axiom-free.

Proof. By negStrip, real_on_midline_of_conj_flip. $\square$

Used by stripKMSrvd_halfStripReal.

Definition 304 (HalfStripReal).  source ↗

The half-strip reality form of the KMS condition (the output of RvD Proposition 3.5): for ξ, η ∈ K, a bounded-holomorphic f on {−1 < Im z < 0} with f(t) = ⟪V_t ξ, η⟫ and f(t − i/2) REAL. This is the reality input RvD Theorem 3.8 actually consumes; it is PROVABLE from StripKMSrvd (stripKMSrvd_halfStripReal, via Prop 3.5), so labelling it instead of all of StripKMS shrinks the unproven surface to exactly the Theorem-3.8 core.

Used by stripKMSrvd_halfStripReal, oneParticleBW_of_comparison, oneParticleBW_of_inputs.

Lemma 305 (stripKMSrvd_halfStripReal).  source ↗

StripKMSrvd ⟹ HalfStripReal — RvD Proposition 3.5, packaged: the correct full-strip KMS condition yields the half-strip reality form (each pair’s witness made real on the mid-line).

Proof. By stripKMSrvd_real_midline. $\square$

Used by oneParticleBW_of_comparison.

Lemma 306 (h1_of_stripKMSrvd).  source ↗

The bottom-edge KMS reality h1 DISCHARGED from StripKMSrvd — RvD Theorem 3.8 g-function complete. For the orbit input η ∈ 𝒦 (strongly-continuous contraction, orbit staying in 𝒦) and ξ = √Rζ ∈ 𝒦, the g-function’s bottom edge g(t − i/2) = ⟪J·deviceVecF(t−i/2), gaussSmearC(t−i/2)⟫ is REAL. Assembly of the whole device g-function argument: the K.M.S. condition (hKMS) applied to the pair (gaussSmear, ξ_t = Δ^{it}ξ) (both in 𝒦: gaussSmear_mem_K, modUnitary_mapsTo_K) gives a bounded-holomorphic f with f(s) = ⟪ξ_t, V_s·gaussSmear⟫ (faithful RvD Def 3.4 convention) and — via the plain conjugate-flip (real_on_midline_of_conj_flip, RvD Prop 3.5) — f(t − i/2) REAL. …

Proof. By gFunction_bottom_real_of_faithful_kms, modUnitary, mem_K_iff_projK, modUnitary_mapsTo_K, gaussSmear, gaussSmear_mem_K, kmsHalfStrip, kmsHalfStripOpen, negStrip, real_on_midline_of_conj_flip. $\square$

Used by oneParticleBW_of_stripKMSrvd_density.

Definition 307 (ComparisonDatum).  source ↗

The comparison datum — the exact OUTPUT of RvD Theorem 3.8’s g-function: for every t, η ∈ 𝒦, and w ⊥ i𝒦 (projIK w = 0), ⟪w, V_t η⟫ = ⟪w, Δ^{it} η⟫. This is the single relation that the (source-garbled) g-pairing / Prop-3.7-device argument produces from the half-strip reality; everything downstream of it — V_t η = Δ^{it} η on 𝒦 (IsSeparating) and the lift to Δ^{it} = V_t (IsCyclic) — is the already-proven modUnitary_eq_of_orbit_compare.

Used by oneParticleBW_of_comparison, comparisonDatum_of_gConstancy.

Lemma 308 (oneParticleBW_of_comparison).  source ↗

Conditional one-particle BW with the TIGHTEST honest labelling. Everything provable is now proved: the Proposition-3.5 reduction (stripKMSrvd_halfStripReal), the Δ-invariance (modUnitary_mapsTo_K), and the operator assembly (modUnitary_eq_of_orbit_compare: separating ⇒ equal on 𝒦, cyclic ⇒ equal everywhere). The SOLE labelled hypothesis hCompare is the exact g-function output HalfStripReal ⟹ ComparisonDatum — the only genuinely source-garbled step of RvD Theorem 3.8. This is the minimal honest statement of “what remains unproven” on the hUniq discharge route.

Proof. By stripKMSrvd_halfStripReal, modUnitary_eq_of_orbit_compare, projIK, modUnitary_mapsTo_K. $\square$

Used by oneParticleBW_of_inputs.

Definition 309 (GConstancy).  source ↗

The g-function constancy output (RvD Theorem 3.8, the analytic conclusion): for ξ, η ∈ 𝒦, ⟪V_t η, Δ^{it} J ξ⟫ = ⟪η, J ξ⟫. This is exactly what the (analytic) g-function g(z) = ⟨h(z), J d_z(R) ζ⟩ produces by being constant on the half-strip — g(t) = ⟨U_t η, JΔ^{it}ξ⟩ (top edge, real), g(0) = ⟨η, Jξ⟩ — using Δ^{it}J = JΔ^{it} (modConj_commute_modUnitary).

Used by comparisonDatum_of_gConstancy, gConstancy_of_inputs.

Lemma 310 (comparisonDatum_of_gConstancy).  source ↗

The g-function constancy output yields ComparisonDatum — the operator-algebra wrapper of RvD Theorem 3.8, reducing the discharge to the analytic g-constancy alone. Given ⟪V_t η, Δ^{it} J ξ⟫ = ⟪η, J ξ⟫ (∀ξ,η∈𝒦): for w ⊥ i𝒦 set ξ = Δ^{−it}(J w) ∈ 𝒦 (J w ∈ 𝒦 since J𝒦 = (i𝒦)^⊥, Δ^{−it} preserves 𝒦). Then J ξ = Δ^{−it} w and Δ^{it} J ξ = w (JΔ^{it}=Δ^{it}J + group law), so g-constancy reads ⟪V_t η, w⟫ = ⟪η, Δ^{−it} w⟫ = ⟪Δ^{it} η, w⟫ (adjoint); conjugating gives ⟪w, V_t η⟫ = ⟪w, Δ^{it} η⟫. The ⟪η,Jξ⟫ right-hand side carries the Δ-side automatically — no separate Δ-version needed. So the ONLY remaining unproven step is the analytic g-constancy itself.

Proof. By projK, projIK, modUnitary, modUnitary_zero, modUnitary_add, modUnitary_adjoint, mem_K_iff_projK, modConj, modConj_sq, projK_modConj_eq_self_of_perp_IK, modUnitary_mapsTo_K, modConj_commute_modUnitary. $\square$

Used by oneParticleBW_of_inputs.

Lemma 311 (gConstancy_of_inputs).  source ↗

Full GConstancy from the two named RvD inputs (the end-to-end assembly of the device g-function discharge). Given a strongly-continuous contraction group V (hcont/hbd/hgrp/hV0), the orbit invariance of 𝒦 (hKinv), the bottom-edge KMS reality h1 (the mid-line Im z = −1/2 reality of the device g-function, supplied by HalfStripReal), and the √R-range density in 𝒦 hdense (every ξ ∈ 𝒦 is a limit of √R ζ_k ∈ 𝒦, available since R is injective), the GConstancy proposition holds. Chains gConstancy_eta_of_bottom (η-side, h1) → gConstancy_xi_of_density (ξ-side, hdense). …

Proof. By gConstancy_eta_of_bottom, gConstancy_xi_of_density. $\square$

Used by oneParticleBW_of_inputs.

Lemma 312 (oneParticleBW_of_inputs).  source ↗

One-particle Bisognano–Wichmann via the device g-function, reduced to the two named RvD inputs. The modular flow IS the candidate flow, modUnitary S t = V t, GIVEN: the strongly-continuous contraction group V with 𝒦-invariance (hInv), the correct full-strip KMS condition (hKMS : StripKMSrvd), and the two RvD Theorem 3.8 inputs that drive the g-function — the bottom-edge KMS reality h1 (mid-line Im z = −1/2 reality) and the √R-range density in 𝒦 hdense. gConstancy_of_inputs yields the full GConstancy, comparisonDatum_of_gConstancy the ComparisonDatum, and oneParticleBW_of_comparison the flow identification. …

Proof. By HalfStripReal, oneParticleBW_of_comparison, comparisonDatum_of_gConstancy, gConstancy_of_inputs. $\square$

Used by oneParticleBW_of_stripKMSrvd_density.

Lemma 313 (oneParticleBW_of_stripKMSrvd_density).  source ↗

One-particle Bisognano–Wichmann from the KMS condition — h1 DISCHARGED, only hdense named. modUnitary S t = V t for a strongly-continuous contraction group V with 𝒦-invariance (hInv) and the correct RvD Def 3.4 KMS condition (hKMS : StripKMSrvd), GIVEN only the √R-range density hdense. The bottom-edge KMS reality — the last analytic input of RvD Theorem 3.8’s device g-function — is no longer a labelled hypothesis: it is derived from hKMS via h1_of_stripKMSrvd (the complete f-transfer assembly). So the entire hUniq discharge now rests on a SINGLE named analytic input, hdense (the √R-range density in 𝒦), with the KMS condition supplied as the genuine RvD Def 3.4 hypothesis.

Proof. By h1_of_stripKMSrvd, oneParticleBW_of_inputs, deviceVecF, modConjBilin, gaussSmearC. $\square$

Used by oneParticleBW_complete.

Lemma 314 (oneParticleBW_complete).  source ↗

One-particle Bisognano–Wichmann from the KMS condition — the COMPLETE, unconditional discharge. modUnitary S t = V t for a strongly-continuous contraction group V with 𝒦-invariance (hInv) and the correct RvD Def 3.4 KMS condition (hKMS : StripKMSrvd) — with NO remaining named analytic input. Both RvD Theorem 3.8 inputs of the device g-function are now theorems: the bottom-edge KMS reality h1 (via h1_of_stripKMSrvd) and the √R-range density hdense (via rvdSqrtR_range_dense_in_K). This is the full, axiom-free formalization of RvD Theorem 3.8: Δ^{it} is the unique strongly-continuous unitary group carrying 𝒦 onto 𝒦 and satisfying the KMS condition — i.e. …

Proof. By oneParticleBW_of_stripKMSrvd_density, rvdSqrtR_range_dense_in_K. $\square$

Used by oneParticleBW_niceWedge, oneParticleBW_wedge_complete.

Lemma 315 (oneParticleBW_wedge_complete).  source ↗

One-particle Bisognano–Wichmann for the WEDGE — KMS-uniqueness DERIVED (no bundled hUniq). modUnitary S t = boostUnitary(−2π t) for the wedge standard subspace 𝒦_W, given ONLY the carrier identity (hcarrier), V = boostUnitary(−2π·) (hVboost), and the genuine RvD Def 3.4 KMS condition hKMS : StripKMSrvd V 𝒦_W. Unlike oneParticleBW_wedge, the KMS-uniqueness is no longer a bundled opaque hypothesis but is DERIVED via oneParticleBW_complete (the machine-checked RvD Theorem 3.8 discharge), and the labelled KMS predicate is the genuine, non-vacuous StripKMSrvd rather than the trivially-satisfiable StripKMS. …

Proof. By boostUnitary_add_apply, boostUnitary_zero_apply, continuous_boostUnitary_apply, boostUnitary_mapsTo_wedgeSubspace, oneParticleBW_complete, projK, mem_K_iff_projK, gaussSmear, gaussSmear_mem_K. $\square$

Used by oneParticle_hFlux_complete.

Lemma 316 (hasDerivAt_modularEnergy_of_boost).  source ↗

Modular energy = boost energy (derivative level), via BW. Given the one-particle BW modUnitary S t u = boostUnitary(−2π t) u, the modular-energy correlation t ↦ ⟪ξ, Δ^{it} ξ⟫ coincides with the boost-energy correlation t ↦ ⟪ξ, boostUnitary(−2π t) ξ⟫ as functions of t, so their derivatives at 0 agree. The modular energy kd = d/dt⟪ξ,Δ^{it}ξ⟫|₀ (the object feeding hFlux) therefore equals the boost energy derivative — reducing hFlux (modular energy = stress flux) to the standard boost-charge = stress-flux identity δ⟨boost⟩ = ∫λ T_kk, the one remaining labelled geometric fact. No unbounded generator needed: the equality is a direct congruence from BW.

Proof. Immediate from the definitions. $\square$

Used by modularEnergy_eq_stressFlux.

Lemma 317 (modularEnergy_eq_stressFlux).  source ↗

One-particle hFlux: the modular energy IS (2π/ℏ)·(stress flux) — hFlux derived from the BW plus the labelled boost-charge identity. hBoostCharge is the single remaining labelled input on this path: the boost-charge = stress-flux identity δ⟨boost⟩ = (2π/ℏ)·T_kk (the conserved Killing charge of the boost equals the stress-tensor flux — standard field theory, needs the field stress tensor which the project has not built, so labelled). Composed with the proved hasDerivAt_modularEnergy_of_boost (modular energy = boost energy, via BW), it gives the modular energy derivative = (2π/ℏ)·T_kk — exactly the hFlux of qiqt_bekenstein_gives_gr at the one-particle (Hilbert) level. …

Proof. By hasDerivAt_modularEnergy_of_boost. $\square$

Used by oneParticle_hFlux_complete.

Lemma 318 (oneParticle_hFlux_complete).  source ↗

oneParticle_hFlux with KMS-uniqueness DERIVED — the genuine StripKMSrvd replaces the bundled opaque hUniq+StripKMS. The modular-energy derivative t ↦ ⟪ξ, Δ^{it}ξ⟫ equals the boost-charge derivative i·(2π/ℏ)·T_kk, with the BW identification modUnitary = boostUnitary now derived via oneParticleBW_wedge_complete (= oneParticleBW_complete, the RvD Theorem 3.8 discharge).

Proof. By oneParticleBW_wedge_complete, modularEnergy_eq_stressFlux. $\square$

Used by component_hFlux_of_wedgeKMS_complete.

Lemma 319 (component_hFlux_of_wedgeKMS_complete).  source ↗

component_hFlux_of_wedgeKMS with KMS-uniqueness DERIVED — the component-level hFlux kd = (2π/ℏ)·T_kk resting on the genuine StripKMSrvd (not the bundled opaque hUniq+vacuous StripKMS). The BW identification is derived via oneParticleBW_complete (RvD Theorem 3.8).

Proof. By oneParticle_hFlux_complete. $\square$

Used by hFlux_of_wedgeKMS_complete.

← all sections · ← OneParticle · SchwartzDecay →