QIQTH.StandardSubspaceModularFlow
← all sections · ← StandardSubspaceModular · StripUniqueness →
StandardSubspaceModularFlow · entries 808–978 of 1000
Definition 808 (modChar). source ↗
The RvD modular character u_t(r), a globally bounded Borel function on ℝ: on (0,2) it is exp(i·t·log((2−r)/r)), and 1 outside (the endpoint convention makes the group law hold pointwise).
Used by deviceOpReal_eq, deviceOpC_bottomEdge_eq, modChar_measurable, modChar_norm, modChar_zero, modChar_add, modChar_conj, modSpecFun, and 7 more.
Lemma 809 (modChar_measurable). source ↗
Proof. Immediate from the definitions.
Used by modSpecFun_measurable.
Lemma 810 (modChar_norm). source ↗
Proof. Immediate from the definitions.
Used by modSpecFun_norm_le.
Lemma 811 (modChar_zero). source ↗
Proof. Immediate from the definitions.
Used by modUnitary_zero.
Lemma 812 (modChar_add). source ↗
Proof. Immediate from the definitions.
Used by modUnitary_add.
Lemma 813 (modChar_conj). source ↗
Proof. Immediate from the definitions.
Used by modUnitary_adjoint.
Lemma 814 (scalarMeasure_eq_specMeasure). source ↗
scalarMeasure(PVM_of_selfAdjoint) = specMeasure. The PVM’s scalar measure μ_x(s) = ‖E(s)x‖² (with E = specProj a projection, so ‖E(s)x‖² = re⟪E(s)x,x⟫ = qForm = μ_x^{spec}(s)) agrees with the Riesz–Markov spectral measure. This connects the bounded-Borel-FC layer (diagInt/bilinDiag, on scalarMeasure) to the integral spectral theorem re_inner_T_eq_integral (on specMeasure).
Proof. By E, scalarMeasure_apply, instIsFiniteMeasureElemRealSpectrumContinuousLinearMapComplexIdSpecMeasure, qForm, specProj, specProj_isSelfAdjoint, reApplyInnerSelf_specProj, specProj_inter.
Used by diagInt_specCoord.
Lemma 815 (borelFC_congr). source ↗
borelFC depends only on the function (not the bound proofs).
Proof. By boundedFC_congr, PVM_of_selfAdjoint.
Used by deviceOpReal_zero, deviceOpReal_eq, deviceOpC_bottomEdge_eq, modUnitary_zero, modUnitary_add, modUnitary_adjoint, borelFC_comm, borelFC_neg, and 9 more.
Lemma 816 (borelFC_adjoint). source ↗
Adjoint of the bounded Borel FC: f(T)⋆ = (conj f)(T). From the hermitian symmetry of the polarized bilinear form (bilinDiag_conj_symm).
Proof. By bilinDiag, bilinDiag_conj_symm, PVM_of_selfAdjoint, inner_borelFC.
Used by borelFC_inner_self, modUnitary_adjoint, cfcCont_star.
Definition 817 (modSpecFun). source ↗
u_t restricted to the spectrum of R — the function fed to the bounded Borel FC.
Used by deviceOpReal_eq, deviceOpC_bottomEdge_eq, modSpecFun_measurable, modSpecFun_norm_le, modUnitary, modUnitary_zero, modUnitary_add, modUnitary_adjoint, and 2 more.
Lemma 818 (modSpecFun_measurable). source ↗
Proof. By modChar, modChar_measurable.
Used by deviceOpReal_eq, deviceOpC_bottomEdge_eq, modUnitary, modUnitary_zero, modUnitary_add, modUnitary_adjoint, modUnitary_commute_rvdRC, cfcΩ_hΩ.
Lemma 819 (modSpecFun_norm_le). source ↗
Proof. By modChar_norm.
Used by deviceOpReal_eq, deviceOpC_bottomEdge_eq, modUnitary, modUnitary_zero, modUnitary_add, modUnitary_adjoint, modUnitary_commute_rvdRC, cfcΩ_hΩ.
Lemma 820 (rvdRC_isSelfAdjoint). source ↗
R = rvdRC S is self-adjoint (it is positive).
Proof. By rvdRC_nonneg.
Used by borelFC_congr_ae, deviceOpC_neg_half_eq, rvdSpecMeasure, deviceOpReal, deviceOpC, deviceOpC_norm_le, deviceOpReal_zero, deviceOpReal_eq, and 34 more.
Definition 821 (modUnitary). source ↗
The continuum modular unitary U_t = Δ^{it} = u_t(R) via the bounded Borel FC of R.
Used by oneParticleBW_niceWedge, oneParticleBW_niceWedge_of_standard, oneParticleBW_niceWedge_reehSchlieder, oneParticleBW_niceWedge_unconditional, hasDerivAt_modularEnergy_of_boost_pos, freeField_modularEnergy_eq_boostCharge, freeField_oneParticle_hFlux, freeField_component_hFlux, and 53 more.
Lemma 822 (modUnitary_zero). source ↗
U_0 = 1.
Proof. By borelFC, borelFC_one, rvdRC, modChar_zero, borelFC_congr, modSpecFun, modSpecFun_measurable, modSpecFun_norm_le, rvdRC_isSelfAdjoint.
Used by comparisonDatum_of_gConstancy, deviceVecF_zero.
Lemma 823 (modUnitary_add). source ↗
Group law U_{s+t} = U_s · U_t — from borelFC_mul and the pointwise law u_{s+t}=u_s·u_t.
Proof. By borelFC, borelFC_mul, rvdRC, modChar_add, borelFC_congr, modSpecFun, modSpecFun_measurable, modSpecFun_norm_le, rvdRC_isSelfAdjoint.
Used by comparisonDatum_of_gConstancy.
Lemma 824 (modUnitary_adjoint). source ↗
U_t⋆ = U_{-t} — from the adjoint relation Φ(f)⋆ = Φ(conj f) and conj u_t = u_{-t}.
Proof. By borelFC, rvdRC, modChar_conj, borelFC_congr, borelFC_adjoint, modSpecFun, modSpecFun_measurable, modSpecFun_norm_le, rvdRC_isSelfAdjoint.
Used by comparisonDatum_of_gConstancy.
Lemma 825 (rvdR_add_rvdPmQ_eq). source ↗
R + D = 2·P (RvD P = ½(R+D)): (P+Q) + (P−Q) = 2P.
Proof. By projIK.
Used by modUnitary_commute_projK_of, commute_projK_of_commute_R_D.
Lemma 826 (mem_K_iff_projK). source ↗
𝒦-membership via its projection: ξ ∈ 𝒦 ↔ P ξ = ξ.
Proof. Immediate from the definitions.
Used by oneParticleBW_niceWedge, h1_of_stripKMSrvd, comparisonDatum_of_gConstancy, oneParticleBW_wedge_complete, modUnitary_eq_of_orbit_compare, gFunction_top_edge_real, modUnitary_mapsTo_K_of_commute, rvdSqrtR_range_dense_in_K, and 1 more.
Lemma 827 (modUnitary_commute_projK_of). source ↗
Reduction of [U_t, P] = 0 to [U_t, R] = 0 ∧ [U_t, D] = 0 via P = ½(R+D).
Proof. By rvdR_add_rvdPmQ_eq.
Used by modUnitary_mapsTo_K_of_commute.
Lemma 828 (modUnitary_mapsTo_K_of_commute). source ↗
Conditional standard-subspace invariance: if U_t commutes with R and D (pointwise), then U_t 𝒦 ⊆ 𝒦. With unitarity this gives U_t 𝒦 = 𝒦 — the property certifying Δ^{it} is the modular flow OF 𝒦. The hypotheses are the two commutators isolated above.
Proof. By projK, mem_K_iff_projK, modUnitary_commute_projK_of.
Used by modUnitary_mapsTo_K_of_commute_D.
Lemma 829 (borelFC_comm). source ↗
Two values of the bounded Borel FC commute (multiplicative + scalar functions commute).
Proof. By borelFC_mul, borelFC_congr.
Used by modUnitary_commute_rvdRC.
Definition 830 (specCoord). source ↗
The coordinate function λ ↦ λ on σ(R) — the integrand of R = ∫λ dE.
Used by deviceOpReal_zero, cfcCont_sqrtTwoSub_eq, specCoord_measurable, specCoord_norm_le, diagInt_specCoord, rvdRC_eq_borelFC, modUnitary_commute_rvdRC, cfcCont_coord, and 2 more.
Lemma 831 (specCoord_measurable). source ↗
Proof. Immediate from the definitions.
Used by rvdRC_eq_borelFC, modUnitary_commute_rvdRC, cfcCont_coord, cfcΩ_coordΩ, rvdRC_mul_E_levelSet.
Lemma 832 (specCoord_norm_le). source ↗
Proof. Immediate from the definitions.
Used by rvdRC_eq_borelFC, modUnitary_commute_rvdRC, cfcCont_coord, cfcΩ_coordΩ, rvdRC_mul_E_levelSet.
Lemma 833 (rvdRC_spectrum_mem_Icc). source ↗
The spectrum of R = P + Q lies in [0, 2] (the TIGHT bound, from the RvD order relations 0 ≤ R and 0 ≤ 2 − R, not the loose norm margin spectrum_subset_covΩ). Lower: 0 ≤ R (rvdRC_nonneg) gives 0 ≤ ω via StarOrderedRing.nonneg_iff_spectrum_nonneg. Upper: for ω ∈ σ(R), 2 − ω ∈ {2} − σ(R) = σ(2·1 − R) = σ(2 − R) (spectrum.singleton_sub_eq), and 0 ≤ 2 − R (rvdTwoSubRC_nonneg) gives 0 ≤ 2 − ω, i.e. ω ≤ 2. This is the spectral location the borelFC construction of the operator device vector (2−R)^{iz}R^{−iz+1/2}ζ = d_z(R)ζ consumes (devChar_norm_le_Icc bounds d_z exactly on [0,2]).
Proof. By rvdRC_nonneg, rvdTwoSubRC, rvdTwoSubRC_isPositive, rvdTwoSubRC_nonneg, rvdRC_isSelfAdjoint.
Used by deviceOpC_neg_half_eq, devSpecReal_norm_le, deviceOpReal_zero, cfcCont_sqrtTwoSub_eq, deviceOpC_bottomEdge_eq, devCharDeriv_norm_le_slab, devChar_slope_norm_le, tendsto_devChar_slope, and 4 more.
Lemma 834 (diagInt_specCoord). source ↗
diagInt(coord) z = ⟪z, R z⟫ (the scalarMeasure=specMeasure bridge + re_inner_T_eq_integral + self-adjoint realness).
Proof. By scalarMeasure, specMeasure, re_inner_T_eq_integral, rvdRC_isSymmetric, scalarMeasure_eq_specMeasure.
Used by rvdRC_eq_borelFC.
Lemma 835 (rvdRC_eq_borelFC). source ↗
R = borelFC(coord) = ∫λ dE — the operator spectral theorem for R, via polarization.
Proof. By diagInt, bilinDiag, PVM_of_selfAdjoint, inner_borelFC, diagInt_specCoord.
Used by modUnitary_commute_rvdRC, cfcCont_coord, cfcΩ_coordΩ, rvdRC_mul_E_levelSet.
Lemma 836 (modUnitary_commute_rvdRC). source ↗
[U_t, R] = 0 (operator form): the modular flow commutes with R.
Proof. By borelFC, modSpecFun, modSpecFun_measurable, modSpecFun_norm_le, rvdRC_isSelfAdjoint, borelFC_comm, specCoord, specCoord_measurable, specCoord_norm_le, rvdRC_eq_borelFC.
Used by modUnitary_commute_rvdR, modUnitary_commute_rvdT.
Lemma 837 (modUnitary_commute_rvdR). source ↗
[U_t, R] = 0 (pointwise on rvdR): U_t(R ξ) = R(U_t ξ).
Proof. By rvdRC, modUnitary_commute_rvdRC.
Used by modUnitary_mapsTo_K_of_commute_D.
Lemma 838 (modUnitary_mapsTo_K_of_commute_D). source ↗
Standard-subspace invariance modulo the covariance: with [U_t,R]=0 discharged, U_t 𝒦 ⊆ 𝒦 follows from the SINGLE remaining obligation [U_t, D] = 0 (the covariance).
Proof. By modUnitary_mapsTo_K_of_commute, modUnitary_commute_rvdR.
Used by modUnitary_mapsTo_K.
Lemma 839 (restrictScalars_star). source ↗
ℂ-adjoint restricted to ℝ equals the ℝ-adjoint (no direct Mathlib lemma).
Proof. Immediate from the definitions.
Used by rvdT_restrictScalars_denseRange, rvdRC_mul_rvdTwoSubRC_denseRange.
Definition 840 (realCommutant). source ↗
The real commutant of a self-adjoint D : H →L[ℝ] H, as a real *-subalgebra of H →L[ℂ] H (over ℝ only, since D is antilinear).
Used by realCommutant_isClosed, commute_of_mem_elemental.
Lemma 841 (realCommutant_isClosed). source ↗
Proof. Immediate from the definitions.
Used by commute_of_mem_elemental.
Lemma 842 (commute_of_mem_elemental). source ↗
Antilinear-CFC commutation: D (self-adjoint, ℝ-linear) commuting with B commutes with everything in elemental ℝ B.
Proof. By realCommutant, realCommutant_isClosed.
Used by rvdPmQ_commute_rvdT.
Lemma 843 (sqrt_mem_elemental). source ↗
CFC.sqrt B ∈ elemental ℝ B for 0 ≤ B (via CFC.sqrt = cfcₙ Real.sqrt = cfc Real.sqrt).
Proof. Immediate from the definitions.
Used by rvdPmQ_commute_rvdT.
Lemma 844 (rvdPmQ_commute_rvdT). source ↗
D·T = T·D (operator form): the antilinear modular conjugation D commutes with the positive modulus T = √(R(2−R)). Whence J = D·T⁻¹ is self-adjoint and J² = 1.
Proof. By projK, projIK, rvdRC, rvdRC_nonneg, rvdPmQ_isSelfAdjoint, rvdTwoSubRC, rvdTwoSubRC_apply, rvdTwoSubRC_nonneg, rvdRC_commute_rvdTwoSubRC, rvdT_sq, rvdT_nonneg, rvdPmQ_commute_A, commute_of_mem_elemental, sqrt_mem_elemental.
Used by rvdPmQ_commute_rvdT_apply.
Lemma 845 (rvdPmQ_commute_rvdT_apply). source ↗
D·T = T·D (pointwise): D(T ξ) = T(D ξ).
Proof. By rvdPmQ_commute_rvdT.
Used by modConj_isSelfAdjoint.
Lemma 846 (rvdT_restrictScalars_denseRange). source ↗
range T is dense (T injective self-adjoint ⟹ (range T)ᗮ = ker T = ⊥).
Proof. By rvdT_isSelfAdjoint, rvdT_injective, restrictScalars_star.
Used by modConj_rvdT, modConj_norm, modConj_isSelfAdjoint, modConj_smul_I, modConj_rvdRC_reflect, rvdSqrtR_range_dense_in_K, modConj_commute_modUnitary.
Definition 847 (modConj). source ↗
The modular conjugation J — the ℝ-linear extension of T ξ ↦ D ξ.
Used by GConstancy, comparisonDatum_of_gConstancy, gConstancy_entire, gConstancy_entire_of_bottom, gConstancy_of_entireVec_limit, gConstancy_real_smul, gConstancy_eta_of_bottom, gConstancy_of_tendsto_xi, and 41 more.
Lemma 848 (modConj_rvdT). source ↗
Proof. By rvdT_norm_eq, rvdT_restrictScalars_denseRange.
Used by modConj_norm, modConj_isSelfAdjoint, modConj_smul_I, modConj_rvdRC_reflect, rvdT_modConj, modConj_rvdPmQ_modConj, modConj_rvdT_of_mem_K, commute_rvdPmQ_of_commute_modConj_rvdT, and 1 more.
Lemma 849 (modConj_norm). source ↗
J is an isometry (‖J η‖ = ‖η‖), by density from ‖J(Tξ)‖ = ‖Dξ‖ = ‖Tξ‖.
Proof. By rvdPmQ, rvdT, rvdT_norm_eq, rvdT_restrictScalars_denseRange, modConj_rvdT.
Used by gFunction_norm_le, modConj_inner_map.
Lemma 850 (modConj_inner_map). source ↗
J preserves the real inner product (it is an isometry): ⟪J η, J ζ⟫ = ⟪η, ζ⟫.
Proof. By modConj_norm.
Used by modConj_sq, modConj_inner_conj.
Lemma 851 (rvdT_real_inner_symm). source ↗
T is real-symmetric — via ℂ-self-adjointness (fast: primary ℂ instance, no scoped-ℝ adjoint).
Proof. By rvdT_isSelfAdjoint.
Used by modConj_isSelfAdjoint.
Lemma 852 (rvdPmQ_real_inner_symm). source ↗
D = P − Q is real-symmetric — via the projection symmetry (fast, no adjoint).
Proof. Immediate from the definitions.
Used by modConj_isSelfAdjoint.
Lemma 853 (modConj_isSelfAdjoint). source ↗
J is self-adjoint (⟪J η, ζ⟫ = ⟪η, J ζ⟫), by density from D·T=T·D (using the fast symmetry lemmas above — avoids the scoped-ℝ adjoint that times out).
Proof. By rvdPmQ, rvdT, rvdPmQ_commute_rvdT_apply, rvdT_restrictScalars_denseRange, modConj_rvdT, rvdT_real_inner_symm, rvdPmQ_real_inner_symm.
Used by modConj_sq, modConj_inner_conj.
Lemma 854 (modConj_sq). source ↗
J² = 1 — the modular conjugation is an involution (⟪ζ, J²η⟫ = ⟪Jζ, Jη⟫ = ⟪ζ, η⟫).
Proof. By modConj_inner_map, modConj_isSelfAdjoint.
Used by comparisonDatum_of_gConstancy, modConj_deviceOpC_neg_half, modConj_inner_conj, modConj_rvdRC_modConj, modConjSqrtR_sq, modConj_rvdSqrtR_modConj, modConj_rvdSqrtTwoSubR_modConj, modConj_rvdSqrtR, and 6 more.
Lemma 855 (modConj_smul_I). source ↗
The modular conjugation J is antilinear: J(i·η) = −i·(J η). On the dense range of T (which is ℂ-linear), J(i·T x) = J(T(i·x)) = D(i·x) = (P−Q)(i·x) = i·(Q−P)x = −i·D x = −i·J(T x) (projK_smul_I/projIK_smul_I), and continuity extends to all η. This is the antilinearity RvD use to place J𝒦 in (i𝒦)^⊥ (Prop 2.2(5)), the source of the w ⊥ i𝒦 vectors of Theorem 3.8.
Proof. By projK, projIK, projIK_smul_I, projK_smul_I, rvdPmQ, rvdT, rvdT_restrictScalars_denseRange, modConj_rvdT.
Used by modConj_smul_conj, modConj_inner_conj.
Lemma 856 (modConj_smul_conj). source ↗
J is conjugate-linear: J(c·η) = conj(c)·(J η). Extends the antilinearity modConj_smul_I (c = i) to all complex scalars via the real decomposition c = Re c + i·Im c and J’s ℝ-linearity. This is the clean statement that bundles J R^{1/2} J (and similar J-sandwiches) as ℂ-linear.
Proof. By modConj_smul_I.
Used by modConj_rvdSqrtR_modConj.
Definition 857 (modConjBilin). source ↗
The J-twisted bilinear form B(v,w) = ⟪J v, w⟫ as a continuous ℂ-BILINEAR map H →L[ℂ] H →L[ℂ] ℂ. ℂ-linear in v by the J-cancellation (inner_modConj_smul_left: J antilinear ∘ inner conj-linear = ℂ-linear), ℂ-linear in w (inner second slot), bounded by ‖v‖·‖w‖ (modConj_norm isometry + Cauchy–Schwarz). This is the bilinear form whose composition with two HOLOMORPHIC curves g(z) = B(d_z(R)ζ, V_z η) is holomorphic — the device-vector RvD g-function.
Used by h1_of_stripKMSrvd, gConstancy_of_inputs, oneParticleBW_of_inputs, oneParticleBW_of_stripKMSrvd_density, gFunction_eq_zero_const, gConstancy_entire, gFunction_top_edge_real_all, gConstancy_entire_of_bottom, and 11 more.
Lemma 858 (modConjBilin_apply). source ↗
modConjBilin applied: B(v, w) = ⟪J v, w⟫.
Proof. Immediate from the definitions.
Used by gFunction_bottom_eq_of_mem_K, gFunction_zero, gFunction_real_eq, gFunction_norm_le.
Lemma 859 (modConj_inner_conj). source ↗
The modular conjugation J is antiunitary: ⟪J η, J ζ⟫ = conj⟪η, ζ⟫. The real part is modConj_inner_map (J is a real isometry); the imaginary part flips sign because J is antilinear (modConj_smul_I): Im⟪Jη, Jζ⟫ = ⟪i·Jη, Jζ⟫_ℝ = −⟪J(i·η), Jζ⟫_ℝ = −⟪i·η, ζ⟫_ℝ = −Im⟪η, ζ⟫. This is the full Tomita reality of J, the engine behind J𝒦 = (i𝒦)^⊥ (RvD Prop 2.2(5)).
Proof. By modConj_inner_map, modConj_isSelfAdjoint, modConj_sq, modConj_smul_I.
Used by modConj_rvdSqrtR_modConj.
Lemma 860 (rvdRC_commute_rvdT). source ↗
T commutes with R (both are continuous functions of R).
Proof. By rvdTwoSubRC, rvdSqrtR, rvdSqrtTwoSubR, rvdRC_commute_rvdTwoSubRC.
Used by modConj_rvdRC_reflect, rvdSqrtR_range_dense_in_K.
Lemma 861 (rvdPmQ_rvdRC). source ↗
D R = (2 − R) D pointwise — from the anticommutation D(R−1) = −(R−1)D.
Proof. By rvdR, rvdPmQ_anticommute_rvdR_sub_one.
Used by modConj_rvdRC_reflect.
Lemma 862 (modConj_rvdRC_reflect). source ↗
J R = (2 − R) J pointwise (the reflection intertwiner), by density from range T.
Proof. By rvdPmQ, rvdT, rvdT_restrictScalars_denseRange, modConj_rvdT, rvdRC_commute_rvdT, rvdPmQ_rvdRC.
Used by modConj_rvdRC_modConj.
Lemma 863 (modConj_rvdRC_modConj). source ↗
J R J = 2 − R — the modular conjugation reflects R (the bounded shadow of J Δ J = Δ⁻¹). One of the canonical Tomita–Takesaki relations, and a prerequisite for the CGP spectral balance.
Proof. By modConj_sq, modConj_rvdRC_reflect.
Used by modConjSqrtR_sq, modConj_projIK_modConj, modConj_projK_modConj.
Lemma 864 (modConjSqrtR_sq). source ↗
The square of B = J R^{1/2} J is 2 − R: B(B ξ) = (2−R) ξ, where B ξ = J(R^{1/2}(J ξ)). The inner J² = 1 (modConj_sq) collapses B² ξ = J R^{1/2} (J J) R^{1/2} J ξ = J R^{1/2} R^{1/2} J ξ = J R J ξ = (2−R) ξ (rvdSqrtR_mul_self + modConj_rvdRC_modConj). This is the b·b = a input to CFC.sqrt_unique: once B is bundled as a ℂ-linear positive operator (it commutes with i· by modConj_smul_I applied twice), square-root uniqueness yields J R^{1/2} J = (2−R)^{1/2} — the sqrt-reflection underlying J𝒦 = (i𝒦)^⊥, reachable WITHOUT general antilinear CFC.
Proof. By rvdRC, rvdSqrtR_mul_self, modConj_sq, modConj_rvdRC_modConj.
Used by modConj_rvdSqrtR_modConj.
Lemma 865 (modConj_rvdSqrtR_modConj). source ↗
The sqrt-reflection J R^{1/2} J = (2−R)^{1/2} (RvD Prop 2.2(5) engine), reached via square-root UNIQUENESS — NOT general antilinear CFC. Bundle B ξ = J(R^{1/2}(J ξ)) as a ℂ-linear operator (ℂ-linear by modConj_smul_conj applied twice), self-adjoint and positive (the antiunitary modConj_inner_conj reduces ⟨B x, y⟩ to conj⟨R^{1/2}(J x), J y⟩, and R^{1/2} ≥ 0), with B·B = 2−R (modConjSqrtR_sq). CFC.sqrt_unique then identifies B with (2−R)^{1/2} = rvdSqrtTwoSubR.
Proof. By rvdTwoSubRC, rvdSqrtR_nonneg, modConj_sq, modConj_smul_conj, modConj_inner_conj, modConjSqrtR_sq.
Used by modConj_rvdSqrtTwoSubR_modConj, modConj_rvdSqrtR.
Lemma 866 (modConj_rvdSqrtTwoSubR_modConj). source ↗
The symmetric sqrt-reflection J (2−R)^{1/2} J = R^{1/2} — immediate from J R^{1/2} J = (2−R)^{1/2} (modConj_rvdSqrtR_modConj) by sandwiching with J and using J² = 1 (modConj_sq).
Proof. By modConj_sq, modConj_rvdSqrtR_modConj.
Used by modConj_deviceOpC_neg_half, modConj_rvdT_modConj, modConj_rvdSqrtTwoSubR.
Lemma 867 (modConj_rvdSqrtR). source ↗
The “moved” sqrt-reflection J R^{1/2} = (2−R)^{1/2} J: J(R^{1/2} y) = (2−R)^{1/2}(J y). (modConj_rvdSqrtR_modConj at J y + J² = 1.)
Proof. By modConj_sq, modConj_rvdSqrtR_modConj.
Used by modConj_rvdT_modConj, rvdSqrtR_modConj_of_mem_K, modConj_fixed_of_sqrtR_mem_K.
Lemma 868 (modConj_rvdT_modConj). source ↗
J T J = T — the modular conjugation commutes with the polar radius T = R^{1/2}(2−R)^{1/2}. J T J = (J R^{1/2} J)(J (2−R)^{1/2} J) = (2−R)^{1/2} R^{1/2} = R^{1/2}(2−R)^{1/2} = T, using both sqrt-reflections and that the square roots commute (rvdSqrtR_commute_rvdSqrtTwoSubR). Hence [J, T] = 0, the keystone giving J D J = D and thence J P J = 1 − Q (J𝒦 = (i𝒦)^⊥).
Proof. By rvdSqrtR, rvdSqrtTwoSubR, rvdSqrtR_commute_rvdSqrtTwoSubR, modConj_rvdSqrtTwoSubR_modConj, modConj_rvdSqrtR.
Used by rvdT_modConj, rvdSqrtR_range_dense_in_K.
Lemma 869 (rvdT_modConj). source ↗
T J = D — combining [J, T] = 0 (J T J = T) with J T = D (modConj_rvdT). T(J η) = J(T η) = D η.
Proof. By modConj_rvdT, modConj_sq, modConj_rvdT_modConj.
Used by modConj_rvdPmQ_modConj.
Lemma 870 (modConj_rvdPmQ_modConj). source ↗
J D J = D — the modular conjugation commutes with D = P − Q. From T J = D (rvdT_modConj): J(D(J ξ)) = J(T(J(J ξ))) = J(T ξ) = D ξ. With J R J = 2 − R this gives J P J = 1 − Q.
Proof. By rvdT, modConj_rvdT, modConj_sq, rvdT_modConj.
Used by modConj_projIK_modConj, modConj_projK_modConj.
Lemma 871 (modConj_projIK_modConj). source ↗
J Q J = 1 − P — the modular conjugation reflects the projection Q = projIK onto 1 − P. J Q J = (J R J − J D J)/2 = ((2−R) − D)/2 = 1 − P (J R J = 2−R, J D J = D). Concretely J(Q(J ξ)) = ξ − P ξ. This is RvD Prop 2.2(5): J carries i𝒦 onto 𝒦^⊥ and 𝒦 onto (i𝒦)^⊥.
Proof. By rvdR, rvdR_apply, rvdRC, rvdRC_apply, rvdPmQ, rvdTwoSubRC, rvdTwoSubRC_apply, modConj_rvdRC_modConj, modConj_rvdPmQ_modConj.
Used by projIK_modConj_eq_zero_of_mem_K.
Lemma 872 (projIK_modConj_eq_zero_of_mem_K). source ↗
J 𝒦 ⊆ (i𝒦)^⊥ (RvD Prop 2.2(5)): for ξ ∈ 𝒦 (P ξ = ξ), J ξ ⊥ i𝒦 (projIK (J ξ) = 0). From J Q J = 1 − P (modConj_projIK_modConj): J(Q(J ξ)) = ξ − P ξ = 0, and J is injective (J² = 1), so Q(J ξ) = 0. This places the modular-conjugated standard-subspace vectors — the J-twisted w-vectors of RvD Theorem 3.8’s g-function — in (i𝒦)^⊥.
Proof. By modConj_sq, modConj_projIK_modConj.
Used by gFunction_top_edge_real.
Lemma 873 (modConj_projK_modConj). source ↗
J P J = 1 − Q — the symmetric reflection: J(P(J ξ)) = ξ − Q ξ. J P J = (J R J + J D J)/2 = ((2−R) + D)/2 = 1 − Q (J R J = 2−R, J D J = D). With J Q J = 1 − P this is the full RvD Prop 2.2(5): J swaps (𝒦, i𝒦) with ((i𝒦)^⊥, 𝒦^⊥).
Proof. By rvdR, rvdR_apply, rvdRC, rvdRC_apply, rvdPmQ, rvdTwoSubRC, rvdTwoSubRC_apply, modConj_rvdRC_modConj, modConj_rvdPmQ_modConj.
Used by projK_modConj_eq_self_of_perp_IK.
Lemma 874 (projK_modConj_eq_self_of_perp_IK). source ↗
(i𝒦)^⊥ ⊆ J𝒦 — the reverse inclusion, giving the equality J𝒦 = (i𝒦)^⊥. For w ⊥ i𝒦 (projIK w = 0), J P J at w gives J(P(J w)) = w − Q w = w, and J²=1 injectivity yields P(J w) = J w, i.e. J w ∈ 𝒦; hence w = J(J w) ∈ J𝒦. So the (i𝒦)^⊥ w-supply of the orbit-identity framework is exactly the J-images of 𝒦.
Proof. By modConj_sq, modConj_projK_modConj.
Used by comparisonDatum_of_gConstancy.
Lemma 875 (rvdPmQ_eq_of_mem_K). source ↗
Bounded Tomita fixedness: for ξ ∈ 𝒦 (P ξ = ξ), D ξ = (2 − R) ξ.
Proof. By projIK, rvdR, rvdRC.
Used by modConj_rvdT_of_mem_K.
Lemma 876 (modConj_rvdT_of_mem_K). source ↗
For ξ ∈ 𝒦, J(T ξ) = (2 − R) ξ — the modular form of the bounded Tomita fixedness, equating the two bounded objects whose R-spectral measures drive the CGP balance.
Proof. By rvdPmQ, modConj_rvdT, rvdPmQ_eq_of_mem_K.
Used by rvdSqrtR_modConj_of_mem_K.
Lemma 877 (commute_projK_of_commute_R_D). source ↗
Generic projK-commutation: a continuous ℂ-linear A commuting with rvdR (= R) and rvdPmQ (= D) pointwise commutes with projK = (R + D)/2. The operator-generic form of modUnitary_commute_projK_of.
Proof. By rvdR_add_rvdPmQ_eq.
Used by rvdSqrtR_range_dense_in_K.
Lemma 878 (commute_rvdPmQ_of_commute_modConj_rvdT). source ↗
[A, D] = 0 from [A, J] = [A, T] = 0: since D = J·T (modConj_rvdT: J(Tξ) = Dξ), an operator commuting with the modular conjugation J and the polar radius T commutes with D = rvdPmQ. For a real symmetric f, cfcCont f commutes with both (J via modConj_cfcΩ/twΩ, T as a function of R), so it commutes with D — the [·, D] = 0 “frontier” step, available for symmetric symbols.
Proof. By modConj_rvdT.
Used by rvdSqrtR_range_dense_in_K.
Lemma 879 (inner_real_of_mem_K_perp_IK). source ↗
RvD Proposition 2.3 — reality across 𝒦 and (i𝒦)^⊥. If x ∈ 𝒦 (projK x = x) and y ⊥ i𝒦 (projIK y = 0), then ⟨x, y⟩_ℂ is real. Reason: Im⟨x, y⟩ = ⟨i·x, y⟩_ℝ, and i·x ∈ i𝒦 while y ⊥ i𝒦, so this real inner product vanishes. This is the reality used in RvD Theorem 3.8 to show the correlation g(t) = ⟨U_t η, J(2−R)^{1/2}R^{−1/2}ζ⟩ is real on the real axis (and, after the KMS flip, on the lower edge), the input to “real on both edges ⟹ constant”.
Proof. By projIK_isSelfAdjoint, projIK_smul_I.
Used by gFunction_top_edge_real.
Lemma 880 (eq_of_mem_K_of_inner_perp_IK). source ↗
Totality of (i𝒦)^⊥ against 𝒦 (RvD Theorem 3.8 closeout): two vectors of 𝒦 with equal inner products against every w ⊥ i𝒦 (projIK w = 0) are equal. Their difference d ∈ 𝒦 is orthogonal to all of (i𝒦)^⊥: taking w = d − Q d ∈ (i𝒦)^⊥ gives ‖d − Q d‖² = Re⟨w, d⟩ = 0, so d = Q d ∈ i𝒦; then d ∈ 𝒦 ⊓ i𝒦 = {0} (IsSeparating). This is the totality step: combined with orbit_inner_eq_of_entire for V and Δ^{it} (both giving ⟨w, ·_t η⟩ = ⟨w, η⟩) it yields V_t η = Δ^{it} η on 𝒦.
Proof. By projIK_idem.
Used by modUnitary_eq_of_orbit_compare.
Lemma 881 (borelFC_add). source ↗
borelFC is additive in f (lift of boundedFC_add).
Proof. By boundedFC_add, PVM_of_selfAdjoint.
Used by borelFC_sub, cfcCont_add.
Lemma 882 (borelFC_smul). source ↗
borelFC is ℂ-homogeneous in f (lift of boundedFC_smul).
Proof. By boundedFC_smul, PVM_of_selfAdjoint.
Used by deviceOpC_slope_normSq, borelFC_neg, cfcCont_smul.
Lemma 883 (borelFC_neg). source ↗
borelFC is additive-inverse compatible: (-f)(T) = -f(T) (from borelFC_smul (-1)).
Proof. By borelFC_congr, borelFC_smul.
Used by borelFC_sub.
Lemma 884 (borelFC_sub). source ↗
borelFC is subtractive: (f − g)(T) = f(T) − g(T) (lift of additivity + borelFC_neg).
Proof. By borelFC_add, borelFC_neg.
Used by deviceOpC_sub, deviceOpC_slope_normSq.
Definition 885 (cfcCont). source ↗
The bounded Borel FC of R = rvdRC S on a continuous function, with the automatic compact-sup bound ‖f ω‖ ≤ ‖f‖.
Used by deviceOpC_neg_half_eq, deviceOpReal_zero, cfcCont_sqrtTwoSub_eq, cfcCont_norm_le, cfcCont_one, cfcCont_mul, cfcCont_add, cfcCont_smul, and 12 more.
Lemma 886 (cfcCont_norm_le). source ↗
Proof. By boundedFC, boundedFC_norm_le, PVM_of_selfAdjoint, borelFC, rvdRC_isSelfAdjoint.
Used by cfcCont_continuous.
Lemma 887 (cfcCont_one). source ↗
Proof. By borelFC, borelFC_one, borelFC_congr, rvdRC_isSelfAdjoint.
Used by cfcCont_sqrtTwoSub_eq, cfcΩ_one.
Lemma 888 (cfcCont_mul). source ↗
Proof. By borelFC, borelFC_mul, borelFC_congr, rvdRC_isSelfAdjoint.
Used by deviceOpReal_zero, cfcCont_sqrtTwoSub_eq, cfcΩ_mul.
Lemma 889 (cfcCont_add). source ↗
Proof. By borelFC, borelFC_congr, rvdRC_isSelfAdjoint, borelFC_add.
Used by cfcCont_sqrtTwoSub_eq, cfcContₗ, cfcΩ_add.
Lemma 890 (cfcCont_smul). source ↗
Proof. By borelFC, borelFC_congr, rvdRC_isSelfAdjoint, borelFC_smul.
Used by cfcCont_sqrtTwoSub_eq, cfcΩ_smul.
Lemma 891 (cfcCont_star). source ↗
Proof. By borelFC, borelFC_congr, borelFC_adjoint, rvdRC_isSelfAdjoint.
Used by deviceOpReal_zero, cfcCont_sqrtTwoSub_eq.
Lemma 892 (cfcCont_coord). source ↗
cfcCont sends the coordinate function to R.
Proof. By borelFC, borelFC_congr, rvdRC_isSelfAdjoint, specCoord_measurable, specCoord_norm_le, rvdRC_eq_borelFC.
Used by deviceOpReal_zero, cfcCont_sqrtTwoSub_eq.
Definition 893 (cfcContₗ). source ↗
cfcCont as a ℂ-linear map (for the continuity bound).
Used by cfcCont_continuous.
Lemma 894 (cfcCont_continuous). source ↗
Proof. By cfcCont_norm_le, cfcContₗ.
Used by cfcΩ_continuous.
Definition 895 (covM). source ↗
The radius M = ‖R‖·‖1‖ bounding the spectrum.
Used by spectrum_subset_covΩ, inclΩ, tauΩ, cfcΩ, cfcΩ_one, cfcΩ_mul, cfcΩ_add, cfcΩ_smul, and 14 more.
Lemma 896 (spectrum_subset_covΩ). source ↗
Proof. Immediate from the definitions.
Used by inclΩ.
Definition 897 (inclΩ). source ↗
The inclusion σℝ R ↪ Ω as a continuous map.
Used by cfcΩ, cfcΩ_one, cfcΩ_mul, cfcΩ_add, cfcΩ_smul, cfcΩ_continuous, cfcΩ_coordΩ, cfcΩ_hΩ.
Definition 898 (tauΩ). source ↗
The involution τ(r) = 2 − r on the symmetric Ω.
Used by twΩ, twΩ_add, twΩ_mul, cfcΩ_intertwine, cfcΩ_hΩ.
Definition 899 (cfcΩ). source ↗
cfcΩ f = f(R) for f continuous on the symmetric domain Ω.
Used by cfcΩ_one, cfcΩ_mul, cfcΩ_add, cfcΩ_smul, cfcΩ_continuous, cfcΩ_coordΩ, cfcΩ_sub, cfcΩ_twΩ_coordΩ, and 3 more.
Lemma 900 (cfcΩ_one). source ↗
Proof. By rvdRC, cfcCont, cfcCont_one, inclΩ.
Used by cfcΩ_twΩ_coordΩ, cfcΩ_intertwine.
Lemma 901 (cfcΩ_mul). source ↗
Proof. By rvdRC, cfcCont, cfcCont_mul, inclΩ.
Used by cfcΩ_intertwine, cfcΩ_hΩ.
Lemma 902 (cfcΩ_add). source ↗
Proof. By rvdRC, cfcCont, cfcCont_add, inclΩ.
Used by cfcΩ_sub, cfcΩ_intertwine.
Lemma 903 (cfcΩ_smul). source ↗
Proof. By rvdRC, cfcCont, cfcCont_smul, inclΩ.
Used by cfcΩ_sub, cfcΩ_twΩ_coordΩ, cfcΩ_intertwine.
Lemma 904 (cfcΩ_continuous). source ↗
Proof. By rvdRC, cfcCont, cfcCont_continuous, inclΩ.
Used by cfcΩ_intertwine.
Definition 905 (coordΩ). source ↗
The coordinate function x ↦ x.1 on Ω (real-valued ⟹ self-adjoint, the SW generator).
Used by coordΩ_star, cfcΩ_coordΩ, cfcΩ_twΩ_coordΩ, cfcΩ_intertwine, cfcΩ_hΩ.
Lemma 906 (coordΩ_star). source ↗
Proof. Immediate from the definitions.
Used by cfcΩ_intertwine.
Definition 907 (twΩ). source ↗
The twist (twΩ f)(r) = conj(f(2−r)).
Used by twΩ_add, twΩ_mul, cfcΩ_twΩ_coordΩ, cfcΩ_intertwine, twΩ_hΩ, cfcΩ_hΩ, modUnitary_commute_rvdPmQ_rs.
Lemma 908 (twΩ_add). source ↗
Proof. By tauΩ.
Used by cfcΩ_intertwine.
Lemma 909 (twΩ_mul). source ↗
Proof. By tauΩ.
Used by cfcΩ_intertwine.
Lemma 910 (cfcΩ_coordΩ). source ↗
Proof. By borelFC, borelFC_congr, rvdRC_isSelfAdjoint, specCoord, specCoord_measurable, specCoord_norm_le, rvdRC_eq_borelFC, cfcCont, covM, inclΩ.
Used by cfcΩ_twΩ_coordΩ, cfcΩ_intertwine, cfcΩ_hΩ.
Lemma 911 (cfcΩ_sub). source ↗
Proof. By cfcΩ_add, cfcΩ_smul.
Used by cfcΩ_twΩ_coordΩ.
Lemma 912 (cfcΩ_twΩ_coordΩ). source ↗
Proof. By rvdRC, covM, cfcΩ_one, cfcΩ_smul, cfcΩ_coordΩ, cfcΩ_sub.
Used by cfcΩ_intertwine, cfcΩ_hΩ.
Lemma 913 (rvdPmQ_mul_rvdRC_rs). source ↗
The base case of the intertwiner: D·R = (2−R)·D in restrictScalars form.
Proof. By rvdR, rvdTwoSubRC_apply, rvdPmQ_mul_rvdR.
Used by cfcΩ_intertwine.
Lemma 914 (cfcΩ_intertwine). source ↗
The continuous intertwiner D·f(R) = conj(f(2−·))(R)·D for every CONTINUOUS f on the symmetric domain Ω. Proved by complex Stone–Weierstrass: both sides are continuous in f, the coordΩ-generated subalgebra is dense, and they agree there (base case D·R=(2−R)·D + the algebra structure). D is antilinear, so the relation is conjugate-linear — hence the “good set” is a plain Subalgebra (not a *-subalgebra), but coordΩ is self-adjoint so the generated subalgebra still has dense closure.
Proof. By rvdRC, rvdTwoSubRC, rvdPmQ_smul_conj, tauΩ, cfcΩ_one, cfcΩ_mul, cfcΩ_add, cfcΩ_smul, cfcΩ_continuous, coordΩ, coordΩ_star, twΩ_add, twΩ_mul, cfcΩ_coordΩ, cfcΩ_twΩ_coordΩ, rvdPmQ_mul_rvdRC_rs.
Used by modUnitary_commute_rvdPmQ_rs.
Lemma 915 (rvdSqrtR_range_dense_in_K). source ↗
The √R-range density in 𝒦 (hdense) — RvD’s ξ = R^{1/2}ζ reconciliation, the LAST analytic input of the device g-function discharge. Every ξ ∈ 𝒦 is a limit of vectors √R ζ_k ∈ 𝒦. …
Proof. By rvdR, projK_idem, rvdRC, rvdSqrtTwoSubR, rvdT, mem_K_iff_projK, rvdT_restrictScalars_denseRange, modConj, modConj_sq, rvdRC_commute_rvdT, modConj_rvdT_modConj, commute_projK_of_commute_R_D, commute_rvdPmQ_of_commute_modConj_rvdT.
Used by oneParticleBW_complete.
Lemma 916 (modChar_reflect). source ↗
u_t is θ-fixed: conj(u_t(2−r)) = u_t(r). (u_t(2−r)=exp(it·log(r/(2−r)))=conj(u_t(r)).)
Proof. Immediate from the definitions.
Used by twΩ_hΩ.
Definition 917 (hΩ). source ↗
The damped modular function as a continuous map on Ω.
Used by twΩ_hΩ, cfcΩ_hΩ, modUnitary_commute_rvdPmQ_rs.
Lemma 918 (twΩ_hΩ). source ↗
hΩ is θ-fixed: twΩ (hΩ) = hΩ (the damped modular function is invariant under r↦2−r + conj).
Proof. By modChar, modChar_reflect.
Used by modUnitary_commute_rvdPmQ_rs.
Lemma 919 (cfcΩ_hΩ). source ↗
cfcΩ(hΩ) = U_t · A with A = R(2−R) — the damped FC factors as the modular unitary times the polynomial damping (borelFC_mul).
Proof. By borelFC, borelFC_mul, modChar, borelFC_congr, modSpecFun, modSpecFun_measurable, modSpecFun_norm_le, rvdRC_isSelfAdjoint, cfcCont, covM, inclΩ, tauΩ, cfcΩ_mul, coordΩ, twΩ, cfcΩ_coordΩ, cfcΩ_twΩ_coordΩ.
Used by modUnitary_commute_rvdPmQ_rs.
Lemma 920 (rvdRC_mul_rvdTwoSubRC_isSelfAdjoint). source ↗
A = R(2−R) is self-adjoint.
Proof. By rvdRC_commute_rvdTwoSubRC, rvdRC_isSelfAdjoint.
Used by rvdRC_mul_rvdTwoSubRC_denseRange.
Lemma 921 (rvdRC_mul_rvdTwoSubRC_injective). source ↗
A = R(2−R) = D² is injective (D injective).
Proof. By rvdPmQ, rvdPmQ_injective, rvdRC_mul_rvdTwoSubRC_apply.
Used by rvdRC_injective, rvdTwoSubRC_injective, rvdRC_mul_rvdTwoSubRC_denseRange.
Lemma 922 (rvdRC_injective). source ↗
R = rvdRC is injective (toward the √R-range density, the ξ = √R ζ reconciliation of the device g-function discharge). From R(2−R) injective (rvdRC_mul_rvdTwoSubRC_injective): R a = R b gives R(2−R)a = (2−R)(R a) = (2−R)(R b) = R(2−R)b (commute), hence a = b. As a self-adjoint operator, R injective ⟹ √R injective ⟹ √R has DENSE RANGE in H — the structural basis of the √R-range density that lifts GConstancy from ξ = √R ζ to all of 𝒦.
Proof. By rvdTwoSubRC, rvdRC_commute_rvdTwoSubRC, rvdRC_mul_rvdTwoSubRC_injective.
Used by rvdRC_E_zero_levelSet.
Lemma 923 (rvdTwoSubRC_injective). source ↗
2 − R = rvdTwoSubRC is injective (the companion to rvdRC_injective, giving E({2}) = 0). From R(2−R) injective: (2−R)a = (2−R)b gives R((2−R)a) = R((2−R)b), i.e. R(2−R)a = R(2−R)b, hence a = b. So 2 is not an eigenvalue of R — the spectral atom at the device-character endpoint r = 2 vanishes, the other half of deviceOpC(−i/2) = √(2−R) (a.e., PVM({0,2}) = 0).
Proof. By rvdRC, rvdRC_mul_rvdTwoSubRC_injective.
Used by rvdSqrtTwoSubR_injective, rvdRC_E_two_levelSet.
Lemma 924 (modConj_rvdSqrtTwoSubR). source ↗
J √(2−R) = √R J — the companion of modConj_rvdSqrtR (J √R = √(2−R) J), for the bottom-edge Tomita algebra. From modConj_rvdSqrtTwoSubR_modConj (J √(2−R) J = √R) at J y + J² = 1.
Proof. By modConj_sq, modConj_rvdSqrtTwoSubR_modConj.
Used by rvdSqrtR_modConj_of_mem_K.
Lemma 925 (rvdSqrtTwoSubR_injective). source ↗
√(2−R) is injective — companion to rvdT_injective: from √(2−R)² = 2−R and 2−R injective (rvdTwoSubRC_injective).
Proof. By rvdTwoSubRC, rvdSqrtTwoSubR_mul_self, rvdTwoSubRC_injective.
Used by rvdSqrtR_modConj_of_mem_K.
Lemma 926 (rvdSqrtR_modConj_of_mem_K). source ↗
RvD Proposition 3.7 (bounded Tomita on √R): for ξ ∈ 𝒦, √R (Jξ) = √(2−R) ξ. This is the BOUNDED form of Δ^{1/2}ξ = Jξ (with Δ^{1/2} = √(2−R)·√R⁻¹): from J(Tξ) = (2−R)ξ (modConj_rvdT_of_mem_K, T = √R √(2−R)) expand J(√R(√(2−R)ξ)) = √(2−R)(√R(Jξ)) (the two sqrt reflections), so √(2−R)(√R(Jξ)) = (2−R)ξ = √(2−R)(√(2−R)ξ), and cancel one √(2−R).
Proof. By rvdTwoSubRC, rvdSqrtTwoSubR_mul_self, rvdT, modConj_rvdSqrtR, modConj_rvdT_of_mem_K, modConj_rvdSqrtTwoSubR, rvdSqrtTwoSubR_injective.
Used by modConj_fixed_of_sqrtR_mem_K.
Lemma 927 (modConj_fixed_of_sqrtR_mem_K). source ↗
√Rζ ∈ 𝒦 ⟹ Jζ = ζ — the bottom-edge condition reconciliation. Resolves the gap between the gConstancy_eta_of_bottom hypothesis √Rζ ∈ 𝒦 and the J-fixedness Jζ = ζ the bottom-edge g-vector simplification needs. From √R(J(√Rζ)) = √(2−R)(√Rζ) (rvdSqrtR_modConj_of_mem_K at ξ = √Rζ) and J(√Rζ) = √(2−R)(Jζ) (modConj_rvdSqrtR): √R√(2−R)(Jζ) = √(2−R)√R ζ = √R√(2−R) ζ (commute), so rvdT(Jζ) = rvdT ζ, and rvdT injective gives Jζ = ζ. (So √Rζ ∈ 𝒦 makes ζ J-fixed: Jξ = Δ^{1/2}ξ on 𝒦 forces Jζ = ζ here.)
Proof. By rvdSqrtTwoSubR, rvdSqrtR_commute_rvdSqrtTwoSubR, rvdT, rvdT_injective, modConj_rvdSqrtR, rvdSqrtR_modConj_of_mem_K.
Used by modConj_deviceVecF_bottom_eq_of_mem_K.
Lemma 928 (rvdRC_mul_E_levelSet). source ↗
Spectral-atom eigen-relation R · E({λ = c}) = c · E({λ = c}): the bounded Borel FC sends the coordinate λ to multiplication, so on the level set {λ = c} the operator R = ∫λ dE acts as the scalar c. Route: R = borelFC(coord) (rvdRC_eq_borelFC), E(s) = borelFC(𝟙_s) (borelFC_indicator), the pointwise identity coord·𝟙_s = c·𝟙_s, then borelFC_mul + borelFC_const. With R/2−R injectivity this kills the endpoint spectral atoms (E({0}) = E({2}) = 0).
Proof. By norm_indicatorOne_le, borelFC, borelFC_mul, borelFC_const, borelFC_indicator, borelFC_congr, specCoord, specCoord_measurable, specCoord_norm_le, rvdRC_eq_borelFC.
Used by rvdRC_E_zero_levelSet, rvdRC_E_two_levelSet.
Lemma 929 (rvdRC_E_zero_levelSet). source ↗
E({λ = 0}) = 0 — no spectral atom at 0: from R · E({0}) = 0 (rvdRC_mul_E_levelSet at c = 0) and R injective (rvdRC_injective). So 0 is not an eigenvalue of R.
Proof. By rvdRC_injective, rvdRC_mul_E_levelSet.
Used by rvdSpecMeasure_zero_levelSet.
Lemma 930 (rvdRC_E_two_levelSet). source ↗
E({λ = 2}) = 0 — no spectral atom at 2: from R · E({2}) = 2 · E({2}), so (2 − R) · E({2}) = 0, and 2 − R injective (rvdTwoSubRC_injective).
Proof. By projK, projIK, rvdTwoSubRC, rvdTwoSubRC_apply, rvdTwoSubRC_injective, rvdRC_mul_E_levelSet.
Used by rvdSpecMeasure_two_levelSet.
Lemma 931 (rvdRC_mul_rvdTwoSubRC_denseRange). source ↗
A.restrictScalars ℝ has dense range (self-adjoint + injective).
Proof. By restrictScalars_star, rvdRC_mul_rvdTwoSubRC_isSelfAdjoint, rvdRC_mul_rvdTwoSubRC_injective.
Used by modUnitary_commute_rvdPmQ_rs.
Lemma 932 (modUnitary_commute_rvdPmQ_rs). source ↗
The modular covariance [U_t, D] = 0 (operator form): the modular flow commutes with the antilinear D = P−Q. From the intertwiner applied to the θ-fixed damped function hΩ (D·(U_t·A)=(U_t·A)·D), D·A=A·D, and cancelling A by its dense range.
Proof. By projK, projIK, rvdRC, rvdTwoSubRC, rvdTwoSubRC_apply, rvdPmQ_commute_A, covM, cfcΩ, twΩ, cfcΩ_intertwine, hΩ, twΩ_hΩ, cfcΩ_hΩ, rvdRC_mul_rvdTwoSubRC_denseRange.
Used by modUnitary_commute_rvdPmQ.
Lemma 933 (modUnitary_commute_rvdPmQ). source ↗
The modular covariance [U_t, D] = 0 (pointwise): U_t(D ξ) = D(U_t ξ). Combined with [U_t, R] = 0 this gives full standard-subspace invariance U_t 𝒦 = 𝒦.
Proof. By modUnitary_commute_rvdPmQ_rs.
Used by modUnitary_mapsTo_K, modConj_commute_modUnitary.
Lemma 934 (modUnitary_mapsTo_K). source ↗
Full standard-subspace invariance U_t 𝒦 ⊆ 𝒦 — both obligations ([U_t,R]=0 and the covariance [U_t,D]=0) now discharged.
Proof. By modUnitary_mapsTo_K_of_commute_D, modUnitary_commute_rvdPmQ.
Used by h1_of_stripKMSrvd, oneParticleBW_of_comparison, comparisonDatum_of_gConstancy, gFunction_top_edge_real.
Lemma 935 (modUnitary_commute_rvdT). source ↗
U_t commutes with T = √(R(2−R)) (both functions of R; via [U_t,R]=0 and Commute.cfc_real).
Proof. By rvdRC, rvdTwoSubRC, rvdSqrtR, rvdSqrtTwoSubR, modUnitary_commute_rvdRC.
Used by modConj_commute_modUnitary.
Lemma 936 (modConj_commute_modUnitary). source ↗
J Δ^{it} = Δ^{it} J — the modular conjugation J commutes with the modular flow. Now UNBLOCKED by the covariance [U_t,D]=0: since D = J·T and U_t commutes with both D and T, J commutes with U_t on the dense range T. (One of the canonical Tomita–Takesaki relations.)
Proof. By rvdPmQ, rvdT, rvdT_restrictScalars_denseRange, modConj_rvdT, modUnitary_commute_rvdPmQ, modUnitary_commute_rvdT.
Used by comparisonDatum_of_gConstancy, gFunction_real_eq, gFunction_top_edge_real, modConj_deviceVecF_bottom.
Definition 937 (gaussSmear). source ↗
The Gaussian-smeared vector (n/π)^{1/2}∫ e^{−n t²} V_t η dt (without the normalisation constant): the construction RvD use to produce a dense set of entire vectors inside the real subspace K.
Used by oneParticleBW_niceWedge, h1_of_stripKMSrvd, gConstancy_of_inputs, oneParticleBW_of_inputs, oneParticleBW_of_stripKMSrvd_density, oneParticleBW_complete, oneParticleBW_wedge_complete, gConstancy_entire, and 14 more.
Lemma 938 (gaussSmear_integrable). source ↗
The smeared integrand is Bochner-integrable: dominated by e^{−n t²}·‖η‖ (a Gaussian), since V_t is norm-non-increasing and the orbit is continuous.
Proof. Immediate from the definitions.
Used by gaussSmear_mem_K, gaussSmear_smul_left, entireVec_sub.
Lemma 939 (gaussSmear_mem_K). source ↗
The smeared vector lands in K. Since e^{−n t²} ≥ 0 is a real scalar and V_t η ∈ K (real-subspace invariance), the Bochner integral stays in the closed real subspace K — because the ℝ-linear orthogonal projection projK commutes with the integral and fixes the integrand (ContinuousLinearMap.integral_comp_comm). First brick of the entire-vector construction.
Proof. By projK, mem_K_iff_projK, gaussSmear_integrable.
Used by oneParticleBW_niceWedge, h1_of_stripKMSrvd, oneParticleBW_wedge_complete.
Lemma 940 (gaussSmear_smul_left). source ↗
The translation property of the smeared vector: V_s (gaussSmear V n η) = ∫ e^{−n t²}·V_{s+t} η dt. Applying the unitary V_s (a continuous linear map) commutes with the Bochner integral (integral_comp_comm) and, via the group law, shifts the orbit. After the change of variables u = s + t the right side is ∫ e^{−n (u−s)²}·V_u η du, whose integrand is entire in the parameter s — this is what makes gaussSmear V n η an entire vector for V (RvD’s key property toward Theorem 3.8).
Proof. By gaussSmear_integrable.
Used by gaussSmearC_ofReal.
Definition 941 (entireVec). source ↗
The normalised entire vector η_n = √(n/π)·gaussSmear V n η — RvD’s dense entire vectors in K.
Used by gConstancy_of_entireVec_limit, gConstancy_eta_of_bottom, entireVec_sub, entireVec_sub_norm_le, entireVec_tendsto.
Lemma 942 (entireVec_sub). source ↗
Mollifier form of the error η_n − η = √(n/π)·∫ e^{−n t²}·(V_t η − η) dt. Subtracting the normalised constant η = √(n/π)·∫ e^{−n t²}·η dt (Gaussian normalisation) from the smeared vector. This is the setup for the density η_n → η: as n → ∞ the Gaussian concentrates at t = 0, where V_t η → η by strong continuity.
Proof. By gaussSmear, gaussSmear_integrable.
Used by entireVec_sub_norm_le.
Lemma 943 (entireVec_sub_norm_le). source ↗
The density error bound ‖η_n − η‖ ≤ √(n/π)·∫ e^{−n t²}·‖V_t η − η‖ dt. Reduces the vector density to a scalar Gaussian-mollifier limit of t ↦ ‖V_t η − η‖, a bounded continuous function vanishing at t = 0 (V_0 η = η + strong continuity). From entireVec_sub + norm_integral_le_integral_norm.
Proof. By entireVec_sub.
Used by entireVec_tendsto.
Lemma 944 (gauss_mollifier_change_of_var). source ↗
Change of variables for the Gaussian mollifier u = √n·t: ∫ e^{−u²}·f(u/√n) du = √n·∫ e^{−n t²}·f(t) dt. The substitution that turns the concentrating Gaussian kernel into a fixed Gaussian e^{−u²} against the rescaled f(u/√n), so the mollifier limit follows from dominated convergence (f(u/√n) → f(0)).
Proof. Immediate from the definitions.
Used by gauss_density_tendsto.
Lemma 945 (gauss_mollifier_integral_tendsto). source ↗
The fixed-Gaussian mollifier limit (dominated convergence): for bounded continuous f, ∫ e^{−u²}·f(u/√n) du → ∫ e^{−u²}·f(0) du as n → ∞. Since u/√n → 0 and f is continuous, f(u/√n) → f(0) pointwise, dominated by e^{−u²}·M.
Proof. Immediate from the definitions.
Used by gauss_density_tendsto.
Lemma 946 (gauss_density_tendsto). source ↗
The scalar Gaussian density √(n/π)·∫ e^{−n t²}·f(t) dt → f(0) as n → ∞, for bounded continuous f. Combines the change of variables u = √n·t (gauss_mollifier_change_of_var) with the fixed-Gaussian limit (gauss_mollifier_integral_tendsto): √(n/π)·∫ e^{−n t²}f = √(1/π)·∫ e^{−u²}f(u/√n) → √(1/π)·∫ e^{−u²}f(0) = f(0). Applied to f(t) = ‖V_t η − η‖ (bounded by 2‖η‖, vanishing at 0) this lands the RvD entire-vector density η_n → η.
Proof. By gauss_mollifier_change_of_var, gauss_mollifier_integral_tendsto.
Used by entireVec_tendsto.
Lemma 947 (entireVec_tendsto). source ↗
RvD entire-vector density η_n → η: the normalised entire vectors η_n = √(n/π)·∫ e^{−n t²}·V_t η dt converge to η as n → ∞, for any strongly-continuous one-parameter contraction V with V_0 η = η. Squeeze: 0 ≤ ‖η_n − η‖ ≤ √(n/π)·∫ e^{−n t²}·‖V_t η − η‖ → ‖V_0 η − η‖ = 0 (entireVec_sub_norm_le + gauss_density_tendsto on the bounded continuous t ↦ ‖V_t η − η‖). With entireVec_mem_K this makes the entire vectors a dense subset of the real subspace K — the totality input for the RvD Theorem 3.8 KMS-uniqueness argument (hUniq).
Proof. By entireVec_sub_norm_le, gauss_density_tendsto.
Used by gConstancy_of_entireVec_limit.
Definition 948 (gaussSmearC). source ↗
The complex orbit of the smeared vector: G(z) = ∫ e^{−n(u−z)²}·V_u η du, an H-valued function of complex time z. On the real axis it is V_s(gaussSmear V n η); it is entire in z.
Used by h1_of_stripKMSrvd, gConstancy_of_inputs, oneParticleBW_of_inputs, oneParticleBW_of_stripKMSrvd_density, gFunction_eq_zero_const, gConstancy_entire, gFunction_top_edge_real_all, gConstancy_entire_of_bottom, and 17 more.
Lemma 949 (gaussSmearC_integrable). source ↗
The complex-orbit integrand is Bochner-integrable for every fixed z: dominated by the shifted Gaussian e^{n·(Im z)²}·e^{−n(u−Re z)²}·‖η‖ (since Re(−n(u−z)²) = −n(u−Re z)² + n(Im z)²).
Proof. Immediate from the definitions.
Used by hasDerivAt_gaussSmearC, gaussSmearC_norm_le.
Lemma 950 (gaussSmearC_ofReal). source ↗
Real-axis agreement gaussSmearC V n η ↑s = V_s(gaussSmear V n η). On the real axis the complex orbit reduces to the genuine unitary-group orbit of the smeared vector: the complex Gaussian kernel e^{−n(u−s)²} collapses to its real value and, after the translation u = s + t, equals ∫ e^{−n t²}·V_{s+t} η dt = V_s(gaussSmear V n η) (gaussSmear_smul_left). This anchors the entire extension gaussSmearC to the actual flow V.
Proof. By gaussSmear_smul_left.
Used by gFunction_bottom_real_of_faithful_kms, gFunction_real_eq.
Lemma 951 (integrable_abs_add_mul_exp_neg_mul_sq). source ↗
Linear×Gaussian integrability Integrable (u ↦ (|u| + c)·e^{−b u²}) for b > 0 — a degree-one polynomial against a Gaussian. |u|·e^{−b u²} is integrable (norm of u·e^{−b u²}, integrable_mul_exp_neg_mul_sq) and c·e^{−b u²} is integrable; their sum dominates the derivative of the complex orbit (the ‖2n(u−z)·e^{−n(u−z)²}‖ bound), so this is the integrable dominating function for the holomorphy of gaussSmearC.
Proof. Immediate from the definitions.
Used by hasDerivAt_gaussSmearC.
Lemma 952 (hasDerivAt_gaussSmearC). source ↗
The complex orbit is entire: gaussSmearC V n η is complex-differentiable at every z₀, with HasDerivAt given by differentiation under the integral sign, (gaussSmearC V n η)'(z₀) = ∫ (2n(u−z₀)·e^{−n(u−z₀)²})·V_u η du. The derivative integrand is dominated, uniformly for z in a unit ball around z₀, by the integrable linear×Gaussian 2n·C₁·‖η‖·(|u−Re z₀|+|Im z₀|+2)·e^{−(n/2)(u−Re z₀)²} — using Re(−n(u−z)²) = −n(u−Re z)²+n(Im z)², the AM-GM bound (u−Re z)² ≥ (u−Re z₀)²/2 − 2, and |Im z| ≤ |Im z₀|+1. This entirety is what makes the KMS correlation z ↦ ⟨gaussSmearC … z, ·⟩ holomorphic on the strip (RvD Theorem 3.8).
Proof. By gaussSmearC_integrable, integrable_abs_add_mul_exp_neg_mul_sq.
Used by differentiable_gaussSmearC.
Lemma 953 (differentiable_gaussSmearC). source ↗
The complex orbit is entire. gaussSmearC V n η is complex-differentiable on all of ℂ (HasDerivAt at every point, hasDerivAt_gaussSmearC). Composed with a continuous-linear functional this gives the entire KMS correlation needed for the strip-uniqueness step of RvD Theorem 3.8.
Proof. By hasDerivAt_gaussSmearC.
Used by differentiableOn_gFunction, diffContOnCl_gFunction, differentiable_corrC.
Definition 954 (corrC). source ↗
The KMS two-point correlation of two entire vectors, corrC ξ V n η z = ⟨ξ, gaussSmearC V n η z⟩ — the analytic object the strip-uniqueness step compares between two candidate modular flows.
Used by corrC_bdd_halfStrip, gFunction_bottom_real_of_kms_match, gFunction_bottom_real_of_faithful_kms, differentiable_corrC, corrC_norm_le.
Lemma 955 (differentiable_corrC). source ↗
The KMS correlation is entire: z ↦ ⟨ξ, gaussSmearC V n η z⟩ is complex-differentiable on all of ℂ, being the continuous-linear functional innerSL ℂ ξ composed with the entire orbit (differentiable_gaussSmearC).
Proof. By gaussSmearC, differentiable_gaussSmearC.
Used by gFunction_bottom_real_of_kms_match.
Lemma 956 (gaussSmearC_zero). source ↗
The complex orbit at 0 is the smeared vector: gaussSmearC V n η 0 = gaussSmear V n η (h(0)=η_n). At z = 0 the complex Gaussian e^{−n(u−0)²} collapses to the real e^{−n u²}. Used to evaluate the KMS correlation at the origin: g(0) = ⟨w, η_n⟩, the comparison point in RvD Theorem 3.8.
Proof. Immediate from the definitions.
Used by gFunction_zero.
Lemma 957 (gaussSmearC_norm_le). source ↗
Gaussian bound on the complex orbit: ‖gaussSmearC V n η z‖ ≤ e^{n(Im z)²}·‖η‖·√(π/n). The complex Gaussian e^{−n(u−z)²} has modulus e^{−n(u−Re z)²+n(Im z)²}, so the orbit’s norm is at most e^{n(Im z)²}·‖η‖·∫ e^{−n(u−Re z)²} = e^{n(Im z)²}·‖η‖·√(π/n). On the closed KMS strip 0 ≤ Im z ≤ 1 this gives a uniform bound e^{n}·‖η‖·√(π/n) — the boundedness hypothesis the strip-uniqueness step requires.
Proof. By gaussSmearC_integrable.
Used by gFunction_eq_zero_const, corrC_norm_le.
Lemma 958 (corrC_norm_le). source ↗
Gaussian bound on the KMS correlation: |corrC ξ V n η z| ≤ ‖ξ‖·e^{n(Im z)²}·‖η‖·√(π/n). Cauchy–Schwarz (innerSL norm ≤ ‖ξ‖) over gaussSmearC_norm_le. On the closed strip 0 ≤ Im z ≤ 1 the correlation is uniformly bounded — the bound hypothesis of StripUniqueness.eqOn_of_bdd_holomorphic_strip.
Proof. By gaussSmearC, gaussSmearC_norm_le.
Used by corrC_bdd_halfStrip.
Definition 959 (modCharC). source ↗
The complexified modular character u_z(r) = exp(i·z·log((2−r)/r)) on (0,2) (and 1 outside) — the analytic continuation of modChar to complex time z.
Used by deviceOpC_bottomEdge_eq, devCharDeriv_norm_le_slab, devChar_slope_norm_le, measurable_modCharC, modCharC_of_mem, modCharC_ofReal, modCharC_add, hasDerivAt_modCharC, and 12 more.
Lemma 960 (measurable_modCharC). source ↗
The complexified character is Borel measurable (in r, for fixed z).
Proof. Immediate from the definitions.
Used by measurable_devChar.
Lemma 961 (modCharC_of_mem). source ↗
On (0,2) the complexified character is the bare exponential.
Proof. Immediate from the definitions.
Used by modCharC_add, hasDerivAt_modCharC, modCharC_norm, modCharC_zero, devChar_neg_half_I.
Lemma 962 (modCharC_ofReal). source ↗
On the real axis the complexification recovers modChar.
Proof. Immediate from the definitions.
Used by deviceOpC_bottomEdge_eq, devChar_ofReal.
Lemma 963 (modCharC_add). source ↗
The complexified modular character is an exponential homomorphism in z: u_{z+w}(r) = u_z(r)·u_w(r). On (0,2) it is exp(i(z+w)L) = exp(izL)·exp(iwL) (Complex.exp_add, L = log((2−r)/r)); off (0,2) both sides are 1. This drives the device’s t-translation d_{(t:ℂ)+z}(r) = u_t(r)·d_z(r) — e.g. the bottom-edge factorization deviceOpC(t−i/2) = Δ^{it}·deviceOpC(−i/2).
Proof. By modCharC_of_mem.
Used by deviceOpC_bottomEdge_eq.
Lemma 964 (hasDerivAt_modCharC). source ↗
The complex z-derivative of the modular character: d/dz u_z(r) = i·log((2−r)/r)·u_z(r). This is the pointwise derivative that, integrated against the spectral measure and dominated in the regular regime, gives holomorphy of the strip extension z ↦ ∫ u_z dμ under the integral sign.
Proof. By modCharC_of_mem.
Used by hasDerivAt_devChar.
Lemma 965 (modCharC_norm). source ↗
The exact modulus of the complexified character on the strip: ‖u_z(r)‖ = exp(−Im(z)·log((2−r)/r)). On the real axis (Im z = 0) this is 1; for Im z ∈ (0,1] it is the modular weight raised to −Im z. This is the seed of the boundedness of the strip extension of ⟪ξ, Δ^{it} ξ⟫ in the regular spectral regime (σ(R) ⊆ [a, 2−a]), where the exponent stays bounded.
Proof. By modCharC_of_mem.
Used by devChar_norm_le, devChar_norm_eq.
Definition 966 (devChar). source ↗
The device character d_z(r) = ((2−r)/r)^{iz}·√r = modCharC z r · √r (RvD Prop 3.7).
Used by deviceOpC_neg_half_eq, devSpecReal, devSpecReal_measurable, deviceOpC, deviceOpC_norm_le, deviceOpReal_zero, deviceOpC_bottomEdge_eq, devCharDeriv_norm_le_slab, and 20 more.
Lemma 967 (measurable_devChar). source ↗
The device character is Borel measurable in r (for fixed z).
Proof. By modCharC, measurable_modCharC.
Used by devSpecReal_measurable, deviceOpC_bottomEdge_eq, tendsto_integral_devChar_remainder_sq, deviceOpC_sub, deviceOpC_slope_normSq, deviceOpC_diff_normSq, tendsto_integral_devChar_diff_sq.
Lemma 968 (devChar_ofReal). source ↗
On the real axis the device character is modChar t · √r (the Δ^{it}·√R part of the continuation).
Proof. By modCharC, modCharC_ofReal.
Used by deviceOpReal_eq.
Lemma 969 (modCharC_zero). source ↗
The modular character at z = 0 is 1 (exp(0) = 1 on (0,2), 1 off it).
Proof. By modCharC_of_mem.
Used by devChar_zero.
Lemma 970 (devChar_zero). source ↗
Device character at z = 0 is √r (= R^{1/2} at the operator level): d_0(r) = √r. The device interpolation starts at √R (so deviceOpC 0 ζ = R^{1/2}ζ = ξ, giving the g-function value g(0) = ⟨η, Jξ⟩).
Proof. By modCharC, modCharC_zero.
Used by deviceOpReal_zero, deviceOpReal_eq.
Lemma 971 (devChar_neg_half_I). source ↗
Device character at the bottom edge z = −i/2 is √(2−r) (= (2−R)^{1/2} at the operator level): d_{−i/2}(r) = √(2−r) for r ∈ (0,2). The device interpolation ends at (2−R)^{1/2} (so deviceOpC (−i/2) ζ = (2−R)^{1/2}ζ = Jξ, the half-modular-shift Δ^{1/2} = J on 𝒦). Computed from Complex.exp(I·(−I/2)·log((2−r)/r))·√r = √((2−r)/r)·√r = √(2−r).
Proof. By modCharC, modCharC_of_mem.
Used by deviceOpC_neg_half_eq.
Lemma 972 (devChar_norm_le). source ↗
The device character is bounded by √2 on the half-strip {−1/2 ≤ Im z ≤ 0}, uniformly over the spectrum r ∈ (0,2) — with NO regular-window assumption (RvD Lemma 3.6 / Prop 3.7). Writing b = −Im z ∈ [0, 1/2], ‖d_z(r)‖ = exp(b·log((2−r)/r))·√r; in log form b·log(2−r) + (1/2 − b)·log r ≤ (1/2)·log 2 since log(2−r), log r ≤ log 2 and the coefficients b, 1/2 − b are nonnegative and sum to 1/2. The √r factor (the +1/2 exponent of R^{−iz+1/2}) is exactly what cancels the r^{−iz} blow-up, so the device continuation is bounded-holomorphic on the half-strip for ANY standard subspace — the U-side boundedness the strip-uniqueness comparison consumes.
Proof. By modCharC, modCharC_norm.
Used by devChar_norm_le_Icc.
Lemma 973 (devChar_norm_le_Icc). source ↗
The device character is bounded by √2 on the CLOSED interval [0,2] (the spectrum-ready strengthening of devChar_norm_le). On the open interior (0,2) this is devChar_norm_le; at the endpoints r ∈ {0,2} the modular character collapses to 1 (r ∉ (0,2)), so d_z(r) = √r with ‖d_z(r)‖ = √r ≤ √2. In particular d_z(0) = 0 (the √r factor kills the r → 0 singularity outright). Since 0 ≤ R ≤ 2, the spectrum of R lies in [0,2], so this is the bound the borelFC construction of the operator device vector (2−R)^{iz}R^{−iz+1/2}ζ = d_z(R)ζ consumes.
Proof. By modCharC, devChar_norm_le.
Used by devSpecReal_norm_le, deviceOpC_bottomEdge_eq, deviceOpC_sub, deviceOpC_slope_normSq, deviceOpC_diff_normSq, tendsto_integral_devChar_diff_sq.
Lemma 974 (devChar_norm_eq). source ↗
The device-character modulus in rpow form: ‖d_z(r)‖ = (2−r)^{−Im z}·r^{1/2+Im z} on (0,2). From ‖d_z(r)‖ = exp(−Im z·log((2−r)/r))·√r (modCharC_norm), converting exp(c·log x) = x^c, ((2−r)/r)^c = (2−r)^c·r^{−c}, and r^{−Im z}·r^{1/2} = r^{1/2+Im z}. This exposes the two rpow-with-nonnegative-exponent factors (−Im z ∈ (0,1/2), 1/2+Im z ∈ (0,1/2) on the open half-strip) that rpow_mul_abs_log_le pairs against the log((2−r)/r) of the derivative.
Proof. By modCharC, modCharC_norm.
Used by devChar_deriv_norm_le.
Lemma 975 (rpow_mul_abs_log_le). source ↗
Uniform x^δ·|log x| bound (the heart of the device-derivative domination): for x ∈ (0,2] and δ ∈ (0,1], x^δ·|log x| ≤ 2/δ + log 2. On (0,1] use log x⁻¹ ≤ (x⁻¹)^{δ/2}/(δ/2) (Real.log_le_rpow_div) so x^δ·|log x| ≤ 2·x^{δ/2}/δ ≤ 2/δ; on [1,2] use log x ≤ log 2, x^δ ≤ 2. This is the polynomial-beats-log estimate that tames the log((2−r)/r) factor of the device z-derivative against the r^{1/2±·} factors of ‖d_z‖, giving the integrable constant dominator.
Proof. Immediate from the definitions.
Used by devChar_deriv_norm_le.
Lemma 976 (devChar_deriv_norm_le). source ↗
Uniform domination of the device z-derivative on a half-strip slab (the assembled dominator for holomorphy of devCorrExt). For z with −Im z = b ∈ [β₀, β₁] ⊂ (0, 1/2) and r ∈ (0,2), the derivative coefficient |log((2−r)/r)|·‖d_z(r)‖ is bounded by the constant √2·(2/β₀ + log2) + √2·(2/(1/2−β₁) + log2), uniformly in r and over the slab. Proof: write ‖d_z(r)‖ = (2−r)^b·r^{1/2−b} (devChar_norm_eq), split |log((2−r)/r)| ≤ |log(2−r)| + |log r|, and apply rpow_mul_abs_log_le to (2−r)^b·|log(2−r)| and r^{1/2−b}·|log r|, bounding the complementary rpow factors by √2. This is the integrable constant dominator (μ finite) that hasDerivAt_integral_of_dominated_loc_of_deriv_le consumes — with NO regular-window assumption.
Proof. By devChar_norm_eq, rpow_mul_abs_log_le.
Used by devCharDeriv_norm_le_slab, devChar_slope_norm_le.
Lemma 977 (hasDerivAt_devChar). source ↗
The complex z-derivative of the device character: d/dz d_z(r) = i·log((2−r)/r)·d_z(r) (same modular frequency as modCharC, since the √r factor is z-constant). This is the pointwise derivative that, integrated against the spectral measure and dominated on the open half-strip (where −Im z ∈ (0,1/2), so the r^{1/2+Im z} factor of ‖d_z‖ keeps log·d_z bounded), gives holomorphy of devCorrExt.
Proof. By modCharC, hasDerivAt_modCharC.
Used by hasDerivAt_devChar_Icc.
Lemma 978 (hasDerivAt_devChar_Icc). source ↗
The device-character z-derivative on the CLOSED interval [0,2] (covering the spectrum endpoints). On (0,2) this is hasDerivAt_devChar. At r ∈ {0,2} the modular character collapses to 1, so d_z(r) = √r is z-constant (derivative 0), and the formula’s coefficient also vanishes because (2−r)/r = 0 there (2/0 = 0 at r=0, 0/2 = 0 at r=2) gives log 0 = 0. So the same HasDerivAt statement holds across [0,2] — the form the differentiate-under-the-spectral-integral holomorphy of devCorrExt needs (the spectrum σ(R) ⊆ [0,2] may include the endpoints).
Proof. By modCharC, hasDerivAt_devChar.
Used by devChar_slope_norm_le, tendsto_devChar_slope, tendsto_integral_devChar_diff_sq.
← all sections · ← StandardSubspaceModular · StripUniqueness →