Fock · section of the QIQT-H book

QIQTH.Fock.CyclicWitness

← all sections · ← BoostKMS · FreeFieldHFlux →

Fock · entries 209–230 of 1000

Definition 209 (bump1W).  source ↗

A width-R 1D bump (rIn = R/2, rOut = R).

bump1W R c  :=  {rIn:=R/2,rOut:=R,rIn_pos:=⋯ ,rIn_lt_rOut:=⋯ }\mathrm{bump1W}\,R\,c \;:=\; \{\mathrm{rIn} :=R / 2 , \mathrm{rOut} :=R , \mathrm{rIn\_pos} :=\cdots , \mathrm{rIn\_lt\_rOut} :=\cdots \}

Used by bump1W_rOut, bump1W_rIn, bumpRealW, bumpRealW_contDiff, bumpCW_contDiff, bumpRealW_support_subset, minkowskiFourier_bumpCW, Krep_bumpCW_zero, and 3 more.

Lemma 210 (bump1W_rOut).  source ↗

(bump1W R hR c).rOut=R(\href{/browser/qiqth-fock-cyclicwitness#d-qiqth-fock-cyclicwitness-bump1w}{\mathrm{bump1W}}\,R\,\mathrm{hR}\,c).\mathrm{rOut} = R

Proof. Immediate from the definitions. □\square

Used by bumpRealW_support_subset, bump1W_fourier_ne_zero.

Lemma 211 (bump1W_rIn).  source ↗

(bump1W R hR c).rIn=R/2(\href{/browser/qiqth-fock-cyclicwitness#d-qiqth-fock-cyclicwitness-bump1w}{\mathrm{bump1W}}\,R\,\mathrm{hR}\,c).\mathrm{rIn} = R / 2

Proof. Immediate from the definitions. □\square

Used by bump1W_fourier_ne_zero.

Definition 212 (bumpRealW).  source ↗

The width-R 2D product bump on V = Fin 2 → ℝ.

bump R cT cX x  :=  (bump1W R hR cT) (x 0)⋅(bump1W R hR cX) (x 1)\mathrm{bump}\,R\,\mathrm{cT}\,\mathrm{cX}\,x \;:=\; (\href{/browser/qiqth-fock-cyclicwitness#d-qiqth-fock-cyclicwitness-bump1w}{\mathrm{bump1W}}\,R\,\mathrm{hR}\,\mathrm{cT})\,(x\,0) \cdot (\href{/browser/qiqth-fock-cyclicwitness#d-qiqth-fock-cyclicwitness-bump1w}{\mathrm{bump1W}}\,R\,\mathrm{hR}\,\mathrm{cX})\,(x\,1)

Used by bumpCW, bumpRealW_contDiff, bumpRealW_support_subset, bumpCW_hasCompactSupport.

Definition 213 (bumpCW).  source ↗

bumpCW R cT cX x  :=  (bump R hR cT cX x)\mathrm{bumpCW}\,R\,\mathrm{cT}\,\mathrm{cX}\,x \;:=\; (\href{/browser/qiqth-fock-cyclicwitness#d-qiqth-fock-cyclicwitness-bumprealw}{\mathrm{bump}}\,R\,\mathrm{hR}\,\mathrm{cT}\,\mathrm{cX}\,x)

Used by bumpCW_contDiff, bumpCW_continuous, bumpCW_hasCompactSupport, bumpNiceTestW, niceWedgeCyclic_bumpW, minkowskiFourier_bumpCW, Krep_bumpCW_zero, Krep_bumpCW_ne_zero_of.

Lemma 214 (bumpRealW_contDiff).  source ↗

(bump R hR cT cX)∈C∞({\href{/browser/qiqth-fock-cyclicwitness#d-qiqth-fock-cyclicwitness-bumprealw}{\mathrm{bump}}\,R\,\mathrm{hR}\,\mathrm{cT}\,\mathrm{cX}})\in C^{\infty}

Proof. By bump1W. □\square

Used by bumpCW_contDiff.

Lemma 215 (bumpCW_contDiff).  source ↗

(bumpCW R hR cT cX)∈C∞({\href{/browser/qiqth-fock-cyclicwitness#d-qiqth-fock-cyclicwitness-bumpcw}{\mathrm{bumpCW}}\,R\,\mathrm{hR}\,\mathrm{cT}\,\mathrm{cX}})\in C^{\infty}

Proof. By bump1W, bumpRealW_contDiff. □\square

Used by bumpCW_continuous, niceWedgeCyclic_bumpW.

Lemma 216 (bumpCW_continuous).  source ↗

Continuous (bumpCW R hR cT cX)\mathrm{Continuous}\,(\href{/browser/qiqth-fock-cyclicwitness#d-qiqth-fock-cyclicwitness-bumpcw}{\mathrm{bumpCW}}\,R\,\mathrm{hR}\,\mathrm{cT}\,\mathrm{cX})

Proof. By bumpCW_contDiff. □\square

Used by Krep_bumpCW_ne_zero_of.

Lemma 217 (bumpRealW_support_subset).  source ↗

support (bump R hR cT cX)⊆{x∣∣x 0−cT∣≤R∧∣x 1−cX∣≤R}\mathrm{support}\,(\href{/browser/qiqth-fock-cyclicwitness#d-qiqth-fock-cyclicwitness-bumprealw}{\mathrm{bump}}\,R\,\mathrm{hR}\,\mathrm{cT}\,\mathrm{cX}) \subseteq \{x||x\,0 - \mathrm{cT}| \le R \wedge |x\,1 - \mathrm{cX}| \le R\}

Proof. By bump1W, bump1W_rOut. □\square

Used by bumpCW_hasCompactSupport.

Lemma 218 (bumpCW_hasCompactSupport).  source ↗

HasCompactSupport (bumpCW R hR cT cX)\mathrm{HasCompactSupport}\,(\href{/browser/qiqth-fock-cyclicwitness#d-qiqth-fock-cyclicwitness-bumpcw}{\mathrm{bumpCW}}\,R\,\mathrm{hR}\,\mathrm{cT}\,\mathrm{cX})

Proof. By bumpRealW, bumpRealW_support_subset. □\square

Used by niceWedgeCyclic_bumpW, Krep_bumpCW_ne_zero_of.

Definition 219 (bumpNiceTestW).  source ↗

A width-R wedge-supported nice generator centred at (0, cX) with 2R < cX (margin δ = cX − 2R).

bumpNiceTestW m R cX  :=  {f:=bumpCW R hR 0 cX,cont:=⋯ ,cpt:=⋯ ,δ:=cX−2⋅R,hδ:=⋯ ,margin:=⋯ ,real:=⋯ ,memLp:=⋯ }\mathrm{bumpNiceTestW}\,m\,R\,\mathrm{cX} \;:=\; \{f :=\href{/browser/qiqth-fock-cyclicwitness#d-qiqth-fock-cyclicwitness-bumpcw}{\mathrm{bumpCW}}\,R\,\mathrm{hR}\,0\,\mathrm{cX} , \mathrm{cont} :=\cdots , \mathrm{cpt} :=\cdots , \delta :=\mathrm{cX} - 2 \cdot R , h\delta :=\cdots , \mathrm{margin} :=\cdots , \mathrm{real} :=\cdots , \mathrm{memLp} :=\cdots \}

Used by niceWedgeCyclic_bumpW.

Lemma 220 (niceWedgeCyclic_bumpW).  source ↗

NiceWedgeCyclic from the width-R bump generator, modulo its amplitude being nonzero.

m≠0→2⋅R<cX→¬K m (⋯ .toSchwartzMap ⋯ )=[vol]0→NiceWedgeCyclic mm \ne 0 \to 2 \cdot R < \mathrm{cX} \to \neg \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,(\cdots .\mathrm{toSchwartzMap}\,\cdots ) =[\mathrm{vol}] 0 \to \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgecyclic}{\mathrm{NiceWedgeCyclic}}\,m

Proof. By niceWedgeCyclic_of_fourier_ne_zero, bumpNiceTestW, fourierL2_Krep_ne_zero. □\square

Used by niceWedgeCyclic_of_bumpW_fourier_ne_zero.

Lemma 221 (minkowskiFourier_bumpCW).  source ↗

The width-R amplitude factorizes (Fubini), mirroring minkowskiFourier_bumpC.

F (bumpCW R hR cT cX) p=(∫(y:R),exp⁡ (−i⋅(p 0⋅y))⋅((bump1W R hR cT) y))⋅∫(y:R),exp⁡ (i⋅(p 1⋅y))⋅((bump1W R hR cX) y)\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-minkowskifourier}{\mathcal{F}}\,(\href{/browser/qiqth-fock-cyclicwitness#d-qiqth-fock-cyclicwitness-bumpcw}{\mathrm{bumpCW}}\,R\,\mathrm{hR}\,\mathrm{cT}\,\mathrm{cX})\,p = (\int (y : \mathbb{R}), \exp\,(-i \cdot (p\,0 \cdot y)) \cdot ((\href{/browser/qiqth-fock-cyclicwitness#d-qiqth-fock-cyclicwitness-bump1w}{\mathrm{bump1W}}\,R\,\mathrm{hR}\,\mathrm{cT})\,y)) \cdot \int (y : \mathbb{R}), \exp\,(i \cdot (p\,1 \cdot y)) \cdot ((\href{/browser/qiqth-fock-cyclicwitness#d-qiqth-fock-cyclicwitness-bump1w}{\mathrm{bump1W}}\,R\,\mathrm{hR}\,\mathrm{cX})\,y)

Proof. By minkowskiDot. □\square

Used by Krep_bumpCW_zero.

Lemma 222 (Krep_bumpCW_zero).  source ↗

The width-R bump amplitude at θ = 0, factored.

K m (bumpCW R hR cT cX) 0=1/2⋅((∫(y:R),exp⁡ (−i⋅(m⋅y))⋅((bump1W R hR cT) y))⋅∫(y:R),((bump1W R hR cX) y))\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,(\href{/browser/qiqth-fock-cyclicwitness#d-qiqth-fock-cyclicwitness-bumpcw}{\mathrm{bumpCW}}\,R\,\mathrm{hR}\,\mathrm{cT}\,\mathrm{cX})\,0 = 1 / \sqrt 2 \cdot ((\int (y : \mathbb{R}), \exp\,(-i \cdot (m \cdot y)) \cdot ((\href{/browser/qiqth-fock-cyclicwitness#d-qiqth-fock-cyclicwitness-bump1w}{\mathrm{bump1W}}\,R\,\mathrm{hR}\,\mathrm{cT})\,y)) \cdot \int (y : \mathbb{R}), ((\href{/browser/qiqth-fock-cyclicwitness#d-qiqth-fock-cyclicwitness-bump1w}{\mathrm{bump1W}}\,R\,\mathrm{hR}\,\mathrm{cX})\,y))

Proof. By minkowskiFourier_bumpCW, massShell, minkowskiFourier. □\square

Used by Krep_bumpCW_ne_zero_of.

Lemma 223 (Krep_bumpCW_ne_zero_of).  source ↗

The width-R amplitude is ≢ 0 as soon as the 1D integral ∫ e^{−imy}·bump1W R cT(y) dy ≠ 0.

∫(y:R),exp⁡ (−i⋅(m⋅y))⋅((bump1W R hR cT) y)≠0→¬K m (bumpCW R hR cT cX)=[vol]0\int (y : \mathbb{R}), \exp\,(-i \cdot (m \cdot y)) \cdot ((\href{/browser/qiqth-fock-cyclicwitness#d-qiqth-fock-cyclicwitness-bump1w}{\mathrm{bump1W}}\,R\,\mathrm{hR}\,\mathrm{cT})\,y) \ne 0 \to \neg \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,(\href{/browser/qiqth-fock-cyclicwitness#d-qiqth-fock-cyclicwitness-bumpcw}{\mathrm{bumpCW}}\,R\,\mathrm{hR}\,\mathrm{cT}\,\mathrm{cX}) =[\mathrm{vol}] 0

Proof. By bumpCW_continuous, bumpCW_hasCompactSupport, Krep_bumpCW_zero, V, Krep_continuous. □\square

Used by niceWedgeCyclic_of_bumpW_fourier_ne_zero.

Lemma 224 (fourier_re_eq).  source ↗

The real part of the 1D Fourier integrand for an arbitrary real weight g: Re(e^{−imy}·g(y)) = cos(my)·g(y).

(exp⁡ (−i⋅(m⋅y))⋅(g y)).re=cos⁡ (m⋅y)⋅g y(\exp\,(-i \cdot (m \cdot y)) \cdot (g\,y)).\mathrm{re} = \cos\,(m \cdot y) \cdot g\,y

Proof. Immediate from the definitions. □\square

Used by bump1W_fourier_ne_zero.

Lemma 225 (bump1W_fourier_ne_zero).  source ↗

The width-R 1D bump Fourier integral is nonzero whenever m·R < π/2: its real part ∫ cos(my)·bump1W R 0(y) dy > 0, since cos(my) > 0 on the support |y| < R (as |my| ≤ mR < π/2).

0<m→∀(hR:0<R),m⋅R<π/2→∫(y:R),exp⁡ (−i⋅(m⋅y))⋅((bump1W R hR 0) y)≠00 < m \to \forall (\mathrm{hR} : 0 < R), m \cdot R < \pi / 2 \to \int (y : \mathbb{R}), \exp\,(-i \cdot (m \cdot y)) \cdot ((\href{/browser/qiqth-fock-cyclicwitness#d-qiqth-fock-cyclicwitness-bump1w}{\mathrm{bump1W}}\,R\,\mathrm{hR}\,0)\,y) \ne 0

Proof. By bump1W_rOut, bump1W_rIn, fourier_re_eq. □\square

Used by niceWedgeCyclic_pos_mass.

Lemma 226 (niceWedgeCyclic_of_bumpW_fourier_ne_zero).  source ↗

NiceWedgeCyclic from a width-R bump whose 1D amplitude is nonzero.

m≠0→2⋅R<cX→∫(y:R),exp⁡ (−i⋅(m⋅y))⋅((bump1W R hR 0) y)≠0→NiceWedgeCyclic mm \ne 0 \to 2 \cdot R < \mathrm{cX} \to \int (y : \mathbb{R}), \exp\,(-i \cdot (m \cdot y)) \cdot ((\href{/browser/qiqth-fock-cyclicwitness#d-qiqth-fock-cyclicwitness-bump1w}{\mathrm{bump1W}}\,R\,\mathrm{hR}\,0)\,y) \ne 0 \to \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgecyclic}{\mathrm{NiceWedgeCyclic}}\,m

Proof. By niceWedgeCyclic_bumpW, Krep_bumpCW_ne_zero_of. □\square

Used by niceWedgeCyclic_pos_mass.

Lemma 227 (niceWedgeCyclic_pos_mass).  source ↗

THE CYCLIC REEH–SCHLIEDER INPUT, UNCONDITIONALLY DISCHARGED FOR ALL m > 0, axiom-free. NiceWedgeCyclic m holds with no hypotheses for every positive mass. Take the width-R wedge bump with R = π/(4m), centred at (0, 2R+1): then m·R = π/4 < π/2, so cos(m y) > 0 on its whole support and the amplitude’s real part ∫ cos(m y)·bump1W R(y) dy > 0 (bump1W_fourier_ne_zero); the complete Wiener–Tauberian machinery does the rest. The free-field one-particle Bisognano–Wichmann’s cyclic Reeh–Schlieder input is now a theorem, not a hypothesis, for the full physical mass range m > 0 — every step (Wiener theorem, FT-holomorphy, L²↔L¹ agreement, witness, amplitude) machine-checked and axiom-free. …

0<m→NiceWedgeCyclic m0 < m \to \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgecyclic}{\mathrm{NiceWedgeCyclic}}\,m

Proof. By bump1W_fourier_ne_zero, niceWedgeCyclic_of_bumpW_fourier_ne_zero. □\square

Used by oneParticleBW_niceWedge_unconditional, freeField_modularEnergy_eq_boostCharge, freeField_oneParticle_hFlux, freeField_component_hFlux, freeField_kd_conclusion, qiqt_gr_freefield.

Lemma 228 (strip_eqZero_of_top_edge_zero).  source ↗

Strip boundary-uniqueness (top edge zero ⟹ bottom edge zero). A function Φ holomorphic on the open strip {−1 < Im z < 0}, continuous and bounded on the closed strip, that vanishes on the entire top edge (Φ(t) = 0 ∀ real t), vanishes on the bottom edge too (Φ(t − i) = 0 ∀ t). Proof: the asymmetric Hadamard three-lines bound with top constant 0 gives ‖Φ z‖ ≤ 0^{1−s}·B^{s} (s = −Im z), which is 0 for every interior point (s < 1), so Φ vanishes on the open strip; the bottom edge then follows by continuity (approach t − i from inside). This is the modular/KMS uniqueness that the separating proof needs.

DifferentiableOn C Φ (im−1′(−1,0))→ContinuousOn Φ (im−1′[−1,0])→BddAbove (norm∘Φ′′im−1′[−1,0])→(∀(t:R),Φ t=0)→∀(t:R),Φ (t−i)=0\mathrm{DifferentiableOn}\,\mathbb{C}\,\Phi\,(\mathrm{im} ^{-1}{}' ({-1},{0})) \to \mathrm{ContinuousOn}\,\Phi\,(\mathrm{im} ^{-1}{}' [{-1},{0}]) \to \mathrm{BddAbove}\,(\mathrm{norm} \circ \Phi '' \mathrm{im} ^{-1}{}' [{-1},{0}]) \to (\forall (t : \mathbb{R}), \Phi\,t = 0) \to \forall (t : \mathbb{R}), \Phi\,(t - i) = 0

Proof. Immediate from the definitions. □\square

Used by niceWedgeSeparating_pos_mass.

Lemma 229 (niceWedgeSeparating_pos_mass).  source ↗

THE SEPARATING Reeh–Schlieder input, DISCHARGED for all m > 0, axiom-free (Pauli–Jordan). NiceWedgeSeparating m: the only v with both v and i·v in the nice-core wedge subspace K is v = 0 (symplectic non-degeneracy / no nonzero complex line). Proof — pure modular/KMS: from the boost-KMS witness (stripKMSrvd_closure) take F_vv for (v,v) and F_c for (i·v, v); both v, i·v ∈ K = closure(genSet). On the TOP edge F_c(t) = ⟪v, U_t(i v)⟫ = i⟪v, U_t v⟫ = i·F_vv(t), so D := F_c − i·F_vv vanishes on the whole top edge. D is holomorphic on the strip, continuous and bounded on its closure, so by strip boundary-uniqueness (strip_eqZero_of_top_edge_zero) it vanishes on the BOTTOM edge too. …

0<m→NiceWedgeSeparating m0 < m \to \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgeseparating}{\mathrm{NiceWedgeSeparating}}\,m

Proof. By niceWedgeGenSet, niceWedgeClosedSubmodule, niceWedgeClosedSubmodule_coe, stripKMSrvd_closure, strip_eqZero_of_top_edge_zero, boostUnitary, boostUnitary_zero_apply. □\square

Used by oneParticleBW_niceWedge_unconditional, freeField_modularEnergy_eq_boostCharge, freeField_oneParticle_hFlux, freeField_component_hFlux, freeField_kd_conclusion, qiqt_gr_freefield.

Theorem 230 (oneParticleBW_niceWedge_unconditional).  source ↗

THE free-field one-particle Bisognano–Wichmann — FULLY UNCONDITIONAL, axiom-free. For every mass m > 0 and every candidate boost representation V t = boostUnitary(2πt), the modular flow of the nice-core wedge standard subspace equals the boost: modUnitary S t = V t, with NO Reeh–Schlieder hypotheses whatsoever. BOTH analytic inputs are now discharged internally and unconditionally: niceWedgeSeparating_pos_mass (Pauli–Jordan symplectic non-degeneracy, via the KMS uniqueness argument) and niceWedgeCyclic_pos_mass (wedge-totality, via the Wiener–Tauberian theorem). …

(∀(t:R)(x:(Lp C 2 vol)),(V t) x=(U (2⋅π⋅t)) x)→∀(t:R),Δ (K m ⋯ ⋯ ) t=V t(\forall (t : \mathbb{R}) (x : (\mathrm{Lp}\,\mathbb{C}\,2\,\mathrm{vol})), (V\,t)\,x = (\href{/browser/qiqth-fock-oneparticle#d-qiqth-fock-oneparticle-boostunitary}{U}\,(2 \cdot \pi \cdot t))\,x) \to \forall (t : \mathbb{R}), \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 = V\,t

Proof. By oneParticleBW_niceWedge_reehSchlieder. □\square

Used by freeField_modularEnergy_eq_boostCharge.

← all sections · ← BoostKMS · FreeFieldHFlux →