RQ-D: flip formula, a comparison lemma for stop-loss terms,
the band lemma near the Dirac curve,
and the heavy part of the far region
Draft — the status of every statement is in CLAIMS.md
RQ-D
October 22, 2026

Abstract
2
For the centred
K, EZK
= K(R) = 1) we
p infinitely divisible laws√ZK (Kolmogorov measure
√
on
the
band
{K([1,
2])
≥
9/10}
∪
{K([−
2,
−1])
≥
9/10}
of probability
prove E|ZK | ≤ √ 2/e
√
measures on [− 2, p2] (Theorem 10); by the audited support bound for maximisers this reduces
C5 (supK E|ZK | = 2/e) to the complementary far region (Corollary 11). In the form needed
at finite q (the q-free condition ID∗ of the audited reduction, with C5 = g(2 ln 54 )) we prove
the band lemma with θ = 0.85, A = 1.54: E|ZK | ≤ max(g(λ+
0.85 (K)), C5 ) for every finitely
supported probability K on [−1.54, 1.54] with K([0.85, 1.54]) ≥ 4/5, and the mirror statement
(Theorem 13). So ID∗ , and with it Conjecture S for all q, reduces to E|ZK | ≤ C5 on the far region
{K([0.85, 1.54]) < 4/5, K([−1.54, −0.85]) < 4/5} (Corollary 14). The proof of the band lemmas
is not a moment argument: an exact identity (Lemma 3) isolates the extremal Poisson part, the
residual enters only through two stop-loss terms, and these are bounded by a new comparison
lemma (Lemma 4: pushing jumps to the right increases Eψ(ZK ) whenever ψ ′′ is nondecreasing)
together with convexity bounds in the jump law. The final inequalities on four-parameter
domains are checked in ball arithmetic. Sections 2–4 are written for a general threshold θ
and support bound A, since the same tools are used for the finite-q band (Section 6). On the
heavy part of that far region, { 12 ≤ K([0.85, 1.54]) < 45 } and its mirror, we prove E|ZK | < C5
(Theorem 16). The positive edge is replaced by its chord law (a convex-order increase) and fixed
on boxes of the two chord rates. The rest enters through a certified degree-16 moment bound
(polynomial majorant, Lagrangian relaxation on cumulant cells). So ID∗ and C5 reduce to the
light part {K([0.85, 1.54]) < 12 , K([−1.54, −0.85]) < 12 } (Corollary 17).

1

Setting

p
p
For q ∈ (0, 1) let χ1 , χ2P
, . . . be i.i.d. with P(χ = (1 − q)/q) = q and P(χ
− q,
p = − q/(1 − q))√= 1 k−1
and R(q) = supα̸=0 E| i αi χi |/∥α∥2 . Conjecture S: R(q) = M (q) := 2 q(1 − q) maxk≥1 k q̂
,
q̂ = max(q, 1 − q).
A Kolmogorov measure is a finite Borel measure K on R; ZK denotes the centred infinitely
divisible random variable with
Z itx
e − 1 − itx
itZK
log Ee
=
K(dx)
(the integrand is − t2 /2 at x = 0),
x2
R
2 = K(R), K({0}) is the Gaussian variance and x−2 K(dx) on R \ {0} is the Lévy
so EZK = 0, EZK

1

d

measure. ZK1 +K2 = ZK1 + ZK2 with independent summands. For a finitely supported K,
X
p

ZK = K({0}) G +
x Nx − K({x})/x2 ,
x∈supp K\{0}

with G ∼ N (0, 1) and independent Nx ∼ Poisson(K({x})/x2 ). Throughout, Nλ denotes a Poisson(λ)
variable (N0 = 0) and
a standard Gaussian, independent of each other and ofpeverything else.
√ G
−λ
We write g(λ) = 2 pλ e ; g(1/x2 ) = E|Zδx | for x ≥ 1, and max g = g(1/2) = 2/e. C5 is the
statement E|ZK | ≤ 2/e K(R)1/2 for all K.

2

Exact identities


Lemma 1 (flip formula). For y ̸= 0 and w ∈ R, |y + w| = |y| + sgn(y) w + 2 − sgn(y) w − |y| + .
Consequently, if Y and W are independent, E|Y
 | + E|W | < ∞, EW = 0 and P(Y = 0) = 0, then
E|Y + W | = E|Y | + 2 E (− sgn(Y ) W − |Y |)+ .
Proof. Let s = sgn(y), so y + w = s(|y| + sw). If |y| + sw ≥ 0 then |y + w| = |y| + sw and
(−sw − |y|)+ = 0. If |y| + sw < 0 then |y + w| = −|y| − sw = |y| + sw + 2(−sw − |y|). Take
expectations; E[sgn(Y )W ] = E sgn(Y ) EW = 0.
Lemma 2 (conditional form). Let Y, W be independent and integrable with EW = 0, EW 2 = ρ2 <
∞, and put ℓ(y) = E|y + W |. Then E|Y + W | = E ℓ(Y ); ℓ is convex and 1-Lipschitz; for every real
y
p
ℓ(y) = y + 2E(−W − y)+ = −y + 2E(W + y)+ ,
|y| ≤ ℓ(y) ≤ y 2 + ρ2 .
Proof. Fubini gives E|Y + W | = Eℓ(Y ); convexity and the Lipschitz bound are inherited from | · |.
The two identities are |x| = x + 2(−x)+ = −x + 2x+ with x = y + W , together with EW = 0.
Jensen gives ℓ(y) ≥ |y| and Cauchy–Schwarz ℓ(y) ≤ (E(y + W )2 )1/2 .
Lemma 3 (OR-region identity with a residual). Let K = KS +R KR with KS ̸= R0 and KR finite
measures, KS carried by [θ, ∞) for some θ > 0, and put Λ = x−2 dKS , m = x−1 dKS , V =
KS (R). Let Y = ZKS and W = ZKR be independent and NS the number of jumps of Y . Then
Y = SNS − m, where NS ∼ Poisson(Λ) and, given NS = n, Sn = J1 + · · · + Jn with Ji i.i.d. of
law νS /Λ, νS (dx) = x−2 KS (dx), carried by [θ, ∞). If moreover θ > m (every jump exceeds the
compensator), then


E|ZK | = 2me−Λ + 2e−Λ E(W − m)+ + 2 E (−W − Y )+ ; NS ≥ 1 ,
p
√
√
and 2me−Λ ≤ V g(Λ) ≤ 2/e V , with equality in the first inequality iff KS is a single atom,
and in both iff KS = V δ√2V .
−2
Proof. νS is carried by [θ, ∞) and has mass
R Λ ≤ θ V < ∞, so Y is compound Poisson with
rate Λ, jump law νS /Λ and compensator x νS (dx) = m. On {NS = 0}, Y = −m < 0; on
{NS ≥ 1}, Y ≥ θ − m > 0. Hence P(Y = 0) = 0 (here KS ̸= 0 is used: m > 0) and, as EY = 0,
E|Y | = 2EY− = 2me−Λ . Lemma 1 with the independence of W and (Y, NS ) gives the √identity.
2
−1
−Λ
Cauchy–Schwarz gives
p m ≤ ΛV , with equality iff x is KS -a.e. constant, so 2me 2 ≤ V g(Λ);
and g ≤√g(1/2) = 2/e with equality iff Λ = 1/2. A single atom V δx has Λ = V /x , which is 1/2
iff x = 2V .

2

3

A comparison lemma for stop-loss terms

For a function ψ and x ∈ R put Dx ψ(z) =
ψ(z) − xψ ′ (z))/x2 , and D0 ψ = ψ ′′ /2.

R1

′′
0 (1 − u) ψ (z + ux) du; for x ̸= 0 this is (ψ(z + x) −

Lemma 4 (comparison). Let ψ : R → R be C 1 with ψ ′ absolutely continuous and ψ ′′ nondecreasing
and bounded. Let K be a finitely supported Kolmogorov measure and T : R → R a map with
T (x) ≥ x on supp K. Then Eψ(ZK ) ≤ Eψ(ZT# K ).
′′
′′
Proof. Step 1 (smooth ψ). Assume first ψ ∈ C 2 with
P ψ nondecreasing and |ψ | ≤ M . For a
2
finitely supported Kolmogorov measure L = σ δ0 + j wj δxj (xj ̸= 0) and a square-integrable X
d

independent of the Z’s, put Φ(s) = Eψ(X + ZsL ), s ≥ 0. Since Z(s+δ)L = ZsL + Yδ with Yδ = ZδL
independent and EYδ = 0, Taylor’s formula with integral remainder gives
i
h Z 1
(1 − u) ψ ′′ (X ′ + uYδ ) du ,
X ′ = X + ZsL .
Φ(s + δ) − Φ(s) = E Yδ2
0

√

P
(j)
Write Yδ = σ δ G − δc + j xj Nδλj with λj = wj /x2j , c = j xj λj . On the event of no jump
P
(probability 1 − δ λj + O(δ 2 )) the contribution is δσ 2 Eψ ′′ (X ′ )/2 + o(δ), by bounded convergence
and continuity of ψ ′′ ; on the event of exactly one jump, of size xj (probability δλj + O(δ 2 )), it is
2
δλj x2j EDxj ψ(X ′ ) + o(δ); on the event E2 of two or more jumps the integrand is at most M
2 Yδ and

P
(j)
E[Yδ2 ; E2 ] ≤ 3 σ 2 δ P(E2 ) + δ 2 c2 + E[( j |xj |Nδλj )2 ; E2 ] = O(δ 2 ) (Poisson moments). Hence Φ has
P
the right derivative E (GL ψ)(X + ZsL ) with GL ψ = x∈supp L L({x})Dx ψ, which is continuous in
s (bounded continuous integrand, weakly continuous law), so Φ ∈ C 1 . Now let K ′ = T# K and
′ ) with independent summands, t ∈ [0, 1]. Applying the above in each
Ψ(t) = Eψ(Z(1−t)K + ZtK
′
variable (the two partial derivatives are jointly continuous, for the same reason),


′
Ψ′ (t) = E (GK ′ ψ − GK ψ)(Z(1−t)K + ZtK
′) ,
X

(GK ′ ψ − GK ψ)(z) =
K({x}) DT (x) ψ(z) − Dx ψ(z) ≥ 0,
P

x∈supp K

R1
because y 7→ Dy ψ(z) = 0 (1 − u)ψ ′′ (z + uy)du is nondecreasing when ψ ′′ is. So Ψ(1) ≥ Ψ(0).
Step 2 (general ψ). Let ϕε be a smooth probability density supported in [−ε, ε] and ψε =
ψ ∗ ϕε . Then ψε ∈ C ∞ , ψε′′ = ψ ′′ ∗ ϕε is nondecreasing and bounded, and |ψε (w) − ψ(w)| ≤
ε sup|v−w|≤ε |ψ ′ (v)| ≤ εC(1 + |w|) since ψ ′ is Lipschitz. As E|Z| < ∞, Step 1 for ψε and ε → 0 give
the claim.
Remark 5. The test functions used below are ψt,h (w) = (w − t + h)2+ /(4h), h > 0: they are C 1 ,
′′ = (2h)−1 1{w > t − h} is nondecreasing, and ψ (w) ≥ (w − t) (for w ≥ t the difference is
ψt,h
+
t,h
(w − t − h)2 /(4h)). The stop-loss function (w − t)+ itself does not satisfy the hypothesis, and
p the
conclusion fails for it: with t = 0, K = δ√2 and T (x) = 2, E(ZK )+ = 12 E|ZK | drops from 12 2/e
to 21 g(1/4) = 21 e−1/4 .
(Not used below.) ψt,h is the pointwise smallest ψ admissible in Lemma 4 with ψ ≥ (w − t)+
and ψ(t + h) = h, so the loss of this step cannot be reduced within the method. Proof, with
t = 0: ψ ′ (h) = 1, and ψ ′′ ≥ 0 because ψ is bounded below. Let u∗ < h be the largest zero of
ψ ′ (u∗ = −∞ if there is none; then ψ ′ (−∞) = 0). The measure µ = ψ ′′ (v) dv on (u∗ , h) has
mass 1 and a nondecreasing density, and Taylor’s formula gives ψ(w) = ψ(u∗ ) + Eµ (w − V )+
for w ∈ [u∗ , h] and, at w = h, ψ(u∗ ) = Eµ V ; so ψ(w) = Eµ max(V, w) and Eµ V ≥ 0. Such
3

a µ is a mixture of uniform laws on [s, h], and for V ∼ U [s, h], E max(V, w) = Fw ( s+h
2 ) with
2

w+h
1
Fw (x) = w + (h−w)
4(h−x) for x ≤ 2 and Fw (x) = x otherwise, a C convex nondecreasing function.
Jensen gives ψ(w) ≥ Fw (Eµ V ) ≥ Fw (0) = ψ0,h (w) for w ∈ [max(u∗ , −h), h]. To the left of u∗ ,
ψ is nonincreasing and ψ0,h nondecreasing; ψ0,h = 0 on (−∞, −h]. For w > h: a probability
density on (−∞, h) that is nondecreasing, bounded by c = ψ ′′ (h−) and has nonnegative mean
2
forces c ≥ 1/(2h), so ψ(w) ≥ w + (w−h)
= ψ0,h (w).
4h

Lemma 6 (stop-loss bounds). Let 0 < θ ≤ A, let KR be a finitely supported Kolmogorov measure
carried by [−A, θ), a = KR ((0, θ)), b = KR ([−A, 0]), ρ2 = a + b, W = ZKR , and
 √
 √
WB = θ Na/θ2 − a/θ2 + b G,
WC = A Nb/A2 − b/A2 + a G.
1
1
2
C
2
For t ∈ R and h > 0 put χB
h (t) = 2h E(WB − t + h)+ , χh (t) = 2h E(WC − t + h)+ . Then for every
t ∈ R:
C
(i) 2E(W − t)+ ≤ χB
h (t) and 2E(−W − t)+ ≤ χh (t);
p
p
(ii) 2E(W − t)+ ≤ t2 + ρ2 − t and 2E(−W − t)+ ≤ t2 + ρ2 − t;
2

d
1
C
•
(iii) χB
h , χh are C , convex and nonincreasing in t, with dt2 χh (t) = P(W• > t − h)/h ∈ [0, 1/h]
a.e.;
B
C
(iv) χB
h (t) and χh (t) are nondecreasing in a and in b (the other fixed), and χh (t) is nondecreasing
in θ.

Proof. (i) 2E(W − t)+ ≤ 2Eψt,h (W ). Apply Lemma 4 to KR with T (x) = θ on (0, θ) and T (x) = 0
d

on [−A, 0]: T# KR = aδθ + bδ0 and ZT# KR = WB . For the second bound, −W = ZK̃ with K̃(B) =
KR (−B), carried by (−θ, A]; take T (x) = A on [0, A] and T (x) = 0 on (−θ, 0), so T# K̃ = bδA + aδ0
d

and ZT# K̃ = WC . (ii) 2(W −t)+ = |W −t|+(W −t), so 2E(W −t)+ = E|W −t|−t ≤ (t2 +ρ2 )1/2 −t;
the same for −W . (iii) For fixed w, t 7→ (w − t + h)2+ is C 1 , convex, nonincreasing, with second
derivative 2 · 1{w > t − h}; differentiate under E (dominated convergence). (iv) Increasing a to a′
replaces WB by WB + θ(N ′ − λ′ ) with an independent centred Poisson term, and increasing b adds
an independent centred Gaussian; for the convex function w 7→ (w − t + h)2+ Jensen’s inequality
(conditionally on WB ) gives monotonicity. The same for WC . Monotonicity in θ is Lemma 4 again
(moving the atom aδθ to aδθ′ , θ′ > θ).

4

The jump law and the band bound

Lemma 7 (one jump). Let J take values in [j0 , j1 ] (j0 < j1 ), with mean µ and variance σ 2 . (a)
0 )φ(j1 )
For every convex φ on [j0 , j1 ]: Eφ(J) ≤ (j1 −µ)φ(jj01)+(µ−j
. (b) If φ ≤ Γ on [j0 , j1 ], where Γ
−j0
is C 1 with Γ′ absolutely continuous and Γ′′ ≤ κ a.e. on [j0 , j1 ], then Eφ(J) ≤ Γ(µ) + κσ 2 /2. (c)
(two-point bound) Let φ ≤ ψ on [j0 , ∞), where ψ is C 1 on [j0 , ∞) with ψ ′ absolutely continuous
and ψ ′′ nonincreasing a.e. (that is, ψ ′ is concave). Let µ > j0 , d = µ − j0 , x = µ + σ 2 /d and
w = d2 /(d2 + σ 2 ). Then Eφ(J) ≤ Tψ (σ 2 ) := (1 − w)ψ(j0 ) + w ψ(x). If moreover ψ is convex and
nonincreasing on R, then for all s2 ≥ σ 2 , j0′ ≤ j0 , 0 ≤ w′ ≤ d2 /(d2 + s2 ) and u′ ≤ d + s2 /d,
Eφ(J) ≤ (1 − w′ ) ψ(j0′ ) + w′ ψ(j0′ + u′ ).

4

RJ
Proof. (a) is convexity, φ(J) lying below the chord. (b) Γ(J) = Γ(µ) + Γ′ (µ)(J − µ) + µ (J −
u)Γ′′ (u) du ≤ Γ(µ) + Γ′ (µ)(J − µ) + κ(J − µ)2 /2; take expectations.
2
2
2
(c) The law P ∗ = (1 − w)δj0 + wδx has mean j0 + w(x − j0 ) = j0 + d2d+σ2 · d +σ
= µ and variance
d
2
4
2
2
(1 − w)d + wσ /d = σ . Let q be the quadratic with q(j0 ) = ψ(j0 ), q(x) = ψ(x), q ′ (x) = ψ ′ (x)
(if σ 2 = 0 then x = µ, w = 1, J = µ a.s. and there is nothing to prove), and k = q − ψ. Then
k(j0 ) = k(x) = k ′ (x) = 0 and k ′ = q ′ − ψ ′ is convex. By Rolle k ′ (ξ) = 0 for some ξ ∈ (j0 , x); a
convex function vanishing at the two points ξ < x is ≤ 0 on [ξ, x] and ≥ 0 on [j0 , ξ] ∪ [x, ∞). So k is
nondecreasing on [j0 , ξ], nonincreasing on [ξ, x] and nondecreasing on [x, ∞); with k(j0 ) = k(x) = 0
this gives k ≥ 0, i.e. ψ ≤ q on [j0 , ∞). As Eq(J) depends only on the mean and variance of J,
Eφ(J) ≤ Eψ(J) ≤ Eq(J) = EP ∗ q = EP ∗ ψ = Tψ (σ 2 ).
For the second statement: if σ 2 < s2 , the two-point law P ∗∗ on {j0 , x(s2 )} with mean µ arises
from P ∗ by splitting the mass at x(σ 2 ) between j0 and x(s2 ) > x(σ 2 ) with conditional mean
x(σ 2 ), so Tψ (σ 2 ) ≤ Tψ (s2 ) for convex ψ (Jensen). Write w̃ = d2 /(d2 + s2 ) and ũ = d + s2 /d, so
Tψ (s2 ) = ψ(j0 ) − w̃ (ψ(j0 ) − ψ(j0 + ũ)). The bracket is ≥ 0 as ψ is nonincreasing, so Tψ (s2 ) ≤
(1 − w′ )ψ(j0 ) + w′ ψ(j0 + ũ) for w′ ≤ w̃, and ψ(j0 ) ≤ ψ(j0′ ), ψ(j0 + ũ) ≤ ψ(j0′ + u′ ) because j0′ ≤ j0
and j0′ + u′ ≤ j0 + ũ.
For KRS ̸= 0 carried by [θ, A] the jump law νS /Λ of Lemma 3 has mean µ1 = m/Λ and second
moment x2 νS (dx)/Λ = V /Λ, hence variance σJ2 = (ΛV − m2 )/Λ2 .
Lemma 8 (feasible parameters). If KS ̸= 0 is carried by [θ, A] and has mass V , then (F1) V /A2 ≤
V
Λ ≤ V /θ2 ; (F2) V /A ≤ m ≤ V /θ; (F3) θΛ ≤ m ≤ AΛ; (F4) m2 ≤ ΛV ; (F5) Λ ≤ ( A1 + 1θ ) m − Aθ
.
Proof. Integrate against KS the pointwise inequalities, valid for x ∈ [θ, A]: A−2 ≤ x−2 ≤ θ−2 ,
A−1 ≤ x−1 ≤ θ−1 , θx−2 ≤ x−1 ≤ Ax−2 , and (x−1 − A−1 )(θ−1 − x−1 ) ≥ 0; (F4) is Cauchy–
Schwarz.
Proposition 9 (band bound). Let 0 < θ ≤ A and let K be a finitely supported probability Kolmogorov measure on [−A, A] with KS = K|[θ,A] ̸= 0; let V, Λ, m be as in Lemma 3, KR = K − KS
with a, b, ρ2 = 1 − V as in Lemma 6, W = ZKR , ℓ(y) = E|y + W | and P2 (Λ) = 1 − e−Λ (1 + Λ). Let
cB ≥ 2E(W − m)+ , cC ≥ 2E(−W − (2θ − m))+ and O ≥ E ℓ(J − m), J ∼ νS /Λ, independent of
W . Then
E|ZK | ≤ e−Λ (m + cB ) + Λe−Λ O + mΛe−Λ + P2 (Λ) cC .
(1)
Moreover O may be taken as µ1 − m + O′ with O′ ≥ 2E[(−W − (J − m))+ ], and then the right side
of (1) equals 2me−Λ + e−Λ cB + Λe−Λ O′ + P2 (Λ)cC .
P
Proof. By Lemmas 2 and 3, E|ZK | = n≥0 P(NS = n) E ℓ(Sn − m). For n = 0, ℓ(−m) = m +
2E(W − m)+ (Lemma 2). For n = 1 the term is Λe−Λ Eℓ(J − m). For n ≥ 2, y = Sn − m ≥ 2θ − m
and ℓ(y)P
= y+2E(−W −y)+ ≤ y+2E(−W −(2θ−m))+ , because y 7→ E(−W −y)+ is nonincreasing.
Finally n≥2 P(NS = n)E(Sn −m) = E(SNS −m)+me−Λ −Λe−Λ (µ1 −m) = mΛe−Λ , using EY = 0
and Λµ1 = m. For the second form, ℓ(y) = y + 2E(−W − y)+ holds for every real y (Lemma 2), so
Eℓ(J − m) = µ1 − m + 2E(−W − (J − m))+ , and e−Λ m + Λe−Λ (µ1 − m) + mΛe−Λ = 2me−Λ .
p
B (m),
Admissible choices,
all
from
Lemmas
2,
6
and
7:
c
=
min(χ
m2 + ρ2 − m), cC =
B
h
p
C
2
2
min(χh (2θ − m), (2θ − m) + ρ − (2θ − m)), any h > 0; for O the chord of the convexpfunction ℓ

B
on [θ −m, A−m] with endpoint values bounded by ℓ(y) ≤ min y +χC
y 2 + ρ2 ,
h (y), −y +χh (−y),
or the variance bound of Lemma 7(b) on [j0 , j1 ] = [θ −m, A−m], µ = µ1 −m, σ 2 = σJ2 , with Γ(y) =
B
y + χC
h (y) (κ = P(WC > θ − m − h)/h), Γ(y) = −y + χh (−y) (κ = P(WB > m − A − h)/h ≤ 1/h)

5

p
2 + ρ2 )3/2 , y = max(θ − m, 0)); these κ bound Γ′′ on the range by
or Γ(y) = y 2 + ρ2 (κ = ρ2 /(ylo
lo
p
Lemma 6(iii). For O′ : the chord on [θ − m, A − m] of the convex functions χC
y 2 + ρ2 − y.
h or
The φ-form of these choices (used in Section 6). Put φ(y) = 2E(−W − y)+ , so that O′ ≥
Eφ(J − m) is required; φ is convex and nonincreasing, and by Lemmas 2 and 6
p
φ(y) ≤ χC
(y),
φ(y)
≤
y 2 + ρ2 − y, φ(y) = −2y + 2E(W + y)+ ≤ −2y + χB
h
h (−y)
for all y ∈ R and h > 0. Admissible O′ (with J ∈ [θ, A], mean µ1 , variance σJ2 , y = J − m): (O1)
the chord of φ itself (Lemma 7(a)), with the endpoint values φ(θ − m), φ(A − m) replaced by any
of the upper bounds above; (O2) Lemma 7(b) with Γ(y) = −2y + χB
h (−y), κ = 1/h (Lemma 6(iii));
(O3) Lemma 7(c) with j0 = θ − m and ψ = χC
,
whose
second
derivative
P(WC > y − h)/h is
h
nonincreasing (Lemma 6(iii)),
ψ
being
convex
and
nonincreasing;
(O4)
if
θ
≥
m: Lemma 7(c) with
p
2
2
2
2
j0 = θ − m ≥ 0 and ψ(y) = y + r − y for any r ≥ ρ , whose second derivative r2 /(y 2 + r2 )3/2
is nonincreasing on [0, ∞). In (O3) and (O4) the mean of J − m exceeds j0 unless J ≡ θ, in which
case Eφ(J − m) = φ(θ − m). Upper bounds for σJ2 : (ΛV − m2 )/Λ2 (exact) and (µ1 − θ)(A − µ1 )
(Bhatia–Davis).

5

The band lemma for C5

√
measure on
Theorem
10
(band
lemma,
θ
=
1,
A
=
p
√ √
√
√ 2). Let K be a probability Kolmogorov
[− 2, 2] with K([1, 2]) ≥ 9/10 or K([− 2, −1]) ≥ 9/10. Then E|ZK | ≤ 2/e. If K is finitely
supported, equality holds only for K = δ±√2 .
√
Proof. Reflection x 7→ −x maps ZK to −ZK , so assume K([1, 2]) ≥ 9/10. Let first K be finitely
supported, KS = K|[1,√2] , V = KS (R) ≥ 9/10, ρ2 = 1 − V .
p
Case
ρ2 = 0. K = KS . If K = δ1 then E|ZK | = E|N1 − 1| = 2/e < 2/e. pOtherwise
R −1
m = x dK < 1, Lemma 3 (with KR = 0, θ = 1) gives E|ZK | = 2me−Λ ≤ g(Λ) ≤ 2/e, with
equality iff K = δ√2 .
√
Case 0 < ρ2 ≤ 1/10. Proposition 9 in its second form, with θ = 1 and A = 2, gives
E|ZK | ≤ F := 2me−Λ + e−Λ cB (m) + Λe−Λ O′ + P2 (Λ)cC (2 − m),
with cB , cC , O′ as listed after Proposition 9. The parameters (a, b, Λ, m) lie in
1
D = {a, b ≥ 0, 0 < a + b ≤ 10
, (Λ, m) satisfy (F1)–(F5) with V = 1 − a − b, θ = 1, A =

√
2},

and F depends only on (a,pb, Λ, m) and the free parameters h. Section 5.1 describes a certified
computation showing F < 2/e on D, which proves the strict inequality.
√ √
√
General K. Choose finitely supported probability measures Kn on [− 2, √
2] with Kn ([1, 2])
√≥
9/10 and Kn → K weakly (move the mass of each cell of a partition of [− 2, 1) and of [1, 2]
of mesh 1/n to a point of the same cell). Then ZKn → ZK in law (the integrand in the Lévy–
2 = 1 gives uniform integrability,
Khintchine exponent is bounded and continuous in x), and EZK
n
so E|ZKn | → E|ZK | (this is the continuity step of RQ-AUD A.8 / A.26(e)).
p
Corollary 11 (C5
to the far√region). If E|ZK | ≤ √2/e for every probability Kolmogorov
√ reduces
√
measure K on [− 2, 2] with K([1, 2]) < 9/10 and K([− 2, −1]) < 9/10, then C5 holds.
p
Proof. Suppose RID := supK E|ZK |/K(R)1/2 > 2/e. By RQ-B Lemma 8.1 (audited, A.13a) a
maximiser K ∗ with K ∗ (R) = 1 exists, and by RQ-B Proposition 8.3 (A.13a) every support point
2
2
x>√
0 of K ∗ satisfies x ≤ 2(1 − u)/RID , where u = P(ZK ∗ > 0), while (1
√ − u) ≤∗ RID /2; hence
x≤
2. Mirrored, every support point x < 0 satisfies |x| ≤ 2u/RID ≤
p 2. So K is carried by
√ √
∗
[− 2, 2], and by Theorem 10 or by the hypothesis, RID = E|ZK | ≤ 2/e, a contradiction.
6

5.1

The certified computation (scripts/verify band.py)

All inequalities are decided in ball arithmetic (python-flint arb, 80 bits); floating point is used
only to choose the parameters h and the subdivision. Outputs: outputs/verify band S.txt,
outputs/verify band B.txt; environment and md5 of the script in outputs/verify band env.txt.
P
Evaluation of χ. For J > 0, λ ≥ 0, s ≥ 0, c ∈ R: E(J(Nλ − λ) − c + sG)2+ = n≥0 pn (λ) Q(J(n −
2
2
λ) − c, s) with Q(d, s) = E(d + sG)2+ = (d
+ ds φ(d/s) (Q(d, 0) = d2+ ). The sum is
P + s λ)Φ(d/s)
n
taken over n ≤ 14; the tail is bounded by n>14 n! ((Jn +C)2 +s2 ) ≤ t15 /(1−q) with C = Jλ +|c|,
t15 its first term and q = 16λ/152 < 1 (ratio of consecutive terms), using Q(d, s) ≤ d2 + s2 and
e−λ ≤ 1.
Part S (0 < ρ2 ≤ r = 1/50). For c = t − h > 0 and a, b ≥ 0, a + b ≤ r: χB
h (t) ≤ a αB + b βB
√
rn−1
1 P
2
with βB = τ (c/ r)/(2h), τ (x) = E(G − x)+ , and αB = 2h n≥1 n! ((n − c)2 + r) (the term
√
√
√
n = 0 is E(√bG − a − c)2+ ≤ b τ (c/ b) ≤ b τ (c/ r); for n ≥ 1, P(Na = n) ≤ a rn−1 /n! and
E(n−a−c+ bG)2+ ≤ (n−a−c)2 +b ≤ (n−c)2 +r when 0 ≤ a ≤ 2(n−c), which holds as c < 0.95);
√
√
rn−1
1 P
(y)
≤
a
α
+
b
β
with
α
=
τ
(c/
symmetrically χC
((
r)/(2h),
β
=
2n − c)2 + r).
n
C
C
C
C
n≥1 2 n!
h
2h
The series are summed to n = 11 with a tail bound of twice the next term. With e−Λ , Λe−Λ ,
P2 bounded on a (Λ, m) box and the chord weights at the box,
p this gives F ≤ M0 + aA
p + bB ≤
−Λ . Since 2me−Λ ≤
2 g(Λ) ≤ (1−ρ2 /2) 2/e, the
1
−
ρ
M0 +ρ2 max(A, B), where M0 bounds
2me
p
p
box is certified if max(A, B) < 12 2/e (then F < 2/e for every ρ2 > 0), or if M0 +rB max(A, B) <
p
2/e with rB = min(r, 1 − m21 /Λ2 ) (from (F4)), or by the crude bound cB ≤ ρ2 /(2m), O′ ≤ ρ,
cC ≤ ρ2 /(2(2 − m)). Result: 1098 boxes, 0 failures.
Part B (1/50 ≤ ρ2 ≤ 1/10). The triangle {a, b ≥ 0, a + b ≤ 1/10} is covered by squares of side
1/256; squares not certified are split into four, down to side 1/1024. For a square [a1 , a2 ] × [b1 , b2 ]
all costs are evaluated at the corner (a2 , b2 ) and the Cauchy–Schwarz terms with ρ2 = a2 + b2
1
1
(monotone by Lemma 6(iv)), and V ∈ [1 − min(a2 + b2 , 10
), 1 − max(a1 + b1 , 50
)]. On a box
[Λ1 , Λ2 ] × [m1 , m2 ] (with m on the grid k/1024) the box is discarded if (F1)–(F5) fail at every
point, and otherwise certified if
p
M + e−Λ1 cB (m1 ) + Λ2 e−Λ2 O′ (m2 , µ1,lo ) + P2 (Λ2 ) cC (2 − m2 ) < 2/e,
√
where M ≥ max 2me−Λ over the box subject to m ≤ ΛVhi (computed exactly from the unimodalC
ity of g), µ1,lo = max(1, m1 /Λ2 ), and O′ (m
p2 , µ) is the smallest of the chords of χh (four float-chosen
2
2
h, common
to both endpoints) and of y + ρ − y, with endpoint values at y = 1 − m2 and
√
y = 2 − m2 . Validity: 2E(W − t)+ and 2E(−W − t)+ are nonincreasing in t, and so are the chord
endpoint functions φ (Lemma 6(iii)); the chord has√nonnegative weights, so it is at most the chord
through the upper values ḡ1 ≥ φ(1 − m), √
ḡ2 ≥ φ( 2 − m); the verifier replaces ḡ1 by max(ḡ1 , ḡ2 )
(still an upper bound, as φ(1 − m) ≥ φ( 2 − m)), which makes this chord nonincreasing in µ1 ,
so its value at µ1,lo bounds it on the box (the same is done for the linear coefficients of Part S);
e−Λ decreases and Λe−Λ , P2 increase on [0, 1]. Boxes are bisected (alternately in m and Λ) until
certified. Result: 341 squares at side 1/256 (85 not certified), 333 at 1/512 (3 not certified), 12 at
1/1024 (all certified); 598 squares certified in all, 1,339,228 (Λ, m) boxes, 95 s on 8 cores.
Controls. (Run before the max(ḡ1 , ḡ2 ) change, which can only increase the computed bounds.)
With r = 0.06 in Part S the linear certificate fails on 426,627 boxes; with the target lowered to
7

p
p
2/e − 0.002 Part S fails on 5,750 boxes, and Part B with target 2/e − 0.001 fails on 110 of 1281
squares at side 1/512 (so the check is not vacuous; the margin is below 10−3 near ρ2 = 0.02). A
float test on 400 random K in the band (scripts/band soundness.py) gives p
F −E|ZK | ≥ 1.5·10−5
(the bound is above the exact value, computed by Poisson enumeration) and 2/e − F ≥ 3.2 · 10−5 .

6

The band lemma in the form needed at finite q

By the audited reduction (RQ-B C19 = RQ-A
√ U.1, A.26) and the finite-q localisation (RQ-C C15,
A.28), Conjecture S for all q ≤ q5 = 1 − 2/ 5 (and hence, with RQ-A MAIN-5, A.25, for all q)
follows from the statement

−
ID∗ : E|ZK | ≤ max g(λ+
for some θ = θ(K),
θ (K)), g(λθ (K)), C5
Z
√
x−2 dK,
C5 = g(2 ln 45 ) = 1.28 2 ln 1.25 = 0.8551004 . . . ,
λ±
θ (K) =
±x≥θ

for all finitely supported probability measures K on [−1.54, 1.54] (A′ of A.28 increases in q and
A′ (q5 ) = 1.538 . . . < 1.54). We prove ID∗ with θ = 0.85 on a band.
Near the Dirac laws with g(Λ) > C5 the bound F has to be sharp to first order in ρ2 , and one
more choice of O′ is needed, together with a lemma that absorbs its constant term into the main
term.
(O5) If µ1 > θ: for every h > 0 and j0′ ≤ j0 = θ − m, with κ = (h − j0′ )2+ /(2h), d = µ1 − θ and
w = d2 /(d2 + σJ2 ) (the exact σJ2 ),
O′ = (1 − w) κ + (1 − w)

ρ2
+ χC
h (µ1 − m).
2h

C
C
Indeed Lemma 7(c) (first statement) with ψ = χC
h gives Eφ(J − m) ≤ (1 − w)χh (j0 ) + wχh (x)
C
C
C
2
with x = µ1 − m + σJ /d ≥ µ1 − m; then w ≤ 1, χh ≥ 0 is nonincreasing, and χh (j0 ) ≤ χh (j0′ ) ≤
κ + ρ2 /(2h), because WC has mean 0 and variance a + b = ρ2 , so that E(WC + e)2+ ≤ E(WC + e)2 =
e2 + ρ2 for e = h − j0′ ≥ 0 and E(WC − c)2+ ≤ EWC2 = ρ2 for c = j0′ − h ≥ 0. The term (1 − w)κ
does not vanish as ρ2 → 0; the next lemma absorbs it into the main term, using the slack that
Cauchy–Schwarz (F4) leaves when σJ2 > 0.

Lemma 12 (absorption). Let KS ̸= 0 be carried by [θ, A], with mass V , Λ, m,pµ1 = m/Λ and σJ2
as above, d = µ1 − θ > 0 and w = d2 /(d2 + σJ2 ). If 0 < D ≤ d and 0 ≤ κ ≤ D2 Λ/V , then
√
2me−Λ + Λe−Λ κ (1 − w) ≤ V g(Λ).
Proof. 1 − w = σJ2 /(d2 + σJ2 ) ≤ σJ2 /D2 = (ΛV − m2 )/(Λ2 D2 ), so √
the left side is at most e−Λ q(m)
2
2
with q(t) = 2t + κ(ΛV − t )/(ΛD ). If κ = 0, q(m) =p2m ≤ 2 √ΛV by (F4). If κ > 0, q is a
∗
2
concave
ΛD2 /(D2 √Λ/V ) = ΛV , so √
q is nondecreasing
on
√ quadratic with
√ vertex t = ΛD /κ ≥ √
√
−Λ
(−∞, ΛV ]; as m ≤ ΛV by (F4), q(m) ≤ q( ΛV ) = 2 ΛV . Finally 2e
ΛV = V g(Λ).
Theorem 13 (ID∗ band lemma, θ = 0.85, A = 1.54). Let K be a finitely supported probability
Kolmogorov measure on [−1.54, 1.54]. If K([0.85, 1.54]) ≥ 4/5 then E|ZK | ≤ max(g(λ+
0.85 (K)), C5 );
if K([−1.54, −0.85]) ≥ 4/5 then E|ZK | ≤ max(g(λ−
(K)),
C
).
5
0.85
−
Proof. Reflection x 7→ −x maps ZK to −ZK and exchanges λ+
θ and λθ , so assume K([θ, A]) ≥ 4/5
with θ = 0.85, A = 1.54. Then KS = K|[θ,A] ̸= 0, V = KS (R) ≥ 4/5, Λ = λ+
θ (K), and

8

KR = K −KS is carried by [−A, θ) with a = KR ((0, θ)), b = KR ([−A, 0]), ρ2 = a+b = 1−V ≤ 1/5.
Proposition 9 in its second form (no sign condition on θ − m) gives
E|ZK | ≤ F := 2me−Λ + e−Λ cB + Λe−Λ O′ + P2 (Λ) cC ,
with cB ≥ 2E(W −m)+ and cC ≥ 2E(−W −(2θ−m))+ from Lemma 6 and O′ any of (O1)–(O4) after
Proposition 9 or (O5) above. Every bound used is a function of (a, b, Λ, m), of σJ2 = (ΛV − m2 )/Λ2
and of free parameters (h, upper bounds for σJ2 ), and (a, b, Λ, m) lies in
D∗ = {a, b ≥ 0, a + b ≤ 51 , (Λ, m) satisfy (F1)–(F5) with V = 1 − a − b}.
The computation of Section 6.1 covers D∗ by boxes in (a, b, Λ, m) and shows on each box that
F ≤ max(g(Λ), C5 ): either directly (F <pmax(g(Λ), C5 ) with all costs at a corner of the box), or,
for a + b ≤ 1/50 and m < θ, from F ≤ 1 − ρ2 g(Λ) + aA + bB (by (F4), or by Lemma 12 when
(O5) is used) and one of the tests (T1)–(T3) of Section 6.1.
Corollary 14 (ID∗ reduces to a far region). Suppose that E|ZK | ≤ C5 for every finitely supported
probability measure K on [−1.54, 1.54] with K([0.85, 1.54]) < 4/5 and K([−1.54, −0.85]) < 4/5.
Then ID∗ holds for every finitely supported probability measure on [−1.54, 1.54].
Proof. On the band use Theorem 13 with θ = 0.85; off the band the hypothesis gives E|ZK | ≤
−
C5 ≤ max(g(λ+
θ ), g(λθ ), C5 ) for every θ.
p
Since max(g(Λ), C5 ) ≤ max g = 2/e, Theorem 13 also settles C5 on its band, and the far region
left for C5 is that of Corollary 14. RQ-C pointed this out at 19:00 UTC. RQ-C’s numerical lower
bounds p
for sup E|ZK | are about 0.827 on this far region and about 0.850 on that of Corollary 11,
against 2/e = 0.8578.
Corollary 15 (C5 reduces to the far region of Theorem 13). (a) The bound of Theorem 13 holds
for every p
probability Kolmogorov measure K on [−1.54, 1.54], finitely
supported or not. √(b) If
√ √
E|ZK | ≤ 2/e√ for every probability Kolmogorov measure K on [− 2, 2] with K([0.85, 2]) <
4/5 and K([− 2, −0.85]) < 4/5, then C5 holds. In particular C5 follows from the hypothesis of
Corollary 14.
Proof. (a) By reflection, assume K([θ, A]) ≥ 4/5 (θ = 0.85, A = 1.54). As in the proof of Theorem 10, move the mass of each cell of a partition of [−A, θ) and of [θ, A] of mesh 1/n to a
point of the same cell. This gives finitely supported probability measures Kn on [−A, A] with
Kn ([θ, A]) = K([θ, A]) ≥ 4/5 and Kn → K weakly, so E|ZKn | → E|ZK | by the continuity step
+
−2 is uniformly continuous on [θ, A] and the cells
there. Moreover λ+
θ (Kn ) → λθ (K), because x
inside [θ, A] carry the same masses under Kn and K. As g is continuous, E|ZK | = lim E|ZKn | ≤
+
lim max(g(λ+
θ (Kn )), C5 ) = max(g(λθ (K)), C5 ).
∗
(b) As in √
the √proof of Corollary 11, if C5 fails there is apmaximiser K ∗ with
√ K (R) = 1,
∗
2]) ≥ 4/5 or
carried√by [− 2, 2] ⊂ [−1.54, 1.54], with E|ZK ∗ | = RID > 2/e. If K ([0.85,
p
±
∗
∗
K ([− 2, −0.85]) ≥ 4/5, part (a) givespE|ZK ∗ | ≤ max(g(λθ (K )), C5 ) ≤ 2/e; otherwise the
hypothesis does. Both contradict RID > 2/e.
p For the last sentence: the hypothesis of Corollary 14 (finitely supported K, bound C5 <
2/e) extends to all probability measures K on [−1.54, 1.54] with K([0.85, 1.54]) < 4/5 and
K([−1.54, −0.85]) < 4/5. To see this, approximate as in (a) with cells inside [−1.54, −0.85],
(−0.85, 0.85) and [0.85, 1.54];
these keep the two masses, so Kn stays in the far region. Every
√ √
probability measure on [− 2, 2] in the far region of (b) is such a K.
9

6.1

The certified computation (scripts/verify bandstar.py)

All inequalities are decided in ball arithmetic (python-flint arb, 80 bits), with θ = 17/20, A =
77/50 and C5 as balls containing the exact values; floating point only chooses the parameters
C
h and the subdivision. The values χB
h , χh are enclosed as in Section 5.1 (lattice sum over
n ≤ 14 plus the geometric tail bound, with jump θ resp. A). Grid points are rounded by
exact comparisons with dyadic rationals. Output: outputs/verify bandstar.txt (summary),
outputs/verify bandstar squares.jsonl (one line per (a, b) square), environment and md5 in
outputs/verify bandstar env.txt.
Squares in (a, b). The triangle {a, b ≥ 0, a + b ≤ 15 } is covered by the squares [a1 , a2 ] × [b1 , b2 ] of
side 1/128 with a1 + b1 < 51 ; a square that is not certified is split into four, down to side 1/8192. On
a square, V ∈ [Vlo , Vhi ] = [1−min(a2 +b2 , 51 ), 1−a1 −b1 ], and every (a, b) of the square with a+b ≤ 15
satisfies a ≤ ā, b ≤ b̄, where (ā, b̄) = (a2 , b2 ) if a2 + b2 ≤ 51 and otherwise ā = min(a2 , ⌈ 51 − b1 ⌉),
C
b̄ = min(b2 , ⌈ 15 − a1 ⌉) (rounded up to multiples of 2−24 ). The costs χB
h , χh are evaluated at (ā, b̄)
(Lemma 6(iv)), and the Cauchy–Schwarz terms with r2 = min(ā + b̄, 15 ) ≥ ρ2 .
Boxes in (Λ, m). For each square, Λ ∈ [Vlo /A2 − 0.01, Vhi /θ2 + 0.01] (in strips of width 1/64) and
m ∈ [2125, 4820]/4096 ⊃ [0.8/A, 1/θ] (in blocks of 64/4096), which contains every point allowed by
(F1)–(F2). A box [Λ1 , Λ2 ] × [m1 , m2 ] is discarded if one of (F1)–(F5) fails at every point of the box
1
for every V ∈ [Vlo , Vhi ]; otherwise it must pass the direct check or (if a2 + b2 ≤ 50
) the slope check
below. Boxes that pass neither are bisected, alternately in m and in Λ, down to m-width 1/4096
and Λ-width 1/16384; a box that still fails makes the square uncertified.
On a box: e−Λ ≤ e−Λ1 , Λe−Λ ≤ max[Λ1 ,Λ2 ] te−t , P2 (Λ) ≤ P2 (Λ2 ) (P2′ (t) = te−t ≥ 0); the
target is bounded
below by T = max(min(g(Λ1 ), g(Λ2 )), C5 ) (g is unimodal); M bounds 2me−Λ =
√
−Λ
2e min(m, ΛV ) (by (F4)) over the box with m ≤ m2 , V ≤ Vhi , computed from the unimodality
of g as in Section 5.1; µ1 = m/Λ ∈ [µlo , µhi ] with µlo = max(θ, m1 /Λ2 ), µhi = min(A, m2 /Λ1 );
d = µ1 − θ ≥ dlo = µlo − θ; σJ2 ≤ s2 = min((Λ2 Vhi − m21 )/Λ21 , dhi (A − θ − dlo )) (exact formula
and Bhatia–Davis); in the box version of Lemma 7(c), j0′ = θ − m2 , w′ = d2lo /(d2lo + s2 ) and
u′ = mind∈[dlo ,dhi ] (d + s2 /d), the far point j0′ + u′ being rounded down to the m-grid. The functions
t 7→ 2E(W − t)+ and φ are nonincreasing, so their bounds are evaluated at the end of the box range
where the function is largest: cB at t = m1 , cC at 2θ − m2 , the endpoint values of φ at θ − m2 and
A − m2 (any pointwise bound of φ may then be used at that point).
p
√
C
2
2
Direct check. With cB = min(χB
y 2 + r2 −y)
h (t), t + r −t) at t = m1 and cC = min(χh (y),
at y = 2θ − m2 , the box is certified if
M + e−Λ1 cB + P2 (Λ2 ) cC + max (te−t ) O′ < T
[Λ1 ,Λ2 ]

′
for one of the
bounds φ̄1 =
p following O , tried in this order: (O1) the chord with endpoint p
C
C (y),
(−y))
at
y
=
θ
−
m
and
φ̄
=
min(χ
y 2 + r2 − y)
min(χh (y), y 2 + r2 − y, −2y + χB
2
2
h
h
at y = A − m2 , with φ̄1 replaced by max(φ̄1 , φ̄2 ) and µ1 by µlo (the chord through these values is
nonincreasing in µ1 , see Section 5.1); (O3) in the box version with three float-chosen h; (O4) in the
box version if θ − m2 ≥ 0; (O2) with Γ(µ) ≤ −2(µlo − m2 ) + χB
h (t), t ≤ −(µhi − m1 ) on the grid,
and σJ2 ≤ s2 , two float-chosen h.
1
Slope check. Used when a2 + b2 ≤ 50
and m2 < θ. The range of ρ2 on the box is [r0 , rB ] with
r0 = a1 + b1 and rB = min(a2 + b2 , 1 − m21 /Λ2 ) (by (F4)); it is bisected up to six times. On a piece

10

[r1 , r2 ]: V ≤ 1 − r1 is used for s2 , and all costs are replaced by linear bounds valid for a, b ≥ 0,
1
a + b ≤ r, with r = min(⌈4096r2 ⌉/4096, 50
) ≥ r2 . For c = t − h > 0 with r/θ ≤ 2(θ − c),
χB
h (t) ≤ a

√

1 X (r/θ2 )n−1
τ (c/ r)
2
(θn − c) + r + b
,
2hθ2
n!
2h

τ (x) = E(G − x)2+ ,

n≥1

√
√
√
because the term n = 0 of the lattice sum is E( bG − a/θ − c)2+ ≤ b τ (c/ b) ≤ b τ (c/ r), and for
√
2 n−1
n ≥ 1, P(Na/θ2 = n) ≤ θa2 (r/θn!)
and E(θn − a/θ − c + bG)2+ ≤ (θn − a/θ − c)2 + b ≤ (θn − c)2 + r
(as 0√≤ a/θ ≤ 2(θn − c)); symmetrically, for c = y − h > 0 with r/A ≤ 2(A − c), χC
h (y) ≤
τ (c/ r)
(r/A2 )n−1
1 P
2
a 2h + b 2hA2 n≥1
((An − c) + r). The series are summed to n = 11, and the rest
n!
is bounded by twice the term n = 12 with
p c replaced by 0 (consecutive terms decrease by a factor
2
below 1/100, as r/θ < 0.03). Further t2 + ρ2 − t ≤ ρ2 /(2t) for t > 0. This gives linear bounds
(α, β) for cB (at m1 ), cC (at 2θ−m2 ), and for O′ through (O1) (the chord, with the max replacement
done coefficientwise),
(O3), (O4) and (O5). In (O5), j0′ = θ − m2 , κ = (h − j0′ )2+ /(2h) must satisfy
p
2
C
κ ≤ dlo Λ1 /(1 − r1 ), (1 − w)ρ2 /(2h) ≤ (1 − w′ )ρ2 /(2h), and χC
h (µ1 − m) ≤ χh (θ − m2 + dlo ) (far
point rounded down to the grid). Put A = e−Λ1 αB + max(te−t )αO + P2 (Λ2 )αC , B likewise and
Mx = max(A, B), for the combination of options that minimises Mx (chosen in floats). Then on
the piece
p
2
F ≤ 1 − ρ2 g(Λ) + ρ2 Mx ≤ 1 − ρ2 g(Λ) + ρ2 Mx ,
by (F4) for (O1), (O3), (O4), and by Lemma 12 (with D = dlo , as Λ ≥ Λ1 , V ≤ 1 − r1 ) for (O5).
The piece is certified by one of: (T1) Mx ≤ 21 min(g(Λ1 ), g(Λ2 )); then F ≤ g(Λ) ≤ max(g(Λ), C5 );
(T2) ĝ + max(r1 (Mx − ĝ/2), r2 (Mx − ĝ/2)) < T with ĝ = max[Λ1 ,Λ2 ] g; then F ≤ ĝ + ρ2 (Mx − ĝ/2) <
T ; (T3) M0 + r2 Mx < T , where M0 bounds 2me−Λ (with
V ≤ 1 − r1 ), and for (O5) M0 =

max M, e−Λ1 (2m2 + κ max(0, Λ2 (1 − r1 ) − m22 )/(Λ1 d2lo )) , which bounds 2me−Λ + Λe−Λ κ(1 − w)
√
√
by the proof of Lemma 12 (e−Λ q(m) ≤ e−Λ q(m2 ) if m2 < ΛV , and ≤ V g(Λ) ≤ M otherwise).
Pieces with m21 > Λ2 (1 − r1 ) are empty by (F4).
The slope check is what makes the theorem hold up to ρ2 = 0 in the range 0.4463 < Λ < 0.5599
where g(Λ) > C5 : there F equals g(Λ) at the Dirac law and the margin is of order ρ2 . In this range
(O3) with h < θ − m loses a factor about 3 in the b-coefficient and (O4) is lossy in the a-coefficient;
(O5) with h ≈ 0.3–0.55 > θ − m ≈ 0.1 is what makes Mx < g/2 near the Dirac curve.
Result. The recorded run of scripts/verify bandstar.py (md5 b5b55ceec828f01d
ebc6c1a422e7270f; 2026-10-22, 18:39:45–18:52:59 UTC, 8 processes, 793 s) certifies every square:
side of the squares
1/128
1/256
1/512
1/1024

squares
351
837
408
80

not certified
215
102
20
0

(Λ, m) boxes
2,094,045
5,839,031
5,825,480
1,135,478

The squares of a level are the children of the squares not certified at the level before, restricted
to those that meet the triangle. So the 1339 certified squares cover the triangle, and the proof of
Theorem 13 is complete. The leaf boxes of the certified squares are disposed of as follows: 3,114,781
are infeasible, 551,105 are certified by (O1), 2,876,016 by (O3), 128,597 by (O4), 1,203,286 by (O2)
and 426 by the slope check. An earlier run (18:25–18:38 UTC) of a copy of the script that differs
only in its docstring, an unused constant and argument, a log flush and the control shift below
(which is 0 by default) gave the same counts (outputs/verify bandstar run2.txt).
11

Controls (not part of the proof ). scripts/verify bandstar controls.py (output
outputs/verify bandstar controls.txt, 60 s) reruns single squares, without refinement, with
the target lowered by a shift (environment variable BANDSTAR TGT SHIFT; test (T1) is then disabled,
1 2
1 2
since it only gives F ≤ g(Λ)). The origin squares [0, 256
] and [0, 128
] are certified at shift 0 and
are not certified at shift 0.0005. The first failing box, Λ ∈ [0.56323, 0.56329], m ∈ [3074, 3075]/4096,
lies on the Dirac curve m2 = Λ, where C5 − g(Λ) ∈ [0.000496, 0.000502], so that the lowered target
is at most g(Λ) + 2 · 10−6 , while F = g(Λ) at ρ2 = 0. (The two neighbouring squares of side 1/128
are not certified without refinement even at shift 0; the certificate run splits them.) The 80 squares
of side 1/1024 of the last level lie along the hypotenuse (a + b ∈ [0.1973, 0.2], a ∈ [0.0566, 0.0958]).
All are certified at shift 0, and at shift 0.001, 63 of them are not. So the certified margin is below
10−3 along the hypotenuse and is 0 on the Dirac curve; the check is not vacuous.
Float soundness test (evidence only). scripts/bandstar soundness2.py draws random
finitely supported K in the band and compares every ingredient bound with its exact value, computed from the exact laws of W (Poisson enumeration) and of J: cB , cC , each option (O1)–(O5)
for Eφ(J − m) (the two-point options also with the larger Bhatia–Davis variance, as in the box
2
version), the bound χC
h (θ − m) ≤ κ + ρ /(2h), the inequality of Lemma 12, and F ≥ E|ZK |.
Two samples were run: 400 random K with ρ2 ≤ 15 (outputs/bandstar soundness2.txt) and
1
400 near-Dirac K with ρ2 ≤ 50
(outputs/bandstar soundness2 dirac.txt). In both, no bound
is below its exact value by more than 10−15 . The two bounds that are equalities in limit cases,
2
−16 and −2.2·10−16 (rounding).
χC
h (θ−m) ≤ κ+ρ /(2h) and Lemma 12, have smallest gaps −8.9·10
On the first sample min(F − E|ZK |) = 2.1 · 10−4 and min(max(g(Λ), C5 ) − F ) = 5.8 · 10−4 ; on the
second these are 1.5 · 10−7 and 7.3 · 10−7 , as expected near the Dirac curve.

7

The heavy part of the far region

Throughout this section τ = 17/20 and A = 77/50. For a probability Kolmogorov measure K
on [−A, A] put V+ = K([τ, A]) and V− = K([−A, −τ ]). The far region of Corollary 14 is {V+ <
4
4
1
1
1
5 , V− < 5 }; we split it into the light part {V+ < 2 , V− < 2 } and the heavy part, where V+ ≥ 2 or
1
V− ≥ 2 .
Theorem 16 (heavy far region). Let K be a probability Kolmogorov measure on [−1.54, 1.54] with
1
4
1
4
2 ≤ K([0.85, 1.54]) < 5 or 2 ≤ K([−1.54, −0.85]) < 5 . Then E|ZK | < C5 .
Corollary 17 (ID∗ and C5 reduce to the light far region). Suppose that E|ZK | ≤ C5 for
every finitely supported probability measure K on [−1.54, 1.54] with K([0.85, 1.54]) < 21 and
K([−1.54, −0.85]) < 12 . Then the hypothesis of Corollary 14 holds. Hence ID∗ holds for every
finitely supported probability measure on [−1.54, 1.54], and C5 holds (Corollary 15).
Proof. Let K be finitely supported on [−1.54, 1.54] with V+ < 54 and V− < 45 . If V+ < 12 and
V− < 12 , the hypothesis gives E|ZK | ≤ C5 ; otherwise Theorem 16 does. This is the hypothesis of
Corollary 14, and Corollary 15 (last sentence) gives C5.
The proof of Theorem 16 is a moment argument for everything except the positive edge [τ, A],
which is handled exactly. Lemma 18 replaces the jumps in [τ, A] by jumps at τ and A (a convexorder increase). Their Poisson counts are then fixed on a box of the two chord rates. Everything
else (the negative edge, the residual, and the part of the chord rates above the lower corner of the
box) is a rest measure W on [−A, τ ]∪{A}. It enters only through its cumulants, which are bounded
by a degree-16 polynomial majorant and a Lagrangian relaxation, both checked in ball arithmetic.
12

7.1

Chord reduction of the positive edge

For a, b ≥ 0 put M (a, b) = aτ 2 + bA2 and Q(a, b) = (aτ + bA)2 /(a + b), with Q(0, 0) = 0.
Lemma 18 (chord reduction). Let K+ be a finite measure on [τ, A], ν(dx) = x−2 K+ (dx), and
Z
Z
A−x
x−τ
#
a+ =
ν(dx),
b+ =
ν(dx),
K+
= a+ τ 2 δτ + b+ A2 δA .
A−τ
A−τ
(i) Q(a+ , b+ ) ≤ K+ (R) ≤ M (a+ , b+ ). (ii) For every finite measure W with bounded support and
every convex ψ : R → R with |ψ(z)| ≤ c(1 + |z|), Eψ(ZK+ +W ) ≤ Eψ(ZK # +W ). In particular
+

E|ZK+ +W | ≤ E|ZK # +W |.
+

R
Proof. Put Λ = ν(R) ≤ τ −2 K+ (R) and m = x ν(dx). Since τ (A − x) + A(x − τ ) = (A − τ )x, we
#
have a+ + b+ = Λ and a+ τ + b+ A = m. If Λ = 0 then K+ = K+
= 0 and there is nothing to prove;
let Λ > 0.
R
(i) Cauchy–Schwarz gives m2 ≤ Λ x2 ν(dx) = ΛK+ (R), i.e. Q(a+ , b+ ) ≤ K+ (R). By convexity,
x−τ 2
2
x2 ≤ A−x
A−τ τ + A−τ A on [τ, A]; integrating against ν gives K+ (R) ≤ M (a+ , b+ ).
d

(ii) As in the proof of Lemma 3, ZK+ = SN − m, where N ∼ Poisson(Λ) and, independently,
Sn = J1 + · · · + Jn with Ji i.i.d. of law ν/Λ. Let Ji# be i.i.d. of law π = (a+ δτ + b+ δA )/Λ, with
x−τ
partial sums Sn# , independent of N . For convex φ and x ∈ [τ, A], φ(x) ≤ A−x
A−τ φ(τ ) + A−τ φ(A), and
integrating against ν/Λ gives Eφ(J1 ) ≤ Eφ(J1# ). Applying this to the convex functions φ(· + s)
and integrating over the other (independent) summands, we may replace J1 , . . . , Jn by J1# , . . . , Jn#
one at a time: Eφ(Sn + y) ≤ Eφ(Sn# + y) for all n and y. Summing against P(N = n) gives
d

#
#
− m + y). By the colouring theorem for Poisson processes, SN
=
Eφ(SN − m + y) ≤ Eφ(SN
d

#
τ Na+ + ANb+ with independent counts, so SN
− m = ZK # . Finally, ZK+ +W = ZK+ + ZW and
+
ZK # +W = ZK # +ZW with independent summands; take φ = ψ, condition on ZW = y and integrate.
+

+

All expectations are finite, since |ψ(z)| ≤ c(1 + |z|) and all the variables are square integrable.
Lemma 19 (the rate functions). On [0, ∞)2 the functions M , Q and M − Q are continuous
and nondecreasing in each variable, M (a, b) − Q(a, b) = ab(A − τ )2 /(a + b) for a + b > 0, and
Q(a, b) ≥ max(aτ 2 , bA2 ).
Proof. For a + b > 0, (aτ 2 + bA2 )(a + b) − (aτ + bA)2 = ab(A − τ )2 , which gives the formula.
The function ab/(a + b) is nondecreasing in each variable: it equals (1/a + 1/b)−1 if a, b > 0 and
0 otherwise. Continuity at 0 follows from 0 ≤ Q ≤ M ≤ A2 (a + b). With s = aτ + bA, ∂a Q =
s (aτ + b(2τ − A))/(a + b)2 ≥ 0 because 2τ = 1.7 > A, and ∂b Q = s (a(2A − τ ) + bA)/(a + b)2 ≥ 0.
Hence Q(a, b) ≥ Q(a, 0) = aτ 2 and Q(a, b) ≥ Q(0, b) = bA2 .

7.2

Reduction to a box of chord rates

For a box B = [a1 , a2 ] × [b1 , b2 ] ⊂ [0, ∞)2 put

µB = 1 − max Q(a2 , b2 ), 12 + M (a2 , b2 ) − M (a1 , b1 ),

capB = (b2 − b1 )A2 ,

CB = τ (Na1 − a1 ) + A(Nb1 − b1 ) (independent Poisson counts) and hB (r) = E|CB + r|. Let WB be
the set of measures W on [−A, τ ] ∪ {A} with W (R) = µB and W ({A}) ≤ capB . Call B empty if
Q(a1 , b1 ) ≥ 54 or M (a2 , b2 ) < 12 .
13

Lemma 20 (box reduction). Let K be a probability Kolmogorov measure on [−A, A] with 21 ≤ V+ <
4
28
17
5 , and let (a+ , b+ ) be the chord rates of K+ = K|[τ,A] (Lemma 18). (i) (a+ , b+ ) ∈ [0, 25 ] × [0, 50 ].
(ii) If (a+ , b+ ) ∈ B, then B is not empty, and there is W ∈ WB with E|ZK | ≤ EhB (ZW ).
Proof. (i) By Lemmas 18(i) and 19, max(a+ τ 2 , b+ A2 ) ≤ Q(a+ , b+ ) ≤ V+ < 54 . So a+ < 0.8/τ 2 =
17
2
1.107 . . . < 28
25 and b+ < 0.8/A = 0.337 . . . < 50 .
(ii) Write Q+ = Q(a+ , b+ ), M+ = M (a+ , b+ ), Qi = Q(ai , bi ) and Mi = M (ai , bi ). By Lemma 19,
Q1 ≤ Q+ ≤ Q2 and M1 ≤ M+ ≤ M2 . If Q1 ≥ 45 then Q+ > V+ , and if M2 < 12 then M+ < V+ ;
both contradict Lemma 18(i). So B is not empty.
Let W0 = K|[−A,τ ) , of mass 1 − V+ , and W1 = W0 + (a+ − a1 )τ 2 δτ + (b+ − b1 )A2 δA . Then
d

#
K+
+ W0 = Kc + W1 with Kc = a1 τ 2 δτ + b1 A2 δA , and ZKc = CB . The measure W1 is carried
by [−A, τ ] ∪ {A}, W1 ({A}) = (b+ − b1 )A2 ≤ capB , and W1 (R) = 1 − V+ + M+ − M1 . We claim
that W1 (R) ≤ µB . Since V+ ≥ max(Q+ , 21 ) by Lemma 18(i), it suffices that max(Q+ , 21 ) − M+ ≥
max(Q2 , 12 ) − M2 :

 if Q2 ≤ 21 , the left side is at least 21 − M+ ≥ 12 − M2 , which is the right side;
 if Q2 > 21 , the left side is at least Q+ − M+ ≥ Q2 − M2 , because M − Q is nondecreasing.
d

Put W = W1 + (µB − W1 (R)) δ0 ∈ WB ; then ZW = ZW1 + σG with σ 2 = µB − W1 (R). Now
E|ZK | ≤ E|ZK # +W0 | by Lemma 18(ii), and E|ZK # +W0 | = E|CB + ZW1 |. Next, E|CB + ZW1 | ≤
+

+

E|CB +ZW1 +σG| by Jensen (E|x+σG| ≥ |x|, conditionally on CB +ZW1 ), and E|CB +ZW1 +σG| =
E|CB + ZW | = EhB (ZW ) by independence.

7.3

The rest: moments, linear functionals, and the certificate inequalities

R
For W ∈ WB put κj (W ) = xj−2 W (dx) for j ≥ 2; so κ2 (W ) = µB (with 00 = 1), and κ3 , κ4 are
the first and second moments of W . Put RB = [−AµB , τ µB + (A − τ )capB ] × [0, A2 µB ].
Lemma 21 (moments of the rest). Let W ∈ WB and Y = ZW . Then Ees|Y | < ∞ for every s.
n
The cumulants
 Y are 0 (first) and κj (W ) (j ≥ 2), and EY = Pn , where P0 = 1, P1 = 0 and
Pn n−1of
Pn = i=2 i−1 κi (W )Pn−i . Moreover (κ3 (W ), κ4 (W )) ∈ RB .
R
P
j
Proof. W has compact support, so K(s) = log EesY = (esx − 1 − sx) x−2 W (dx) = j≥2 sj! κj (W )
is an entire function. Comparing the coefficients of sn−1 /(n − 1)! in M′ = K′ M, where M = eK ,
gives the recursion. For the last claim, with w = W ({A}) ≤ capB : κ3 ≤ τ (µB − w) + Aw ≤
τ µB + (A − τ )capB , κ3 ≥ −AµB , and 0 ≤ κ4 ≤ A2 µB .
Lemma 22 (linear Rfunctionals). Let R be a Borel function on [−A, τ ] ∪ {A}, bounded above on
[−A, τ ] by S. Then R dW ≤ µB S + capB (R(A) − S)+ for every W ∈ WB .
R
Proof. With w = W ({A}) ∈ [0, capB ] we have W ([−A, τ ]) = µB − w ≥ 0. So R dW ≤ (µB −
w)S + wR(A) = µB S + w(R(A) − S) ≤ µB S + capB (R(A) − S)+ .
A cell is a rectangle C = [k3− , k3+ ] × [k4− , k4+ ]. We write WB (C) = {W ∈ WB : (κ3 (W ), κ4 (W )) ∈
C}. All statements below are about W ∈ WB (C), and every real parameter in them (s3 , s4 , the
multipliers, the coefficients of φ) is arbitrary. The certificate supplies them, and they need not be
optimal.

14

j−2 − s x − s x2 and S ≥
(a) Cumulant ranges.
3
4
R Let j ∈ {3, . . . , 16}, s3 , s4 ∈ R, g(x) = x
sup[−A,τ ] g. Then κj = g dW + s3 κ3 + s4 κ4 , so Lemma 22 gives

κj ≤ Uj := µB S + capB (g(A) − S)+ + max(s3 k3− , s3 k3+ ) + max(s4 k4− , s4 k4+ ).
The lower bound Lj comes in the same way from −g (with its own s3 , s4 ). For j = 3, 4 the ranges
are intersected with C. If Lj > Uj for some j, then WB (C) = ∅.
(b) Empty cells (Farkas). Let g(x) = −s3 x − s4 x2 and S ≥ sup[−A,τ ] g. For every W ∈
R
WB (C) we have 0 = g dW + s3 κ3 + s4 κ4 ≤ Φ := µB S + capB (g(A) − S)+ + max(s3 k3− , s3 k3+ ) +
max(s4 k4− , s4 k4+ ). So Φ < 0 implies WB (C) = ∅.
(c) The Lagrangian bound. Let φ(r) =
Expanding the Pk with κ2 = µB gives
′

Eφ(ZW ) = c +

P16

k
k=0 ck r .

16
X
j=3

pj κj +

By Lemma 21, Eφ(ZW ) =

X

P

k ck Pk .

eα κα ,

α∈P

where P is the set of sorted tuples α = (α1 ≤ · · · ≤ αt ), t ≥ 2, αi ≥ 3, that occurQ
in some Pk ,
k ≤ 16, together with their prefixes of length ≥ 2 (81 tuples, t ≤ 5), and κα = i καi . The
coefficients c′ , pj , eα are exact polynomials in µB and the ck . For α = (α′ , j) ∈ P (α′ the prefix
′
of length t − 1) let X = κα (or X = κα1 if t = 2) and Y = κj . Let [Y − , Y + ] = [Lj , Uj ] from
(a), and let [X − , X + ] be the interval product of the ranges from (a) of the factors of X. Likewise
[κα,− , κα,+ ] is the interval product of the ranges of the καi . With wα = κα the following are ≥ 0
on WB (C):
wα − X − Y − Y − X + X − Y − ,

wα − X + Y − Y + X + X + Y + ,

−wα + X + Y + Y − X − X + Y − ,
−wα + X − Y + Y + X − X − Y + ,
Z
Z
P
t−1
|x|sα dW + wα
(sα = i (αi − 2)),
|x|sα dW − wα ,
µt−1
µB
B
k3+ − κ3 ,

κ3 − k3− ,

k4+ − κ4 ,

κ4 − k4− .

The first four are the McCormick inequalities (X − X − )(Y − Y − ) ≥ 0, (X + − X)(Y + − Y ) ≥ 0,
(X + − X)(Y − Y − ) ≥ 0, (X − X − )(Y +
0. The
are Hölder’s inequality: for µB > 0
Q− Y ) ≥
Q nexts two
p
p
/s
s
i
i
and P
the probability measure W/µ
≤ i (E|x|
R ) s = E|x| with pi = αi − 2 ≥ 1 and
Q BR, iαE|x|
t−1
α
−2
s=
pi (Lyapunov), so |κ | ≤ i |x| i dW ≤ µB
|x| α dW ; if µB = 0 then W = 0. The last
four are
multiples
of these expressions
W ). Since
R the definition of WB (C). Add nonnegative
R
P
P to Eφ(ZP
κj = xj−2 dW , the result has the form c′′ + R dW + α e′α wα with R(x) = j p′j xj−2 + s γs |x|s .
By Lemma 22 and wα ∈ [κα,− , κα,+ ],
X
Eφ(ZW ) ≤ β := c′′ + µB SR + capB (R(A) − SR )+ +
max(e′α κα,− , e′α κα,+ ),
α

for any SR ≥ sup[−A,τ ] R. On [−A, 0] and on [0, τ ], R is a polynomial.
Lemma 23 (majorant test). Let L ≥ τ a1 + Ab1 and na , nb ≥ 0. For n ≤ na , m ≤ nb put
πnm = P(Na1 = n)P(Nb1 = m) and cnm = τ (n−a1 )+A(m−b
1 ). Let T ≥ P(Na1 > na )+P(Nb1 > nb )
P
and e = (T (τ 2 a1 + A2 b1 ))1/2 . (i) hB (r) ≤ H(r) := n≤na ,m≤nb πnm
P|cnm + r| + T |r| + e for all r. (ii)
hB (r) = r for r ≥ L, and hB (r) ≤ −r +δ for r ≤ −L, where δ = 2 n≤na ,m≤nb πnm (cnm −L)+ +2e.
(iii) Let φ be a polynomial and ε ≥ 0. Suppose the Taylor coefficients of t 7→ φ(L + t) − L − t and
of t 7→ φ(−L − t) − L − t − δ are nonnegative, and φ + ε ≥ H on [−L, L]. Then φ + ε ≥ hB on R.
15

2 = τ 2 a + A2 b .
Proof. Let E = {Na1 ≤ na , Nb1 ≤ nb }, so P(E c ) ≤ T , and recall ECB = 0, ECB
1
1
2 )1/2
(i) E[|CB + r|; E] is the sum, and E[|CB + r|; E c ] ≤ |r|P(E c ) + E[|CB |; E c ] ≤ T |r| + (P(E c )ECB
(Cauchy–Schwarz). (ii) CB ≥ −τ a1 − Ab1 ≥ −L, so CB + r ≥ 0 and hB (r) = r for r ≥ L. For
r ≤ −L, |CB + r| = |r| − CB + 2(CB − |r|)+ , so hB (r) = −r + 2E(CB − |r|)+ ≤ −r + 2E(CB − L)+ .
On E this is the sum, and on E c use (CB − L)+ ≤ |CB | and Cauchy–Schwarz as in (i). (iii) For
t ≥ 0, φ(L + t) ≥ L + t = hB (L + t) and φ(−L − t) ≥ L + t + δ ≥ hB (−L − t) by (ii); on [−L, L]
use (i).

On [−L, L], H is piecewise linear, with kinks at 0 and at the points −cnm . The test φ + ε ≥ H
is therefore one polynomial upper bound per piece, sup(H − φ) ≤ ε.
Lemma 24 (cell certificate). If φ + ε ≥ hB on R and Eφ(ZW ) ≤ β for all W ∈ WB (C), then
EhB (ZW ) ≤ β + ε for all W ∈ WB (C).
Proof. hB ≤ φ + ε pointwise, and E|φ(ZW )| < ∞ by Lemma 21.
Proof of Theorem 16. Reflection x 7→ −x maps ZK to −ZK and exchanges V+ and V− , so assume
4
1
2 ≤ V+ < 5 . By Lemma 20(i), the chord rates (a+ , b+ ) lie in some leaf box B of the cover of
28
[0, 25
] × [0, 17
50 ] described in Section 7.4. By Lemma 20(ii), B is not empty, so the computation
has a tiling of RB by cells with certificates for B. Also by Lemma 20(ii), there is W ∈ WB with
E|ZK | ≤ EhB (ZW ). By Lemma 21, (κ3 (W ), κ4 (W )) ∈ RB , so it lies in some cell C of the tiling.
Then WB (C) ̸= ∅, so the certificate of C is not an emptiness certificate ((a) or (b)). It is therefore a
polynomial φ with φ+ε ≥ hB (Lemma 23) and Eφ(ZW ) ≤ β (by (c)), where β +ε < C5 . Lemma 24
gives E|ZK | ≤ β + ε < C5 .

7.4

The certified computation (scripts/verify plus.py)

The verifier scripts/verify plus.py and its library scripts/plus verify lib.py use only
python-flint: fmpq for exact rationals and arb balls at 128 bits. Every inequality is decided by
a comparison of balls that is certain. The certificate data are IEEE doubles, which are exact
dyadic rationals and are converted exactly. τ , A,√the box and cell endpoints, µB , capB and RB are
exact rationals, and C5 is a ball containing 1.28 2 ln 1.25.
Polynomial upper bounds. For a polynomial p given by ball coefficients and an interval [u, u′ ],
an upper bound for sup[u,u′ ] p is computed by branch and bound. On a piece [m−d, m+d] with exact
centre m, the Taylor
coefficients
P
Pqk of p(m + t) are computed by Horner shifts in ball arithmetic.
Then p ≤ q0 + k odd |qk |dk + k≥2 even max(qk , 0)dk on the piece. Pieces are bisected while this
bound exceeds the best value found by more than a tolerance. The result is the maximum of the
bounds of the final pieces; the tolerance affects only the tightness. This is used for S in (a) and
(b), for SR in (c) (separately on [−A, 0] and [0, τ ]), and for each piece of H − φ in Lemma 23.
√
Majorant data. In Lemma 23, na is chosen in floating point (about a1 + 12 aP
1 + 20, likewise
nb ). The P
probabilities πnm are balls, and T is the upper end of the ball (1 − n≤na P(Na1 =
n)) + (1 − m≤nb P(Nb1 = m)), clipped at 0. L is the double stored in the certificate (between 7.20
and 14.63), checked to be ≥ τ a1 + Ab1 . The kinks −cnm are exact rationals. The returned ε is the
upper end of the largest piece bound, and ε = 0 if all are ≤ 0.

16

28
] × [0, 17
Boxes. The rate rectangle [0, 25
50 ] is divided into 16 × 16 boxes. A box that the generator
could not certify was split into four, up to four times. The box with indices (ia , ib ) at level d is
−4−d × [i , i + 1] · 17 2−4−d . The verifier checks that the recorded leaves tile the
[ia , ia + 1] · 28
b b
25 2
50
rectangle. Every index must lie in its grid (0 ≤ ia , ib < 24+d ), so every leaf lies in exactly one
initial box, and each of the 256 initial boxes must contain at least one leaf. For each initial box,
its leaves must be pairwise non-nested dyadic sub-squares whose areas add up to its area. Distinct
non-nested dyadic squares have disjoint interiors, so their union then has full measure, and being
closed it is the whole box. A leaf recorded as empty must satisfy Q(a1 , b1 ) ≥ 54 or M (a2 , b2 ) < 12 in
exact arithmetic.

Cells. For every other leaf, the verifier checks that the recorded cells tile RB (quadtree leaves
with indices in their grid, the same test; in this run of depth ≤ 2), and checks each cell certificate. A certificate of type ‘ok’ passes if φ has 17 finite coefficients (degree ≤ 16), the tail test
of Lemma 23(iii) holds at L, and β + ε < C5 . Here ε is computed as above, the ranges [Lj , Uj ]
(3 ≤ j ≤ 16) come from (a) with the certificate’s (s3 , s4 ), and β from (c) with the certificate’s
multipliers (negative entries are replaced by 0). A cell certified empty by (a), i.e. with Lj > Uj for
some j, passes whatever its type. A certificate of type ‘empty farkas’ passes if Φ < 0 in (b).
Result. The recorded run (outputs/plus cert/verify v1.txt; 2026-10-22, 22:24:54–
22:25:19 UTC, 8 processes; python 3.12.3, python-flint 0.9.0) of scripts/verify plus.py
(md5 c754a7305654c6635025f7e405dd98bb) with scripts/plus verify lib.py (md5
8111a51880ffc9e29485682579cadb54) on the five files outputs/plus cert/certs v1 r0.jsonl,
. . . , certs v1 r4.jsonl (their md5s are printed in the run) reports:
box level d
0
1
2
3
4

certified leaves
96
71
66
44
3

empty leaves
134
12
6
3
1

That is 436 leaves tiling the rectangle, 0 failures, and 1237 cell certificates: 1236 of type ‘ok’ and
1 of type ‘empty farkas’. The cells have depth 0 (109), 1 (536) and 2 (592). The largest certified
bound β + ε is 0.854883 < C5 = 0.8551004 . . ., in the box [0.0525, 0.0700] × [0.2072, 0.2125] (where
V+ is close to 12 ). Boxes were split until their bound was below the generator’s target C5 − 2 · 10−4 ,
so many bounds sit just below that target. The eight largest are all at a+ ≤ 0.175, near V+ = 12 as
well as further inside the region (outputs/plus cert/stats v1.txt). This proves Theorem 16.
An earlier run (21:47 UTC, outputs/plus cert/verify v1 first.txt) of a first version of the
verifier (md5 0e412f55eda9b9a4c7a92e8e8def58f6) gave the same counts. That version did not
check that the box indices lie in their grid, so a missing initial box could have been replaced by an
out-of-range copy of a box. The data satisfy the check, and the recorded version makes it.
How the certificates were found (not part of the proof ). scripts/plus cert.py solves,
for each box and cell, a linear program in floating point (HiGHS), on a grid of r and of the support
of W . The primal is a discretised moment problem. The moment rows are written in the Chebyshev
basis Tk (r/L), and columns for the Taylor coefficients of the tails at ±L are included. The duals give
φ and the multipliers, and an exchange step adds violated grid points. scripts/plus driver.py
runs the adaptive box and cell refinement (run plus driver.py v1 4 4 2 4, 21:27–21:38 UTC,
17

log outputs/plus cert/log v1.txt; generator target C5 − 2 · 10−4 ). The certificates of run v1
were produced before a repair step for narrow wells of φ − H near ±L (fix wells) was added to
plus cert.py. The repair lowers ε but plays no role in the verification.
Controls
(not
part
of
the
proof ). scripts/verify plus controls.py
(outputs/plus cert/controls v1.txt) reruns all box checks with C5 replaced by C5 − s.
For s = 0, 10−4 , 3 · 10−4 , 10−3 , 3 · 10−3 , respectively 0, 0, 9, 50, 187 of the 280 non-empty boxes fail.
So the certified margin of the worst boxes lies between 10−4 and 3 · 10−4 . Removing any one box
record, or one cell of a box, makes the corresponding tiling test fail, and so does moving one box
or cell index out of its grid.
Float
self-tests
(evidence
only). scripts/test plus verify.py
(outputs/plus cert/selftest v1 r*.txt, all pass on all five files) runs five tests.
 It compares the moment polynomials Pn (n ≤ 16) with a direct expansion for two Poisson
atoms and a Gaussian (relative difference 3 · 10−14 ).
 It compares the polynomial upper bound with dense evaluation, the exact value at the dense
maximiser being below the bound.
 It compares hB − φ on a dense grid of [−3L, 3L] with ε (never above ε).
 It draws 3000 random W ∈ WB per file. Every κj lies in its certified range, and Eφ(ZW ) ≤ β,
with smallest gap 4.6 · 10−4 .
 End to end, on 747 random K in the heavy region (edge laws with any V+ ∈
[max(Q, 21 ), min(M, 45 ))), E|ZK |, computed in floating point by Poisson enumeration, stays
below the certified bound of its cell by at least 0.033.

The float supremum over the heavy region of the bound with exact moments of W , i.e. with no cell
or McCormick loss, is about 0.8387 (scripts/plus scan.py, outputs/far extra/plus scan/, 7
seeds). The box, cell and relaxation losses together raise the maximum from about 0.8387 to the
certified 0.8549.

18

