The exact reconstruction threshold for the three-state symmetric channel

1 Introduction

The reconstruction problem asks whether many distant, noisy descendants retain information about their common ancestor. On a tree, the growth in the number of descendants competes with the loss of information across each edge. For a symmetric channel with nontrivial eigenvalue \lambda and mean offspring number d, the Kesten–Stigum condition d\lambda^2>1 gives reconstruction. Whether this condition is also necessary depends on the channel. We determine the answer for three states at every branching parameter in two basic tree families. Through existing tree-to-graph and algorithmic results, the Poisson theorem also determines the weak-recovery threshold for the symmetric three-community sparse stochastic block model with positive connectivity parameters and mean degree greater than one.

1.1 Model and result

Let the root spin \sigma_\rho be uniform on \{1,2,3\}. Along each edge, independently conditional on its parent spin, transmit through

The tree is either the rooted b-ary tree, with an integer b\ge2 children at every vertex, or a Galton–Watson tree with independent \operatorname{Pois}(d) offspring counts, where d>1. For the regular model set d=b. The tree is independent of the root spin. The observation at depth \ell consists of the unlabelled tree T_{\le\ell} through that depth together with the spins attached to its vertices \partial T_\ell at depth \ell; neither interior spins nor an ordering of siblings are observed. Define

In the Poisson case this expectation includes both the tree and the spins, without conditioning on survival. Reconstruction means \lim_{\ell\to\infty}a_\ell>0; non-reconstruction means that this limit is zero. The limit exists by information degradation.

Thus the positive threshold is \lambda=d^{-1/2}. On the negative side reconstruction occurs precisely when d>4 and -1/2\le\lambda<-d^{-1/2}. In particular, the three-coloring channel \lambda=-1/2 is non-reconstructible at branching parameter four in both models.

1.2 History and significance

The branching-process work of Kesten and Stigum [8] underlies the classical second-moment reconstruction bound. Broadcasting and its relation to the Ising model were developed by Evans, Kenyon, Peres, and Schulman [4]. For more than two states, nonlinear information in the boundary can change the threshold. This possibility occurs for symmetric channels with five or more states [13, Theorem 1.2]; the three-state assertion therefore needs more than the second-moment bound.

Mézard and Montanari [9, Conjecture 2 and the following paragraph] predicted sharpness of the Kesten–Stigum bound for three-state symmetric channels of either sign up to a branching cutoff, and proposed the extension to all branching parameters. See also Conjecture 1 of Sly [13] for the all-degree regular-tree formulation. Sly proved this for all sufficiently large regular branching parameters, including non-reconstruction at equality [13, Theorem 1.1]. Mossel, Sly, and Sohn established the corresponding large-mean Poisson-tree result, for both signs and including equality [10, Theorem 1.12]. At small degrees, Bhatnagar and Maneva developed finite representations of posterior laws and proved, among other bounds, non-reconstruction for three-colorings on the regular ternary tree [2, Theorem 12]. Theorem 1.1 removes the large-branching restriction in these two tree families. It resolves the three-state regular-tree prediction in its all-degree form and includes the low-branching and coloring endpoints for the observed Poisson tree.

For the symmetric stochastic block model, the cavity-method analysis of Decelle, Krzakala, Moore, and Zdeborová predicted the Kesten–Stigum transition in the assortative three-community case [3, Section IV.A]. Ricci-Tersenghi, Semerjian, and Zdeborová gave further evidence for the three-state prediction for either sign, through local analysis of the posterior recursion and numerical cavity solutions [12, Sections III.D.1 and IV.H]. Mossel, Sly, and Sohn proved information-theoretic impossibility at and below the Kesten–Stigum bound for three or four communities when the mean degree is sufficiently large [10, Theorem 1.5]. Their tree-to-graph transfer has no large-degree restriction [10, Theorem 2.1]. Together with the above-threshold algorithm of Abbe and Sandon [1, Corollary 1 and Lemma 1], the Poisson part of our theorem therefore gives the exact three-community weak-recovery threshold stated in Corollary 1.2 below.

A related three-state model with branch-dependent couplings on a binary Cayley tree is studied by Mukhamedov and Akın [11]. Their work concerns disordered translation-invariant Gibbs measures and their extremality; our theorem concerns the same homogeneous symmetric channel on every edge of the regular or observed Poisson tree.

1.3 Proof strategy and its precedents

For a root posterior p=(p_1,p_2,p_3), write m_i=3p_i and identify the three spin labels with 1,\omega,\omega^2, where \omega=e^{2\pi\mathrm{i}/3}. The complex posterior mean and its two basic invariants are

The posterior recursion passes each child experiment through one edge and combines the resulting conditionally independent branch observations. Section 2 gives this recursion and proves that the limiting posterior law is a fixed point, including at the coloring endpoint. Non-reconstruction is equivalent to \E x=0 under that law. A linear estimator proves reconstruction above the threshold. Channel and offspring degradation reduce the converse to critical equality and the coloring case at branching parameter four.

At positive equality, Section 3 compares two expressions for the change of an entropy functional across the recursion. The expected symmetrized-entropy identity goes back to Formentin and Külske [5, Proposition 3.3 and equation (15)]. Our functional combines entropy and symmetrized entropy with a quadratic centered-logarithm term. The fixed-point identities express its change through the correlation generated by combining branches, while a radial inequality bounds it below by a positive multiple of \E x^2. Moment estimates make these two bounds incompatible at a nonuniform limiting fixed point. Appendix A proves the radial inequality analytically. Related entropy methods include the sharp nonlinear information-contraction inequalities for the Potts channel and non-reconstruction criteria of Gu and Polyanskiy [7].

The negative argument separates small and large posterior moments. Sly’s large-branching proof already combines a moment estimate near the uniform posterior with a global Gaussian contraction, including a rigorous numerical verification [13, Section 1.5, Lemmas 4.7–4.8, and Appendix A]. Here Section 4 proves a uniform quantitative gap: at every negative equality, any nonuniform symmetric fixed point satisfies \E x>1/20. Pair inequalities for x, y, and x^2 yield this gap through a moment bootstrap. Section 5 then uses weighted logarithm identities to exclude the remaining fixed points away from the coloring channel.

Near coloring, Section 6 constructs finite experiments that are more informative than the true boundary observation. It suffices for one such upper experiment to have \E x<1/20: the true limiting fixed point then falls below the gap and must be uniform. The upper recursion need not itself converge to the uniform experiment. Bhatnagar and Maneva introduced finite surveys of posterior laws and combined certified finite recursion with local contraction [2, Sections 3.1–3.3 and Theorem 12]. Their construction includes completion by perfectly informative messages for omitted offspring tails and downward-rounded masses [2, Section 3.3, implementation remarks 1 and 4]. We use this finite-experiment approach with the gap above and explicit three-state refinement kernels. Gu’s recent binary-hypertree work proves a related rigorous population-dynamics procedure and proposes a Potts extension based on degradation and local non-reconstruction [6, Sections 4 and 7].

The quantitative radial bound, uniform fixed-point gap, and exact certificates supply the estimates needed throughout the parameter range. The negative argument is computer-assisted: the polynomial, interval, and finite-experiment programs are printed in Appendix D. Their mathematical interpretation and arithmetic bounds are proved in the text. All decimal constants denote exact terminating rationals, and no simulation estimate enters a certification decision. Section 7 assembles the tree classification; Table 1 there records the parameter ranges of its analytic and finite arguments.

1.4 A consequence for community detection

We now use a and b for within- and between-community connectivity parameters, independently of the notation for regular branching above. Fix a,b>0 with d=(a+2b)/3>1. For all sufficiently large n, choose \sigma_1,\ldots,\sigma_n independently and uniformly from \{1,2,3\}. Conditional on these labels, form a graph G_n on \{1,\ldots,n\} by including each unordered pair independently, with probability a/n if its endpoints have the same label and b/n otherwise. For two labelings \sigma,\widehat\sigma\in\{1,2,3\}^n, define their overlap by

The permutation accounts for the fact that the names of the communities cannot be recovered from the graph.

The proof of Corollary 1.2, including the passage from averaged tree non-reconstruction to the fixed-tree hypothesis of the transfer theorem, is given in Section 7.

2 Posterior experiments and reductions

We represent the spin set by \mathcal S=\{1,\omega,\omega^2\}, where \omega=\exp(2\pi\mathrm{i}/3), and write S_v for the complex spin at a vertex v. In the probabilistic recursions, D denotes an offspring count, and

All probabilities in the Poisson model are unconditional: the observed tree is part of the data, and extinction is not removed from the sample space.

2.1 Observations, likelihoods, and posterior coordinates

For calculations we construct the tree with ordered children. At each vertex, independently, we draw its offspring count and then the spins of its children through K_\lambda. The root spin is uniform and is independent of all offspring counts. The resulting tree is locally finite almost surely. Let

denote its depth-\ell observation, initially with this auxiliary ordering retained. The unlabelled observation retains the rooted tree and its boundary-spin decoration, but forgets all sibling orders.

An experiment consists of a uniform spin S\in\mathcal S and an observed datum Y. Write

Thus the likelihood vector m takes values in the compact simplex

For coordinatewise expressions we use \langle h\rangle=\frac13\sum_{i\in\mathcal S}h_i. When coordinates are written as numerical triples indexed by 0,1,2, coordinate i\in\{0,1,2\} corresponds to the spin label \omega^i. The complex posterior and its two basic invariants are

Here the i inside the coordinate average is the spin label, not the imaginary unit. Fourier inversion on the three-element group gives

More precisely, each of the three coordinates satisfies

To verify the first identity, expand (\zeta\overline{i}+\overline{\zeta}i)^3 and use i^3=1. The second follows from \sum_i v_i=0, \sum_i v_i^2=6x, and \prod_i v_i=2y. The convex-hull constraint on \zeta, together with \prod_i m_i\geq0, gives

For later use these also imply, when x>0,

Indeed |r|\leq\sqrt{x}\leq1, and the last inequality in Equation (2.6) gives the upper bound on x. Combining the two bounds on x gives 0\leq1-3r^2+2r^3=(1-r)^2(1+2r), and hence r\geq-1/2.

The marginal law of a posterior likelihood vector is always balanced: \E m_i=1. Bayes’ formula states that its conditional law under input i is tilted by m_i. More generally, for a bounded measurable function g of the original datum,

Conversely, every probability law Q on \mathcal M satisfying \int m_i\,Q(dm)=1 defines an experiment by taking Q(dm\mid S=i)=m_iQ(dm). Its posterior likelihood vector is precisely the observed m. Thus balanced laws on \mathcal M are sufficient to describe the experiments used below.

The posterior vector also loses no inferential information from an existing experiment. In fact \PP(S=i\mid Y,m)=m_i/3=\PP(S=i\mid m), so S and Y are conditionally independent given m. The original datum can therefore be conditionally simulated from m without knowing S. All observation spaces here are standard Borel, so the required conditional kernels exist.

Our experiments are invariant under every permutation of the three spin labels. In complex coordinates these permutations are generated by \zeta\mapsto\omega\zeta and \zeta\mapsto\overline{\zeta}. This invariance is retained by all the tree recursions and limits below.

2.2 The exact posterior recursion

Suppose Y is a child experiment with likelihood vector m. The child spin has a uniform marginal, and the conditional law of Y given parent spin i, relative to the child marginal law, has density

Thus the datum retains its original marginal law under the uniform parent prior. The edge operation sends

To combine n experiments that are independent conditional on a common input, let Q_1,\ldots,Q_n be their marginal likelihood laws. Under the product marginal law Q_1\otimes\cdots\otimes Q_n, set

Conditional on input i, the joint datum has density W_i relative to that product law. Averaging over the input gives the marginal density Z, and Bayes’ formula gives the last expression in Equation (2.13). In particular, \int Z\,d(Q_1\otimes\cdots\otimes Q_n)=1. The value of m^{\mathrm{out}} on \{Z=0\} may be set equal to (1,1,1); this set has zero probability after the tilt. When n=0, empty products are one, Z=1, and the output is the uninformative vector (1,1,1).

We say that one experiment is degraded from another when its datum is obtained from the latter by a random kernel independent of the input spin. If Y' is degraded from Y, their posterior likelihoods satisfy

for every integrable convex function \Phi of the posterior vector. This is the tower property followed by conditional Jensen. In particular it applies to total variation, x, and x^2: total variation is the convex function \max_i|m_i-1|/3, while \zeta is linear in m and its squared and fourth powers of the modulus are convex. Applying degradation kernels separately to conditionally independent branches shows that edge transmission and branch composition preserve this order.

2.3 Convergence, fixed points, and extinction

Unless a different experiment is specified, we henceforth use

for the limiting experiment. Its law is trivial precisely when \mu=0, since x=0 is equivalent to m=(1,1,1). By Lemma 2.2 and Proposition 2.4, non-reconstruction is equivalent to \mu=0.

2.4 Reconstruction above the second-moment threshold

2.5 Decreasing the channel strength or the offspring mean

At \lambda=0, every positive-depth boundary is independent of the root conditional on the tree, so the advantage is zero. For each fixed d, Proposition 2.8 reduces the remaining subcritical channel parameters of either sign to their admissible equality parameters. Negative equality is admissible exactly when d\geq4; for smaller branching parameters, non-reconstruction at the coloring channel \lambda=-1/2 and branching parameter four will imply all the needed negative-channel statements by the same proposition.

3 Positive channels at equality

We prove that the limiting posterior is uniform when 0<\lambda<1 and d\lambda^2=1. Throughout this section, m has the limiting fixed-point law supplied by Proposition 2.4, v=m-1, and

Thus \alpha=1-1/d for the regular model and \alpha=1 for the Poisson model. A subscript e means evaluation at the edge message m_e=1+\lambda v. We argue by contradiction, assuming \mu>0.

3.1 An entropy identity with an additive correction

For a positive message of coordinate average one, define

Here and below logarithms are natural. The expected additivity of J below is the symmetric-channel form of the symmetrized-entropy recursion of Formentin and Külske [5, Proposition 3.3, equation (15)]: their functional equals 2J in our normalization. We prove the identities needed here, including the centered-log correction B. Lemma 2.5 gives strictly positive fixed-point coordinates and integrability of these functions: their coordinate factors are bounded, and their logarithmic factors have degree at most two.

Under a fixed input spin i, tilting and permutation symmetry give

Centered log coordinates add under products: the common normalizing constant disappears on centering. Conditional independence of the branches therefore gives

For clarity, the off-diagonal term in the second formula, before division by two, is 4\E[D(D-1)](\E J_e)^2.

For a product of n edge experiments write Z_n for its likelihood normalizer relative to their independent marginal laws, and set

This is a relative entropy and is nonnegative. Expanding the logarithm of the normalized output likelihood gives

Each branch retains its original marginal distribution after the joint likelihood tilt, which justifies the individual terms in this expansion. The combination

therefore satisfies the exact identity

The useful feature of this combination is its positive radial defect: for every positive message of coordinate average one,

Lemma A.1 proves this pointwise inequality by radial differentiation and explicit polynomial sign decompositions. Since d=\lambda^{-2}, its expectation and Equation (3.4) imply

We will contradict this inequality by bounding \E J above and H below. The additive identity for J also restricts the possible values of \mu,\nu,\eta; we establish those restrictions first.

3.2 Moment information from the additive identity

The cubic identity in Equation (2.5), together with \av{v}=0 and \av{v^2}=2x, gives the additional moment relation

We also use |y|\le x^{3/2} from Equation (2.6).

3.3 Correlation generated by successive branches

3.4 The strict contradiction

4 Negative equality: exclusion of small fixed points

Throughout this section \lambda=-a, 0<a\le 1/2, and d=a^{-2}\ge4. The offspring count is either the constant integer d or \operatorname{Pois}(d). We consider a permutation-invariant fixed point of the posterior recursion and use

All finite decimals in this section and the next denote exact rational numbers. In particular, none of the strict comparisons below is a floating-point comparison.

We first establish the pair inequalities used in the proof. If a current message has invariants (X,y_0) and an edge message has invariants (z,B_0), define d_x,d_e,d_n to be the output means of x,y,x^2 minus X+z,y_0+B_0,X^2+z^2, respectively. The output mean here averages the six relative label permutations with their likelihood tilt. Conditional on the permutation orbits of two independent symmetric marginal messages, these are exactly the relative orientations of their product experiment. If the child before the edge has invariants (w,Y), then

Set

(The letter W in this section denotes only this pair expression.)

5 Negative equality: a global weighted logarithm inequality

The local result leaves only fixed points with \mu>1/20. We now exclude these except in a short interval near the coloring channel. The scalar inequality in this section is certified by the integer interval calculation in Appendix B, with its complete source in Section D.2.

For a positive likelihood vector m=1+v define

Here \av{\cdot} is the average of the three coordinates. Edge subscripts mean evaluation on 1-av, and we use

The functions T,W,Y extend continuously to the closed simplex, with T=1 and W=Y=0 whenever any coordinate vanishes. Indeed G times any fixed power of the logarithms tends to zero as a coordinate vanishes: for example the product \prod_i m_i^{1/3} times \sum_i|\log m_i|^3 is bounded by a sum of terms having a factor m_i^{1/3}|\log m_i|^3\to0 and the other coordinates are bounded by three. This observation also proves boundedness of these extensions.

5.1 A pointwise inequality from exact identities

The identities above give several functions with expectation zero. We combine them so that the scalar bounds on h and z produce a function that is strictly positive at every message. For a nontrivial fixed point, choose signed rational constants c_0,c_1,s_1 and a positive rational \delta, and put

The relation defining s_0 removes the cubic term of T+c_0W+s_0Y near the uniform message. Indeed, expansion at v=0 gives

Its quadratic term also cancels on subtracting d times its edge evaluation, since da^2=1. By Lemma 5.2, the random expression

has expectation zero. In particular, the final term changes the pointwise expression without changing its expectation, since \E\widehat T=z.

Fix an applicable pair (H,U) from Lemma 5.3. Replace h in (5.6) by \overline h=1-\xi/2-H\xi^2-(H/2)\xi^3 and z by \underline z=\xi+U\xi^2, and call the resulting expression P. The only changes are in terms whose signs are controlled:

Here \widehat T\ge0, \delta>0, and \xi\ge0. The possibly negative coefficients c(\xi) and s(\xi) multiply identities that remain exact. Thus \E P\le0 for any nontrivial fixed point; it remains to choose the constants so that P>0 pointwise.

Expanding the relaxed expression gives

where

We use the following rational choices on three closed a bands:

The final row uses the stronger scalar bounds for Poisson offspring. Overlapping endpoints can use either applicable row. For purposes of the pointwise inequality, extend the hatted functions to a=0 by

These are their continuous limits: use G_e^3=1-3a^2x-2a^3y for \widehat T and \log(1-av_i)=-av_i+O(a^2) for the centered edge logarithms.

6 A finite certificate at the coloring boundary

We now prove non-reconstruction at the remaining negative equalities, including the channel \lambda=-1/2. Throughout this section a=-\lambda>0, p=(p_0,p_1,p_2) is a posterior probability vector, and \zeta=\sum_{i=0}^2p_i\omega^i, where \omega=e^{2\pi\mathrm{i}/3}. In this section the input spin S denotes its index in \{0,1,2\}; its complex representative is \omega^S. Write \mu=\E|\zeta|^2. Proposition 4.1 says that a symmetric fixed point at da^2=1 with \mu\leq 1/20 is the uniform posterior. It will therefore suffice to dominate one finite-depth experiment by an explicit experiment with \mu<1/20. The dominating process need not itself be at equality or converge to the uniform posterior.

6.1 Explicit refinements of posterior experiments

The finite representation follows the survey method of Bhatnagar and Maneva [2, Sections 3.1–3.3 and Theorems 5–8]: posterior vectors are replaced by barycentric mixtures on a finite grid, and rounding deficits and omitted offspring tails are completed by perfectly informative messages. We give explicit refinement kernels for every operation and exact arithmetic certificates for the three-state parameter ranges used here.

For experiments with the same input spin S, write \mathcal E\preceq \mathcal F if a Markov kernel, independent of S, transforms the data of \mathcal F into data with the conditional laws of \mathcal E. Such a kernel is called a garbling. Under the uniform prior, an experiment with datum Y, marginal law \rho, and posterior p(Y) satisfies

Its full labeled posterior is an equivalent experiment: the reverse kernel from p to Y is the conditional marginal law \rho(dy\mid p(Y)=p). Equation (6.1) proves that this kernel also works under every input spin. All conditional distributions used here exist on the finite or standard Borel spaces in question.

We compress a permutation-invariant posterior law by storing one mass for each orbit under the six coordinate permutations. The represented datum is always the full labeled posterior. Under its marginal law, draw an orbit, uniformly permute its representative, and retain the resulting vector. Repeated coordinates cause no difficulty, since each distinct orientation has the same multiplicity among the six permutations. Observing only the orbit index would be a different experiment and is not used below.

Both independent composition and edge transmission preserve \preceq. In detail, if G_j garbles the jth upper branch into the jth lower branch, instantiate the upper branch data independently conditional on their common input spin, and use the product kernel \prod_jG_j with independent auxiliary randomness. Under each input this recovers the product of the lower conditional laws. For an edge, averaging these same conditional identities against the channel K_\lambda(i,j) proves the claim. Mixing over an input-independent count also preserves the order: retain the count and apply the appropriate product garbling conditional on it. These facts justify each induction below; no monotonicity of the numerical rounding map is assumed.

6.2 Grid spreading and exact product tables

Fix

There are 469 representatives in \mathcal H. An integer vector of nonnegative masses (m_h)_{h\in\mathcal H} summing to N represents the symmetric posterior law with orbit probabilities m_h/N and posteriors h/H. Denote the pure and uniform orbit laws by \mathsf P and \mathsf U.

For an integer vector r\geq0 of positive total T, set

If k=0, choose n/H. If k=1, choose (n+e_i)/H with probability b_i/T. If k=2, choose (n+\mathbf1-e_i)/H with probability (T-b_i)/T. These are valid grid vectors and probabilities. For k=2 the expected increment in coordinate j is \sum_{i\ne j}(1-b_i/T)=b_j/T; the other two cases are immediate. The chosen vector therefore has mean r/T, and Lemma 6.1 proves refinement. The construction commutes with label permutations.

For rational edge magnitude a=A/B\leq1/2, first reduce A/B to lowest terms. A child grid posterior q/H gives parent likelihood entries

whereas its plain likelihood entries are 3q_i/H. To combine two orbit representatives p,q, fix the orientation of p and average the six relative permutations \pi of q. This is sufficient because a simultaneous permutation changes only the output orientation, which remains uniform within its orbit. The following table specifies the three operations used by the verifier:

In each case, with T=\sum_i r_i, the posterior is r/T and the relative permutation’s probability after the likelihood tilt is T/D_{\mathrm{tab}}. For example the mode 1 tilt is \frac13\sum_i(3p_i/H)(e_{\pi(i)}(q)/(BH))=T/(BH^2); the additional permutation factor is 1/6. The other rows follow in the same way. A permutation with T=0 has zero probability and contributes nothing, including at a=1/2.

Multiply these probabilities by the grid spread. The resulting table numerators are respectively T when k=0, b_i when k=1, and T-b_i when k=2, all over the row’s common denominator D_{\mathrm{tab}}. Aggregate contributions reaching the same output orbit. Write the integer result as w_{p,q}(h). For every pair,

Indeed the spread has mass one, and averaging either input likelihood over uniform label permutations gives one in each coordinate. The verifier additionally asserts (6.5) for every entry.

For input integer mass laws m,n, keep output units

and add N-\sum_h\ell_h units to the pure orbit. The unfloored quantity divided by N is the exact orbit mass of the spread product, so Lemma 6.2 proves that this operation dominates the indicated exact product. Denote it by \mathcal C_0,\mathcal C_1 or \mathcal C_2. Modes 0 and 2 have symmetric tables in p,q: exchange the inputs, invert the relative permutation, and relabel the output. Thus their code uses pairs p\leq q with diagonal coefficient m_pn_p and off-diagonal coefficient m_pn_q+m_qn_p. Mode 1 uses all ordered pairs.

6.3 Regular and Poisson upper recursions

For the regular tree with four children at each vertex at a=1/2, start at m^{(0)}=\mathsf P and set

The two copies of h^{(t)} are independent conditional on the root; each dominates the product of two edge-transformed upper child experiments. The refinement and composition arguments give, by induction, domination of the exact four-branch depth-t experiment.

For a Poisson tree of chosen mean d_+ and rational magnitude a_+, fix an upper child law m. Its count-specific upper laws are

Each Q_n dominates the exact n-branch experiment, with the child law m held fixed throughout this count recursion. Write q_n(h) for its integer units. If p_n=e^{-d_+}d_+^n/n! and w_n are integer lower weights satisfying 0\leq w_n/N\leq p_n, form

and complete the mass to N at the pure orbit.

To justify the count and tail operations, first draw the count with its exact probabilities p_n, then the upper experiment Q_n conditional on that count and the common input spin. For omitted counts one may take Q_n=\mathsf P, which dominates every experiment: given a revealed spin, simulate the required conditional data. With count included as data the resulting mixture dominates the exact Poisson experiment. For each count n, the upper law is a calibrated posterior experiment: if \rho_n is its labeled marginal law, then its conditional law under input i is 3p_i\rho_n(dp), as in (6.1). The product tilt, barycentric refinement, and pure completion all preserve this identity, including the chosen pure law at omitted counts. Since the count has input-independent probabilities p_n, its joint law with the input and posterior is \PP(S=i,n,p\in dp)=p_n p_i\rho_n(dp). Consequently the posterior given (n,p) is p. Posterior sufficiency therefore allows count to be forgotten while preserving equivalence. Its orbit masses are W_h=\sum_n p_nq_n(h)/N, interpreting q_n as the chosen pure law on omitted counts. Equation (6.9) satisfies \ell_h/N\leq W_h for every orbit. Lemma 6.2 applies to this one exact mixture, including the tail and all rounding losses. Thus iterating this completed Poisson operation from \mathsf P gives upper laws at every depth.

Here the weights are constructed entirely with integers. Put S_0=10^{15} and d_+=d_{\max}/200\leq881/200. Beginning with l_0=u_0=S_0, compute for 1\leq n\leq41

These enclose S_0d_+^n/n!. The degree-41 Taylor polynomial of e^{-d_+} is a lower bound, since its degree-42 Lagrange remainder is positive. Hence, with

we have w_0/N\leq e^{-d_+}. Positivity of L, and all arithmetic bounds, are proved in Appendix C. Continue with w_n=\lfloor w_{n-1}d_{\max}/(200n)\rfloor until the first zero. Induction gives w_n/N\leq p_n. For n\geq9 one has d_+/n<1/2, so the positive integer weights eventually vanish.

6.4 Closed parameter coverage and certificate outputs

For j=0,\ldots,26 set

Choose a_+=A/10^6, where A is the least positive integer such that

The integer binary search in the verifier finds this A without square roots. Its upper endpoint 500000 is valid since d_{\min}\geq800, so a_+\leq1/2 is admissible. Minimality also gives (A-1)^2d_{\min}<200\cdot10^{12}. For every equality point d\in I_j, a=d^{-1/2}, we have d\leq d_+ and a\leq a_+.

By Proposition 2.8, these coordinatewise bounds imply that, at every finite depth, the equality experiment with parameters (d,-a) is degraded from the single corner experiment (d_+,-a_+). The two kernels use thinning probability d/d_+ and channel factor c=a/a_+\in[0,1], respectively. They require only the observed tree, its boundary spins, and independent randomness, and remain valid at the closed bin endpoints, including a_+=1/2.

The intervals (6.11) share endpoints and have union [4,881/200]. There is overlap with the analytic Poisson range in Proposition 5.1, because

Consequently these rectangles cover every Poisson equality not already covered there. No continuity assertion about the rounded recursion, or sampling of intermediate parameters, is involved. Figure 1 illustrates the domination in the first bin.

For each grid representative,

Define the integer

The certificate stops exactly when 20M(m)<NH^2, equivalently \mu(m)<1/20. The exact code is included in Section D.3. With assertions enabled it returns iteration 162 for argument -1, the regular coloring recursion with four children at each vertex. For arguments j=0,\ldots,26, the Poisson recursions return, in order,

All comparisons determining these integers use exact integer arithmetic. Appendix C gives the bounds preventing overflow and the correspondence between each code operation and the constructions proved above.

7 Completion and the stochastic block model

Table 1 collects the arguments for the equality cases. In the table, a=|\lambda| denotes the negative channel magnitude.

We return to the stochastic block model of Section 1.4, where a,b>0 are the within- and between-community connectivity parameters and d=(a+2b)/3>1. The remaining step is to apply the external tree-to-graph and algorithmic results to the tree theorem.

The corollary covers both a>b and a<b. Its positive-parameter hypothesis is part of the statement: the boundary cases a=0 or b=0 are not included. In particular, the negative equality has d>4 here; the coloring equality a=0, b=6, d=4 is excluded.

A The radial inequality

This appendix proves the pointwise inequality used for positive channel parameters. Its algebraic certificates are given explicitly, so the proof requires no numerical or computer-assisted verification.

B Correctness of the interval certificate

This appendix explains the integer interval certificate for the strict positivity of the polynomial (5.8). The coefficients are those in (5.9), with the matching parameter choices in (5.10). The certified domain consists of every probability vector on three states, every \xi\in[3/100,1], and each of the three closed a intervals

The third interval uses the Poisson values H=1/12, U=1/2; the first two use H=1/16, U=15/32. The source is supplied unchanged as verification/interval.cpp; see also Section D.2. Assertions and signed 128-bit integer arithmetic are part of the certificate. We first explain what its arithmetic computes and then why normal completion proves the claimed inequality over the entire domain.

B.1 Coordinates, formulas, and boundary extensions

The quantities being checked are invariant under permutation of the three coordinates. After sorting a probability vector in decreasing order, it has the representation

Indeed, the largest probability is positive; take the eighteenth roots of the other two probabilities divided by it. The formulas below are valid on the larger square 0\le q,r\le1, which will allow rectangular intervals that cross the diagonal r=q.

Set m_i=3p_i and v_i=m_i-1. Then

In particular, -1\le v_i\le2 everywhere on the square. For positive q,r, write L_q=\log q and L_r=\log r. The centered logarithms u_i=\log m_i-\frac13\sum_j\log m_j are

Consequently the functions used in the weighted argument are exactly

These expressions explain the constants 216 and 648 in coeff. The entries returned by qt are enclosures of q^{18} and q^6(\log q)^j, 0\le j\le3, together with their derivatives; the analogous entries are used for r.

For the edge functions put

Define

For a>0, b_i=\log(e_i)/a, so the centered edge logarithms are aw_i. Since \sum_i v_i=0,

Factoring 1-G_e^3 gives the formulas used in the code:

Here \widehat T=T_e/a^2, \widehat W=W_e/a^2, and \widehat Y=Y_e/a^2 when a>0. The last identity uses \frac13\sum_iw_i^3=w_1w_2w_3 for three centered coordinates. Thus the code variables Te, We, and Ye are the hatted quantities. At a=0, the formulas give continuously

There is no division by a in the implemented expressions. Substituting (B.2) and (B.3) into the four entries returned by coeff gives, term by term, (D_0,D_1,D_2,D_3) in (5.9). In the parameter structure, del, ch, and cu mean \delta,H,U, and the code forms s_0=c_0+1/3.

All boundary probability vectors are included. Each function q^6(\log q)^j, 0\le j\le3, is assigned value zero at q=0. Its derivative for q>0 is

where the second term is omitted when j=0. Both the function and its derivative tend to zero at zero. Thus the expressions have continuous first derivatives up to the boundary; when qr=0 they give T=1 and W=Y=0. Since Z\ge1 and e_i>0 throughout the domain, all four D_i have the same regularity, including at a=0.

B.2 Integer intervals and machine safety

Let S=2^{40}. An object I with integer endpoints (l,h) represents [l/S,h/S]. The functions unit and integer represent a grid point and a small integer, respectively. With positive denominator, rat(b,c) represents

The helpers mf(b,c) and floor_div(b,c) compute the mathematical floors of bc/S and b/c, also for negative numerators: the negative branch uses the negative of the corresponding positive ceiling. Upper endpoints are obtained by negating a floor of a negated expression. Addition and subtraction are exact on the grid. Multiplication chooses the appropriate endpoint extrema in each sign case; when both intervals cross zero it takes the minimum of the two potentially negative products and the maximum of the two potentially positive products. The square operation assigns lower endpoint zero when its input crosses zero.

For a positive interval [l/S,h/S], the reciprocal is enclosed by

Negative reciprocals use odd symmetry. An assertion excludes intervals containing zero. Consequently all elementary interval operations contain their exact real counterparts. Intersecting a value interval with a separately established range is also sound. The two uses of this operation, clip, are the range [-1,2] for v_i and the logarithmic-product bounds proved below.

These statements concern exact integer operations, so absence of overflow must be established before using their outputs. Every potentially growing endpoint calculation is passed through safe, which asserts

before converting the signed 128-bit integer b to a signed 64-bit endpoint. Inductively, two input endpoints have product of magnitude less than 2^{124}. The product is formed after promoting to signed 128 bits, and the rounding offset S-1 still leaves its magnitude below 2^{127}. Endpoint addition is also promoted before checking. Reciprocal numerators are S^2=2^{80}; adding the denominator minus one for upward rounding is safe. Rational-construction numerators and denominators in the prescribed runs are small fixed integers. No unchecked negation or absolute value can encounter the minimum signed 64-bit integer, because endpoints have magnitude below 2^{62}.

The remaining raw integer expressions have separate small bounds. All box coordinates lie in [0,S] in grid units, so midpoint sums are at most 2S. Cube-root search candidates are below 2S, their endpoint sums are at most 4S, and the two cube-comparison operands are below 8S^3=2^{123}. The fixed multiples of S, loop indices, and initial-grid numerators fit signed 64 bits. The unchecked visit counter is treated separately by the concrete sanitized executions recorded below; the depth bound alone does not keep its total number of increments within the signed 64-bit range. Logarithm scaling uses at most forty doublings on the actual arguments. Thus a range assertion is never being asked to detect an overflow that has already occurred: oversized derivative or value enclosures stop at safe before narrowing. All floating-point casts in this source occur in failure diagnostics, not in acceptance tests.

B.3 Logarithms, divided logarithms, and cube roots

The function atanh2 evaluates the fifteen terms

by Horner’s rule with outward interval operations. For |w|\le u<1 the absolute remainder is at most

The code asserts |w|\le1/3+4/S<3/8. With u=3/8, the remainder bound, in grid units, is the exact rational number

The padding [-2/S,2/S] therefore covers the omitted tail; all polynomial-evaluation errors are already covered by interval rounding.

To enclose \log(x/S) for a positive integer endpoint x, ln scales an interval containing x/S by powers of two. If m is the resulting interval and k the accumulated exponent, then x/S\in2^km. Multiplication by two is exact on this grid; halving, when used, rounds outwards. The identities

give the enclosure after adding k\log2. The domain assertion in atanh2 checks the needed range even after rounding. All positive arguments actually passed to ln are either coordinate endpoints in [1/S,1], or endpoints of 1-av_i bounded away from zero, so the scaling loops terminate within the stated bounds.

The divided logarithm has the integral and power-series representations

For |t|\le1/4, L_endpoint evaluates \sum_{n=0}^{22}t^n/(n+1) and its derivative \sum_{n=1}^{22}nt^{n-1}/(n+1) independently. Bounding both coefficient sequences by one bounds their absolute tails by

respectively. Each receives padding [-1/S,1/S]. Outside this small interval the exact identities

use only nonzero denominators. On the entire real domain t<1, differentiation of the integral representation gives

Thus both \mathcal L and \mathcal L' increase, including at negative arguments. The lower enclosure at the left endpoint and upper enclosure at the right endpoint suffice to enclose each function on an interval. This is precisely the rule used by L.

For a nonnegative integer x<8S, cb_floor uses binary search and the exact comparison

to return \lfloor S(x/S)^{1/3}\rfloor. Its initial search bracket [0,2S] is valid by x<8S. Applying this function to the two input endpoints, then increasing the upper result by one grid unit, encloses the cube root. The derivative enclosure is obtained from 1/(3t^{2/3}) using the already enclosed positive root.

The outward rounding of an a endpoint enlarges the prescribed bands by less than 1/S, and never introduces negative a. Hence throughout the actual boxes a\le477/1000+1/S. Even the interval enclosures of 1-av_i, after multiplication rounding and clipping v_i to [-1,2], have lower endpoint greater than 45/1000 and upper endpoint less than 1478/1000. The successive product of the three factors has lower endpoint at least (45/1000)^3-3/S>0 and upper endpoint at most (1478/1000)^3+3/S<8. These bounds justify the logarithm, divided-logarithm, reciprocal, and cube-root domains on every initial box and descendant. The cube-root lower enclosure is positive as well, so its derivative reciprocal is valid.

B.4 Logarithmic products and derivative propagation

The zero endpoints in (B.1) are treated without evaluating their logarithms. For 0<q\le1, set t=-\log q\ge0. For integers 0\le j\le3 and real h\ge5,

For j=0 this is immediate. For j>0 its maximum is (2j/(he))^j\le1, since 2j/h\le6/5<e. It follows that

For even j the products are nonnegative, and for odd j they are nonpositive. These are the exact external ranges used by qt_direct to intersect the power-and-logarithm enclosures. When the lower endpoint is zero, the same ranges directly supply an enclosure, with no logarithm call. When the lower endpoint is positive, monotonicity of \log supplies its interval, and intersecting its upper bound with 0 is valid because q\le1. The derivative returned for every logarithmic product is exactly the interval version of (B.4). The derivative of q^{18} is 18q^{17}. Cached enclosures depend only on the interval endpoints; qt puts their derivatives in the appropriate q or r gradient coordinate.

An object J consists of a value interval and three derivative intervals, corresponding to (q,r,a). Constants have zero gradients and variables have the appropriate unit gradient. Addition, multiplication, squares, and reciprocals apply the identities

Cube roots and \mathcal L use the derivative enclosures just proved and the chain rule. Induction over these operations proves that the value and every first partial derivative of the actual formula are enclosed throughout the box. Tightening a value enclosure by an external range does not replace the underlying function by a clipped function: its previously enclosed derivatives remain valid, and the tighter values can be used in subsequent product and chain rules. All these statements extend to zero coordinate endpoints by the continuous derivative extensions already established.

B.5 Bernstein coefficients and the acceptance test

For fixed (q,r,a) write the polynomial as P(\xi)=D_0+D_1\xi+D_2\xi^2+D_3\xi^3. On a subinterval [l,h], substitute \xi=l+(h-l)t, 0\le t\le1, and express P in the basis \binom3j t^j(1-t)^{3-j}. The multipliers of D_1,D_2,D_3 in the four coefficients are

and the multiplier of D_0 is always one. Expanding the four basis polynomials verifies these identities. All basis polynomials are nonnegative and their sum is one; strictly positive coefficients therefore imply P(\xi)>0 on the whole closed subinterval.

The function rows uses successive intervals with endpoints

These twelve intervals cover [3/100,1] without gaps. For each it stores the first three rows of (B.9); the fourth row equals the first row for the next interval. It finally adds (1,1,1). Thus the 37 stored rows account for all 48 coefficients of the twelve cubic representations, including both extreme endpoints. The row multipliers are themselves evaluated by rational interval arithmetic and have zero gradients with respect to (q,r,a).

Let F denote one of these Bernstein coefficients on a box B=\prod_{i=1}^3[l_i/S,h_i/S]. The interval calculation in dot encloses F and all its first derivatives. A positive lower endpoint immediately accepts this coefficient. Otherwise define the grid midpoint and coordinate radii by

Nonnegative endpoints ensure that C++ integer division computes this floor; \rho_i is the larger of the two distances to the endpoints. If M_i is the maximum absolute endpoint of the derivative enclosure, in real units, then for every z\in B the segment from c to z lies in B and

This follows by integrating the gradient along that segment, also when a coordinate endpoint is zero. The code encloses F(c) anew, rounds each product M_i\rho_i upwards, and adds their integer upper endpoints with overflow checks. Its strict comparison value.v.l > total is therefore sufficient for F>0 throughout B. A box is accepted only when every stored row passes one of these two tests.

B.6 Subdivision, coverage, and observed completion

For a band [a_-,a_+], the initial exact boxes before outward rounding are

where 0\le i<24, 0\le j\le i, and 0\le k<16. Every (q,r) with 0\le r\le q\le1 belongs to one of the displayed q,r rectangles, including all grid boundaries. There are 16\sum_{i=0}^{23}(i+1)=4800 initial boxes per run. Their endpoints are rounded outwards, so none of the required domain is lost. The extra points included by rounding are harmless, as are portions of diagonal rectangles with r>q: the same functions and derivative bounds are valid there. The a enlargement and all analytic domains were checked above. Adjacent bands may use different parameters, since each certifies its own entire closed band.

On entry, visit skips a box only if its lower r endpoint exceeds its upper q endpoint. Such a box contains no point with r\le q. If any coefficient fails both acceptance tests, the code chooses a coordinate with maximal recorded derivative-radius contribution and cuts at its grid midpoint. The choice affects efficiency only. The two closed children include the midpoint and their union is the parent. If the chosen contribution is zero, the depth exceeds 80, or the chosen grid radius is at most one, an assertion fails rather than accepting an unresolved box.

Induction back up any normally completed recursion tree now proves that every required point in its root box has all Bernstein coefficients strictly positive. The leaves either pass the sound acceptance tests or contain no required point. Together with (B.12), (B.10), and the sorted parametrization, normal completion of all three runs proves the pointwise inequality on the full stated domain. This includes the uniform message, boundary probability vectors, a=0, all band endpoints, and all \xi endpoints. In particular there is no exception at the uniform message: there P(\xi)=\delta\xi^2+ U\delta\xi^3>0.

The unchanged source was replayed with GCC 13.3.0 on x86_64 Linux, using assertions enabled. From the package root the reproduction commands are

g++ -std=c++17 -O3 -UNDEBUG verification/interval.cpp \
  -o /tmp/appendix_b
/tmp/appendix_b 0
/tmp/appendix_b 1
/tmp/appendix_b 2

Only the documented arguments 0,1,2 are part of this protocol; the source does not validate other argument values. Compiling with assertions disabled is not this certificate. All three runs exited normally with status zero and the following visit counts:

The counts include internal subdivision nodes and boxes skipped by the diagonal test. All three executions were also repeated on the unchanged source with -O2 -UNDEBUG -fsanitize=undefined and -fno-sanitize-recover=undefined. They completed with the same counts and no sanitizer diagnostics. This supplies the separate check of the unchecked visits++ counter for these prescribed executions. The counts identify the finite completed executions; their correctness implication is the enclosure and coverage argument above, not a sample-based inference. The source SHA-256 is

76d1443b1194597ee77749e8030c825f2b9aae46b5c172d9eccf0745078c28e3

C Exact arithmetic and reproduction of the grid certificate

The complete C++17 program in Section D.3 implements the recursions of Section 6. Its parameters are fixed at H=72, N=10^{12}, and \mathtt{SCALE}=10^{15}. It uses signed 64-bit integers for table coefficients and mass units, and signed 128-bit integers for products and accumulators. The compiler must also provide a plain int type of at least 32 bits. Assertions must be enabled; in particular the build must not define NDEBUG. For example, from the paper directory, the following commands compile and run all 28 cases:

g++ -std=c++17 -O3 -UNDEBUG -Wall -Wextra \
    verification/grid.cpp -o grid
for j in $(seq -1 26); do ./grid "$j"; done

The program writes progress diagnostics to standard error and the case number followed by its stopping iteration to standard output. Only the diagnostics convert to floating point. Successful outputs are specified in (6.15), together with -1 162.

C.1 Correspondence of code and probability operations

The routine init enumerates all sorted nonnegative integer triples of sum 72. It finds 469 triples, identifies the pure representative (72,0,0) and the uniform representative (24,24,24), and stores an index for every representative. The routine indexof sorts a candidate triple and verifies the resulting index. A Law is a vector of orbit masses in units of 1/N. The routine complete adds the missing units at the pure orbit, which is exactly Lemma 6.2.

The constructor Table(mode,A,AD) first reduces the channel fraction. The variables lhs, rhs, raw, T, and den are the entries and denominator of (6.4). For each of the six relative permutations, n, rem, and miss are the floor vector, remainders, and deficit in the grid spread. The corner weights are T, rem[c], or T-rem[c], as appropriate. After aggregating equal output indices, the constructor checks that their sum is den. These checks include every grid pair, not only pairs visited by an iteration. Zero normalizers are omitted because they have zero tilted mass.

The routine combine implements (6.6). Symmetric modes use the triangular pair table and the stated off-diagonal coefficient; mode 1 uses ordered pairs. Its row-skipping condition is safe: an ordered row contributes zero when its first mass is zero, while a triangular row contributes zero when both first-index masses are zero. The table position advances by the full skipped row length. After division by N\,\mathtt{den}, each mass is rounded down and complete is applied.

The functions down and up compute floor and ceiling of a nonnegative integer ratio. The latter uses \lceil x/y\rceil=\lfloor(x+y-1)/y\rfloor for x\geq0, y>0. The function w_zero implements (6.10). The routine poisson fixes its incoming child law inc, starts part at the uniform zero-count law, and uses mode 1 once for each positive count weight. Its orbit sums are exactly (6.9); the final complete handles all omitted mass. No count product is needed after the first zero weight. The regular branch of run is (6.7). Finally, mu_num is M in (6.14), and the strict stopping test is 20M<NH^2. Each run allows 400 iterations and asserts failure if none succeeds. All reported stopping iterations are below that bound.

C.2 Bounds on every arithmetic class

For all Poisson table calls, the reduced fraction satisfies B\leq10^6 and A\leq B/2. Thus

Each total T is at most three times the bound on a raw coordinate; all of these quantities fit signed 64 bits. The only mode 2 call is at the reduced fraction A/B=1/2, where D_{\mathrm{tab}}=373248 and Hr_i\leq3359232. Mode 0 has smaller bounds. Every nonnegative aggregated table weight and every partial sum of weights is bounded by its denominator, by (6.5).

Input masses are nonnegative and sum to N, so their ordered pair mass is N^2. The triangular implementation has the same total after the off-diagonal terms are combined. Consequently every nonnegative product accumulator and its partial sums are at most

The source casts an input factor to the 128-bit type Big before multiplying. Dividing by ND_{\mathrm{tab}} yields a mass between zero and N, safely convertible back to 64 bits. The uncompleted masses sum to at most N; likewise the Poisson mixture masses sum to at most N, since they are lower bounds on a probability mixture. These facts bound all 64-bit partial sums in complete and poisson.

Here are bounds for the Taylor calculation independent of machine floating point. If t_n=S_0d_+^n/n!, the lower and upper endpoint errors satisfy

Indeed an error satisfies \epsilon_n\leq(d_+/n)\epsilon_{n-1}+1; expanding this recurrence bounds it by \sum_{j\geq0}d_+^j/j!=e^{d_+}, since each product of j successive denominators is at least j!. As d_+<5 and e<3, the endpoint errors are less than 243. The sum of all endpoint magnitudes through degree 41 is therefore bounded by

This also bounds every signed partial sum in (6.10). The endpoint multiplication by d_{\max}\leq881 is carried out in 128 bits before division, and the same holds for multiplication by N and for the Poisson weight recurrence. These products are all less than 2^{127}-1 under the displayed bounds.

The lower sum L is positive. In fact Taylor’s theorem gives

The middle inequality uses the elementary integer comparison 5^{42}/42!<10^{-20}. Thus the nonnegative-argument conditions of down hold at the final Taylor step as well as in its term recurrences. Since w_n/N\leq p_n, every Poisson weight is at most N. In particular w_8\leq N<2^{40}, and the recurrence gives w_n\leq w_{n-1}/2 for n\geq9, since d_+/n<1/2. Thus w_{48}<1, so the first zero occurs by n=48. The count loop and its denominator therefore satisfy n\leq48 and 200n\leq9600, well within the plain integer type. Every product w_nq_n(h) is at most N^2 and is evaluated in 128 bits.

For h\in\mathcal H, the bracket in (6.14) belongs to [0,H^2]. Hence every partial sum in mu_num is at most

The factor 20 in the stopping comparison is applied after converting to Big. The binary-search comparisons for (6.12) likewise use 128 bits before taking integer squares and products.

There are at most 18 unaggregated contributions per grid pair (six permutations, at most three corners). Thus even a full ordered table has at most 18\cdot469^2=3959298 entries before aggregation. All table positions and vector indices fit an ordinary signed 32-bit integer, and the source also checks an explicit 100000000 entry limit. Candidate grid coordinates belong to \{0,\ldots,H\}, and all small grid sums and products fit these integer types. This accounts for the unguarded indexing arithmetic as well as the probabilistic accumulators.

The supplied source therefore implements a finite exact-arithmetic certificate: positivity, normalization, rounding direction, all parameter choices, and the final strict inequalities are independent of compiler floating-point behavior.

D Exact verification programs

The three programs below are part of the proof. They use integer or rational arithmetic for every certification decision. In the C++ programs, floating-point conversion is used only for diagnostic output. The mathematical meaning and arithmetic guarantees of the programs are proved in Sections 4–5, Section 6, and Appendices B and C, and in the pair derivation below.

Reproduction protocol

The accompanying directory verification/ contains pair.py, interval.cpp, and grid.cpp, exactly the sources printed below. Run Python with SymPy installed and with assertions enabled. Compile the C++ sources with a compiler supporting signed __int128 and a plain int type of at least 32 bits, also with assertions enabled. For example, from the paper directory:

python verification/pair.py
g++ -std=c++17 -O3 -UNDEBUG verification/interval.cpp -o interval
g++ -std=c++17 -O3 -UNDEBUG verification/grid.cpp -o grid
for j in 0 1 2; do ./interval "$j"; done
for j in -1 $(seq 0 26); do ./grid "$j"; done

Do not use Python’s -O option, and do not define NDEBUG. Only the displayed argument ranges are part of the protocol. The bundled runner verification/reproduce.py verifies the source hashes, runs this suite, checks the expected outputs, and saves the commands, software versions, exit statuses, and logs in its designated output directory. Its usage is documented in the accompanying README.

Successful execution of the pair program produces no output. The interval runs finish with visited-box counts 414080, 756096, and 1004426, respectively. The grid run with argument -1 stops at iteration 162. The other grid stopping iterations are recorded in Section 6. The certificate sources were replayed with Python 3.12.13, SymPy 1.14.0, and GCC 13.3.0 on x86_64 Linux; all 32 mathematical executions and five environment/compiler checks passed. Separately, the three interval cases were replayed with -O2 -UNDEBUG, -fsanitize=undefined, and -fno-sanitize-recover=undefined. All three exited successfully, with the same progress logs and no sanitizer diagnostics. This supplemental check is distinct from the ordinary runner protocol and supplies the execution check on the visit counter discussed in Appendix B.

The SHA-256 digests of the three source files, in the above order, are

These digests identify the exact files; the correctness arguments are provided in the text, and the successful runs establish the finite assertions required there.

D.1 Pair coefficient certificate

We prove the a=1/2 case of Lemma 4.2 for strictly positive input vectors, using its notation for the input invariants and pair excesses. The main-text proof then extends these bounds to every 0\le a\le1/2 and to the closed simplex. Parametrize sorted unnormalized vectors by

This covers every strictly positive sorted vector up to scale: for h_0\ge h_1\ge h_2>0, take s=(h_0-h_1)/(3h_2) and t=2(h_1-h_2)/(3h_2) to obtain p=2h/h_2. Put P=\sum_i p_i, Q=\sum_i q_i, and e_i=Q-q_i, with E=\sum_i e_i=2Q. Then e_i/E=(1-q_i/Q)/2, as required for the coloring edge. For an unnormalized vector r of total R, put

The identities for the posterior invariants give N_x(r)=R^2x(r/R) and N_y(r)=R^3y(r/R). These are the two numerators returned by xy in the source.

For each of the two choices \widetilde e=(e_0,e_1,e_2) and \widetilde e=(e_0,e_2,e_1), let

with indices modulo three. The likelihood normalizer is 3T_j/(PE); multiplying by the cyclic probability 1/3 gives weight T_j/(PE). Since \sum_jT_j=PE, these are probability weights. The two choices, each followed by the three rotations, enumerate all six relative permutations. Repeated representatives at a stabilizer remain valid uniform group averages.

For each reflection class separately, clear the positive denominator

The three expressions out[0], out[1], and out[2] divided by D are exactly

namely the tilted output means of x,y,x^2 within that class. For every call in the source,

The powers 4-2i-3j and 4-2k-3l in these calls are nonnegative, so the cleared objects are polynomials. Hence dx, de, and dn are D times the class-specific excesses.

The correction im, after division by D, is

Indeed this follows immediately by dividing 27\operatorname{odd}(p)\operatorname{odd}(\widetilde e) [PE(T_0T_1T_2)^3]PE/64 by (D.1). Swapping the last two edge coordinates negates I. Although D itself depends on the reflection class, the normalized correction in (D.2) has exactly the indicated sign change.

To see explicitly what is certified, temporarily write d_x,d_e,d_n for the excesses within one reflection class. The seven polynomials checked in that class are the following expressions multiplied by D:

The last line, divided by two, bounds Cd_n-2d_e+23I. All arithmetic in this certificate consists of integer polynomial addition and convolution, and exact scalar division, in \mathbb Z[s,t,u,v]. Each of the fourteen polynomials has total degree 28 and all its coefficients are nonnegative. For either reflection the numbers of nonzero coefficients in the displayed order are

The supplied executable certificate checks every coefficient by the assertion min(f.coeffs())>=0; absent monomials have coefficient zero. Its unchanged-source execution, with Python assertions enabled, terminates successfully. Thus these are exact polynomial nonnegativity statements on the entire nonnegative quadrant, rather than evaluations on a set of test points.

Divide each class’s seven inequalities by its own positive D and then average the two normalized classes. All right-hand invariant terms are unchanged by reflection, and the I terms cancel by (D.2). This gives precisely (4.1)–(4.4) for a=1/2.

The complete polynomial calculation is the following source.

D.2 Interval positivity certificate

D.3 Finite experiment certificate