Hellinger contraction with arbitrary Boolean output bias

1 Introduction

The Hellinger conjecture asks whether a single coordinate maximizes a particular loss of Hellinger affinity under product noise, among all Boolean functions on a uniform cube. Its formulation retains the mean of the function, so biased functions are part of the question. Anantharam, Bogdanov, Chakrabarti, Jayram, and Nair formulated it in their 2017 manuscript and proved that it implies the Courtade–Kumar conjecture on the most informative Boolean function [ABCJN17, CK14]. This connection makes a sharp inequality for the square-root profile significant beyond that profile itself.

Let X be uniform on \{-1,1\}^n. For -1\le\rho\le1, let Y_i=X_i Z_i, where the independent signs Z_i, also independent of X, satisfy \Pr(Z_i=1)=(1+\rho)/2. The noise operator is

We write H(t)=\sqrt{1-t^2} for -1\le t\le1.

Thus the conjecture is resolved positively in its full, unbalanced form. Signed coordinate functions f(x)=\pm x_i, also called dictators, attain equality for every \rho. The implication proved in [ABCJN17, Proposition 1] also shows that signed coordinates maximize the mutual information between f(X) and Y, which is the Courtade–Kumar conclusion. We state and prove this implication in Corollary 8.1, keeping its binary-entropy normalization explicit. Throughout the paper the input measure is uniform; arbitrary output bias means that no restriction is imposed on m.

To identify its Hellinger meaning, suppose f is nonconstant and let P_\pm be the conditional law of Y given f(X)=\pm1. Bayes’ formula and symmetry of the noise kernel give P_\pm(y)=2^{-n}(1\pm T_\rho f(y))/(1\pm m). Their Hellinger affinity is

Thus the left side of Equation (1.1) is the weighted affinity loss H(m)(1-A(P_+,P_-)).

Earlier results and methods. The original information problem of Courtade and Kumar [CK14] asks how much information a single Boolean summary retains about a noisy input. The square-root formulation of Anantharam et al. [ABCJN17] replaces binary entropy by Hellinger affinity while preserving an implication to that information bound. It also supplies a compression principle for arbitrary convex profiles, whose concave form we use in Section 3.

Chen and Nair [CN24, Theorem 2, Equation (6), and Remark 5] proved a mean-dependent lower bound using the Gaussian isoperimetric profile. Let \phi_{\rm G} and \Phi_{\rm G} be the standard Gaussian density and distribution function, and put I_{\rm G}(p)=\phi_{\rm G}(\Phi_{\rm G}^{-1}(p)) for 0<p<1, with I_{\rm G}(0)=I_{\rm G}(1)=0. Writing s=\sqrt{1-\rho^2}, their estimate is

This bound holds for every Boolean mean. It implies the Hellinger inequality wherever its right side reaches H(m)-1+s, but at m=0 it gives only \sqrt{2/\pi}\,s, below the sharp value s for s>0. Their proof in Section III.B splits the cube into two sections and closes a recursion for a profile of their means. It connects this induction to Bobkov’s local two-point inequality and its tensorization on the discrete cube [Bob97, Proposition 1 and Lemma 1]. The induction below uses this local-to-product strategy with an asymmetric profile and a sheared two-point comparison; its scalar inequalities are proved here.

Durcik, Ivanisvili, Roos, and Xie [DIRX26, Theorem 1.1 and Section 5] proved the sharp square-root sensitivity inequality for balanced Boolean functions, confirming the low-noise consequence predicted by the Hellinger conjecture.

Recent preprints of Chen et al. [CGJ+26], Ky and Tran [KT26], and Mahdavifar and Beirami [MB26] announce proofs of the ordinary Courtade–Kumar inequality. The Hellinger inequality studied here is a distinct functional statement: the implication in [ABCJN17] runs from the Hellinger estimate to the ordinary Boolean information bound.

Proof strategy. A differential approach to the Hellinger conjecture was developed by Chen, Gohari, and Nair in 2025 [CGN25, Section III, Lemma 6 and Theorem 7]. They express the noise-semigroup derivative of \E H(T_\rho f) as a sum of edge costs and bound that derivative through scalar profiles. We use the same derivative identity, in the normalization specified in Section 4. The calibrated edge comparison and the spectral estimates needed for our continuation argument are proved below.

There are two complementary parts to the proof. For s\le .84, we compress to increasing Boolean functions and induct in dimension. For each fixed s we choose a concave function G:[0,1]\to[0,\infty) and a nonnegative polynomial B on [-1,1], and prove the stronger bound

The identity G(p)+G(1-p)=2H(2p-1) recovers the Hellinger profile when this bound is averaged with the bound for the increasing function -f(-x). The polynomial B is chosen so that the reflected lower bound is at least H(m)-1+s. The induction step controls the gain from mixing two sections by their probability difference after subtracting a multiple of their difference in G. Cauchy–Schwarz then gives an inequality involving only the section averages and their mean gap. Its monotone quadratic-root bound allows substitution of the induction hypotheses. A coordinate with small positive correlation with the output confines the comparison to a fixed scalar domain.

For s\ge .84, we continue from the established range. At a first failure of the target bound, its equality case would have semigroup energy no greater than the corresponding coordinate energy. The change of variable F(0)=0, F'=H^{-3/2} bounds the energy below by the Dirichlet energy of F(T_\rho f). Near zero bias, a sharper edge bound uses a symmetric comparison pair \pm x_0 with H(x_0)=\E H(T_\rho f). This retains the exact cost of a noised coordinate. The resulting energy balance separates a variance gain from the possible spread of the first Fourier level; controlling that spread excludes a crossing unless f is a signed coordinate. For intermediate biases, even–odd Fourier decomposition reduces the energy estimate to pointwise bounds with explicit bias margins. Large biases instead admit a direct proof from forward and reverse cube norm estimates. Figure 1 displays how their parameter ranges fit together.

The proof is computer-assisted only through fixed scalar inequalities, independent of n. Every decimal appearing as an inequality constant denotes its exact rational value. We give the transformations, domains, arithmetic recursions, and positive bounds that certify these inequalities; the supplementary sources reproduce the finite calculations.

Organization. Section 2 fixes the cube conventions. Section 3 proves the dimension-induction range. Section 4 reduces the rest to excluding an energy crossing. Sections 5, 6, and 7 treat the three bias regimes and complete the proof. Appendix A records the exact-arithmetic conventions; Appendix B proves the scalar estimates needed for the induction.

2 Cube conventions and elementary reductions

All averages and inner products below use the uniform measure on the relevant cube. For a real function u on \{-1,1\}^n, write

The functions \chi_S form an orthonormal basis: independence makes \E\chi_S\chi_T equal to 1 if S=T and to 0 otherwise. Consequently,

For later use set W_k(u)=\sum_{|S|=k}\widehat u(S)^2.

Let \E_i average only coordinate i, and define

Thus D_i u(x)=(u(x)-u(x^{(i)}))/2, where x^{(i)} reverses coordinate i. The projections D_i are self-adjoint and satisfy

Independence in the noise definition gives T_\rho\chi_S=\rho^{|S|}\chi_S. Hence, for \tau\ge0, T_{e^{-\tau}}=e^{-\tau\mathcal N}. These elementary facts are also standard in the analysis of Boolean functions [O’D14]; their normalizations are specified here to fix every factor of two.

We first remove the endpoints and symmetries. The identity

shows that it suffices to consider \rho\ge0. At \rho=0, the left side of Equation (1.1) is zero. At \rho=1, it equals H(m)\le1. For a constant f, it is again zero. For 0<\rho<1 and nonconstant f, every input has positive noise probability, so

All differentiations involving H below are therefore legitimate. Finally, replacing f by -f preserves both sides of Equation (1.1) and reverses m.

3 Dimension induction

We first prove the desired inequality in the range reached by dimension induction. Every decimal in this section denotes an exact rational number.

We strengthen the desired bound to an inequality for a nonsymmetric function of the noisy output. Averaging this inequality with its reflected version will recover H. The induction uses an asymmetric function G and a polynomial profile B. The scalar inequalities that support it are stated in Lemma 3.4 and proved by the finite arithmetic certificates in Appendix B. We first establish the two reductions that explain their domains.

3.1 Compression and a small coordinate

The following sorting argument is the concave-profile form of the compression principle of Anantharam, Bogdanov, Chakrabarti, Jayram, and Nair [ABCJN17, Proposition 2]. We include the short proof to specify its direction for H. We order the cube coordinatewise using -1<1. A function is increasing if it is nondecreasing in each coordinate.

Call a coordinate active if the function depends on it. Inactive coordinates may be omitted from all expectations below. Define

3.2 The scalar interface

For the fixed value of s, use one row of Table 1 whose interval contains s. The profile polynomials use a finer subdivision of these same intervals, specified in Appendix B. At a shared endpoint, choose the parameters and the profile consistently from one adjoining interval. Put \delta=(1-\rho)/2, so that 4\delta(1-\delta)=s^2; the auxiliary bounds in the table satisfy r_0^2\le\delta\le r_1^2.

Define

All rows have U<0, V\ge0, and L+U\ge .488. Thus \lambda(h)\ge L+U>0 for 0\le h\le1, and G is nonnegative, with G(0)=G(1)=0. Its defining asymmetry cancels under reflection:

The profiles in the next lemma are explicit polynomials of the form

where only finitely many c_j are nonzero, and T_0(u)=1, T_1(u)=u, T_{j+1}(u)=2uT_j(u)-T_{j-1}(u). The integer coefficients and their arithmetic verification are given in Appendix B.

With these functions, the estimate we will propagate is

for every increasing Boolean function f. Its dual f^*(x)=-f(-x) is increasing and has mean -m. Noise commutes with input reversal, so averaging the proposed estimates for f and f^* and using Equation (3.3) would give

Thus we need a profile whose reflected average reaches H(m)-1+s, and an estimate for G that passes from two sections to their parent. The next lemma supplies the two-point gap used in this passage, the reflected comparison, the condition that closes induction on the small-coordinate domain, and the initial cases.

The four assertions of Lemma 3.4, including the entire three-coordinate base case, are proved in Appendix B. We now show how the pair bound and profile comparison propagate the asymmetric estimate from three active coordinates to arbitrary dimension.

3.3 Averaging and dimension induction

4 A continuation criterion

The notation in this section and the next three is independent of the induction parameters. Fix a nonconstant Boolean f, use output-sign symmetry to take m=\E f\ge0, and put

We work with .84\le s<1, so 0<r\le .2944.

Define

For the parameter \tau=-\log\rho, one has \partial_\tau d=-\mathcal N d. Since H'(z)=-z/H(z), Equation (2.1) yields

This identity is the Hellinger edge derivative of Chen, Gohari, and Nair [CGN25, Section III, Lemma 6] in our generator normalization: their parameter has \rho=e^{-2t}, so \tau=2t here.

The following change of variable will be used in the two smaller bias regimes:

The function F is odd, increasing, and has finite limits at \pm1.

The two smaller bias ranges will combine these energy comparisons with upper bounds on the variance of d and its odd part. Booleanity supplies the following bounds.

At a hypothetical crossing, the fixed mean lies either in the central band 0\le m\le r^2/2, in the intermediate band r^2/2\le m\le .74, or in the large-bias band .74\le m<1. The next sections exclude the crossing in the first two bands and prove the target directly in the third.

5 The central band

We retain the notation of Section 4. In the band containing the signed coordinates, we sharpen the basic energy comparison to preserve their exact edge cost. The resulting bound will force any function satisfying the crossing conditions to be a signed coordinate.

Throughout the proof all terminating decimals denote exact rational numbers. Under (5.1), set

The symbol \alpha is local to this section. Write R_0=.2944. Since 0<r\le R_0 and m\le R_0^2/2, the exact comparison (.999)^2<1-R_0^4/4 gives

Here F(x)\ge x for x\ge0, and (.91595)^2<.839. The symmetric pair of values \pm x_0 has H(x_0)=b, so its H-average equals that of d and its transformed squared amplitude is M. Its edge energy is x_0^2/b. When m=0, the crossing identity gives b=s and x_0=\rho, recovering a noised coordinate.

5.1 The calibrated edge cost

For 0\le v<F(1)^2, define

The endpoint value F(1) is finite, since the integrand defining F has an integrable singularity of order 3/4 at 1.

Define the slope and energy excess at the calibration by

The first identity follows by differentiating x^2/H(x) with respect to F(x)^2; the second uses M+\Phi(M)=(1-b^2)/b and K=(1-s^2)/s. In particular, p_*,\Delta\ge0.

5.2 Reduction to variance and first-level estimates

Let a_i be the degree-one Fourier coefficients of g, and put

Thus H_0 is the Fourier weight above degree one. Counting degrees gives \sum_i\E(D_i g)^2\ge\Var g+H_0. All arguments of \Phi used below belong to its open domain: since the cube is finite, G_{\max}:=\max|g|<F(1); every half-difference |D_i g| and coefficient |a_i| is at most G_{\max}, while M=F(x_0)^2<F(1)^2 because b>0. In a coordinate attaining l, Jensen’s inequality and monotonicity of \Phi give \E\Phi((D_i g)^2)\ge\Phi(\E(D_i g)^2)\ge\Phi(l). Lemma 5.2 and the tangent inequality for \Phi at M yield

Here q-l is the degree-one weight outside a largest coordinate. Put

We will prove

with strict inequality unless m=0 and g^2=M everywhere. Substituting this estimate into (5.11) cancels \Delta. We will then control the remaining negative term by proving

These two bounds give \mathcal E(d)>K whenever the variance inequality is strict. We first prove that inequality, then establish the first-level comparison and treat the remaining equality case.

5.3 A variance gain around the calibration

Define, on 0\le t<1,

Writing u=\sqrt{H(d)}, one has g=k(u)d, k(y)=\alpha, and

Both identities follow by differentiation; the second also holds at u=1 by continuity.

To estimate the variance of g, separate its mean from the known mean \E d=m by subtracting \alpha d. Define

The right side defining D depends only on u, because R^2=(1-u^4)(k(u)-\alpha)^2. The added multiple of u^2-y^2 has zero expectation. Since \E u^2=b=y^2, \E g=\E R+\alpha m, and (\E R)^2\le\E R^2, one obtains

5.4 Concentration of the first Fourier level

6 Intermediate biases

We retain the notation of Section 4. In particular, 21/25\le s<1, r=1-s^2, d=T_\rho f, m=\E f\ge0, h=H(m), b=\E H(d), and g=F(d), where F(0)=0 and F'=H^{-3/2}. The first-level bound of Lemma 4.3 is denoted by

All terminating decimals in this section denote exact rational numbers.

6.1 Parity and an energy reduction

For a function u on the cube, write

These are the projections onto the even and odd Fourier degrees. Every nonconstant even degree is at least two, whereas an odd degree other than one is at least three. As in Lemma 4.3, Parseval and W_1(f)\le w give

The edge comparison of Lemma 4.2, followed by the same degree count for g, gives

To use the extra even-degree contribution, we compare g=F(d) with its affine approximation at m. Set v=1-s and a=F'(m)=h^{-3/2}. The tangent deficit of H at m is

Concavity gives V\ge0, and at a putative crossing,

The variance expansion

is valid without any assumption on \E g. On the nonconstant even subspace, apply the identity

with u=g_e-\E g and v_0=a(d_e-m). Dropping the odd part of \Var(g-ad) then gives

This compensates for half the even part of the variance penalty. Define the remaining pointwise expression by

Inserting the variance expansion into (6.2) and using (6.1) now gives

Define

Since r=v(1+s), the identity 3v-rQ_*/2=r/s shows that the following strict inequality suffices:

6.2 Pointwise bounds and the bias margins

Near m=r^2/2, a positive multiple of V^2 supplies the needed gain because \E V=v. For m\ge1/5, the gap Q_*-Q will instead allow a small negative multiple of V. We first use these estimates to prove Proposition 6.1, then prove the estimates in angular coordinates.

6.3 Proof of the pointwise comparison

6.4 The six exact polynomial certificates

For completeness, we specify the entire finite calculation behind (6.24)–(6.25). It uses rational arithmetic and the tensor Bernstein basis described in Appendix A. Explicitly, for U(A,B)=\sum_{a,b}u_{ab}A^aB^b of coordinate degrees at most (n_1,n_2), its coefficients in that basis are

The Bernstein basis functions are nonnegative on the unit square and sum to one. Thus a positive minimum of these coefficients proves positivity throughout that square.

For \mathcal S, use (A,B)\in[0,1]^2, \sigma\in\{-1,1\}, and the two charts

They cover the required rectangle: choose the first chart when T/(21/100)\ge |x|/(1/2), and the second when the reverse inequality holds. In each chart \mathcal S\circ C_{j,\sigma} has a factor A. To make the expansion entirely explicit, if \mathcal S(T,x)=\sum c_{ij}T^ix^j, then every nonzero term has i+j even and at least two, and the divided polynomials are

Their degrees are at most (8,18) and (8,6), respectively. The values at A=0 are polynomial extensions; after multiplying back by A\ge0, the origin is included in the nonstrict sign claim.

For \mathcal L_\eps, subdivide into sixteen equal rectangles. For j,k\in\{0,1,2,3\}, use the affine map

Each resulting polynomial has coordinate degrees at most (6,20). If the untransformed coefficient of T^ix^j is c_{ij}, the coefficient of A^aB^b after any affine map (T,x)=(\ell_T+w_TA,\ell_x+w_xB) is exactly

Thus (6.20)–(6.22), (6.24)–(6.25), and (6.26)–(6.32) specify every coefficient by a finite rational sum.

Table 2 records the minimum coefficients. An entry M in the last column means \lfloor C\min\mathcal B_{ij}\rfloor=M, with the minimum also taken over all sixteen boxes in the last two rows. In particular the minimum is at least M/C>0. These six integer comparisons are the finite arithmetic part of the pointwise proof; the accompanying exact reconstruction scripts implement the displayed sums.

7 Large biases

The last bias range admits a direct estimate. We retain the reduction 0\le\rho\le1. As throughout the proof, H(t)=\sqrt{1-t^2}, expectation is uniform on the cube, and

All terminating decimals in this section denote exact rational numbers.

Write U=T_\rho\mathbf1_{\{f=-1\}}=(1-d)/2, so that H(d)=2\sqrt U\sqrt{1-U}. Expanding \sqrt{1-U} will reduce the desired lower bound on b to a lower bound on \E U^{1/2} and upper bounds on the higher moments \E U^{k+1/2}, k\ge1. These are supplied by reverse and forward cube norm inequalities, respectively.

The forward inequality belongs to the classical hypercontractive theory of Bonami and Beckner [Bon70, Bec75]; the reverse inequality is due to Borell [Bor82]. We derive both from the cube logarithmic Sobolev inequality using Gross’s semigroup method [Gro75]. The sharp reverse time constant is also given by Mossel, Oleszkiewicz, and Sen [MOS13, Equation (1.2) and Theorem 1.10] with logarithmic Sobolev constant 2. The proof below fixes the uniform-bit normalization and the limiting argument for inputs with zeros.

7.1 The cube norm inequalities

For a positive function z on a finite probability space, write

Recall the operators from Section 2: on the cube, let \E_i average only coordinate i, and set D_i=I-\E_i and \mathcal N=\sum_iD_i. These self-adjoint projections give

In particular, if v_+,v_- and w_+,w_- are the two values on a coordinate edge, its conditional contribution is

7.2 Reduction to a series of powers

8 Completion of the proof

8.1 The information-theoretic consequence

For 0\le p\le1, write

with 0\log_2 0=0. Mutual information in the next statement is measured in bits. The argument is the implication of Anantharam, Bogdanov, Chakrabarti, Jayram, and Nair [ABCJN17, Proposition 1 and Lemma 1], reproduced here in our normalization. It applies to Boolean summaries of a uniform input, including summaries with nonzero mean.

A Exact arithmetic conventions

All constants in the certificates are rational; a terminating decimal denotes the corresponding rational number exactly. This appendix explains the common sign-certification rules. The individual polynomials, parameter maps, and subdivision orders are specified where they are used.

A.1 Bernstein coefficients

We use the standard enclosure supplied by the Bernstein form of a polynomial; see Cargo and Shisha [CS66, Section 3] for the univariate coefficient identity and range bound. We include the tensor-product formula and its proof to make the rational checks explicit. Let P(x,y)=\sum_{k=0}^N\sum_{\ell=0}^K a_{k\ell}x^ky^\ell. On the unit square its Bernstein expansion is

where

Indeed,

by the binomial theorem after factoring out x^k; multiplying two such identities proves the formula. The basis functions in Equation (A.1) are nonnegative and sum to one. Therefore

The univariate version is obtained by omitting y.

For a rational rectangle, first substitute the affine maps from the unit square. For a polynomial obtained after a rational or algebraic change of variables, the displayed denominator is cleared only where it is positive, as verified in the corresponding argument. A positive common scale may be applied to all coefficients, making every calculation integral. If a table reports \lfloor C\min b_{ij}\rfloor for a stated C>0, a positive table entry is an exact strict sign certificate.

Subintervals can be handled either by direct substitution or by de Casteljau subdivision. For subdivision at 1/2, start from a Bernstein row (b_0,\ldots,b_N), repeatedly replace neighboring entries by their arithmetic mean, and take the left and right outer diagonals as the Bernstein rows on the two halves. This rule follows by substituting x=t/2 and x=(1+t)/2 into the basis expansion. It is exact over the rationals; a common power of two clears all new denominators. For rectangles, apply the rule separately in each coordinate.

A.2 Intervals and derivative enclosures

An interval [a,b] encloses a real quantity if a\le x\le b. Addition, subtraction, multiplication, and reciprocal use the endpoint extrema, with a reciprocal taken only when zero is excluded. Square roots are taken only on nonnegative intervals. For a positive integer scale Q, rounding a lower endpoint down to a multiple of 1/Q and an upper endpoint up preserves enclosure. Scaled square roots reduce to integer square-root bounds: for an integer A\ge0,

Consequently no floating-point operation is needed for an interval certificate.

A derivative enclosure supplies a second bound on a box. If a function has center enclosure I_0, coordinate half-widths h_i, and derivative magnitude bounds M_i, then

This follows by integrating the derivative along a segment from the center. The same statement holds with bounded limiting derivatives at a boundary whenever the resulting Lipschitz estimate extends continuously. At a square-root singularity the direct interval enclosure is used instead. The pair certificate in Appendix B specifies which bounds are used and how uncertified boxes are subdivided. An undefined local interval operation causes further subdivision, never acceptance.

A.3 Supplementary sources

The complete certificate sources accompany the paper in the directory verification/. They are organized as follows.

The accompanying README gives the compiler and Python requirements and a single command to reproduce the calculations. The C++ source uses outward-rounded integer intervals with signed extended 128-bit intermediates; Appendix B gives the relevant bounds. The principal Python profile certificate uses arbitrary-precision integer arithmetic. The symbolic reconstruction scripts use exact rational coefficients. The arguments proving the enclosure rules, the complete domain coverage, and the passage from the scalar inequalities to the dimension-free theorem are part of the paper.

B The scalar certificates

This appendix proves the scalar assertions of Lemma 3.4. We first verify the two-point inequality in three regions. The normalized checks near the two endpoints also prove concavity of G, which is then used in the third region. We next verify the polynomial conditions that make the reflected profile reach the target and close the dimension induction. Finally, we prove the initial estimate on at most three coordinates. In the profile and base checks the noise parameter varies over a whole interval; endpoint bounds and interval enclosures, respectively, will control that variation. All decimal numbers in this appendix are exact terminating decimals. The seven choices of (L,U,V,\alpha,\Lambda,\mu) and the bounds (r_0,r_1) are those of Table 1. A parameter choice is fixed throughout each calculation. At an endpoint shared by two ranges one uses an entire row, including its profile, consistently. The finite computations below involve only fixed polynomials and functions of at most three real variables; there is no dimension-dependent search. Their arithmetic recursions and all numerical input data are specified here. The accompanying files verification/interval_certificate.cpp and verification/profile_certificate.py implement these recursions.

B.1 Reduction of the pair inequality

Write \delta=(1-\rho)/2, so s^2=4\delta(1-\delta). The table bounds r_0^2\leq\delta\leq r_1^2 follow by comparing

These are rational comparisons, and a\mapsto4a(1-a) is increasing on [0,1/2]. We prove the pair assertion for s>0 and p_0<p_1; when p_0=p_1, both its deficit and its shear are zero.

For a smooth function F, use divided differences

with repeated arguments interpreted by continuous extension whenever the function is smooth there. Put z=p_1-p_0, p_t=p_0+tz, and

The interpolation identity

gives D=s^2z^2K. Moreover, the shear in Equation (3.5) is zW. Thus the strict inequality

implies its required nonstrict inequality. We will also prove D\geq0.

The following change of variable gives smooth normalized expressions near the endpoints, where derivatives of G otherwise interfere with interval evaluation. For 0\leq y<1, put q=\sqrt{1-y^2}, h=2qy, and e=(1+h\lambda(h))^{-1}, and define

Direct substitution into Equation (3.2), or multiplication by 1+h\lambda(h), proves

For every parameter row, U<0, V>0, and \lambda(h)\geq L+U\geq.488 on [0,1]. Consequently all the denominators just used are positive, and N,R,M are smooth at the arguments used below, which stay strictly below 1. Also N(y),R(y)>0 for 0\leq y<1.

The three expressions separate different endpoint behaviors. N removes the factor p from G(p) at p=0, while R removes the factor \sqrt{1-p} at p=1. The second representation of G(y^2) shows that the right derivative is G'(0)=4L: M measures the remainder after subtracting this tangent. Consequently the shear z-(G(p_1)-G(p_0))/(4L) vanishes for the linear function G(p)=4Lp. Using M in the first endpoint region preserves this cancellation before any interval bounds are taken; using R in the second removes the square-root factor there.

Two endpoint regions. Case 1 is

Case 2 is

In both cases introduce j\in[0,r_1] and set

retaining only parameters with r_0^2\leq\delta\leq r_1^2. Indeed

It increases in both variables and, for each fixed u, runs continuously from 0 to at least r_1^2. Hence every required \delta is represented. The identities

identify the two noisy mixture points (their order is reversed in Case 2). They also give u\leq w,t\leq1.

Let m^i, for i=w,t, be the divided-difference tuple of the function a\mapsto M(va) in Case 1 and a\mapsto R(va) in Case 2 at the three nodes (u,i,1). Its seven entries are indexed by 0,1,2,01,02,12,012; for example, m^i_{02} is the first divided difference on the endpoint nodes. The common endpoint entries are written m_0,m_2,m_{02}. Set

In Case 1 define

The finite sign check in Subsection B.2 proves

Here the endpoint first difference of b^{3/2}M(v\sqrt b) on (u^2,1) is F, and its second difference on (u^2,i^2,1) is P_i. For clarity, the identities behind the latter statement are

They follow by factoring differences of squares and applying the product rule for divided differences stated below. The final formula in Equation (B.6) has a continuous extension at the corner u=i=0. Using Equation (B.4) gives, for a nondegenerate pair,

The left side of Equation (B.7) is therefore \Delta/v. Since v>0 for an actual pair, Equation (B.7) implies Equation (B.2) in Case 1.

In Case 2 define

The second finite sign check is

Applying the same difference-of-squares identities to \sqrt b R(v\sqrt b) now gives

Thus the left side of Equation (B.9) equals v^2(u+w)\Delta. For a required pair v>0; and u+w=0 would force u=j=0 and \delta=0, excluded here. This proves Equation (B.2) in Case 2.

Strict concavity, before the third region. The preceding sign checks also hold at repeated nodes, by their smooth normalized formulas. Fix u=1 and any permitted j=\delta>0. Such a value lies in the certified interval [0,r_1], since \delta\le r_1^2<r_1. Then w=t=1. In Case 1, S_0=N(v)>0 and the Z^2 term of Equation (B.7) vanishes, so that inequality directly forces Z>0. In Case 2, S_1=R(v)>0, and Equation (B.9) likewise directly forces Z>0. No prior sign of K is used in either inference. For v>0 the identities above imply K=-G''(p_0)/8>0 on, respectively, (0,.64] and [.36,1). These intervals cover (0,1); hence G is strictly concave there. Since G is continuous on [0,1], its interpolation deficit is strictly positive for any distinct endpoint pair and any interpolation weight in (0,1), including pairs containing 0 or 1. It follows that D>0 and K>0 for every actual pair under consideration. This proves the separate assertion D\geq0 and supplies the sign of K needed next.

The remaining region. Cases 1 and 2 cover p_1\leq.64 and p_0\geq.36. Any pair outside them is in Case 3:

Put

Here z\geq.28, so these denominators stay positive. The endpoint increments in G are bP and (u'-u)Q, respectively. As b=(u+u')(u'-u), this proves Z=(u+u')K and identifies W with Equation (B.1). Set

The third finite check proves the disjunction

The first alternative suffices because Y_0=(u+u')\Delta. In the second alternative take the convex combination of the brackets in Y_1,Y_2 with weights 2u/(u+u') and (u'-u)/(u+u'). It is

For s>0 we have u+u'>0, and the concavity already proved gives Z=(u+u')K>0. Therefore the second alternative also implies Equation (B.2). The three regions prove Equation (3.5), subject only to the following explicit finite sign checks.

B.2 Interval arithmetic for the three pair regions

Enclosures and derivatives. All intervals may have rational endpoints. The particular certificate rounds outwards after every operation to multiples of Q_*^{-1}, where Q_*=10^{12}. Store an interval as [a/Q_*,b/Q_*] with integers a\leq b. Addition and subtraction use their ordinary endpoint rules. For multiplication, take the least and greatest of the four endpoint products and round their quotients by Q_* down and up. For a positive interval its reciprocal endpoints are

For a nonnegative interval the square-root endpoints are Q_*^{-1}\lfloor\sqrt{aQ_*}\rfloor and Q_*^{-1}\lceil\sqrt{bQ_*}\rceil; integer square comparison computes these exactly. Failed positivity or domain conditions never certify a box. A power with a nonnegative small integer exponent is evaluated by repeated interval multiplication, including for squares; this may overestimate but remains an enclosure.

An interval expression may be augmented by its three first derivatives. Use the sum and product rules, and

The latter derivative is used only when the lower bound for the root is strictly positive. In Case 3 the radicands defining l',u' are known nonnegative on the whole box; direct value evaluation may therefore replace a negative interval lower endpoint by zero. Derivative evaluation does not use this clipping and fails at an uncertified root singularity.

The function \mathcal E(a,b) has a special rule on 0\leq a\leq b. Enclose h=a/(a+b) by [0,1/2], intersecting with direct interval division if a+b has a positive lower bound. Its value is enclosed by ah, and its differential by

At (0,0) the function is continuous and Lipschitz on this cone, so the same difference bounds hold by limits from its interior; differentiability at that point is not assumed. The required order relations u\leq w,t and l\leq l' hold throughout each parameter box, not just on its \delta-restricted subset. Thus these enclosures apply on the line segments used in the mean-value estimate below.

Tuples without division by node distances. For three nodes let a denote the tuple of values and divided differences of a function. Addition is componentwise. For c=ab, the product rule is

For a=c^{-1} use

for a=\sqrt c use

The last two formulas solve ac=1 and a^2=c using Equation (B.14). They remain valid at repeated nodes by continuity and use no inverse node distance. All entries can themselves be intervals, or intervals augmented by the three derivatives. A constant tuple has that constant in its three value entries and zero in the other entries. Write X(a,b,c,g) for the tuple with value entries (a,b,c), all three first differences g, and second difference zero.

To specify the evaluation completely, the tuple-valued function \operatorname{table}(x,k) is obtained by the following straight-line recipe; \operatorname{sq} means multiplication of an expression by itself.

q2 = 1-x*x; q = sqrt(q2); h = 2*(q*x)
a = L+h*(U+V*h); e = inv(1+h*a)
if k==1:
  return 4*(L*x+q*((2*sq(L)-1)-2*U*q2
                  +h*((2*L*U)-2*V*q2+(2*L*V)*h)))*e
if k==2: return 4*(q2*(q+x*a))*e
return 4*(q*(x+q*a))*e

These are exactly M,R,N in that order. The expressions to test are specified below, retaining the evaluation order of the certificate. Tuple subscripts are strings of node indices, so 12 and 012 denote first and second divided differences. Products and quotients on one line associate from left to right. The symbols alpha, Lambda, mu, and E stand for \alpha,\Lambda,\mu,\mathcal E, respectively.

term(m,u,i):
  e = E(u,i); o = inv(1+u)
  return ((1-o*e)*m[2]+(i+e)*m[12]
                         +e*u*(m[012]-o*m[02]))/(1+i)

expr(u,v,j,k):
  d = j*(2*u+(1-u)*j); w = u+(1-u)*j
  t = sqrt(1-(1-u)*d)
  m = table(X(v*u,v*w,v,v),k)
  n = table(X(v*u,v*t,v,v),k)
  if k==1:
    F = (1+u*u/(1+u))*m[2]+u*u*u*m[02]/(1+u)
    Z = .125*(term(m,u,w)+term(n,u,t))
    H0 = alpha*(4*L-v*m[2])
                            +(1-alpha)*u*u*(4*L-v*u*m[0])
    di = d*(1-u); wi = 1-sq(w)
    return [Z*H0+(4*Lambda)*di*wi*v*sq(Z)
                                      -mu*v*sq(F)/sq(4*L)]
  half = .5*Lambda
  F = (m[2]+u*m[02])/(1+u)
  Z = .125*((F-m[12]-u*m[012])/(1+w)
                 +(u+w)/(u+t)*(F-n[12]-u*n[012])/(1+t))
  H0 = (alpha-half)*u*m[0]+(1-alpha-half)*m[2]
                                       +half*(w*m[1]+t*n[1])
  return [Z*H0-mu*(u+w)*sq(v+F/(4*L))]

expr3(l,u,r):
  z = 1-sq(l)-sq(u); b = sq(r)*z
  lp = nroot(sq(l)+b); up = nroot(sq(u)+b)
  n = table(X(l,l,lp,1),3); a = table(X(u,u,up,1),2)
  P = n[2]+E(l,lp)*n[02]; Q = a[2]+u*a[02]
  Z = (Q+(u+up)*P)/(8*(1-sq(r))*z)
  W2 = sq(1-(u*a[0]-l*l*n[0])/(4*L*z))
  half = .5*Lambda
  Y0 = Z*((alpha-half)*u*a[0]+half*up*a[2]
                    +(1-alpha)*l*l*n[0]+half*b*P)
                                            -mu*(u+up)*W2
  rest = half*(up-u)*P
  Y1 = Z*((.5*alpha)*a[0]+rest)-mu*W2
  Y2 = Z*(half*Q+rest)-mu*W2
  return [Y0,Y1,Y2]

Here nroot is the square-root operation with the value-only clipping already specified; on derivative tuples it is the ordinary strict-domain root. These recipes are the normalized expressions in Equations (B.7), (B.9), and (B.11).

The box test. An initial box has coordinates (u,v,j) in Cases 1 and 2 and (l,u,r) in Case 3, with the ranges specified above. A subdivision bisects all three coordinates, giving eight children. First exclude a box in Cases 1 and 2 if the interval between the low-low and high-high corner values of \delta(u,j) misses [r_0^2,r_1^2]. The monotonicity in Equation (B.5) proves this exclusion sound, with the corner arithmetic rounded outwards.

For every remaining scalar expression F one may certify F>0 either by a positive lower endpoint of its interval value on the whole box, or by the following derivative test. Let c_i,h_i be the exact center and half-width of its coordinate intervals, and normalize the coordinates by x_i=c_i+h_i\xi_i with |\xi_i|\leq1. Initialize the derivative of coordinate x_i with respect to \xi_i to an outward enclosure of h_i, and its other derivatives to zero. If I_c encloses F(c) and J_i encloses \partial F/\partial\xi_i on the full box, the sufficient test is

The mean-value theorem, with the limiting argument for Equation (B.13) when needed, proves the test. In Case 3 different components can use different tests: the box is good if the first component is positive, or if both the second and third are positive. It is unnecessary for the same branch of the disjunction to hold on different boxes.

More formally, with d the remaining permitted depth, the entire finite decision procedure is

verify(box,d):
  if the box is excluded by the delta restriction: return true
  attempt interval values and, if needed, center/derivative bounds
  if the Case 1 or 2 expression is certified positive: return true
  if Case 3 has component 0 positive, or components 1 and 2 positive:
      return true
  # An invalid arithmetic operation never certifies a box.
  if d==0: return false
  return AND(verify(child,d-1) for the eight children)

In the supplied implementation any invalid attempt immediately proceeds to subdivision; it does not turn a failed bound into a certificate. A sign-certified leaf proves the required inequality on its entire box; an excluded leaf has empty intersection with the required delta range. Induction up the finite subdivision tree therefore proves the inequalities on the initial region subject to that restriction.

Evaluation of the recursions with Q_*=10^{12} gives true for all 21 initial boxes at the depths in Table 4. This is a finite list of integer comparisons, as specified above. In particular it proves the strict sign assertions in Equations (B.7), (B.9), and (B.12), including the normalized boundary values used for the concavity argument. The recorded execution of the accompanying C++ certificate has no failed terminal leaf.

Arithmetic range and trust. The mathematical procedure can use arbitrary-precision integers. The supplied C++ implementation instead guards each stored scaled endpoint by |a|,|b|\leq10^{18}. Endpoint sums and differences before the guard are at most 2\cdot10^{18} in magnitude, and the sum of three derivative magnitudes in Equation (B.17) is at most 3\cdot10^{18}; these fit signed 64-bit integers. Each endpoint product is at most 10^{36}, below the signed 128-bit maximum; the reciprocal numerator is 10^{24}, and root radicands are at most 10^{30}. The integer root search uses upper bound 10^{15}+1, whose square also fits signed 128 bits. At depths at most 14, dyadic grid indices are below 2^{14}; the pre-conversion grid products in the source are below 2\cdot10^{16}. Its unguarded integer constructor receives only the displayed small constants. Thus intermediate operations as well as stored values fit their integer types. An overflow guard failure causes subdivision, not acceptance. The computational verification uses ordinary exact integer arithmetic and reviewed source execution; it does not require floating-point rounding assumptions or claim proof-assistant verification.

B.3 The seventeen polynomial profiles

It remains to choose a profile that satisfies the reflected comparison and the induction closure condition, Lemma 3.4(2)–(3). We use seventeen polynomials of the form

where T_0=1, T_1=m, and T_{j+1}=2mT_j-T_{j-1}. The form in Equation (B.18) gives B(0)=1 and B(\pm1)=0 exactly. The coefficient data below assign each polynomial to a closed interval [s_0,s_1] contained in one parameter group. Before giving those data, we reduce the remaining properties to five sign checks.

The required signs and their implications. Use the polynomial quotients

They are polynomial identities, including at m=0 or x=0. For B(m)=\sum b_km^k, explicit coefficient recipes are

There is thus no evaluation of a quotient by a vanishing variable.

For each of the seventeen profiles on its assigned interval, we verify

Here the piecewise affine upper boundary b(m) is completely specified by the successive knot pairs, multiplied by 16,

In particular b(m)\leq1-|m|, so all arguments m\pm x are in [-1,1].

These sign assertions suffice for the reflection and profile parts of the scalar lemma, as follows. First B=(1-m^2)P\geq0. The polynomial E_B is even, and 1-H(m)=m^2/(1+H(m)), whence

For E_B<0 the certified bound at s_1 implies the one at any 0\leq s\leq s_1; for E_B\geq0 it is immediate. Thus Equation (3.6) follows, including m=0, where both sides equal s, and m=\pm1.

For fixed (m,x), J_s is affine in s, J_0=1, and the certificate gives J_{s_1}>0. Therefore J_s>0 on [0,s_1], and its square is monotone there: decreasing when C>0, increasing when C<0, constant when C=0. Consequently

The expression subtracted from \mu J_s^2 in \mathcal V_s is independent of s within the row. The two endpoint certificates therefore imply \mathcal V_s>0 throughout the row. This proves Equation (3.7) for either sign of A or C. It is the positivity of the affine factor that justifies this step; endpoint positivity of a general quadratic alone would not suffice.

B.4 Profile data and exact sign verification

Coefficient data. Each line below lists 1000s_1 followed by (c_1,c_2,\ldots); unlisted coefficients are zero. Its interval is [s_0,s_1], where s_0 is the previous endpoint, starting at zero. The group is the first row of Table 1 whose upper endpoint is at least s_1; no profile interval straddles a group boundary.

5: 26797227, 21421001, 5128970, 9234452, 692060, 4904060, -868991, 3430822, -1620202, 2642536, -1572003, 1611382, -790463, 573913, -196263, 125941, -28650, 17140.

17: 26545421, 20782313, 4702871, 8733755, 262302, 4632398, -1223407, 3219225, -1751136, 2367765, -1499679, 1323103, -650254, 364146, -98062, 32125.

39: 23422612, 23811053, 2720392, 9481334, 342747, 3521407, 293182, 1243280, 94220, 628296, -211618, 367918, -115140, 71341.

70: 28627418, 18132350, 6560313, 4688850, 3090858, 280132, 2014606, -721794, 1092862, -413975, 251954, -30987.

108: 25845226, 21339334, 2692615, 7536216, -587180, 2879744, -642549, 859994, -135519, 99765.

160: 28111431, 22222528, 3686628, 6969749, 260698, 2311757, -230942, 626183, -39197, 65219.

220: 31980620, 22310973, 3943312, 6252289, 221019, 1801879, -204196, 345834.

300: 37050025, 22730221, 6023971, 4990611, 1410047, 1047683, 133030, 195650.

400: 46891988, 25975928, 8279226, 5707508, 1896038, 1189721, 225195, 190389.

490: 57774207, 30017282, 10752796, 6552311, 2404507, 1338857, 310628, 193643.

570: 67261317, 34557385, 13515609, 7744945, 3024441, 1590294, 428436, 214704.

630: 76105766, 38746702, 15974003, 8801748, 3567377, 1794423, 517893, 232715.

700: 92621845, 50731247, 23924150, 14690765, 6918336, 4309886, 1672440, 1096916, 239750, 209175.

750: 100973193, 55145076, 26634158, 15924290, 7601086, 4546032, 1797080, 1099352, 246042, 192495.

800: 114390772, 63949520, 33959789, 20265973, 11129205, 6354835, 3302519, 1693517, 778655, 305292, 118236.

827: 126357200, 73807375, 40646383, 25693312, 14417512, 9123323, 4734690, 2955541, 1274070, 786030, 225052, 144665.

840: 140455073, 85610577, 50361189, 33435466, 20391097, 13705759, 8022488, 5381807, 2815510, 1892888, 793925, 548406, 137909, 116217.

We now verify the five sign conditions in Equation (B.20) for these data.

Bernstein bounds. For a polynomial in coordinates (u,v)\in[0,1]^2, of degree at most N in u and K in v, write R(u,v)=\sum r_{ij}u^iv^j. The formula of Appendix A gives its Bernstein coefficients of orders (N,K) as

The Bernstein enclosure proved in Appendix A puts the polynomial between the least and greatest coefficients on the full box. For a univariate polynomial set K=0 and omit the second coordinate.

For P start with [-1,1]; for E_B use [0,1]. For the other three polynomials use each consecutive pair of knots (a,c),(a+h,c+d) from Equation (B.21), in their actual rational units, and substitute

For each polynomial S to be checked, sufficient orders are N=\deg_{\mathrm{tot}}S and K=\deg_xS before substitution, because m^ix^j has u-degree at most i+j and v-degree j. These rectangles cover the entire closed domain. Subdivision bisects both coordinates. Equivalently, on a subdivided rectangle m\in[a,a+h], t\in[c,c+d], substitute

All these substitutions and Equation (B.23) are rational.

For the columns P,J,\mathcal V every final coefficient must be strictly positive. For the E_B column, on each interval with lower endpoint a, each negative coefficient e must instead satisfy

These two comparisons prove 1+s_1e(1+H(a))>0 with the sign checked before squaring. Since H(m)\leq H(a) on that interval and the polynomial is bounded below by its least Bernstein coefficient, this proves the second line of Equation (B.20) everywhere on the interval. If its least coefficient is nonnegative there is nothing to check.

For each row in Table 5, perform the five Bernstein checks with its listed depths and coefficients. The rational comparisons in Equations (B.23)–(B.24) all hold. One can stop early on boxes whose signs are already certified: subsequent Bernstein coefficients are convex combinations of the previous ones. This supplies a finite arithmetic verification of Equation (B.20). For completeness, the following integer scalings specify exactly how the accompanying Python certificate performs these rational calculations.

Exact integer scaling and subdivision. Put D_*=10^8, and write

The Chebyshev recurrence first forms the integer polynomials \widehat P=D_*P, \widehat B=D_*B. Applying the coefficient recipes following Equation (B.19) to \widehat B gives \widehat E=D_*E_B, \widehat A=D_*A, \widehat C=D_*C. The five polynomials supplied to the coefficient checker are

Thus their positive scale factors relative to the mathematical polynomials P,E_B,J_s,\mathcal V_s,\mathcal V_s are, respectively,

For an integer polynomial p(m,x)=\sum p_{ij}m^ix^j and an initial map

multiply the power coefficients after substitution by d_*^N. Explicitly add

to the coefficient of u^{k+l}v^j, for 0\leq k\leq i, 0\leq l\leq j. Transform the first axis by

and the second by T^{(K)}. The divisions are exact, since N!/\binom Ni=i!(N-i)!. The resulting integer matrix is d_*^NN!K! times its Bernstein coefficient array, a positive scale.

For an axis of order n, its left-half subdivision matrix has entries

with \binom{i}{k}=0 for k>i. This is 2^n times the usual de Casteljau half-subdivision. Reversing both row and column indices gives the right-half matrix. Apply both matrices on both axes at each subdivision, retaining their positive common factors. Order-zero axes have only one child. Positivity tests are therefore tests of integers.

For the E_B column with depth d, set q_*=2^d and, on [i/q_*,(i+1)/q_*], let c be the least integer coefficient produced by the preceding transformation with d_*=q_*. Its scale relative to E_B is D_*q_*^NN!. Define

If h_*\leq0, the test passes immediately. Otherwise the exact tests are

They are precisely Equation (B.24) for the minimum coefficient. This accounts for every factor of 1000, 2, and D_* in the certificate. Python uses unbounded integers and exact rational evaluation here, so integer overflow is not an additional hypothesis.

B.5 The three-coordinate base case

We finish by proving Lemma 3.4(4). An increasing function on fewer than three coordinates can be viewed as a function on three. Constants satisfy Equation (3.8) because G(0)=G(1)=B(\pm1)=0. Consider a nonconstant function whose positive set has size at most four. Up to coordinate permutations, a positive set of size one is the top vertex; one of size two adds one of its three neighbors; and one of size three adds two of those neighbors. A vertex with only one positive coordinate would force its entire upper subcube of size four to be positive. Hence a positive set of size four either is that subcube, giving a dictator, or consists of the three vertices with two positive coordinates and the top vertex, giving majority. Larger positive sets are obtained from these by the duality f^*(x)=-f(-x).

For a dictator, T_\rho f=\rho x_i and Equation (3.3) gives equality in Equation (3.8), since B(0)=1. For majority,

Again the asymmetric term averages to zero by input reversal. Evaluating the two absolute-value classes of T_\rho f gives

Indeed, s\sqrt{3+s^2}\ge2s^2 for 0\le s\le1, while, with u=s^2,

The resulting lower bound for the numerator is 33/4-s^2/4\ge8. Thus only the three unbalanced positive sets \{7\}, \{7,6\}, and \{7,6,5\} in binary coding (identify -1 with 0 and +1 with 1, then read the three bits as a binary integer), and their duals, require the scalar base certificates below. In particular the base assertion treats both orientations of B; no symmetry of B is assumed.

For D\in\{\{7\},\{7,6\},\{7,6,5\}\} put m_D=|D|/4-1 and \sigma_i=2\mathbf1_D(i)-1, where i\in\{0,\ldots,7\}. If d_{ij} denotes Hamming distance, define

A noise transition from i to an opposite point j has probability \delta^{d_{ij}}(1-\delta)^{3-d_{ij}}. Since s^2=4\delta(1-\delta), e_i is exactly the boundary-crossing probability. Thus d_i:=T_\rho f(i)=\sigma_i(1-2e_i), H(d_i)/s=h_i, and d_i/(1+H(d_i)\lambda(H(d_i)))=q_i. It follows that the two quantities to bound below are exactly

For the dual, global input reversal merely reindexes the average and negates its noised output, which explains the sign \eta in both places.

There is no division by s in Equation (B.27). Opposite points are distinct, so 1\leq d_{ij}\leq3; the sole possible negative power is (1-\delta)^{-1}, nonsingular over all the row intervals. These formulas have continuous extensions to s=0, even if I_i=0. In that limit I_i is one quarter of the number of opposite neighbors, e_i=0, h_i is the square root of that number, and q_i=\sigma_i. The two limits of \E G/s are, for the three listed sets in order,

Accordingly the first closed row interval is a valid domain for the normalized certificate, although Equation (3.8) itself only needs s>0.

For each profile row divide [s_0,s_1] into exactly 128 equal subintervals. On each, evaluate Equation (B.27) in the displayed order with the interval arithmetic at scale Q_*=10^{12} from Subsection B.2, and form the average in Equation (B.28). All signed profile evaluations B(\eta m_D) are exact rational numbers. The base column of Table 5 is a lower bound, simultaneously for all 128 intervals, all three sets, and both signs, for

Equivalently, compare 10^4(\text{interval lower bound}-B(\eta m_D)) directly with the listed integer. No approximate floor operation is needed. The 128 outward-enclosed intervals cover the entire row, including both endpoints. Every entry in the base column is positive, which proves Equation (3.8) for the unbalanced cases and hence for all increasing functions on at most three coordinates.

Together the pair-region certificates, the profile signs, and the base certificate prove all assertions of Lemma 3.4.