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 \[ K_\lambda(i,j)= \begin{cases} (1+2\lambda)/3,&i=j,\\ (1-\lambda)/3,&i\ne j, \end{cases} \qquad -\tfrac12\le\lambda\le1. \tag{1}\] 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 \[ a_\ell=\mathbb E\left\| \mathbb P(\sigma_\rho=\cdot\mid T_{\le\ell},\sigma_{\partial T_\ell}) -\operatorname{Unif}\{1,2,3\}\right\|_{\mathrm{TV}}. \tag{2}\] 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.

History and significance

The branching-process work of Kesten and Stigum (Kesten and Stigum 1966) underlies the classical second-moment reconstruction bound. Broadcasting and its relation to the Ising model were developed by Evans, Kenyon, Peres, and Schulman (Evans et al. 2000). 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 (Sly 2011, Theorem 1.2); the three-state assertion therefore needs more than the second-moment bound.

Mézard and Montanari (Mézard and Montanari 2006, 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 (Sly 2011) for the all-degree regular-tree formulation. Sly proved this for all sufficiently large regular branching parameters, including non-reconstruction at equality (Sly 2011, Theorem 1.1). Mossel, Sly, and Sohn established the corresponding large-mean Poisson-tree result, for both signs and including equality (Mossel et al. 2025, 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 (Bhatnagar and Maneva 2011, Theorem 12). Theorem 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 (Decelle et al. 2011, sec. 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 (Ricci-Tersenghi et al. 2019, sec. 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 (Mossel et al. 2025, Theorem 1.5). Their tree-to-graph transfer has no large-degree restriction (Mossel et al. 2025, Theorem 2.1). Together with the above-threshold algorithm of Abbe and Sandon (Abbe and Sandon 2018, Corollary 1 and Lemma 1), the Poisson part of our theorem therefore gives the exact three-community weak-recovery threshold stated in Corollary 2 below.

A related three-state model with branch-dependent couplings on a binary Cayley tree is studied by Mukhamedov and Akın (Mukhamedov and Akın 2026). 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.

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 \[\zeta=p_1+\omega p_2+\omega^2p_3,\qquad x=|\zeta|^2,\qquad y=\Re(\zeta^3).\] 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 \(\mathbb Ex=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 (Formentin and Külske 2009, 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 \(\mathbb Ex^2\). Moment estimates make these two bounds incompatible at a nonuniform limiting fixed point. Appendix 8 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 (Gu and Polyanskiy 2023).

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 (Sly 2011, sec. 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 \(\mathbb Ex>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 \(\mathbb Ex<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 (Bhatnagar and Maneva 2011, secs. 3.1–3.3 and Theorem 12). Their construction includes completion by perfectly informative messages for omitted offspring tails and downward-rounded masses (Bhatnagar and Maneva 2011, sec. 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 (Gu 2026, sec. 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 11. 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.

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 \[\operatorname{ov}(\sigma,\widehat\sigma) =\max_{\pi\in S_3}\frac1n\sum_{v=1}^n \mathbf1_{\{\widehat\sigma_v=\pi(\sigma_v)\}}.\] The permutation accounts for the fact that the names of the communities cannot be recovered from the graph.

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

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 \[O_\ell=(T_{\leq\ell},(S_v)_{|v|=\ell})\] 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 \[ p_i=\mathbb P(S=i\mid Y),\qquad m_i=3p_i,\qquad v_i=m_i-1, \qquad i\in\mathcal S. \tag{4}\] Thus the likelihood vector \(m\) takes values in the compact simplex \[\mathcal M=\{(m_i)_{i\in\mathcal S}:m_i\geq0,\ \textstyle\sum_i m_i=3\}.\] 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 \[ \zeta=\mathbb E[S\mid Y]=\langle i m_i\rangle,\qquad x=|\zeta|^2,\qquad y=\operatorname{Re}(\zeta^3). \tag{5}\] Here the \(i\) inside the coordinate average is the spin label, not the imaginary unit. Fourier inversion on the three-element group gives \[ v_i=\zeta\overline{i}+\overline{\zeta}i =2\operatorname{Re}(\zeta\overline{i}),\qquad \langle v^2\rangle=2x,\qquad \langle v^3\rangle=2y. \tag{6}\] More precisely, each of the three coordinates satisfies \[ v_i^3=3xv_i+2y,\qquad \prod_{i\in\mathcal S}(1+t v_i)=1-3t^2x+2t^3y. \tag{7}\] 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 \[ 0\leq x\leq1,\qquad |y|\leq x^{3/2},\qquad 1-3x+2y\geq0. \tag{8}\] For later use these also imply, when \(x>0\), \[ -\frac12\leq r:=\frac yx\leq1,\qquad r^2\leq x\leq\frac1{3-2r}. \tag{9}\] Indeed \(|r|\leq\sqrt{x}\leq1\), and the last inequality in Equation (8) 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: \(\mathbb Em_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, \[ \mathbb E[g(Y)\mid S=i]=\mathbb E[m_i(Y)g(Y)]. \tag{10}\] 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 \(\mathbb P(S=i\mid Y,m)=m_i/3=\mathbb P(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.

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 \[ m_{e,i}=\sum_{k\in\mathcal S}K_\lambda(i,k)m_k =1+\lambda(m_i-1)=1+\lambda v_i. \tag{13}\] Thus the datum retains its original marginal law under the uniform parent prior. The edge operation sends \[ \zeta\longmapsto\lambda\zeta,\qquad x\longmapsto\lambda^2x,\qquad y\longmapsto\lambda^3y. \tag{14}\]

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 \[ W_i=\prod_{j=1}^n m_{i,j},\qquad Z=\langle W\rangle=\frac13\sum_{i\in\mathcal S}W_i,\qquad m_i^{\mathrm{out}}=\frac{W_i}{Z}\quad(Z>0). \tag{15}\] 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 (15). 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 \[ m(Y')=\mathbb E[m(Y)\mid Y'],\qquad \mathbb E\Phi(m(Y'))\leq\mathbb E\Phi(m(Y)) \tag{18}\] 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.

Convergence, fixed points, and extinction

Unless a different experiment is specified, we henceforth use \[ \mu=\mathbb Ex,\qquad \nu=\mathbb Ex^2,\qquad \eta=\mathbb Ey \tag{21}\] for the limiting experiment. Its law is trivial precisely when \(\mu=0\), since \(x=0\) is equivalent to \(m=(1,1,1)\). By Lemma 4 and Proposition 6, non-reconstruction is equivalent to \(\mu=0\).

Reconstruction above the second-moment threshold

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

An entropy identity with an additive correction

For a positive message of coordinate average one, define \[ \begin{aligned} I&=\langle m\log m\rangle,& J&=\frac12\langle v\log m\rangle,\\ u_i&=\log m_i-\langle \log m\rangle,& B&=\frac12\langle m u^2\rangle. \end{aligned} \tag{27}\] 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 (Formentin and Külske 2009, 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 7 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 \[\mathbb E[u_{e,i}\mid S=i]=\mathbb E\langle m_eu_e\rangle=2\mathbb EJ_e, \qquad \mathbb E[u_{e,i}^2\mid S=i]=\mathbb E\langle m_eu_e^2\rangle=2\mathbb EB_e.\] Centered log coordinates add under products: the common normalizing constant disappears on centering. Conditional independence of the branches therefore gives \[ \mathbb EJ=d\mathbb EJ_e,\qquad \mathbb EB=d\mathbb EB_e+2\alpha(\mathbb EJ)^2. \tag{28}\] For clarity, the off-diagonal term in the second formula, before division by two, is \(4\mathbb E[D(D-1)](\mathbb EJ_e)^2\).

For a product of \(n\) edge experiments write \(Z_n\) for its likelihood normalizer relative to their independent marginal laws, and set \[H_n=\mathbb E_{\mathrm{prod}}[Z_n\log Z_n],\qquad H=\mathbb EH_{D}.\] This is a relative entropy and is nonnegative. Expanding the logarithm of the normalized output likelihood gives \[\mathbb EI=d\mathbb EI_e-H.\] Each branch retains its original marginal distribution after the joint likelihood tilt, which justifies the individual terms in this expansion. The combination \[ F=3I-2J+\frac45B \tag{29}\] therefore satisfies the exact identity \[ \mathbb E(F-dF_e)=-3H+\frac85\alpha(\mathbb EJ)^2. \tag{30}\]

The useful feature of this combination is its positive radial defect: for every positive message of coordinate average one, \[ F(m)-\lambda^{-2}F(1+\lambda v) \ge\frac{1-\lambda^2}{2}x^2\qquad(0<\lambda<1). \tag{31}\] Lemma 23 proves this pointwise inequality by radial differentiation and explicit polynomial sign decompositions. Since \(d=\lambda^{-2}\), its expectation and Equation (30) imply \[ \frac{1-\lambda^2}{2}\nu+3H \le\frac85\alpha(\mathbb EJ)^2. \tag{32}\] We will contradict this inequality by bounding \(\mathbb EJ\) above and \(H\) below. The additive identity for \(J\) also restricts the possible values of \(\mu,\nu,\eta\); we establish those restrictions first.

Moment information from the additive identity

The cubic identity in Equation (7), together with \(\langle v\rangle=0\) and \(\langle v^2\rangle=2x\), gives the additional moment relation \[ \langle v^4\rangle=3x\langle v^2\rangle+2y\langle v\rangle=6x^2. \tag{33}\] We also use \(|y|\le x^{3/2}\) from Equation (8).

Correlation generated by successive branches

The strict contradiction

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 \[s_0=c_0+1/3,\qquad c(\xi)=c_0+c_1\xi,\qquad s(\xi)=s_0+s_1\xi.\] 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 \[T=x-\tfrac23y+O(\|v\|^4),\qquad W=2x-2y+O(\|v\|^4),\qquad Y=2y+O(\|v\|^4).\] Its quadratic term also cancels on subtracting \(d\) times its edge evaluation, since \(da^2=1\). By Lemma 17, the random expression \[\begin{align*} E_0={}&T-h\widehat T +c(\xi)[W-(1-\xi)\widehat W] +s(\xi)[Y-(1-\xi)\widehat Y]\\ &+\delta\xi(z-\widehat T) \tag{69}\end{align*}\] has expectation zero. In particular, the final term changes the pointwise expression without changing its expectation, since \(\mathbb E\widehat T=z\).

Fix an applicable pair \((H,U)\) from Lemma 18. Replace \(h\) in (69) 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: \[ P-E_0=(h-\overline h)\widehat T +\delta\xi(\underline z-z)\le0. \tag{70}\] Here \(\widehat T\ge0\), \(\delta>0\), and \(\xi\ge0\). The possibly negative coefficients \(c(\xi)\) and \(s(\xi)\) multiply identities that remain exact. Thus \(\mathbb EP\le0\) for any nontrivial fixed point; it remains to choose the constants so that \(P>0\) pointwise.

Expanding the relaxed expression gives \[ P=D_0+D_1\xi+D_2\xi^2+D_3\xi^3, \tag{71}\] where \[\begin{align*} D_0={}&T-\widehat T+c_0(W-\widehat W)+s_0(Y-\widehat Y),\\ D_1={}&c_1(W-\widehat W)+s_1(Y-\widehat Y) +c_0\widehat W+s_0\widehat Y+(1/2-\delta)\widehat T,\\ D_2={}&c_1\widehat W+s_1\widehat Y+H\widehat T+\delta,\\ D_3={}&U\delta+(H/2)\widehat T. \tag{72}\end{align*}\] We use the following rational choices on three closed \(a\) bands: \[ \begin{array}{c|rrrr|cc} a\text{ band}&1000c_0&1000c_1&1000s_1&1000\delta&H&U\\ \hline \bigl[0,.190\bigr]&-268&-60&-55&130&1/16&15/32\\ \bigl[.190,.448\bigr]&-269&67&47&55&1/16&15/32\\ \bigl[.448,.477\bigr]&-271&58&49&50&1/12&1/2 \end{array} \tag{73}\] 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 \[\widehat T=x,\qquad\widehat W=2x,\qquad\widehat Y=0.\] 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.

Explicit refinements of posterior experiments

The finite representation follows the survey method of Bhatnagar and Maneva (Bhatnagar and Maneva 2011, secs. 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 \[ \mathbb P(S=i,Y\in dy)=p_i(y)\rho(dy),\qquad \mathbb P(Y\in dy\mid S=i)=3p_i(y)\rho(dy). \tag{74}\] 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 (74) 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 \(j\)th upper branch into the \(j\)th 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.

Grid spreading and exact product tables

Fix \[H=72,\qquad N=10^{12},\qquad \mathcal H=\{(h_0,h_1,h_2)\in\mathbb Z_{\geq0}^3: h_0\geq h_1\geq h_2,\ h_0+h_1+h_2=H\}.\] 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 \[n_i=\left\lfloor\frac{Hr_i}{T}\right\rfloor,\qquad b_i=Hr_i-n_iT,\qquad k=H-\sum_i n_i=\frac{\sum_i b_i}{T}\in\{0,1,2\}.\] 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 20 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 \[\frac{e_i(q)}{BH},\qquad e_i(q)=(B+A)H-3Aq_i,\] 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: \[ \begin{array}{c|c|c|c} \text{mode}&\text{operation}&r_i&D_{\mathrm{tab}}\\ \hline 0&\text{plain--plain}&p_i\,3q_{\pi(i)}&6H^2\\ 1&\text{plain--edge}&p_i\,e_{\pi(i)}(q)&6BH^2\\ 2&\text{edge--edge}&e_i(p)e_{\pi(i)}(q)&18B^2H^2 \end{array} \tag{77}\] 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, \[ w_{p,q}(h)\geq0,\qquad \sum_h w_{p,q}(h)=D_{\mathrm{tab}}. \tag{78}\] Indeed the spread has mass one, and averaging either input likelihood over uniform label permutations gives one in each coordinate. The verifier additionally asserts (78) for every entry.

For input integer mass laws \(m,n\), keep output units \[ \ell_h=\left\lfloor \frac{\sum_{p,q}m_pn_qw_{p,q}(h)}{N D_{\mathrm{tab}}} \right\rfloor, \tag{79}\] 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 21 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.

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 \[ h^{(t)}=\mathcal C_2(m^{(t)},m^{(t)}),\qquad m^{(t+1)}=\mathcal C_0(h^{(t)},h^{(t)}). \tag{80}\] 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 \[ Q_0=\mathsf U,\qquad Q_n=\mathcal C_1(Q_{n-1},m). \tag{81}\] 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 \[ \ell_h=\sum_{n\text{ retained}} \left\lfloor\frac{w_nq_n(h)}N\right\rfloor \tag{82}\] 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 (74). 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 \(\mathbb P(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 (82) satisfies \(\ell_h/N\leq W_h\) for every orbit. Lemma 21 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\) \[l_n=\left\lfloor\frac{l_{n-1}d_{\max}}{200n}\right\rfloor, \qquad u_n=\left\lceil\frac{u_{n-1}d_{\max}}{200n}\right\rceil.\] 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 \[ L=S_0+\sum_{\substack{1\leq n\leq41\\n\text{ even}}}l_n -\sum_{\substack{1\leq n\leq41\\n\text{ odd}}}u_n, \qquad w_0=\left\lfloor\frac{NL}{S_0}\right\rfloor, \tag{83}\] we have \(w_0/N\leq e^{-d_+}\). Positivity of \(L\), and all arithmetic bounds, are proved in Appendix 10. 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.

Closed parameter coverage and certificate outputs

For \(j=0,\ldots,26\) set \[ d_{\min}=800+3j,\quad d_{\max}=803+3j,\quad I_j=[d_{\min}/200,d_{\max}/200],\quad d_+=d_{\max}/200. \tag{84}\] Choose \(a_+=A/10^6\), where \(A\) is the least positive integer such that \[ A^2d_{\min}\geq200\cdot10^{12}. \tag{85}\] 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 10, 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 (84) share endpoints and have union \([4,881/200]\). There is overlap with the analytic Poisson range in Proposition [wei:exclusion], because \[ \frac{881}{200}-\frac1{(477/1000)^2} =\frac{453049}{45505800}>0. \tag{86}\] 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, \[\left|\sum_i\frac{h_i}{H}\omega^i\right|^2 =1-\frac{3(h_0h_1+h_1h_2+h_2h_0)}{H^2}.\] Define the integer \[ M(m)=\sum_hm_h\bigl[H^2-3(h_0h_1+h_1h_2+h_2h_0)\bigr]. \tag{87}\] The certificate stops exactly when \(20M(m)<NH^2\), equivalently \(\mu(m)<1/20\). The exact code is included in Section 11.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, \[ \begin{gathered} 104,103,103,103,102,102,102,102,102,\\ 101,101,101,101,101,101,\\ 100,100,100,100,100,100,100,\\ 99,99,99,99,99. \end{gathered} \tag{88}\] All comparisons determining these integers use exact integer arithmetic. Appendix 10 gives the bounds preventing overflow and the correspondence between each code operation and the constructions proved above.

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 \[ p=\frac{(1,q^{18},r^{18})}{Z},\qquad Z=1+q^{18}+r^{18},\qquad 0\le r\le q\le1. \tag{110}\] 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 \[v=\left(\frac3Z-1,\frac{3q^{18}}Z-1, \frac{3r^{18}}Z-1\right),\qquad x=\frac16\sum_{i=1}^3v_i^2,\qquad y=\frac12v_1v_2v_3.\] 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 \[(-6(L_q+L_r),\ 12L_q-6L_r,\ 12L_r-6L_q).\] Consequently the functions used in the weighted argument are exactly \[\begin{align*} G&=\frac{3q^6r^6}{Z},& T&=1-G,\\ W&=\frac{216}{Z}q^6r^6(L_q^2+L_r^2-L_qL_r),\\ Y&=\frac{648}{Z}q^6r^6 (2L_q^3+2L_r^3-3L_q^2L_r-3L_qL_r^2). \tag{111}\end{align*}\] 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 \[e_i=1-av_i,\qquad G_e=(e_1e_2e_3)^{1/3},\qquad \mathcal L(t)=\begin{cases}-\log(1-t)/t,&t\ne0,\\1,&t=0. \end{cases}\] Define \[b_i=-v_i\mathcal L(av_i),\qquad w_i=b_i-\frac13\sum_jb_j.\] For \(a>0\), \(b_i=\log(e_i)/a\), so the centered edge logarithms are \(aw_i\). Since \(\sum_i v_i=0\), \[G_e^3=1-3a^2x-2a^3y.\] Factoring \(1-G_e^3\) gives the formulas used in the code: \[ \widehat T=\frac{3x+2ay}{1+G_e+G_e^2},\qquad \widehat W=\frac{G_e}{3}\sum_iw_i^2,\qquad \widehat Y=aG_ew_1w_2w_3. \tag{112}\] 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 \[G_e=1,\qquad \widehat T=x,\qquad \widehat W=2x,\qquad \widehat Y=0.\] There is no division by \(a\) in the implemented expressions. Substituting (111) and (112) into the four entries returned by coeff gives, term by term, \((D_0,D_1,D_2,D_3)\) in (72). 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 \[ 6q^5(\log q)^j+jq^5(\log q)^{j-1}, \tag{113}\] 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\).

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 \[\left[\frac{\lfloor Sb/c\rfloor}{S}, \frac{\lceil Sb/c\rceil}{S}\right].\] 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 \[\left[\frac{\lfloor S^2/h\rfloor}{S}, \frac{\lceil S^2/l\rceil}{S}\right].\] 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 \[-2^{62}<b<2^{62}\] 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.

Logarithms, divided logarithms, and cube roots

The function atanh2 evaluates the fifteen terms \[2\sum_{n=0}^{14}\frac{w^{2n+1}}{2n+1}\] by Horner’s rule with outward interval operations. For \(|w|\le u<1\) the absolute remainder is at most \[\frac{2u^{31}}{31(1-u^2)}.\] 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 \[ S\frac{2(3/8)^{31}}{31(1-(3/8)^2)} =\frac{617673396283947}{119978708822917120} <\frac1{100}<2. \tag{114}\] 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 \[\log t=2\operatorname{atanh}\frac{t-1}{t+1},\qquad \log2=2\operatorname{atanh}\frac13\] 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 \[ \mathcal L(t)=\int_0^1\frac{ds}{1-st} =\sum_{n=0}^{\infty}\frac{t^n}{n+1} \quad (|t|<1). \tag{115}\] 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 \[ \frac{(1/4)^{23}}{1-1/4}=\frac1{48S},\qquad \frac{(1/4)^{22}}{1-1/4}=\frac1{12S}, \tag{116}\] respectively. Each receives padding \([-1/S,1/S]\). Outside this small interval the exact identities \[\mathcal L(t)=-\frac{\log(1-t)}t,\qquad \mathcal L'(t)=\frac{(1-t)^{-1}-\mathcal L(t)}t\] use only nonzero denominators. On the entire real domain \(t<1\), differentiation of the integral representation gives \[\mathcal L'(t)=\int_0^1\frac{s\,ds}{(1-st)^2}>0,\qquad \mathcal L''(t)=2\int_0^1\frac{s^2\,ds}{(1-st)^3}>0.\] 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 \[m^3\le xS^2\] 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.

Logarithmic products and derivative propagation

The zero endpoints in (110) 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\), \[q^{h/2}|\log q|^j=e^{-ht/2}t^j\le1.\] 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 \[ |q^5(\log q)^j|\le q^{5/2}\le q^2,\qquad |q^6(\log q)^j|\le q^3. \tag{117}\] 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 (113). 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 \[\partial_i(fg)=f\,\partial_i g+g\,\partial_i f,\qquad \partial_i(f^2)=2f\,\partial_i f,\qquad \partial_i(f^{-1})=-f^{-2}\partial_i f.\] 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.

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 \[ \begin{array}{c|ccc} j& D_1&D_2&D_3\\ \hline 0&l&l^2&l^3\\ 1&(2l+h)/3&l(l+2h)/3&l^2h\\ 2&(l+2h)/3&h(h+2l)/3&lh^2\\ 3&h&h^2&h^3 \end{array} \tag{118}\] 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 \[ \frac1{1000}(30,50,75,100,150,200,300,400,500,650,800,900,1000). \tag{119}\] These twelve intervals cover \([3/100,1]\) without gaps. For each it stores the first three rows of (118); 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 \[c_i=\frac{\lfloor(l_i+h_i)/2\rfloor}{S},\qquad \rho_i=\frac{h_i-\lfloor(l_i+h_i)/2\rfloor}{S}.\] 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 \[ F(z)\ge F(c)-\sum_{i=1}^3M_i\rho_i. \tag{120}\] 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.

Subdivision, coverage, and observed completion

For a band \([a_-,a_+]\), the initial exact boxes before outward rounding are \[ \left[\frac i{24},\frac{i+1}{24}\right] \times\left[\frac j{24},\frac{j+1}{24}\right] \times\left[a_-+\frac{k}{16}(a_+-a_-), a_-+\frac{k+1}{16}(a_+-a_-)\right], \tag{121}\] 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 (121), (119), 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: \[\begin{array}{c|c|r} \text{argument}&a\text{ interval}&\text{calls to \texttt{visit}}\\ \hline 0&[0,190/1000]&414080\\ 1&[190/1000,448/1000]&756096\\ 2&[448/1000,477/1000]&1004426 \end{array}\] 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

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

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 (77). 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 (79). 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 (83). 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 (82); the final complete handles all omitted mass. No count product is needed after the first zero weight. The regular branch of run is (80). Finally, mu_num is \(M\) in (87), 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.

Bounds on every arithmetic class

For all Poisson table calls, the reduced fraction satisfies \(B\leq10^6\) and \(A\leq B/2\). Thus \[0\leq e_i\leq(B+A)H\leq108000000, \quad D_{\mathrm{tab}}=6BH^2\leq31104000000, \quad Hr_i\leq559872000000.\] 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 (78).

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 \[D_{\mathrm{tab}}N^2 \leq31104000000000000000000000000000000<2^{127}-1.\] 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 \[0\leq t_n-l_n< e^{d_+},\qquad 0\leq u_n-t_n< e^{d_+}.\] 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 \[S_0e^{d_+}+42\cdot243<243(S_0+42)<2^{63}-1.\] This also bounds every signed partial sum in (83). 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 \[\frac{L}{S_0} \geq e^{-d_+}-\frac{d_+^{42}}{42!} -\frac{41\cdot243}{S_0} >\frac1{243}-10^{-20}-\frac{9963}{10^{15}}>0.\] 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 (87) belongs to \([0,H^2]\). Hence every partial sum in mu_num is at most \[NH^2=5184000000000000<2^{63}-1.\] The factor \(20\) in the stopping comparison is applied after converting to Big. The binary-search comparisons for (85) 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.

Pair coefficient certificate

We prove the \(a=1/2\) case of Lemma 15 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 \[p=(6s+3t+2,3t+2,2),\qquad q=(6u+3v+2,3v+2,2),\qquad s,t,u,v\ge0.\] 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 \[N_x(r)=\frac{3\sum_i r_i^2-R^2}{2},\qquad N_y(r)=\frac{27\prod_i r_i-R^3+3R N_x(r)}2.\] 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 \[r_i^{(j)}=p_i\widetilde e_{i+j},\qquad T_j=\sum_i r_i^{(j)},\qquad j=0,1,2,\] 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 \[ D=PE(T_0T_1T_2)^3P^4E^4. \tag{122}\] The three expressions out[0], out[1], and out[2] divided by \(D\) are exactly \[\sum_{j=0}^2\frac{N_x(r^{(j)})}{PE T_j},\qquad \sum_{j=0}^2\frac{N_y(r^{(j)})}{PE T_j^2},\qquad \sum_{j=0}^2\frac{N_x(r^{(j)})^2}{PE T_j^3},\] namely the tilted output means of \(x,y,x^2\) within that class. For every call in the source, \[\frac{\texttt{mon}(i,j,k,l)}D=X^i y_0^j z^kB_0^l.\] 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 \[ I=\frac{27\,\operatorname{odd}(p)\operatorname{odd}(\widetilde e)} {64P^3E^3},\qquad \operatorname{odd}(p)=4(p_1-p_2)(p_0-p_1)(p_0-p_2). \tag{123}\] Indeed this follows immediately by dividing \(27\operatorname{odd}(p)\operatorname{odd}(\widetilde e) [PE(T_0T_1T_2)^3]PE/64\) by (122). Swapping the last two edge coordinates negates \(I\). Although \(D\) itself depends on the reflection class, the normalized correction in (123) 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\): \[\begin{align*} &13Xz-2d_n,\\ &11Xz-d_e,\\ &250d_e+79Xz,\\ &-20Xz-40W+40y_0B_0+51S-20(d_x-2I),\\ &6Xz-6W+y_0B_0+S-(d_e+I),\\ &2(d_e+I)-12Xz+12W-2y_0B_0+19S,\\ &-4Xz+44W-14y_0B_0+52S_A+111S_B -\{5(d_n+10I)-4(d_e+I)\}. \end{align*}\] 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 \[13672,\ 13672,\ 13674,\ 13625,\ 13625,\ 13625,\ 13625.\] 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 (123). This gives precisely (47)–(50) for \(a=1/2\).

The complete polynomial calculation is the following source.

Interval positivity certificate

Finite experiment certificate