QIQTH.KMSCorrelation

← all sections · ← KGStressConservation · LocalizedMode →

KMSCorrelation · entries 469–489 of 1000

Lemma 469 (corrC_bdd_halfStrip).  source ↗

Uniform bound of the KMS correlation on the HALF strip {−1/2 ≤ Im z ≤ 0} (the strip RvD Thm 3.8 / Prop 3.5 actually use): ‖corrC ξ V n η z‖ ≤ ‖ξ‖·e^{n/4}·‖η‖·√(π/n), since (Im z)² ≤ 1/4 there. The bounded-holomorphic input the correct-strip g-function argument consumes (with diffContOnCl_corrC restricted to kmsHalfStripOpen and eqOn_of_im_zero_edge_halfStrip).

Proof. By corrC_norm_le. $\square$

Used by gFunction_bottom_real_of_kms_match.

Lemma 470 (gFunction_eq_zero_const).  source ↗

The device g-function is constant on the real axis (RvD Theorem 3.8 constancy, the analytic heart of the GConstancy output): if the device g-function g(z) = ⟪J·d_z(R)ζ, V_z η_n⟫ is real on BOTH half-strip edges Im z = 0 and Im z = −1/2, then g(t) = g(0) for every real t. The g-function is bounded-holomorphic (diffContOnCl_gFunction, gFunction_norm_le + gaussSmearC_norm_le give the uniform bound 2√2‖ζ‖·e^{n/4}‖η‖√(π/n) since (Im z)² ≤ 1/4), so the two-edge half-strip Phragmén–Lindelöf (eqConst_of_im_zero_halfStrip) forces it constant on the open half-strip; continuity to the closure (Set.EqOn.closure) propagates the constant to the real axis. …

Proof. By gFunction_norm_le, diffContOnCl_gFunction, gaussSmearC_norm_le, kmsHalfStripOpen, eqConst_of_im_zero_halfStrip. $\square$

Used by gConstancy_entire.

Lemma 471 (gConstancy_entire).  source ↗

GConstancy for the entire vectors (RvD Theorem 3.8 output, assembled): from the g-function constancy g(t) = g(0) and the edge value identities, ⟪V_t η_n, Δ^{it}(J ξ)⟫ = ⟪η_n, J ξ⟫ for ξ = √R ζ, η_n = gaussSmear. gFunction_eq_zero_const gives g(t) = g(0); gFunction_real_eq evaluates the top edge g(t) = ⟪Δ^{it}(Jξ), V_t η_n⟫, gFunction_zero the origin g(0) = ⟪Jξ, η_n⟫; conjugating (inner_conj_symm) flips both slots to the GConstancy form. This is exactly GConstancy S V evaluated at (η_n, √R ζ) — the analytic conclusion of RvD Theorem 3.8, modulo the two edge-reality inputs.

Proof. By gFunction_eq_zero_const, gFunction_zero, gFunction_real_eq. $\square$

Used by gConstancy_entire_of_bottom.

Lemma 472 (gFunction_top_edge_real_all).  source ↗

Top-edge reality of the g-function, ∀ z form (the h0 input to gFunction_eq_zero_const): if ξ = √R ζ ∈ 𝒦 and the V-orbit V_s(gaussSmear) stays in 𝒦, then Im g(z) = 0 on the whole edge Im z = 0. Any z with Im z = 0 is real (z = ↑z.re), so this is just gFunction_top_edge_real at t = z.re. Geometric — the always-available top edge of the device g-function.

Proof. By gFunction_top_edge_real. $\square$

Used by gConstancy_entire_of_bottom.

Lemma 473 (gConstancy_entire_of_bottom).  source ↗

GConstancy for the entire vectors, reduced to the BOTTOM-EDGE KMS reality (the precise residual of the RvD Theorem 3.8 discharge). With the geometric inputs (ξ = √R ζ ∈ 𝒦, the V-orbit stays in 𝒦) the top-edge reality is automatic (gFunction_top_edge_real_all), so the ENTIRE analytic g-function argument collapses to a single hypothesis: h1, the reality of g on the mid-line Im z = −1/2. That mid-line reality is exactly the KMS input (HalfStripReal / StripKMSrvd). Conclusion: ⟪V_t η_n, Δ^{it}(Jξ)⟫ = ⟪η_n, Jξ⟫ (GConstancy at the entire vector η_n and ξ = √R ζ) — everything but the bottom-edge KMS step is now machine-checked.

Proof. By gConstancy_entire, gFunction_top_edge_real_all. $\square$

Used by gConstancy_eta_of_bottom.

Lemma 474 (gConstancy_of_entireVec_limit).  source ↗

GConstancy density: GConstancy holds for η if it holds for every normalised entire vector entireVec V n η (n → ∞). The entire vectors converge to η (entireVec_tendsto), and both sides ⟪V_t·, w⟫, ⟪·, w⟫ are continuous, so the constant equality passes to the limit (tendsto_nhds_unique). This lifts the entire-vector GConstancy (gConstancy_entire_of_bottom) to the genuine η ∈ 𝒦.

Proof. By gaussSmear, entireVec_tendsto. $\square$

Used by gConstancy_eta_of_bottom.

Lemma 475 (gConstancy_real_smul).  source ↗

GConstancy is real-scalar linear in the vector: if GConstancy holds for v, it holds for c • v (c : ℝ). V_t is ℂ-linear (so commutes with the real scalar) and ⟪·, w⟫ pulls out conj(c) = c (inner_smul_left, c real). This bridges gConstancy_entire_of_bottom (for gaussSmear) to the normalised entire vector entireVec = √(n/π) • gaussSmear the density limit consumes.

Proof. Immediate from the definitions. $\square$

Used by gConstancy_eta_of_bottom.

Lemma 476 (gConstancy_eta_of_bottom).  source ↗

GConstancy for η ∈ 𝒦 reduced to the bottom-edge KMS reality (the full density+scaling closeout): ⟪V_t η, Δ^{it}(Jξ)⟫ = ⟪η, Jξ⟫ for ξ = √R ζ, given the geometric inputs (ξ ∈ 𝒦, the orbit stays in 𝒦 for every entire vector) and the bottom-edge reality h1 for every entire vector. Chains gConstancy_entire_of_bottom (GConstancy for gaussSmear V n η) → gConstancy_real_smul (scale to the normalised entireVec = √(n/π)·gaussSmear) → gConstancy_of_entireVec_limit (n → ∞, entireVec → η). So the FULL GConstancy at η (any η ∈ 𝒦 with the orbit hypotheses) now rests only on the bottom-edge mid-line KMS reality — the single labelled input of RvD Theorem 3.8.

Proof. By gConstancy_entire_of_bottom, gConstancy_of_entireVec_limit, gConstancy_real_smul, entireVec. $\square$

Used by gConstancy_of_inputs.

Lemma 477 (gConstancy_of_tendsto_xi).  source ↗

GConstancy is closed in ξ (continuity in the second-slot vector): if GConstancy at (η, ξ_k) holds for a sequence ξ_k → ξ, it holds at (η, ξ). Both sides ⟪V_t η, Δ^{it}(J·)⟫ and ⟪η, J·⟫ are continuous in ξ (modConj, modUnitary continuous, inner continuous), so the equality passes to the limit (tendsto_nhds_unique). This lifts GConstancy from ξ = √R ζ (gConstancy_eta_of_bottom) to any ξ in the closure of the √R-range — and √R has dense range (R injective via rvdRC_mul_rvdTwoSubRC_injective), the ξ = √R ζ reconciliation.

Proof. Immediate from the definitions. $\square$

Used by gConstancy_xi_of_density.

Lemma 478 (gConstancy_xi_of_density).  source ↗

GConstancy at every ξ ∈ 𝒦, from the √R-vector GConstancy + the √R-range density (the ξ-side closeout). Given GConstancy holds at every √R ζ ∈ 𝒦 (hsqrt, supplied by gConstancy_eta_of_bottom) and the √R-range is dense in 𝒦 (hdense: every ξ ∈ 𝒦 is a limit of √R ζ_k ∈ 𝒦 — the structural fact that √R has dense range, R injective via rvdRC_mul_rvdTwoSubRC_injective), GConstancy holds at every ξ ∈ 𝒦 by closedness in ξ (gConstancy_of_tendsto_xi). This is exactly the ∀ ξ ∈ 𝒦 premise of the comparison wrapper comparisonDatum_of_gConstancy, completing the ξ-reconciliation modulo the named √R-density input.

Proof. By gConstancy_of_tendsto_xi. $\square$

Used by gConstancy_of_inputs.

Lemma 479 (modUnitary_eq_of_orbit_compare).  source ↗

CORRECTED top-level assembly of RvD Theorem 3.8 (hUniq discharge, faithful form). Supersedes modUnitary_eq_of_orbit_inner, whose hypotheses ⟨w, ·_t η⟩ = ⟨w, η⟩ are VACUOUS (they would force V_t = id; see the FRAMEWORK CAVEAT in AxiomAudit). The correct orbit datum is the U-vs-Δ comparison ⟨w, V_t η⟩ = ⟨w, Δ^{it} η⟩ directly — what RvD’s g-function constancy + the KMS-matching against ⟨h(z), Δ^{it}ξ⟩ actually produce (the KMS condition is applied to the pair (η, Δ^{it}ξ), so Δ^{it} genuinely enters; it does NOT factor through ⟨w, η⟩). This hypothesis is satisfiable and non-vacuous. …

Proof. By projK, clm_eq_of_eqOn_K, mem_K_iff_projK, eq_of_mem_K_of_inner_perp_IK. $\square$

Used by oneParticleBW_of_comparison.

Lemma 480 (clm_eq_of_inner_self_eq).  source ↗

Polarization bridge: diagonal quadratic forms pin a bounded operator (final step of the diagonal-correlation route to the hUniq discharge). Over ℂ, two bounded operators with equal diagonal forms ⟨ξ, A ξ⟩ = ⟨ξ, B ξ⟩ for all ξ are equal — the polarization identity packaged as inner_map_self_eq_zero applied to A − B. This converts the SCALAR correlation equality that strip-uniqueness delivers (modCorrExt, the Δ-side ⟨ξ, Δ^{iz} ξ⟩, against a competitor’s KMS extension F) into the operator identity Δ^{it} = V_t. Unlike the discredited corrC(Jξ) constancy route, this bridge is non-vacuous: it is the standard, correct closeout once the diagonal correlations ⟨ξ, V_t ξ⟩ = ⟨ξ, Δ^{it} ξ⟩ are shown equal for every ξ.

Proof. Immediate from the definitions. $\square$

Used by borelFC_congr_ae.

Lemma 481 (borelFC_congr_ae).  source ↗

The bounded Borel FC depends only on the a.e. class of its symbol: f(R) = g(R) whenever f =ᵐ g against every spectral measure μ^R_x. Via rvdSpec_borelFC_diag (⟪x, f(R)x⟫ = ∫ f dμ^R_x) the diagonals agree (integral_congr_ae), so clm_eq_of_inner_self_eq gives f(R) = g(R). This is the tool for deviceOpC(−i/2) = √(2−R): the device character d_{−i/2} and √(2−r) differ ONLY on the spectral endpoints {0,2}, which carry no spectral mass once R and 2−R are injective (E({0,2}) = 0).

Proof. By clm_eq_of_inner_self_eq, rvdSpec_borelFC_diag. $\square$

Used by deviceOpC_neg_half_eq.

Lemma 482 (deviceOpC_neg_half_eq).  source ↗

The bottom-edge device operator is √(2−R): deviceOpC(−i/2) = rvdSqrtTwoSubR. The device character d_{−i/2}(r) = √(2−r) on (0,2) (devChar_neg_half_I) and the continuous symbol √(2−·) gives √(2−R) (cfcCont_sqrtTwoSub_eq); the two symbols differ ONLY at the spectral endpoints {0,2} (where the piecewise modCharC = 1 swaps the value), and those are μ^R_x-null (rvdSpecMeasure_endpoints), so borelFC_congr_ae identifies the operators. This completes the device/J algebra at the bottom edge: J·deviceOpC(−i/2)ζ = J√(2−R)ζ = √R ζ = ξ — RvD’s (2−R)^{1/2}ζ = Jξ, the half-modular-shift Δ^{1/2} = J on 𝒦. The sole prior unproven step of the bottom-edge KMS reality (A) is thereby reduced to the KMS reflection (a2/a3).

Proof. By borelFC_congr_ae, rvdSpecMeasure, cfcCont_sqrtTwoSub_eq, rvdSpecMeasure_endpoints, borelFC, rvdRC, rvdRC_isSelfAdjoint, rvdRC_spectrum_mem_Icc, cfcCont, devChar, devChar_neg_half_I. $\square$

Used by modConj_deviceOpC_neg_half.

Lemma 483 (modConj_deviceOpC_neg_half).  source ↗

J applied to the bottom-edge device vector: J·deviceOpC(−i/2)ζ = √R(Jζ). From deviceOpC(−i/2) = √(2−R) (deviceOpC_neg_half_eq) and the bottom-edge sqrt swap J√(2−R) = √R·J (modConj_rvdSqrtTwoSubR_modConj + modConj_sq). For a J-fixed ζ this is √Rζ = ξ.

Proof. By deviceOpC_neg_half_eq, rvdSqrtTwoSubR, modConj_sq, modConj_rvdSqrtTwoSubR_modConj. $\square$

Used by modConj_deviceVecF_bottom_eq.

Lemma 484 (modConj_deviceVecF_bottom_eq).  source ↗

The bottom-edge g-vector: J·deviceVecF(t − i/2) = Δ^{it}·√R(Jζ). Combines the device/J commute (modConj_deviceVecF_bottom) with J·deviceOpC(−i/2)ζ = √R(Jζ) (modConj_deviceOpC_neg_half). This is the FIRST slot of the bottom-edge g-function g(t − i/2) = ⟪J·deviceVecF(t−i/2), gaussSmearC(t−i/2)⟫ made explicit, now that deviceOpC(−i/2) = √(2−R) is proven.

Proof. By modConj_deviceOpC_neg_half, deviceOpC, modConj_deviceVecF_bottom. $\square$

Used by modConj_deviceVecF_bottom_eq_fixed.

Lemma 485 (modConj_deviceVecF_bottom_eq_fixed).  source ↗

The bottom-edge g-vector for a J-fixed ζ: J·deviceVecF(t − i/2) = Δ^{it}·√Rζ = Δ^{it}ξ (ξ = √Rζ). This is RvD’s (2−R)^{1/2}ζ = Jξ at the operator-vector level: the bottom-edge device vector, conjugated by J, is exactly the modular flow Δ^{it} applied to ξ = √Rζ. The reality of ⟪Δ^{it}ξ, gaussSmearC(t−i/2)⟫ is then the bottom-edge KMS input h1.

Proof. By modConj_deviceVecF_bottom_eq. $\square$

Used by modConj_deviceVecF_bottom_eq_of_mem_K.

Lemma 486 (modConj_deviceVecF_bottom_eq_of_mem_K).  source ↗

The bottom-edge g-vector under the gConstancy_eta_of_bottom hypothesis √Rζ ∈ 𝒦: J·deviceVecF(t − i/2) = Δ^{it}·√Rζ = Δ^{it}ξ. The condition √Rζ ∈ 𝒦 makes ζ J-fixed (modConj_fixed_of_sqrtR_mem_K, the bounded Tomita relation Jξ = Δ^{1/2}ξ on 𝒦), so the general bottom-edge value Δ^{it}√R(Jζ) collapses to Δ^{it}√Rζ. This resolves the √Rζ∈𝒦-vs-Jζ=ζ condition gap, in exactly the form the bottom-edge KMS reality h1 consumes.

Proof. By modConj_deviceVecF_bottom_eq_fixed, modConj_fixed_of_sqrtR_mem_K. $\square$

Used by gFunction_bottom_eq_of_mem_K.

Lemma 487 (gFunction_bottom_eq_of_mem_K).  source ↗

The bottom-edge g-function value made fully explicit (for √Rζ ∈ 𝒦): g(t − i/2) = ⟪J·deviceVecF(t−i/2), w⟫ = ⟪Δ^{it}·√Rζ, w⟫ = ⟪Δ^{it}ξ, w⟫. With w = gaussSmearC(t−i/2), the bottom-edge KMS reality h1 becomes precisely Im⟪Δ^{it}ξ, gaussSmearC(t−i/2)⟫ = 0 (ξ = √Rζ ∈ 𝒦) — the clean target of the remaining a2/a3 KMS reflection (RvD’s reality on the lower edge, via Δ^{1/2} = J and the half-strip Phragmén–Lindelöf transfer from the proven mid-line KMS function stripKMSrvd_real_midline).

Proof. By modConj_deviceVecF_bottom_eq_of_mem_K, modConj, modConjBilin_apply. $\square$

Used by gFunction_bottom_real_of_kms_match.

Lemma 488 (gFunction_bottom_real_of_kms_match).  source ↗

The g-function bottom-edge reality from the KMS f-transfer (RvD Theorem 3.8’s actual route). The bottom-edge g-value equals the auxiliary orbit correlation with the device FROZEN at its bottom-edge value ξ_t = Δ^{it}ξ (ξ = √Rζ ∈ 𝒦): g(t−i/2) = ⟪ξ_t, gaussSmearC(t−i/2)⟫ = corrC ξ_t V n η (t−i/2). corrC ξ_t is entire (differentiable_corrC) and bounded on the half-strip (corrC_bdd_halfStrip). RvD’s argument: the K.M.S. condition applied to the pair (η, Δ^{it}ξ) yields a bounded-holomorphic f matching this auxiliary corrC ξ_t on the real axis with f(t−i/2) REAL. …

Proof. By corrC_bdd_halfStrip, gFunction_bottom_eq_of_mem_K, differentiable_corrC, eqOn_of_im_zero_edge_halfStrip. $\square$

Used by gFunction_bottom_real_of_faithful_kms.

Lemma 489 (gFunction_bottom_real_of_faithful_kms).  source ↗

The bottom-edge KMS reality h1 from the FAITHFUL-convention half-strip witness. RvD Definition 3.4 (read from source, pp.194-195) states the KMS function with the orbit in the LINEAR inner-product slot: f(t) = ⟨U_tξ, η⟩ with RvD’s ⟨·,·⟩ linear-first (forced — ⟨h(z),Δ^{it}ξ⟩ must be entire), i.e. in Mathlib f(t) = inner ℂ η (V_t ξ). For the pair (ξ' = gaussSmear, η' = ξ_t = Δ^{it}ξ) this is f(s) = ⟪ξ_t, V_s·gaussSmear⟫ = corrC ξ_t V n η s (the real-axis value of the bottom-edge auxiliary gFunction_bottom_eq_of_mem_K + gaussSmearC_ofReal). …

Proof. By gFunction_bottom_real_of_kms_match, gaussSmearC_ofReal, corrC. $\square$

Used by h1_of_stripKMSrvd.

← all sections · ← KGStressConservation · LocalizedMode →