Dependencies

\(\tfrac {\varepsilon }{2}\int _{\mathbb R} e^{-\varepsilon |u|}\, du = 1\) exactly, for every \(\varepsilon {\gt} 0\).

Every \(L^2\)-admissible non-trivial zero \(\rho \) of \(\zeta (s)\) satisfies \(\mathrm{Re}(\rho ) = \tfrac {1}{2}\).

Dark energy (cosmological constant \(\Lambda \)) is the only free parameter in the gravitational action consistent with shadow symmetry.

At \(L=1\): the open six-point cubic tree (4 vertices, 3 internal edges) with one pair sewing gives 4 external legs, 4 internal edges, cycle rank 1 — the one-loop box topology.

\(c_{2D} = 0 \Rightarrow c_{4D}^{\mathrm{Weyl}} = 0 \Rightarrow n_{\mathrm{gen}} = 3\) (Boyle–Turok 2021).

The three Cayley–Dickson doublings \(\mathbb {R}\to \mathbb {C}\), \(\mathbb {C}\to \mathbb {H}\), \(\mathbb {H}\to \mathbb {O}\) correspond to exactly \(3\) fermion generations.

\(f\) is completely monotone on \((0,\infty )\) if \((-1)^n f^{(n)}(t) \geq 0\) for all \(n\) and all \(t{\gt}0\). Absent from Mathlib at the pinned commit c44e0c8 — no Bernstein/Hausdorff–Widder theory exists upstream.

\(\Phi \) is completely positive if \(\Phi \otimes \mathrm{id}_\beta \) maps positive semidefinite matrices to positive semidefinite matrices for every finite auxiliary dimension \(\beta \).

A structure with fields doubleDisc (tree \(\to \) pair shadow discontinuity), inverseMellin, closePair (the same closure described directly in momentum space), and a field sewing_identity asserting inverseMellin(doubleDisc T a b) = closePair T a b. This is the paper’s own boxed “remaining analytic theorem” (\(\mathcal M^{-1}_{5,6}[\mathrm{dDisc}_{\rm sh}^{(56)}\widetilde T_6] = \tfrac {i}{\ell ^2+i0}T_6(\ell ,p_1,\dots ,-\ell )\)), stated here as a local hypothesis rather than a global axiom or an unnamed gap. Nothing in this file proves sewing_identity for an explicit six-point celestial amplitude, and it is not claimed to be proved. ShadowPairSewing.tree_to_loop_extraction is the (structurally trivial) corollary that the extraction pipeline commutes, conditional on this one named hypothesis.

\(T(\psi _1,\psi _2) := (\overline{\psi _2},\, -\overline{\psi _1})\).

\(\xi (s) = \tfrac {1}{2} s(s-1) \pi ^{-s/2} \Gamma (s/2) \zeta (s)\).

The \(L^2(\mathbb {A}^\times /\mathbb {Q}^\times )\) spectral decomposition is well-defined after Haar regularization:

1. \(K^1\) compact \(\Rightarrow \) finite Haar measure \(\Rightarrow \) \(L^\infty \subseteq L^2\)

2. Peter-Weyl on \(K^1\): \(L^2(K^1) = \bigoplus _\chi \mathbb {C}\cdot \chi \)

3. Plancherel: \(\| f\| ^2 = \sum _\chi |\hat f(\chi )|^2\)

Algebraic core proved: l_infty_subset_l2_compact (1 sorry: integral_mono with bounded functions, Mathlib 4.19 gap). Three axioms: peter_weyl_K1, plancherel_K1, spectrum_discrete_K1.

For \(r{\gt}-1/2\): \(\int _0^\infty (e^{-rx}-e^{-x})e^{-x/2}\, dx = 1/(r+1/2)-2/3\).

For \(r{\gt}1/2\): \(\int _0^\infty (e^{-rx}-e^{-x})e^{x/2}\, dx = 1/(r-1/2)-2\). Together with Lemma 19.8, these are the two purely elementary pieces of the paper’s Archimedean Laplace transform \(A_\infty (r)\); the remaining digamma piece is not formalized here. (Mathlib now supports a real digamma function \(\psi =\Gamma '/\Gamma \) via GppDigamma.digamma — see the QG-Blackbody chapter — but the specific Gauss integral representation of \(\psi \) at general \(r\) this lemma would need is a further step not yet established, distinct from the special values and functional equation already proved.) \(A_\infty \) itself is not assembled in this file.

The Born rule \(P(\psi ) = |\langle \phi |\psi \rangle |^2\) arises as the unique probability measure on \(L^2(K^1)\) induced by Haar measure and Gleason’s theorem.

Proved clean: Haar measure gives a probability measure on \(K^1\); \(\| f\| ^2 = \int |f|^2 d\mu \) normalizes to \(1\). Axioms: K1_haar_probability, born_from_haar, gleason_uniqueness (Gleason 1957, not in Mathlib).

With \(D(x) := Q(x)\) the propagator-denominator function, the closed box denominator \(Q(\ell )\, Q(\ell -p_1)\, Q(\ell -p_1-p_2)\, Q(\ell +p_4)\) is literally the missing closure edge \(Q(\ell )\) times the three denominators already present in the open six-point chain. A definitional identity once the open-chain object is named.

For \(\sigma \neq 1/2\), the symmetric Cesàro mean \((\int _{1/R}^{R} r^{2\sigma -2}\, dr)/(2\log R)\) tends to \(+\infty \) as \(R \to \infty \). Together with the exact value \(1\) at \(\sigma = 1/2\) (born_rule_cesaro), this makes \(\sigma = 1/2\) the unique locus where the inversion-invariant mean is finite and nonzero.

If \(\mathrm{Re}(\rho ) \neq \tfrac {1}{2}\) then \(1-\bar\rho \neq \rho \).

\(t \mapsto e^{-at}\) is completely monotone for \(a \geq 0\). In the paper’s notation this is one term of \(\mathcal{K}(t)=\sum _{\gamma {\gt}0} m_\gamma e^{-\gamma ^2 t}\).

\(s = 1-s \iff \mathrm{Re}(s) = \tfrac {1}{2}\).

The norm-\(1\) idèle class group \(K^1\) is compact (Fujisaki’s lemma, Weil 1974, Ch. IV §2).

Let \(G\) be a compact second-countable topological group, \(\mu \) a Haar measure, and \(\phi : G \to G\) a bicontinuous group automorphism. Then \(\phi _*\mu = \mu \).

The only normed division algebras over \(\mathbb {R}\) are \(\mathbb {R}\), \(\mathbb {C}\), \(\mathbb {H}\), \(\mathbb {O}\) (Hurwitz 1898). There are exactly \(3\) Cayley–Dickson doublings.

Status: carried as the hypothesis HurwitzDimensionHypothesis, not an axiom — the former axiom was retired on 2026-08-30 because no theorem consumed it. The dimension-counting content this chapter actually uses (cdStages_card, exactly_three_doublings, nda_dimensions_image, sedenion_dim_outside_nda_set) is proved outright, with no axiom.

Gap: the real classification is not in Mathlib 4.19.0 (only the complex Gelfand–Mazur theorem is). Note also that Mathlib’s NormedDivisionRing extends DivisionRing and is therefore associative, so \(\mathbb {O}\) does not inhabit it: as literally stated the \(8\) case is vacuous and the reachable content is the Frobenius classification \(\{ 1,2,4\} \). Any attempt to discharge this hypothesis should first restate it over a genuine composition-algebra structure.

If \(\overline{s} = 1 - s\) then \(\mathrm{Re}(s) = \tfrac {1}{2}\).

\(\int _0^\infty e^{-(1+u)t}e^{-\gamma ^2 t}\, dt = 1/(u+1+\gamma ^2)\). The paper’s displayed step converting the Hadamard partial-fraction sum into the heat expansion, by uniqueness of the Laplace transform.

For \(s = \tfrac {1}{2} + i\gamma \), the character \(a \mapsto |a|^{s-1/2}\) has absolute value \(1\).

\(\int _0^\infty e^{-ct}\, dt = 1/c\) for \(c{\gt}0\).

For \(s \in \mathbb {C}\), \(\overline{s} = 1 - s \iff \mathrm{Re}(s) = \tfrac {1}{2}\). (The involution whose fixed locus is the critical line is \(s \mapsto 1-\overline{s}\), not \(s \mapsto 1-s\): the latter fixes only the single point \(s = \tfrac 12\).)

If \(\xi (\rho ) = 0\) then \(\xi (1-\rho ) = 0\).

If \(\zeta (\rho ) = 0\) then \(\zeta (1-\rho ) = 0\).

For \(|\alpha | {\lt} \varepsilon \): \(\tfrac {\varepsilon }{2}\int _{\mathbb R} e^{-\varepsilon |u|}e^{\alpha u}\, du = \varepsilon ^2/(\varepsilon ^2 - \alpha ^2)\).

On any compact topological group, \(\phi _*\mu = \mu \) for \(\phi = (-)^{-1}\). Instance: \(\mathbb {A}^\times /\mathbb {Q}^\times \) with Haar measure \(d^\times a\) satisfies \(d^\times (a^{-1}) = d^\times a\).

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 \(c_{4D}^{\mathrm{Weyl}} = 0\) and SM gauge group, anomaly cancellation (Boyle–Turok 2021) forces \(48 = 16 \times 3\) Weyl fermions, i.e., \(n_{\mathrm{gen}} = 3\).

For the null celestial momentum direction \(q(x,y) = (1{+}x^2{+}y^2,\, 2x,\, 2y,\, 1{-}x^2{-}y^2)\) (metric \((+,-,-,-)\); \(\langle q(x,y),q(x,y)\rangle =0\) identically, for every \(x,y\)) and every \((x_5,y_5)\ne (0,0)\), \(M\in \R \), writing \(r^2:=x_5^2+y_5^2\),

the resulting momenta satisfy \(\omega _5\, q(x_5,y_5) + \omega _6\, q(x_6,y_6) = (M,0,0,0)\) componentwise. Proved clean: ‘Loops_from_Cuts_in_Celestial_Holography.tex‘, Theorem "Cut geometry: antipodal pairing and uniform measure" (‘thm:measure‘) — the algebraic core of the paper’s own claimed solution, verified here by direct vector computation (‘field_simp‘/‘ring‘ on each of the four components after ‘fin_cases‘), independent of and prior to any measure-theoretic argument. Not attempted: uniqueness of this solution (a separate fact about the orbit structure of null directions on the two-sphere), and the phase-space measure reduction itself, \(\dd \Pi _2 = \dd ^2z/[8\pi ^2(1{+}|z|^2)^2]\), \(\int \dd \Pi _2=1/(8\pi )\) — this needs genuine \(\delta ^4\)-constrained pushforward-measure and Jacobian machinery this repository has not built, and is left open as the natural next step of this thread.

This is the bridge from the physics statement (time reversal is antiunitary) to the matrix statement analysed below (time reversal involves a transpose).

On the principal series \(a=d/2+it\): \(K_{\infty ,d}(a) = |\Gamma (d/2+it)|^2/\Gamma (d)\), positive whenever \(d{\gt}0\). Shadow reflection becomes Hermitian conjugation exactly on this line, via \(d-a=\overline{a}\).

For the Archimedean shadow kernel \(K_{\infty ,d}(a) := \Gamma (a)\Gamma (d-a)/\Gamma (d)\): \(K_{\infty ,d}(a) = K_{\infty ,d}(d-a)\).

\(K_{\infty ,2}(\Delta ) = \pi ^2\Gamma _C(\Delta )\Gamma _C(2-\Delta ) = \pi ^2\cdot \Gamma _R(\Delta )\Gamma _R(\Delta +1)\cdot \Gamma _R(2-\Delta )\Gamma _R(3-\Delta )\) — the celestial \(d=2\) cut decomposes exactly into two shadow-paired real Archimedean Gamma sectors, \((\Gamma _R(\Delta ),\Gamma _R(2-\Delta ))\) and its shift \((\Gamma _R(\Delta +1),\Gamma _R(3-\Delta ))\).

For \(0{\lt}s{\lt}1\),

Proved clean: the Beta-reflection integral underlying Loops_from_Cuts_in_Celestial_Holography.tex’s dispersion-relation reconstruction (thm:disp, thm:celdisp), whose Mellin kernel \(\int _0^\infty S^{\sigma -1}/(s'{+}S)\, \dd S = s'^{\sigma -1}\pi /\sin (\pi \sigma )\) reduces, via \(S=s'u\), to the base case \(\int _0^\infty u^{\sigma -1}/(1{+}u)\, \dd u=\pi /\sin (\pi \sigma )\) — a “second Euler Beta integral” on \((0,\infty )\) confirmed absent from Mathlib v4.19.0 by direct grep (only the \((0,1)\) form, Complex.betaIntegral, exists). This theorem is Complex.betaIntegral s (1-s) unfolded to its defining real interval integral and evaluated via Complex.Gamma_mul_Gamma_eq_betaIntegral combined with the reflection formula Complex.Gamma_mul_Gamma_one_sub, cast down to \(\R \) via Complex.ofReal_cpow (valid uniformly on \(x\in [0,1]\), both endpoints included) and intervalIntegral.integral_ofReal. Not attempted: the substitution \(x=t/(1{+}t)\) mapping \((0,1)\leftrightarrow (0,\infty )\) needed to reach the paper’s actual \((0,\infty )\) dispersion kernel — the natural tool is MeasureTheory.integral_image_eq_integral_abs_deriv_smul with a fresh \(\mathrm{Ioo}\, 0\, 1\to \mathrm{Ioi}\, 0\) diffeomorphism, genuine new infrastructure this repository has not built (the algebra was checked by hand, not yet coded), left open as the well-scoped next step.

For real \(a\) with \(|a|{\lt}1\) and \(w\in \mathbb {C}\) with \(|w|=1\), the Blaschke factor \((w-a)/(1-aw)\) has modulus exactly \(1\).

Under \(\Delta = 2s\), shadow \(\Delta \leftrightarrow 2-\Delta \) is the functional equation \(s \leftrightarrow 1-s\).

If \(\Phi \) is completely positive then its Choi matrix is positive semidefinite. Proved for an arbitrary finite-dimensional linear map, not just the transpose. Its contrapositive (GppChoiMatrix.not_completelyPositive_of_not_posSemidef_choiMatrix) is the tool used below.

An exact finite computation: the same product of Kronecker deltas on both sides.

The constructed CHSH value equals \(-1-\sqrt2\) (GppCHSHViolation.chshValue_eq), exceeds the classical bound \(2\) in modulus, and respects Tsirelson’s bound \(2\sqrt2\) (GppCHSHViolation.chshValue_within_tsirelson_bound). All three proved clean.

At the angle configuration \(\theta _{ab}=0,\ \theta _{ab'}=\pi /2, \theta _{a'b}=\theta _{a'b'}=\pi /4\), the CHSH combination \(S = E(a,b)-E(a,b')+E(a',b)+E(a',b')\) with \(E(\theta )=-\cos \theta \) evaluates exactly to \(-1-\sqrt2\) (chshValue_eq), so \(|S| = 1+\sqrt2 {\gt} 2\), exceeding the classical bound, while respecting Tsirelson’s bound \(|S|\le 2\sqrt2\) (chshValue_within_tsirelson_bound). Separately, ckw_forces_zero_concurrence formalizes the elementary consequence of the CKW monogamy inequality: given \(1+x^2 \le y^2 \le 1\), necessarily \(x=0\).

Honest boundary: this is standard textbook CHSH/CKW material, not GPP-specific; the source’s stronger claim that Haar measure on \(\mathrm{Gr}(2,4)\) forces exactly the Tsirelson bound is not formalized, nor is the general quantum correlation-function formalism — only the source’s own explicit numerical evaluation.

\(\mathrm{Re}(\Delta ) = 1\) under \(\Delta = 2s\) gives \(\mathrm{Re}(s) = \tfrac {1}{2}\).

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).

The diagonal lift \(D(s):=(s,s)\) of a scalar 1D weight has \(\Delta (D(s))=2s\) and spin \(J(D(s))=0\).

\(\psi (x+1) = \psi (x) + 1/x\), for \(x\) avoiding the poles of \(\Gamma \).

\(\psi (n+1) = -\gamma + H_n\) (the \(n\)-th harmonic number), for every \(n\in \mathbb {N}\).

\(\psi (1) = -\gamma \), the Euler–Mascheroni constant.

\(\psi (1/2) = -\gamma - 2\log 2\), via Legendre’s duplication formula (already differentiated in Mathlib).

If \(c_{2D} = 0\) (shadow unitarity), then the dark matter relic density \(\Omega _{\mathrm{DM}} {\gt} 0\).

Physics: shadow symmetry breaking generates the DM mass scale; unitarity of the shadow amplitude fixes the abundance. Formalized via axioms shadow_breaking_gives_abundance and shadow_unitarity_abundance_pos.

\(\varphi (2-\Delta )\varphi (\Delta ) = 1\) wherever \(\Lambda (\Delta )\neq 0\) and \(\Lambda (2-\Delta )\neq 0\). This is not evidence toward RH: Eisenstein scattering already contains \(\zeta (s)\) in its functional-equation normalization without that proving anything about its zeros.

With \(\Lambda \) the completed Riemann zeta function and \(\varphi (\Delta ):=\Lambda (\Delta -1)/\Lambda (\Delta )\): \(\varphi (\Delta ) = \Lambda (2-\Delta )/\Lambda (\Delta )\) — immediate from \(\Lambda (1-w)=\Lambda (w)\).

Under \(\Lambda \mapsto \Lambda ^\perp \), the symplectic normalisation forces \(\omega \mapsto \omega ^{-1}\).

\(2^{1-s} = 1\) iff \(s = 1 - 2\pi i k/\log 2\) for some \(k \in \mathbb Z\); every such zero has \(\operatorname {Re} s = 1\) (GppCompletedEta.eta_periodic_zero_re), outside the open critical strip.

\(\xi (s) = \xi (1-s)\) for all \(s \in \mathbb {C}\) away from poles. This is the arithmetic shadow symmetry.

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.

With \(\Gamma _R(s):=\pi ^{-s/2}\Gamma (s/2)\) and \(\Gamma _C(s):=2(2\pi )^{-s}\Gamma (s)\): \(\Gamma _C(s) = \Gamma _R(s)\Gamma _R(s+1)\), for every complex \(s\).

\(\varphi ^2\) and \(\varphi ^{-2}\) are the roots of \(X^2-(\operatorname {tr}A)X+(\det A)\); the discriminant \((\operatorname {tr}A)^2-4\det A = 5\).

The expanding eigenvalue of the minimal-trace hyperbolic element and the finite-place shadow kernel at the independently-selected discriminant, evaluated at the principal-series center, are the same real number: \(\varphi ^2\).

For \(x{\gt}0\): \(x=1+1/x \iff x=\varphi \).

With \(K_{q,1}(s):=(1-q^{-1})/[(1-q^{-s})(1-q^{-(1-s)})]\) (no occurrence of \(\varphi \) in this definition): \(K_{5,1}(1/2)=\varphi ^2\).

For \(x\neq -1\): \(\dfrac {2x+1}{x+1}=x \iff x=\varphi \text{ or } x=-\varphi ^{-1}\).

For any finite point configuration \(x:\mathrm{Fin}\, N\to \mathbb {R}\), weights \(c:\mathrm{Fin}\, N\to \mathbb {C}\), and frequency \(n\in \mathbb {Z}\): \(\sum _{j,k}\bar c_jc_ke^{in(x_j-x_k)}=\bigl|\sum _jc_je^{-inx_j}\bigr|^2\). Pure finite algebra, generalizing the pre-existing gram_square_nonneg (Convolution Squares chapter) to complex amplitudes.

For a finite set of frequencies \(F\subset \mathbb {Z}\) and real weights \(a:\mathbb {Z}\to \mathbb {R}\): \(\sum _{j,k}\bar c_jc_k\sum _{n\in F}a_ne^{in(x_j-x_k)} =\sum _{n\in F}a_n\bigl|\sum _jc_je^{-inx_j}\bigr|^2\), derived from Theorem 23.3 by pure finite-sum reordering.

With \(C(t):=t/(4\sinh (2\pi t))\) the already-derived celestial cut kernel and \(H(t):=(t^2+1/4)\, C(t)\) the Casimir-weighted Archimedean kernel: \(H(t)\geq 0\) for every real \(t\). Proof: \(t\) and \(\sinh (2\pi t)\) always share sign, so their ratio is nonnegative (the \(t=0\) case is Lean’s total-division junk value \(0/0=0\), itself \(\geq 0\)).

The shadow involution \(\phi : g \mapsto g^{-1}\) preserves the Haar measure on any compact group (instance: \(\mathrm{Gr}(2,4)\)).

With \(\zeta _p(s):=(1-\exp (-s\log p))^{-1}\) the local Euler factor as a genuine function of \(s\in \mathbb {C}\) (via Complex.exp, in EulerFactorLogDeriv.lean), \(\zeta _p\) has derivative \(-\bigl(\text{minusLogDerivZetaP}\, p\, s\bigr)\cdot \zeta _p(s)\) at every \(s\) with \(1-p^{-s}\ne 0\), where \(\text{minusLogDerivZetaP}\, p\, s:=\log (p)\cdot p^{-s}/(1-p^{-s})\) — i.e. this closed form genuinely is \(-\zeta _p'/\zeta _p\), from an actual HasDerivAt chain-rule computation through Complex.exp and HasDerivAt.inv, not asserted from the geometric-series shortcut.

For a Hermitian matrix, entrywise complex conjugation coincides with transposition.

With cutKernelExt the continuous extension of cutKernel replacing Lean’s junk value \(0/0=0\) at \(t=0\) by the genuine limit \(C(0)=1/(8\pi )\) (proved from Real.sinh’s derivative at \(0\), , not asserted), and \(H_{\mathrm{ext}}(t):=(t^2+1/4)\, C_{\mathrm{ext}}(t)\): \(H_{\mathrm{ext}}(0) =1/(32\pi )\) () and \(H_{\mathrm{ext}}(t)\geq 0\) for every real \(t\).

For any integer \(n\) with \(|n|{\gt}2\): \(|n|\geq 3\). Applied to \(A\) (trace \(3\), determinant \(1\)): \(A\) attains the minimal possible trace of a hyperbolic element of \(SL_2(\mathbb {Z})\).

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 \(p{\gt}1\) and every real \(t\): the finite-place shadow kernel \(K_p(t):=(1-p^{-1})/(1-2p^{-1/2}\cos (t\log p)+p^{-1})\) is strictly positive. This is the value of the classical Poisson kernel on the circle (radius \(r=p^{-1/2}\)), whose Fourier-coefficient sequence \((r^{|n|})_n\) is termwise nonnegative.

For every \(0\le r{\lt}1\): \(K_r-1\) is positive-type in the sense of GppHaarPositivityWeil.PositiveType — for every finite point configuration and weights, \(\sum _{j,k}\bar c_jc_k(K_r-1)(x_j-x_k)\geq 0\) — for the genuine, untruncated kernel, not merely at finite truncation. Obtained from Theorem 23.5 by passing to the limit \(N\to \infty \): the two-sided Fourier series \(K_r(\theta )-1=\sum _{n\ne 0}r^{|n|}e^{in\theta }\) is established as a genuine HasSum () via Summable built from the geometric tail bound (not by tracking HasSum values through Int.rec, which is what had timed out); \(K^0_{r,N}\to K_r-1\) follows (); and positivity passes to the limit via ge_of_tendsto.

With \(K^0_{r,N}(\theta ):=\sum _{0{\lt}|n|\le N}r^{|n|}e^{in\theta }\) the truncated, vacuum-excluded finite-place kernel: \(\sum _{j,k}\bar c_jc_kK^0_{r,N}(x_j-x_k)\geq 0\) for every truncation \(N\), every finite point configuration, and every \(0\le r\). Follows from Theorem 23.4 plus Finset.sum_nonneg, via the intermediate corollary gram_square_freqSum_nonneg.

If \(\chi _s \in L^2(K^1)\) is an eigenfunction of the shadow involution \(T: a \mapsto a^{-1}\), then \(\mathrm{Re}(s) = \tfrac {1}{2}\).

The proof assembles: Haar self-duality \(\Rightarrow \) \(T\) preserves \(L^2\); Plancherel on \(K^1\) \(\Rightarrow \) \(T\)-eigenvalue is unitary; unitarity \(\Rightarrow \) \(\mathrm{Re}(s) = \tfrac {1}{2}\).

Adèlic infrastructure (Hecke characters, Peter–Weyl on \(K^1\)) awaits Mathlib.NumberTheory.NumberField.Adeles.

The celestial central charge \(c_{2D}\) equals \(\kappa _0\) times the Weyl anomaly \(c_{4D}^{\mathrm{Weyl}}\).

Formalized: the identity is not asserted. It is carried as the explicit hypothesis Link6Hypothesis, so every consumer displays its dependence on Link 6 in its own statement rather than inheriting a global axiom. The five axioms this entry previously named (link6_from_physics plus Weinberg soft-graviton, Cachazo–Strominger celestial OPE, Capper–Duff one-loop Weyl anomaly, Adler–Bardeen non-renormalization) were retired on 2026-08-30; the four physics inputs survive as documented open_ placeholders. The algebraic corollary link6_corollary (\(c_{2D} = 0 \iff c_{4D}^{\mathrm{Weyl}} = 0\), given \(\kappa _0 {\gt} 0\)) is proved clean and is unconditional on Link 6 itself.

For real \(z_0,\varepsilon ,x\) with \(\varepsilon \neq 0\), \(\dfrac {1}{(x-z_0)+i\varepsilon } - \dfrac {1}{(x-z_0)-i\varepsilon } = \dfrac {-2i\varepsilon }{(x-z_0)^2+\varepsilon ^2}\), exactly, with no limiting procedure — the finite-\(\varepsilon \) content of “the jump of a regulated simple pole is a Lorentzian kernel.”

Away from \(x=z_0\), the Lorentzian kernel \(\varepsilon /((x-z_0)^2+\varepsilon ^2)\) tends to \(0\) as \(\varepsilon \to 0^+\) — the rigorous, non-distributional half of “the regulated jump concentrates at the pole.” The complementary mass statement \(\int _\R \varepsilon /((x-z_0)^2+\varepsilon ^2)\, dx = \pi \) for every \(\varepsilon {\gt}0\) (a standard Cauchy/Poisson-kernel fact, reducible to Mathlib’s integral_univ_inv_one_add_sq by the affine substitution \(x=z_0+\varepsilon u\)) is numerically certified in verify_dispersion.py but not additionally formalized this session — the substitution needs a translation-invariance-of-Lebesgue-measure lemma not chased down; named honestly as a gap rather than forced.

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\), the partial products of \(1+\lambda ^2/n^2\) converge to \(1/P(\lambda )\). Proved clean: an immediate corollary of Theorem 17.5.

For a connected cubic tree with \(n = 4+2L\) external leaves (\(V_T = n-2\) trivalent vertices, \(I_T = n-3\) internal edges), sewing \(L\) disjoint pairs among the designated \(2L\) extra leaves leaves \(4\) external legs and \(I = I_T + L = 3L+1\) internal edges, with cycle rank \(\beta _1 = I - V_T + 1 = L\). Proved for all \(L\) by direct computation on the vertex/edge counts (omega); no combinatorial machinery beyond arithmetic is needed since only the counts, not an explicit graph object, are formalized here.

The orthogonal complement \(\Lambda \mapsto \Lambda ^\perp \) on \(\mathrm{Gr}(2,4)\) acts as the antipodal map on \(S^2\) via the Penrose correspondence.

\(L^2(K^1, d^\times a)\) decomposes into finite-dimensional irreducibles, so any left-invariant self-adjoint operator on \(L^2(K^1)\) has discrete spectrum.

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\), 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 real \(t\): \(\left|\dfrac {p^{-it}-p^{-1/2}}{1-p^{-1/2-it}}\right|=1\) at every prime \(p\) (), and the diagonal operator built from this weight on \(\ell ^2(\text{primes})\) is unitary (reusing directly).

For any prime \(p\) and \(\Delta \in \mathbb {C}\): \(|p^{-(\Delta -1)/2}|=1\) iff \(\operatorname {Re}\Delta =1\) — the full iff, both directions, at a single eigenvalue.

On \(\operatorname {Re}\Delta =1\), the diagonal operator for \(A^{\Delta -1}\) is unitary: exact \(\ell ^2\)-norm preservation () plus a genuine two-sided inverse via the conjugate weight, both compositions equal to the identity operator ().

For every \(N\) and every nonzero real polynomial of degree \(\le N\), the weighted polynomial Gram sum over the arithmetic Fisher measure on \(\{ \log p^k\} \) is strictly positive, unconditionally — via the prime-power witness \(2,4,8,\dots ,2^{N+1}\): all carry von-Mangoldt weight \(\log 2\) at pairwise distinct log-support points \((k{+}1)\log 2\), so no nonzero degree-\(N\) polynomial can vanish on all \(N{+}1\) of them.

\(\sum _{n\geq 2}\Lambda (n)n^{-1/2}e^{-(\log n)^2/(4t)}\) is exactly one half of GppWeilLadder.primeSide evaluated at the heat Gaussian \(x\mapsto e^{-x^2/(4t)}\), since that test function is even. Consequence: the whole support-ladder toolkit of WeilSupportLadder.lean applies verbatim to the heat trace’s prime side — the two threads are the same object.

If the Weil/Yakaboylu paired form is positive semidefinite on every finite subset of the nontrivial zero set, then every non-trivial zero of \(\zeta (s)\) satisfies \(\mathrm{Re}(s) = \tfrac {1}{2}\).

Status: the former arithmetic_admissibility axiom (which asserted RH verbatim) is retired. The conditional above is proved with no axioms beyond Mathlib’s built-ins; the open analytic content is the positivity hypothesis (explicit formula / operator compression).

Every nontrivial zero lies on the critical line iff the paired form is positive semidefinite on every finite subset of the nontrivial zero set. A rigorous reduction — not a proof of RH: the analytic input that would discharge the positivity hypothesis is not claimed.

The Einstein field equations \(G_{\mu \nu } = 8\pi G T_{\mu \nu }\) are uniquely determined by:

1. Shadow symmetry \(\Delta \mapsto 2-\Delta \) (diffeomorphism covariance),

2. Two-derivative truncation (\(c_{4D}^{\mathrm{Weyl}} = 0\)),

3. Positive energy (Weyl anomaly positivity).

Algebraic core proved: graviton_shadow_dimension: \((2:\mathbb {Z}) - 2 = 0\) (by decide); lovelock_uniqueness_algebraic: trivial stub.

Axioms: lovelock_theorem (Lovelock 1971), shadow_forces_massless_graviton, c0_eliminates_higher_curvature.

\(\int _0^\infty u/\cosh ^2 u\, du = \log 2\) — that is, \(\eta (1) = \log 2\) in Mellin disguise, proved with no series interchange via the explicit antiderivative \(u\tanh u - \log \cosh u\).

\(D(1-s) = \mathrm{Shadow}_2(D(s))\): the 1D shadow \(s\mapsto 1-s\) and the 2D celestial shadow \((h,\bar h)\mapsto (1-h,1-\bar h)\) intertwine exactly under the diagonal lift.

On the principal series \(\Delta = 1+i\lambda \), time reversal \(T\) sends \(\Delta \mapsto 2-\Delta \): the shadow transform. (Most-cited result in ONON52: 16 cross-references.)

The discontinuity of a celestial amplitude across the shadow cut \(z \mapsto \bar{z}\) (i.e., \(\Delta \mapsto 2-\bar\Delta \)) equals the loop integrand, replacing Feynman diagrams with analytic continuation.

Correction, re-audited 2026-08-15: the cited declaration GppShadowDisc.shadow_discontinuity is a theorem foo : True := trivial stub, not a proof of the statement above. The four “proved clean” facts below it are real, kernel-checked theorems in ShadowDiscontinuity.lean — but they are elementary complex-analysis/algebra lemmas the main claim would use as ingredients, not a proof of the claim itself. See Section 7.2 for the concrete topology-level advance on this thread and the precise remaining analytic gap.

Proved clean (as standalone lemmas, not as a proof of the boxed claim above):

• \(\mathrm{Disc}\, f(x) = 2i\, \mathrm{Im}\, f(x)\) (basic complex analysis).

• Shadow is an involution: \(2-(2-s)=s\).

• Shadow equals conjugate on principal series \(\Delta = 1+i\lambda \).

• Residue at simple pole: algebraic identity.

Gap: celestial amplitude theory, unitarity cut equations, celestial OPE (not in Mathlib 4.19.0). Tracked honestly as three named stubs, celestial_amplitude_has_cut, disc_equals_loop_integrand, shadow_disc_mellin_density — none discharged by this chapter.

The map \(\Delta \mapsto 2-\Delta \) has order \(2\).

Fix a celestial null 4-vector \(q(x,y) = (1+x^2+y^2,\, 2x,\, 2y,\, 1-x^2-y^2)\) (the real Lorentzian slice \(\bar z = z^*\), \(z=x+iy\)) and the frame legs \(p_1=(-E,0,0,E)\), \(p_2=(-E,0,0,-E)\), \(p_4=(E,-E\sin \theta ,0,-E\cos \theta )\). Writing \(A := 2q{\cdot }p_1\), \(A' := 2q{\cdot }p_2\), \(B := 2q{\cdot }(p_1{+}p_2)\), \(C := 2q{\cdot }p_4\): \(A = -4E\) identically (no \(z\)-dependence), \(A' = -4E|z|^2 \le 0\), \(B = -4E(1+|z|^2) {\lt} 0\) for \(E{\gt}0\), and \(C\) clears its \((1-\cos \theta )\) factor to an exact sum of two squares, hence \(C \ge 0\) for \(\cos \theta {\lt} 1\) (i.e. \(t \ne 0\)). Consequently, for any physical t-channel threshold \(B''{\gt}0\) and any point with \(C \ne 0\) (away from the collinear point), the two tied-leg sewing coefficients \(-1/(2ACB)\) and \(-1/(2A'CB'')\) have a nonpositive product — they are never both nonnegative and never both nonpositive. This is the exact algebraic content behind the numerical finding (checked at 39/39 structured and 666/666 random kinematic points, zero exceptions, in discovery/shadow_ope/sign_opposition_sweep.py) that the tied-leg discontinuities \(\mathrm{Sewn}_s\), \(\mathrm{Sewn}_t\) always carry opposite-sign imaginary parts. Pure real algebra and elementary geometry: no Mellin transforms, no complex analysis, no Legendre functions.

Item 1c684543. For holomorphic \(F\) and scalar \(\lambda \), put \(D_\lambda (s)=F'(s)-\lambda F(s)\), \(R_\lambda (s)=F(s)/D_\lambda (s)\). Writing a zero \(\rho \) of \(F\) of multiplicity \(m=k+1\ge 1\) as \(F(z)=(z-\rho )^{k+1}g(z)\) (\(g\) analytic, \(g(\rho )\ne 0\)): \(D_\lambda (z)=(z-\rho )^k w(z)\) with \(w(z):=(k+1)g(z)+(z-\rho )(g'(z)-\lambda g(z))\) (), and \(w(\rho )=(k+1)g(\rho )\ne 0\) (). Hence \(R_\lambda (z)/(z-\rho )\to 1/(k+1)\) as \(z\to \rho \) (\(z\ne \rho \)) — the item’s own stated asymptotic \(R_\lambda (s)=(s-\rho )/m+O((s-\rho )^2)\), i.e. a genuine simple zero at \(\rho \) for every finite \(\lambda \); and \(R_\lambda (z)\to 0\) as \(z\to \rho \) (), the "zeros of \(R_\lambda \) are (among) the zeros of \(F\)" half of the item’s conclusion.

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 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 \).

The Weil explicit formula expresses \(\sum _\rho h(\rho )\) in terms of local data. Meyer’s (2005) spectral interpretation identifies the adèlic \(L^2\) spectrum with the multiset of zeta zeros, closing arithmetic_admissibility.

Gap: Weil explicit formula and Meyer’s spectral-Weil identity require full adèlic Fourier analysis (not in Mathlib 4.19.0). Documented as three axioms: weil_explicit_formula, meyer_spectral_weil_identity, weil_distribution_positivity.

For every \(n \geq 1\), the Dirichlet eta function \(\eta (s) = (1-2^{1-s})\zeta (s)\) satisfies \(\eta (2n)/\zeta (2n) = 1 - 2^{1-2n}\), unconditionally (requires \(\zeta (2n) \neq 0\), from riemannZeta_ne_zero_of_one_le_re). The concrete instance \(\eta (4)/\zeta (4) = 7/8\) (eta_four_div_zeta_four’) and the explicit value \(\eta (4) = 7\pi ^4/720\) (eta_four_eq, via riemannZeta_four) are also proved.

Honest boundary: the physical identification of this ratio with a fermion/boson thermal-capacity ratio in \(3{+}1\) dimensions is not formalized — only the arithmetic value.

The partial products \(\prod _{p {\lt} n}(1-p^{-2})\) over primes converge to \(6/\pi ^2 = 1/\zeta (2)\), obtained by inverting Mathlib’s convergent Euler product \(\prod _{p{\lt}n}(1-p^{-2})^{-1} \to \zeta (2)\) (riemannZeta_eulerProduct) term-by-term and evaluating via riemannZeta_two.

Honest boundary: the physical identification \(\alpha /\pi ^2 = (\alpha /6)\prod _p(1-p^{-2})\) with the fine-structure constant is not formalized — only the underlying arithmetic identity both rest on.

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.

\(\int _0^\infty e^{-r^2t}(4\pi t)^{-1/2}\, dt = 1/(2r)\) for \(r{\gt}0\). The \(x=0\) case of the paper’s boxed identity \(e^{-rx}/(2r) = \int _0^\infty e^{-r^2t}(4\pi t)^{-1/2}e^{-x^2/(4t)}\, dt\).

For \(a,b{\gt}0\): \(\int _0^\infty t^{-1/2}e^{-at-b/t}\, dt = \sqrt{\pi /a}\, e^{-2\sqrt{ab}}\). This is a genuine \(K_{1/2}\) Bessel evaluation, confirmed absent from Mathlib entirely at the pin, proved here without any Bessel-function machinery: the substitution \(t=(\sqrt{b}/\sqrt{a})w^2\) reduces it to an auxiliary integral \(\kappa (c) := \int _0^\infty e^{-c(w^2+w^{-2})}\, dw\); the \(w\mapsto 1/w\) symmetry of the integrand doubles it to \(2\kappa (c)=\int _0^\infty (1+w^{-2})e^{-c(w^2+w^{-2})}\, dw\); the substitution \(p=w-1/w\) — a bijection \((0,\infty )\to \mathbb {R}\) whose derivative is exactly the weight \(1+w^{-2}\) — turns this into a two-sided Gaussian integral, closed by Real.integral_gaussian. This is the general-\(x\) instance of the paper’s boxed subordination formula, in full.

For \(u\) integrable on \((-a,a)\) with \(\int _{-a}^{a}u=0\):

i.e. the two integral operators differ by the single \(x\)-independent constant \(\int y^2/(4a)\cdot u(y)\, dy\) — exactly the item’s own claimed reduction, as a pointwise integral identity. Pure intervalIntegral linearity plus ring on the kernel’s algebraic decomposition; no functional-analytic machinery needed for this half.

Item dcebf59f. With \(A(z):=(z-i)I(z)\), \(B(z):=(z+i)I(-z)\) for an arbitrary function \(I:\mathbb {C}\to \mathbb {C}\), \(A(-z)=-B(z)\) and \(B(-z)=-A(z)\) follow purely algebraically from the definitions (no properties of \(I\), the operator \(T\), or the reflection \(R\) needed), hence \(W_0:=A+B\) is odd, \(W_\pi :=A-B\) is even, and \(\hat m(z):=-i\, W_0(z)/W_\pi (z)\) is odd. Costs nothing: the item’s own formulas already reduce this layer entirely to algebra once expressed through the same \(I\).

The singlet \(\psi \) satisfies \(\mathrm{SWAP}\, \psi = -\psi \) with \(\psi \neq 0\) (GppHalfFlipMatrix.SWAP_mulVec_psi, GppHalfFlipMatrix.psi_ne_zero), giving an explicit negative eigenvector. Note this is the strong statement — not positive semidefinite in Mathlib’s own sense — rather than merely “has a negative eigenvalue”.

For any Schwartz-Bruhat function \(\Phi \) on \(\mathbb {A}\): \(Z(\Phi , s) = Z(\hat\Phi , 1-s)\). Follows from Haar self-duality + Poisson summation over \(\mathbb {Q} \subset \mathbb {A}\).

\(e^{au}\) defines a tempered distribution on \(\mathbb {R}\) iff \(a=0\). Two sorries: requires SchwartzMap.tsum not yet in Mathlib.

Proved clean, with no sorry and no axiom. Chaining the three results above: the Choi matrix of the transpose is SWAP, SWAP is not positive semidefinite, so by the Choi criterion the transpose is not completely positive.

Why this matters here. By 12.5, antiunitary time reversal carries a transpose. So the half-flip is not an artefact of a phase convention: the operation genuinely fails to be a channel, and the obstruction is the same negative eigenvector that makes the singlet antisymmetric.

If \(\zeta (\rho ) = 0\) with \(\mathrm{Re}(\rho ) \neq \tfrac {1}{2}\), there exist at least two distinct zeros with \(\mathrm{Im}(s) = \mathrm{Im}(\rho )\). (Zero sorries, zero axioms.)

\(\langle x,C_{K_r-1}x\rangle \ge 0\) for every \(x\in \mathrm{Ell2Z}\) and every \(0\le r{\lt}1\), as a direct corollary of the general fact that a bounded diagonal operator with nonnegative-real-part Fourier symbol is positive semidefinite (), applied to \(C_{K_r-1}\)’s already-known eigenvalue signs (\(0\) at \(n=0\), \(r^{|n|}\ge 0\) elsewhere).

On \(\mathrm{Ell2Z}:=\ell ^2(\mathbb {Z},\mathbb {C})\), the natural Fourier-coefficient model (Parseval-dual to the circle: convolution by a kernel becomes diagonal multiplication by its Fourier coefficients), let \(C_{K_r}\), \(P_0\), \(C_{K_r-1}\) be the bounded diagonal ContinuousLinearMaps with Fourier symbols \(r^{|n|}\); \(0\) at \(n=0\) and \(1\) elsewhere (the vacuum-deleting projection); and \(0\) at \(n=0\), \(r^{|n|}\) elsewhere, respectively. Then \(C_{K_r-1}=P_0\, C_{K_r}\, P_0\) as genuine bounded-operator composition (), for every \(0\le r{\lt}1\).

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.

If \(Z \subseteq \mathbb C\) is closed under an involution \(\iota \) and the paired form \(\sum _{\rho \in S} \overline{c(\iota \rho )}\, c(\rho )\) has nonnegative real part on every finite \(S \subseteq Z\), then every point of \(Z\) is fixed by \(\iota \).

Abstract nested-infimum order theory, applicable to Suzuki’s localized Weil ground energy \(\lambda _a\) once it is supplied concretely: if a family of test-function sets \(S_a\) is nested and \(\lambda _a\) is the greatest lower bound of a ratio functional over \(S_a\), then (i) \(\lambda \) is antitone; (ii) a uniform global lower bound over \(\bigcup _a S_a\) is equivalent to \(\operatorname {range}\lambda \) being bounded below (phrased via BddBelow rather than a literal sInf, to avoid Real.sInf’s junk-value convention on sets unbounded below); (iii) antitone plus not bounded below forces \(\lambda _a\to -\infty \). Genuinely proves (formalization_queue item 1b12010b) exactly the order-theoretic content that item asked for, with no reference to what the ratio functional or test spaces concretely are.

Same abstract setting. The global ratio set \(R''\bigcup _a S_a\) and the family \(\operatorname {range}\lambda \) have the same lower bounds (), from which: \(L\) is the global greatest lower bound iff it is the greatest lower bound of the localized ground energies, the two sets are bounded below together, and — with nesting — \(\lambda _a\to L\). Sharpens Theorem 24.1(ii), which matched only the existence of a bound on each side: the two optimal constants are the same real number, reached as a limit, so localization loses nothing. Accompanied by the dichotomy : an antitone \(\lambda \) either diverges to \(-\infty \) or converges to \(\bigsqcap _a\lambda _a\), with no third case, so no downstream statement needs to assume convergence.

With \(c:=vw\), \(g:=v/w\) (the item’s own \(c_j\), \(g_j\) formulas for \(v=\eta ^*u_j\), \(w=u_j^*e_0\)), \(c=g w^2\) unconditionally — a plain complex square, not the modulus square \(|w|^2\) the item’s converse direction uses for the same quantity. The two agree only when \(w\) is real (witnessed concretely: \(w=i\) gives \(w^2=-1\ne 1=|i|^2\)).

Item 68566b83. An integral over \([0,\infty )\) of an everywhere-positive integrable integrand is strictly positive — via MeasureTheory.setIntegral_pos_iff_support_of_nonneg_ae, reduced to the integrand’s support meeting \([0,\infty )\) in a set of positive (here infinite) Lebesgue measure. Once \(k(t)=\operatorname {Re}(\eta ^*e^{-tA}e_0)\) and the integral is identified with \(\operatorname {Re}(\eta ^*(A-zI)^{-1}e_0)\) (the item’s separate Laplace-resolvent identity, not attempted), this is exactly “cross-heat positivity forces cross-resolvent positivity.”

Item 5e10a4f0. If a determinant-ratio identity \(B_{\det }(z)=f(z)\, A_{\det }(z)\) holds with both factors positive for \(z{\lt}\lambda _{\min }(A)\), then \(B_{\det }(z){\gt}0\) there — algebraically immediate once stated correctly, and (once \(B_{\det }\) is identified with \(z\mapsto \det (B-zI)\)) exactly “\(B\) has no eigenvalue below \(\lambda _{\min }(A)\).” A boundary/continuity refinement strengthens this to \(B_{\det }(\lambda _{\min }(A)){\gt}0\) too, given continuity and a no-common-eigenvalue hypothesis at \(\lambda _{\min }(A)\) itself — the item’s full “\(\lambda _{\min }(A){\lt}\lambda _{\min }(B)\)” claim.

Item 0182d9cf. If continuous functions on a preconnected set never cross and one starts strictly below the other at some point, it stays strictly below everywhere — via IsPreconnected.intermediate_value₂: a crossing point would otherwise be forced between the two points.

Item 4d97d8eb. A numerator with a finite limit divided by a denominator whose norm blows up tends to zero — the reusable fact behind “\(q^*(x_i)=q_i\)” for the barycentric Pick interpolant \(q^*(z)=B(z)/A(z)\), since \(B(z)-q_iA(z)\) stays finite at \(x_i\) (the \(k=i\) pole term cancels identically, \(q_i-q_i=0\)) while \(\| A(z)\| \to \infty \) there.

Item 9cc1e2f8, flagged since the sixth-pass write-up as the natural next target because it needs genuine monotonicity/IVT reasoning, not just block-matrix algebra. If \(g\) is continuous and strictly increasing on an open interval \((a,b)\), tends to \(-\infty \) approaching \(a\) from the right, and to \(+\infty \) approaching \(b\) from the left, then \(g\) has exactly one zero in \((a,b)\) — via IsPreconnected.intermediate_value_Iii for existence and StrictMonoOn.injOn for uniqueness. This is the fully general core behind “the secular equation \(f(z)=0\) has exactly one root in each gap \((\alpha _j,\alpha _{j+1})\),” stripped of the specific rational-function structure.

\(T\psi \) is orthogonal to \(\psi \) for every \(\psi \).

\(T(T\psi ) = -\psi \). Proved clean. This is the half-flip itself: applying time reversal twice returns the state up to a global sign, so \(T\) generates a \(\mathbb {Z}_4\), not a \(\mathbb {Z}_2\), on spin-\(\tfrac 12\).

For every prime-like real \(p{\gt}1\) and real \(t\), \(W_p(p,t) = 2\operatorname {Re}(\text{minusLogDerivZetaP}\, p\, (1/2+it))\) exactly — i.e. \(W_p(p,t)=2\operatorname {Re}(-\zeta _p'/\zeta _p(1/2+it))\), genuinely proved rather than checked numerically. The proof computes both sides’ real and imaginary parts directly (Complex.exp_re/exp_im, Complex.div_re, Complex.normSq_apply) rather than manipulating cpow splittings, closing with the classical Poisson-kernel identity KrClosed_sub_one_eq_two_mul_re: for real \(r,\theta \) with \(0\le r{\lt}1\), \(K_r(\theta )-1 = 2\operatorname {Re}[re^{i\theta }/(1-re^{i\theta })]\). The \(r{\lt}1\) hypothesis is genuinely needed, not merely convenient: at \(r=1,\theta =0\) the denominator \(1-re^{i\theta }\) vanishes and Lean’s total division sends the two sides to different junk values, so the identity is false without it — this matches exactly the one case that ever arises (\(r=p^{-1/2}{\lt}1\) for \(p{\gt}1\)).

On the strip \(1 - \varepsilon {\lt} \sigma {\lt} 1 + \varepsilon \): \(\tfrac {\varepsilon }{2}\bigl(\int _0^1 t^{\sigma -2+\varepsilon }\, dt + \int _1^\infty t^{\sigma -2-\varepsilon }\, dt\bigr) = \varepsilon ^2/(\varepsilon ^2-(\sigma -1)^2)\), with value \(1\) at \(\sigma = 1\) and limit \(0\) as \(\varepsilon \to 0^+\) for \(\sigma \neq 1\): the Kronecker-delta selection \(\rho ' = 1-\bar\rho \).

The nontrivial zero set of \(\zeta \) is closed under \(\rho \mapsto 1 - \bar\rho \) — a proved theorem (functional equation composed with the proved conjugation symmetry), not an assumption.