For every real \(s {\gt} 0\),

Proved clean, for all real \(s{\gt}0\), not merely the sampled \(s=1,2,3\): a \(\pi \)-substitution reduces the integral to the pre-existing zeta-bridge identity of § Thread S (SinhZetaBridge.sinh_mellin_zeta) at exponent \(s+1\). Corollaries give \(m_1 = 1/8\) and \(m_3 = 1/16\) exactly.

For every real \(\lambda \neq 0\),

Proved clean: Euler’s reflection formula (\(\Gamma (z)\Gamma (1-z) = \pi /\sin (\pi z)\), unconditional in Mathlib) shifted by one factor of \(i\lambda \), with \(\sin (x\cdot i) = i\sinh (x)\) turning the denominator real.

For the \(L\)-fold chain convolution of \(P\) against itself,

and for every \(L \geq 1\): \(0 {\lt} \mathcal{M}_L \leq (1/8)^L\). This is a statement about the convolution integral \(\mathcal{M}_L\) itself, not a claim about any physical loop amplitude.

Proved clean, for every \(L\) at once (not instantiated at small \(L\)): the \(L\)-fold integral is encoded via a recursively-defined chain kernel realizing Fubini/Tonelli’s own iterated-integral expansion of \(\mathcal{M}_L\) (peeling off one loop variable, its external weight, and its connecting rung, at a time), carried entirely in the extended nonnegative reals so Tonelli’s theorem and monotonicity of the integral are unconditional — exactly mirroring the paper’s own proof, which bounds every rung \(P(|\lambda _j-\lambda _{j+1}|)\) by \(1\), discards it, and factorizes what remains via \(\int _0^\infty P(\lambda )d\lambda = \pi /4\).

With \(\kappa (t) := (2\sinh t)^{-1}\), for every real \(s {\gt} 1\),

Proved clean: ‘kinematic_block_v1.tex‘, Proposition prop:zetabridge(a), at the paper’s own kernel normalization — a direct corollary of the pre-existing Thread S zeta bridge (the leading factor of \(2\) there cancels \(\kappa \)’s own \(1/2\)).

For every real \(\lambda \),

as a genuine infinite product (the partial products converge). Proved clean: blackbody_law_qg_dtoupin_v1.tex, Test T4 — stronger than the paper’s own numerical certification, which truncates at \(N=2000\) with a Hurwitz-zeta tail bound. Derived from Mathlib’s Euler product for \(\sin \) via the substitution \(z=i\lambda \).

For every real \(\lambda \) with \(|\lambda |{\lt}1\),

equivalently \(\log P(\lambda ) = -\sum _{k\ge 1}(-1)^{k+1}\zeta (2k)\lambda ^{2k}/k\). Proved clean: blackbody_law_qg_dtoupin_v1.tex, Test T5 ("cumulants are even zeta values"). Derived by taking \(\log \) of the Weierstrass product (Theorem 17.5), expanding each factor’s \(\log (1+x)\) as its Taylor series, and swapping the resulting double sum (joint summability from an explicit product majorant).

For every real \(\lambda {\gt} 0\), with \(n_B(y) := 1/(e^y-1)\) the Bose occupation number,

Proved clean: the zero-point contributions of the two Bose terms cancel exactly, leaving a genuine Planck-form identity for \(P\).

For every real \(\lambda \neq 0\), the partial products of \(1+\lambda ^2/n^2\) converge to \(1/P(\lambda )\). Proved clean: an immediate corollary of Theorem 17.5.

For every real \(\lambda \neq 0\), with \(n_B(y) := (e^y-1)^{-1}\) the Bose–Einstein occupation number,

Proved clean: from Modular_Thermality_of_the_Celestial_Spectral_ Weight.tex and Spectral_Weight_from_Principal_Series.tex (identical statement in both) — the papers Daniel has designated as the canonical replacements for the earlier haar-QG/kinematic-block/blackbody series. Pure hyperbolic algebra: \(n_B(y) - n_B(2y) = 1/(2\sinh y)\) from \(e^{2y}-1=(e^y-1)(e^y+1)\), no Mathlib gap. The paper’s two other equivalent forms (the oscillator-sum series and the \(E(x)=(x/2)\coth (x/2)\) zero-point-cancellation form) are not separately formalized: Mathlib has no coth function, and the oscillator sum is definitionally the same geometric series already inside Real.sinh’s own definition.

For every integer \(n\), the complex-analytic continuation \(P_{\mathbb C}(z) := \pi z/\sinh (\pi z)\) of the Plancherel weight has, at \(z = in\),

Proved clean: Modular_Thermality_of_the_Celestial_Spectral_Weight.tex, Proposition "Equivalent descriptions" item (iv). Res is not invoked as a named Mathlib operator (no general residue-calculus API exists at the pinned commit); the residue is instead the literal punctured-neighborhood limit the paper’s own script evaluates numerically, formalized here as a genuine Tendsto statement. Proof: \(\sinh (\pi (in+\varepsilon )) = (-1)^n\sinh (\pi \varepsilon )\) (addition formula plus \(\sinh (\pi in)=0\), \(\cosh (\pi in)=(-1)^n\)), and \(P_{\mathbb C}(\varepsilon )\to 1\) as \(\varepsilon \to 0\) from Complex.hasDerivAt_sinh via the chain rule.

For every real \(\lambda \neq 0\),

as a genuine unconditional HasSum, not a numerically-truncated approximation. Proved clean: the first half of the cumulant-law chain (item (v) of the "Six faces"/"Equivalent descriptions" proposition, \(\log P(\lambda ) = -\sum (-1)^{k+1}\zeta (2k) \lambda ^{2k}/k\)) — from thm:sinh-weierstrass above, dividing by the nonzero constant \(\pi \lambda \), applying Real.log (continuous at the limit, proved positive here from Real.sinh’s strict monotonicity), and upgrading the resulting convergent partial sums of logs to a genuine HasSum via nonnegativity of every term. Not attempted: expanding each \(\log (1+x)\) into its own power series and swapping the resulting double sum to reach the paper’s closed \(\zeta (2k)\) form — the genuinely new remaining work, scoped precisely in docs/FORMALIZATION_PLAN.md.

For the Gamma-product continuation \(P_{\mathbb C}(z) := \Gamma (1+iz)\Gamma (1-iz)\) and every \(z\ne 0\) with \(1\pm iz\ne 0\) (automatic for real \(z\)),

Proved clean: ‘Principal_Series_Kinematic_Blocks.tex‘, Theorem "Weight-shift relations and the resulting differential equation" — the digamma-free first half (the shift relations themselves), a pure consequence of ‘Complex.Gamma_add_one‘ (‘Γ(s+1)=sΓ(s)‘) applied to each Gamma factor. The theorem’s second half — the resulting first-order ODE for ‘P‘’s Fourier partner, needed for ‘thm:resolved‘’s digamma-moment identification — remains blocked on Mathlib’s missing digamma function.