Context and main result

Strassen’s rank-seven algorithm for \(2\times2\) multiplication gave \(\omega\le\log_2 7\), establishing subcubic arithmetic complexity (Strassen 1969). Approximate bilinear algorithms and their conversion to exact algorithms (Bini 1980), Schönhage’s asymptotic sum inequality (Schönhage 1981), and Strassen’s laser method (Strassen 1987) made tensor powers and degenerations central to subsequent advances. Coppersmith and Winograd combined low-border-rank tensors with arithmetic-progression constructions (Coppersmith and Winograd 1990). Their extraction method restricts powers of a small tensor to direct sums of matrix products, whose dimensions enter the asymptotic sum inequality; their tensor-square analysis gave \(\omega<2.375477\) (Coppersmith and Winograd 1990, sec. 8). Higher powers and more detailed analyses of these tensors led to the improvements of Stothers, Vassilevska Williams, and Le Gall (Stothers 2010; Vassilevska Williams 2012; Le Gall 2014).

Rectangular multiplication requires separate control of the three matrix dimensions. Early work of Coppersmith and of Lotti and Romani developed this direction (Coppersmith 1982; Lotti and Romani 1983); later constructions of Coppersmith, Le Gall, and Le Gall and Urrutia improved the available rectangular and dual bounds (Coppersmith 1997; Le Gall 2012; Le Gall and Urrutia 2018). Recent advances include the refined laser method of Alman and Vassilevska Williams (Alman and Vassilevska Williams 2024), the asymmetric hashing of Duan, Wu, and Zhou (Duan et al. 2023), and the square and rectangular analyses of Vassilevska Williams, Xu, Xu, and Zhou (Vassilevska Williams et al. 2023) and Alman, Duan, Vassilevska Williams, Xu, Xu, and Zhou (Alman et al. 2025). The four-author work establishes \(\alpha\ge0.321334\); these two papers also give detailed tables of rectangular estimates. Dupont et al. subsequently optimized the asymmetric framework at a larger scale to obtain \(\omega<2.371177\) (Dupont et al. 2026), a bound incorporated into the updated table of (Alman et al. 2025).

The common extraction problem is to separate many candidate products that share variables, while accounting for the cost of every operation used to separate them. We adjoin auxiliary group tensors that both resolve shared labels and supply useful matrix-product factors. Their full rank cost enters the resulting inequalities. This construction gives the following bounds.

Corollary 52 transfers the strict square and \(k=0.709\) inequalities to every field of characteristic zero or outside one finite set of positive characteristics, in the same arithmetic-operation model. It selects two fixed exact rank schemes, realizes their coefficients over one number field, and specializes their polynomial identities. The exceptional primes are not computed. Corollary 53 also gives the same dual-exponent bound over every field of characteristic zero. No dual-exponent transfer in positive characteristic is asserted.

The square bound also lowers the arithmetic exponent of basic linear-algebra tasks. Given \(A\in\mathbb C^{n\times n}\) and \(b\in\mathbb C^n\), one can compute \(\det A\) and, when \(A\) is nonsingular, \(A^{-1}\) and the solution of \(Ax=b\), using \(O(n^c)\) field operations for some fixed \(c<2.258\), with exact zero tests for pivot selection. Choose \(\omega<c<2.258\) and apply the fast elimination reductions of Strassen (Strassen 1969) and Ibarra, Moran, and Hui (Ibarra et al. 1982, Theorem 2.1 and Corollary 2.1).

Two applications of the same separation lemma prove the theorem. The square bound uses finite tensor constructions, a differential comparison for their attainable values, and an exact numerical certificate. The dual and rectangular bounds come from explicit conditional-label trees and rational entropy certificates. We also optimize all leaf probability laws in a specified finite family of such trees, obtaining a bound for every aspect ratio in \([0,1]\). The square and rectangular construction families, and the precise way a square estimate augments the latter, are described below.

Separating labels with an auxiliary tensor

A trilinear tensor is a sum of monomials \(xyz\), with variables drawn from three finite coordinate sets \(X,Y,Z\). Its rank is the least number of products of three linear forms needed to express it. A restriction substitutes linear forms separately on the three sides. A degeneration allows parameter-dependent substitutions and takes a leading coefficient. Border rank is the least rank of tensors approaching the given tensor. These operations are local: a coordinate substitution cannot depend on information visible only on another side.

Suppose that the supported monomials carry \(K\) labels, and that each of two sides can independently determine the label from its own coordinate. The third side may still share variables between labels. The pairwise separation lemma, 7, tensors the input with a finite abelian group-addition tensor of rank \(K^{1+o(1)}\). Local projections then give a direct sum over the labels, with a size-\(K\) dot-product factor on the two original readers in every summand. The label is now visible on all three sides. Dot-product factors on the three possible reader pairs combine into a matrix multiplication tensor.

The construction combines Fourier diagonalization of the group tensor with tags of equal Euclidean norm and a separate constant-inner-product slice for each tag. Its geometry adapts Behrend’s construction (Behrend 1946), following the progression-free constructions of Salem and Spencer (Salem and Spencer 1942). The use of group algebras also has an established place in the approach of Cohn and Umans (Cohn and Umans 2003); the local separation identity needed here is proved in full. It preserves every original coordinate and coefficient, including additional tensor indices correlated across occurrences. Consequently the same identity can be applied inside a previously restricted tensor. A separate support argument ensures that every summand counted in an application is nonzero.

Successive separations are organized by exact conditional counts. Once a preceding label is direct on all three sides, each side can locate the positions on which the next operation acts. Fixing the number of each possible continuation makes the next auxiliary tensor and the output dimensions common to all branches. The multinomial counts and entropy chain rule are the standard method-of-types tools (Shannon 1948; Csiszár 1998); locality and the uniform tensor accounting are proved alongside them here.

The square bound: finite constructions and comparison

The square argument starts from the six-term Coppersmith–Winograd tensor \[T=\sum_{\substack{i+j+k=2\\0\le i,j,k\le2}}x_i y_j z_k,\] which has border rank three (Coppersmith and Winograd 1990, sec. 7, equation (10)). A five-term degeneration of \(T\) has three groups, each detectable on one designated side. A local degeneration of three copies retains \(75\) scalar components. Separating their successive labels gives the elementary estimate \(\omega\le9\log3/\log75<2.290108\) in 11. This example displays the auxiliary-rank accounting before the larger construction is introduced.

For a proposed exponent \(\beta\), suppose a finite construction from \(n\) copies of \(T\) and an auxiliary tensor of border rank at most \(R\) produces \(L\) independent matrix products of common dimensions \(a\times b\) by \(b\times c\). Its normalized score is \[\frac{\log L-\log R+(\beta/3)\log(abc)}{n}.\] Schönhage’s asymptotic sum inequality implies that a score strictly greater than \(\log3\) proves \(\omega<\beta\). Thus the square argument must produce a strict score gain while retaining the entire auxiliary charge.

We organize the finite constructions by their source distribution. There are six collections of original tensor occurrences, called orientation banks, one for each permutation of the three sides. The distribution records the same exact frequencies in the original coordinates of each bank. This keeps a physical permutation of a tensor distinct from a change of its recorded law. The square sections use \(\alpha\) for this vector-valued source law; the dual exponent in 1 is a scalar. A construction preserves arbitrary unresolved tensors attached to its original words, and its output labels identify distinct surviving words. Taking the closure of the finite law–score pairs gives a continuous concave attainable-value function. Conditional pooling and a new application of the group separator to each longer pool provide the composition properties needed in the comparison.

The key analytic step uses restrictions on sums of the local grades \(i,j,k\). Each side can read its own sum. Windows placed at progression-free target indices force the three locally read targets to agree, creating another direct label. The progression-free construction and the matching argument have the ancestry of Behrend and Coppersmith–Winograd (Behrend 1946; Coppersmith and Winograd 1990). To exploit the new labels, a finite-horizon control steers every word allowed by its controls into the assigned terminal window. This every-word guarantee is what permits all the resulting tensor summands to be counted. Exact rational prefix populations then translate the finite control tree into local tensor maps with common auxiliary supplies.

This construction forces a differential inequality on any smooth function touching the attainable value from below. The covariance of the local grades determines the weighted combination of second derivatives in this inequality. Smooth touching tests and strict comparison follow the viscosity-solution methodology of Crandall and Lions and of Crandall, Ishii, and Lions (Crandall and Lions 1983; Crandall et al. 1992); the required inequality and comparison are proved directly from the finite tensor constructions. A rational polynomial chart and a polynomial barrier then give the strict score gain at an interior source distribution. Boundary constructions supply the initial lower estimates, while explicit residual, interpolation, and rounding bounds turn the finite integer checks into inequalities on the entire comparison domain.

Finally, a strict gain in the closed attainable set selects one actual finite construction with score greater than \(\log3\). Its law may be close to the chart’s central law. All control horizons, rational approximations, group sizes, and bank sizes are fixed before the asymptotic sum inequality is applied.

Rectangular bounds and finite-family optimization

The rectangular argument tracks the three matrix dimensions separately. A readable label tree partitions a tensor’s support until each leaf is one monomial; at every node, conditional on the preceding labels, the next child is independently readable on two specified sides. Fix a rational probability law on its leaves and apply the tree to an admissible number of copies with those exact leaf frequencies; arbitrary leaf laws follow by approximation. The number of child words at a node is a multinomial coefficient. The product of these coefficients is exactly the number of final direct summands, so the leading auxiliary rank charge is canceled by this multiplicity in the equal-summand inequality. The three remaining logarithmic dimensions are the conditional entropies accumulated on the three reader pairs. This is 40.

Explicit polynomial degenerations giving border-rank bounds two and three supply the initial trees. Their supports have three colors, with a designated side able to detect its own color. A completion takes several copies, chooses a center color, and retains color words containing at most one distinct noncenter color. Local color tests implement this leading-term degeneration and preserve the conditional trees. Deleting one color at the end gives a fully readable tree. The family \(\mathcal F_7\) consists of both bases, at most seven completions of sizes two or three, all center choices, all pairs of retained colors, and all choices of a distinguished side.

For each member of this finite family, a three-state recurrence maximizes every nonnegative weighted sum of its incident and nonincident conditional entropies over all leaf laws. Its support function therefore describes the closed downward convex hull of the normalized rate pairs exactly. 46 turns this description into a maximization over one real parameter for each aspect ratio. An available square estimate contributes one additional rate point. In particular, the square part of 1 supplies the point for \(p=2.258\). This finite-family optimization is distinct from the square attainable-value construction with orientation banks and count windows.

Two explicit laws give the dual and rectangular conclusions. For the dual exponent, an exact conditional-independence identity preserves all the entropy of a uniform coordinate word on its incident reader pairs. This equality certifies exponent two, and the remaining entropy certifies the inner dimension. A small fiber histogram gives the rectangular point. Rational enclosures establish their strict numerical margins. The same finite family also gives an independent square bound below \(2.267\) by an integer leaf count.

13 compares the resulting bounds with the specified numerical tables of (Vassilevska Williams et al. 2023; Alman et al. 2025), augmented by the same square point \(p=2.258\) and closed under the ordinary combination operations stated there. The new bounds strictly improve this table baseline for \(0.321334<k<1\). This comparison concerns recorded upper estimates. Extensions to additional estimates retain their stated separator or envelope hypotheses, and strict improvement is asserted only where the enlarged baseline itself exceeds two.

Organization

2 establishes the tensor and arithmetic-exponent conventions. 3 proves the shared separation lemma and the finite tensor constructions. The square argument begins in [val:section,ap:section], which define the attainable values and prove the count-window comparison. 6 establishes the three-state boundary estimate used by the numerical certificate in 7. 8 extracts the finite witness proving the square part of 1. [sec:trees,sec:completion,sec:optimization] develop conditional entropy, completion trees, and exact finite-family optimization. 12 proves the remaining parts of 1, and 13 gives the baseline comparisons. Section 14 proves the finite-exception field corollary from two exact rank witnesses and the characteristic-zero dual corollary using accuracy-dependent witnesses. The appendices give barrier coefficients and reproduction details.

Pairing conventions and the input rank

We use the tensor and matrix-dimension conventions of Section 2. A pairing on \(X,Y\) of length \(m\), with a scalar third side, is \(\langle1,m,1\rangle\); the other orientations are \(\langle m,1,1\rangle\) on \(X,Z\) and \(\langle1,1,m\rangle\) on \(Y,Z\). Their tensor products satisfy \[ \langle a,1,1\rangle\otimes\langle1,b,1\rangle \otimes\langle1,1,c\rangle\cong\langle a,b,c\rangle. \tag{3}\] The logarithmic volumes of such factors therefore add.

The input is the six-term specialization of the Coppersmith–Winograd tensor (Coppersmith and Winograd 1990, sec. 7, equation (10)), \[ T=CW_1=x_2y_0z_0+x_0y_2z_0+x_0y_0z_2 +x_0y_1z_1+x_1y_0z_1+x_1y_1z_0. \tag{4}\] Write \(\mathcal S=\{200,020,002,011,101,110\}\) for its support, abbreviating \((i,j,k)\) by \(ijk\). At every position the three indices sum to two. The maps in our square construction for this input have algebraic coefficients. The general preservation identities below also allow arbitrary complex coefficients in the unresolved tensors.

We use the following established theorem in exactly its border-rank form; see also the explicit statement in Ambainis et al. (2014, Theorem 3.1).

The auxiliary rank \(R\) in (5) is part of the input cost. Thus, for a proposed exponent \(\beta\), a finite realization with \[ \log L-\log R+\frac{\beta}{3}\log(abc)>n\log3 \tag{6}\] proves \(\omega<\beta\). We never cancel an auxiliary tensor as a tensor identity; only its explicitly charged logarithmic rank will be offset by output multiplicity.

Supplying a label to its missing party

Suppose a tensor is partitioned into pieces whose \(X\)-variables are disjoint and whose \(Y\)-variables are disjoint. Each of these two parties can then determine the same piece label from its own variable. The \(Z\)-variables may still be shared. The next lemma resolves this last sharing without resolving the terms inside a piece. We call this operation GROUP.

The construction uses equal-norm shells, following the geometry of Behrend (1946), together with affine slices that constrain two independently chosen auxiliary indices. Its auxiliary tensor is the multiplication tensor of a finite abelian group, linking the construction to the group-theoretic tensor approach of Cohn and Umans (2003). The identity and its full rank charge are proved below.

For repeated uses at different label counts, fix one such group \(G_K\) for each \(K\), and write \(A_K=\mathcal A_{G_K}\). This is the auxiliary-tensor notation used in the conditional-label entropy bound.

The geometry rules out a stronger collision than the usual three-term-progression condition: the two slice points \(u,u'\) are chosen independently. Their difference is perpendicular to \(t_s\); any nonzero such displacement from \(t_s\) lies outside its sphere. Requiring the endpoint to be another tag therefore forces that difference to vanish. Figure 1 shows this displacement argument.

This preservation statement is a locality statement, not a nonvanishing statement. If an earlier support restriction makes a designated source word absent, its fiber is zero and cannot be counted as an output. Our finite constructions below explicitly retain every counted word. The later count construction will require a separate guarantee for every complete controlled path.

Exact types and a finite hierarchy of labels

For a probability vector \(p\) on a finite alphabet, write \(H(p)=-\sum_i p_i\log p_i\), with \(0\log0=0\). Exact types provide the finite counting form of entropy used here; see Csiszár (1998) for the method of types. For rational \(p\) and admissible integers \(N\), the number of words having exactly \(Np_i\) occurrences of symbol \(i\) is \[ \binom{N}{(Np_i)_i} =\exp\bigl(NH(p)+O(\log(N+1))\bigr). \tag{9}\] The implicit constant depends only on the fixed alphabet. We use exact types so that the number of positions assigned to every later conditional operation is independent of the previously selected direct output.

The following lemma makes precise how multiple separation steps share auxiliary tensors and count each label once. Its accounting is the conditional-entropy chain rule (Shannon 1948), applied to labels that the tensor maps can actually read.

Nothing in this lemma permits arbitrary support deletion. The locally obtainable support and the two-sided readability must be established for each hierarchy. Once they are established, exact conditional types select its desired joint frequencies through accessible labels.

An explicit four-component construction

First remove the term \(101\) from \(T\). Scale each of \(x_1,z_1,y_0,y_2\) by \(t\). The five other terms have degree one in \(t\), whereas \(101\) has degree three. Dividing by \(t\) and taking the limit gives \[ T\unrhd T'=A+B+C, \quad A=x_0(y_0z_2+y_1z_1),\quad B=(x_2y_0+x_1y_1)z_0,\quad C=x_0y_2z_0. \tag{11}\] A local predicate on each side identifies exactly one group: \(Z>0\) identifies \(A\), \(X>0\) identifies \(B\), and \(Y=2\) identifies \(C\). Exactly one of these predicates holds on every retained term. We call any such three-group partition a W-partition; the three predicates, rather than the original numerical indices, are its one-hot flags.

Delete \(C\) by setting \(y_2=0\), and take \((A+B)^{\otimes N}\), with \(4\mid N\). Retain coarse words with \(N/2\) copies of \(A\) and \(N/2\) copies of \(B\). This is local on \(X\), since a zero \(X\) index means \(A\) and a positive one means \(B\). The \(Z\) side also identifies the word, with the roles reversed. There are \(\binom{N}{N/2}\) coarse words. Lemma 7 separates them by supplying their label to \(Y\), and gives each word a pairing on \(X,Z\) of logarithmic length \(N\log2+o(N)\).

Inside a fixed coarse word, \(A\)’s two terms \(002,011\) are each identified by \(Y\) and by \(Z\). Retain \(N/4\) occurrences of each among the \(N/2\) \(A\) positions and separate their words. This adds a pairing on \(Y,Z\) of logarithmic length \((N/2)\log2+o(N)\). Similarly, \(B\)’s two terms \(200,110\) are each identified by \(X,Y\); resolving their equal-frequency words adds a pairing on \(X,Y\) of the same logarithmic length. These restrictions are conditional on the already-direct coarse word and therefore are local.

The three pairings combine by (3). The total logarithmic output count, auxiliary rank, and volume are each \(N\log4+o(N)\). Theorem 6 consequently gives \[ \omega\leq\frac{3\log3}{\log4}=2.377443751\ldots. \tag{12}\] The scalar original terms alone would not supply any volume to which \(\omega\) could be applied. Here the three pairing orientations supply that volume, while all three auxiliary rank costs have been included.

Completion and the 75-component bound

A W-partition has a useful local description even when its three groups contain unresolved tensors: side \(i\) knows precisely the positions at which its own group occurs. This permits a degeneration of a block of several occurrences before any group has been made direct. We call the following operation COMPLETE.

For the groups \(A,B,C\) in (11), assign labels \(0,1,2\) in that order. The group sizes are \(2,2,1\). A completed block has three group sizes \[2^b,\qquad4^b-2^b,\qquad3^b-2^b.\] Delete its all-\(A\) group: its active \(Z\) predicate is that every original index is positive. The remaining groups will be denoted \(P_B\) and \(P_C\). The \(X\) side recognizes \(P_B\) by the occurrence of a positive index, and the \(Y\) side recognizes \(P_C\) by the occurrence of index two. Since only these two groups remain, either side independently determines which group occurs.

The neighboring block lengths illustrate that this particular completion is not monotone in \(b\):

No optimization claim over all restrictions of the corresponding power is needed. The length-three construction already gives the stated bound.

Parity and conditional W constructions

Completion gives one way of making a new W-partition. A different local restriction on three occurrences supplies two useful W labels, which can be resolved in either order. We call this operation PARITY.

If the three occurrences have internal scalar counts \((a_i)_i,(b_i)_i,(c_i)_i\), the fiber with majority \(i\) and odd-count label \(j\) has size \[ M_{ij}= \begin{cases} a_ib_ic_i,&i=j,\\ a_ib_ic_j+a_ib_jc_i+a_jb_ic_i,&i\ne j. \end{cases} \tag{15}\] Each term for \(i\ne j\) describes one singleton placement. For the boundary weights \((2,2,1)\) on all three occurrences, this is \[(M_{ij})=\begin{pmatrix}8&24&12\\24&8&12\\6&6&1\end{pmatrix}.\] For example, delete the third majority row and resolve the remaining binary majority label. Within the first direct row delete its first odd-count column; within the second direct row delete its second column. These are permitted conditional local deletions because the majority is already direct. Each row then has size 36, giving 72 original scalar components. Lemma 9 yields \(\omega\leq9\log3/\log72=2.311966920\ldots\). This illustrative restriction is weaker than Theorem 11. Parity is useful because its two conditional groupings enlarge the finite construction family at nonuniform distributions.

Finite recipes and weighted laws

We now track the source law and score of a finite tree of W constructions. Fix labels \(0,1,2\) on each original W-partitioned occurrence before applying the tree. These are its canonical labels: later physical permutations may change which side reads a flag, but the original labels are still counted in this fixed ordering.

For the score calculations below, fix a finite operation tree and its rational conditional laws. Admissible exact-type populations, together with the efficient GROUP tensors of (8), give a family of finite realizations. The limiting score of this fixed tree and law data is the limit along increasing populations; each member remains one finite recipe with fixed tensor supplies and maps. A later operation may depend on a label only once that label is direct on all three sides. At every stage, previously produced pairings are separate tensor factors; their internal indices are never used to choose subsequent controls.

For a realization on \(n\) original occurrences, let \(L\) be its direct multiplicity, \(R\) its auxiliary rank bound, and \(v\) its additional matrix multiplication volume. The rates are \[D=\frac{\log L}{n},\qquad A=\frac{\log R}{n},\qquad M=\frac{\log v}{n}.\] Here \(M\) excludes any tensor initially present inside a coarse group. For the W recipes the convenient formal score is \(u_\gamma=\gamma(D-A)+M\), where \(\gamma\geq1\). For \(0<\beta\leq3\), \[u_{3/\beta}=\frac3\beta\left(D-A+\frac\beta3M\right).\] Thus \(u_\gamma\) rescales the normalized score expression in (6) so that the coefficient of the added volume is one. Its definition assumes no bound on \(\omega\). Definitions 16 and 17 will specify the banked realizations and the closure of their law–score pairs. For a fixed tree consisting only of pairwise separation, completion, parity, and conditional exact types, its total \(D-A\) tends to zero when the group/type supplies grow. Consequently its limiting score is independent of \(\gamma\).

A binary leaf deletes one W label locally and resolves the remaining binary word by Lemma 7. At law \(q\) on that pair, its limiting score is \(H(q)\). If positive numbers \(d_i\) are assigned as weights for choosing a law, the weighted score is \(H(q)+\sum_iq_i\log d_i\). Maximizing on the retained pair \(i,j\) gives \(\log(d_i+d_j)\). These weights may guide selection of a finite rational law; they do not change the coefficients of a tensor.

For completion of \(b\) occurrences with weights \(d_{r,i}\), the three fiber weights are \[ w_0=\prod_{r=1}^b d_{r,0},\qquad w_i=\prod_{r=1}^b(d_{r,0}+d_{r,i})-\prod_{r=1}^b d_{r,0} \quad(i=1,2). \tag{16}\] When the weights are scalar term counts, this is literal counting of the supports in Lemma 10. For arbitrary positive weights it is the corresponding generating polynomial. For parity the analogous matrix is (15).

Physical orientations and canonical laws

A physical permutation acts on the full tensor factors of an occurrence or completed block. Each original occurrence keeps both its canonical label and its net physical side permutation. For \(\sigma\in\mathfrak S_3\), the orientation bank \(\sigma\) is the collection of original occurrences with that net permutation relative to their canonical coordinates. We will arrange that all six banks have the same exact canonical label histogram. Their common normalized histogram is the source law; it is not the aggregate law of the physical flags after the bank orientations are forgotten.

The exact types used below fix canonical histograms within each relative orientation. The next lemma shows how the six global physical permutations then distribute these counts equally among the original banks, while keeping one common auxiliary supply.

In particular, rotating the flags of an intermediate completed block changes its grouping and its readers, but does not recode the labels of the original occurrences inside it. To recover a canonical label from a physically permuted occurrence, undo that occurrence’s permutation.

Resolving and composing nested recipes

An operation in the finite library may complete two occurrences, physically transpose that completed block, and then complete it with a third occurrence. Resolving its original word calls for a hierarchy inside the final fiber. The following statement supplies that hierarchy for any fixed finite composition of completion gates.

To spell out the three-position case used in the library, let \(c(i,j)\) be the two-child completion label: it is zero for \((i,j)=(0,0)\), and is \(a\in\{1,2\}\) if both entries belong to \(\{0,a\}\) and at least one equals \(a\). It is undefined on \((1,2),(2,1)\). Write \[a=c(i,j),\qquad z=a-k\pmod3,\qquad s=c(z,r), \quad k\in\{0,1,2\}.\] The subtraction by \(k\) represents the physical rotation of the whole first completed block. In a fixed final fiber \(s\), first resolve the top-level operand labels \((z,r)\). This fixes \(a=z+k\pmod3\), after which the inner word \((i,j)\) can be resolved using the pair of sides belonging to that inner completion, with its physical rotation included. If \(C_s\) is an arbitrary rational law on the retained triples, the two levels supply \[ H(C_s)=H(Z,R\mid S=s) +\sum_{z,r}\mathbb P(Z=z,R=r\mid S=s) H(I,J\mid Z=z,R=r,S=s). \tag{17}\] Here \(Z\) is a deterministic function of \(I,J\), so no intermediate label adds a second entropy count. The intermediate rotation changes the grouping flag and its physical reader; it does not recode \(I,J,R\) when the original canonical word histogram is calculated.

The words in (18) are counted in their original canonical coordinates. The resulting \(q\) is the exact common law of the original orientation banks, providing the finite input to the banked-value construction of the next section.

Canonical banks and preservation of unresolved tensors

Let \(\mathcal S=\{200,020,002,011,101,110\}\) and \(\mathcal W=\{100,010,001\}\). The latter is the support of the ordinary three-state tensor \[\mathsf W=x_1y_0z_0+x_0y_1z_0+x_0y_0z_1.\] An element of either alphabet is a triple of local grades. We use \(\mathcal B\) to denote either alphabet in definitions that apply to both. Write \(\mathfrak S_3\) for the group of permutations of the three tensor sides. A banked input of size \(N\) has \(N\) occurrences in each orientation \(\sigma\in\mathfrak S_3\), for a total of \(n=6N\) occurrences. Its original component words are \[w=(w_{\sigma,t})_{\sigma\in\mathfrak S_3,\ 1\le t\le N}, \qquad w_{\sigma,t}\in\mathcal B.\] The triple \(w_{\sigma,t}\) is expressed in canonical coordinates: its physical grade triple is \(\sigma w_{\sigma,t}\). Thus physical side \(j\) observes the canonical coordinate \(\sigma^{-1}(j)\). Both \(T\) and the ordinary \(\mathsf W\) tensor are symmetric under these physical permutations, so this banking does not change the underlying input tensor. Its purpose is to record types and permitted transposes accurately.

A banked word has exact law \(\alpha\in\Delta(\mathcal B)\) if, separately for each \(\sigma\), every symbol \(s\) occurs \(N\alpha_s\) times. In particular, \(\alpha\) is not the histogram obtained by forgetting the bank orientations. All normalizations below divide by \(6N\).

We allow additional, unresolved local indices. To state the preservation requirement precisely, for every original component word \(w\) attach an arbitrary three-tensor \(P_w\) on these additional indices. The tensors \(P_w\) may share their variable spaces, may correlate all the positions, and may be zero. Denote the resulting input by \(\mathcal T(P)\): its restriction to the original word \(w\) is the original scalar component at \(w\) tensored with \(P_w\). This description includes preceding local count restrictions by setting the corresponding fibers to zero. It does not assert that all such families arise as independent products.

The maps in this paper retain each original local index and act on auxiliary coordinates conditionally on that index and on already direct labels. Consequently they commute with local projections depending only on the original indices. The same statement holds when the maps are expressed as leading monomial degenerations. This observation concerns locality; it does not prove nonvanishing after an earlier projection. Nonvanishing will be checked by support identities for the algebraic primitives and by the universal path condition in Lemma 28 for arithmetic-progression (AP) count constructions.

Lemma 7 supplies (20) term by term. Indeed its sphere and slice argument decides the retained auxiliary terms without referring to any coefficient of \(P_w\). Local singleton projections and direct matchings have the same preservation property. The conditional composition rules of Section 4.2 use only these identities; they never presume independence of unresolved fibers.

For the banking operation of Lemma 13, group the original input occurrences of a finite schedule by their relative physical orientation \(\tau\). The lemma requires their total canonical histogram \(H_\tau\) to be fixed independently of the direct history and shared by all six globally permuted replicas. Exact types of complete original words supply these grouped histograms in the completion and parity recipes. When an already strong child is physically permuted as a whole, each of its original input banks supplies a fixed histogram by Definition 16. The letter at an individual position may still vary between direct outputs.

In outer replica \(\sigma\), the group of relative orientation \(\tau\) has absolute orientation \(\sigma\tau\). Each absolute bank therefore receives one copy of \(H_\tau\) for every \(\tau\), and has histogram \(\sum_\tau H_\tau\). Equal conditional pool sizes alone would not imply this histogram identity. The pool sizes instead fix how many child calls and auxiliary supplies are used; the grouped types or strong child banks supply the required letter counts. A physical permutation of an intermediate macro acts on every original occurrence inside it.

Finite recipes and the closure of their values

A structural recipe is a finite expression describing local projections and leading degenerations, direct-label-controlled maps, locally imposed exact joint and conditional types, auxiliary GROUP calls, and tensor products on specified collections of positions. Its bank sizes, rational types, and integer group parameters are finite. A conditional choice is permitted only after its controlling label is direct on all three sides. Each byproduct matrix multiplication factor is kept as a separate factor: later decisions use original-word labels and do not read, identify, or spend its indices.

We use the following two classes of such recipes.

1. The \(\mathsf W\) class starts with singleton projections, binary deletion followed by GROUP, and the finite COMPLETE and PARITY compositions of Proposition 15. It allows rational time-sharing on separate positions, physical permutation banking, and finite AP count compositions of previously constructed recipes.

2. The six-state class starts with singleton projections, the direct matching construction of Proposition 24, and the five-state face substitutions of Proposition 25 using finite \(\mathsf W\) recipes. It has the same time-sharing, banking, and finite AP closure.

Both classes also allow two explicit finite rearrangements. First, one may reindex the orientation banks by \(\sigma\mapsto\sigma\tau\) for a fixed \(\tau\in\mathfrak S_3\), with the corresponding canonical letter relabeling; Lemma 19 proves its precise effect. Second, one may conditionally recompile an earlier finite recipe: expand its finite direct-label refinement tree, take finitely many replicas, impose a rational exact type of complete terminal transcripts through its induced conditional types, and replace corresponding GROUP calls by GROUP on the longer conditional pools. All other original support predicates are retained on their old macroblocks. This is a finite construction rule using the same local primitives, not an operation on scores. Its instances must preserve Definition 16 and nonzero support like every other recipe; Lemma 21 proves those requirements for the uniform terminal type used below. Neither rearrangement authorizes an infinite composition.

Here an AP composition is the finite count-window construction of Lemma 28. Its children are finite recipes, not calls to an attainable-value function. The full expression can therefore be expanded to a finite tree. Equivalently, take the union of all finite levels of this construction rule. The \(\mathsf W\) class is defined independently of the six-state class.

A recipe belongs to these classes only when its local identities establish Definition 16, its counted original words survive all of its restrictions, and its auxiliary profile and output dimensions are fixed across its direct histories. These are algebraic conditions, not inequalities for numerical scores. The primitive support proofs, exact conditional-type composition, and Lemma 28 establish these conditions for the listed generators. In particular, introducing the AP closure here does not assume the differential inequality that it will later prove.

The auxiliary tensor in every recipe is a product of finite group tensors. We charge the product of their ranks, which is also their tensor product’s rank by Fourier diagonalization and flattening. It is harmless to charge a larger certified bound. No tensor already present in an unresolved fiber is included in the byproduct volume.

For a realization with \(n=6N\) original occurrences, \(L=|\Lambda|\) counted nonzero direct summands, auxiliary rank bound \(R\), and common additional volume \(v=abc\), put \[ D=\frac{\log L}{n},\qquad A=\frac{\log R}{n},\qquad M=\frac{\log v}{n}. \tag{21}\] For \(0<\beta\le3\) and \(\gamma\ge1\), respectively, the two scores are \[ f_\beta=D-A+\frac\beta3M, \qquad u_\gamma=\gamma(D-A)+M. \tag{22}\] These are formal tensor rates. Their definitions impose no assumption on \(\omega\). In particular, on the same realization \(u_{3/\beta}=(3/\beta)f_\beta\).

Allowing smaller scores makes these sets downward closed. The closure allows irrational laws and limits of finite recipes of increasing size; it does not introduce an infinite composition acting on a finite tensor. In particular, if \(F_\beta(\alpha)>c\), then some actual finite realization has score greater than \(c\), possibly at a law arbitrarily close to \(\alpha\).

Conditional pooling and monotonicity in the formal parameter

A finite GROUP call pays a small excess of auxiliary rank over its number of labels. Tensor-repeating that particular finite map does not remove its normalized excess. The following lemma replaces each GROUP call by a new one acting on a long conditional pool. It is the requisite justification for monotonicity in \(\gamma\). The face substitution below evaluates the W value at \(\gamma=3/\beta\); monotonicity will let the certificate use a lower estimate obtained at a smaller formal parameter.

A direct matching lower bound

The first boundary estimate separates original scalar components without an auxiliary tensor. The matching argument uses progression-free hashing and collision removal as in Coppersmith and Winograd (1990, sec. 6); we give the details with the bank normalization needed here.

The five-component face

On one face the six-state tensor has a genuine three-state \(\mathsf W\) partition. The remaining distinctions within its coarse groups must be separated only after that partition has been resolved. This gives the second boundary estimate used in the certificate.

Locally readable target windows

We require many target indices with no nonconstant three-term arithmetic progression. We use the integer form of the progression-free set construction of Behrend (Behrend 1946), proved in Lemma 23. Using such labels to separate tensor products follows the progression-free extraction method of Coppersmith–Winograd (Coppersmith and Winograd 1990, secs. 4–7); the count-window restriction needed here is given explicitly below.

For a length-\(n\) word with grades \(g_1,\ldots,g_n\), its centered grade sum is \(\sum_{t=1}^n(g_t-\mu_0)\). Use the targets \[ y_j^{\mathrm{grade}}=(j,j,-2j)\sqrt n/L, \qquad j\in J, \tag{36}\] and coordinate windows with radius \(\rho=\sqrt n/(10L)\). Each side reads its own centered sum. Because the three centered sums add to zero, a retained triple whose three local window labels are \(j_0,j_1,j_2\) satisfies \[|j_0+j_1-2j_2|\leq3/10.\] The left side is an integer, and hence is zero. The progression-free property gives \(j_0=j_1=j_2\). Windows are disjoint on every side, including the side whose target spacing is twice as large. Thus a nonzero retained tensor has a shared direct target label.

In a physical orientation bank \(\sigma\in\mathfrak S_3\), the mean \(\mu_0\), the target vector, and the local windows are all permuted by \(\sigma\). The coordinate-sum test is expressed in canonical coordinates. A physical side reads the corresponding permuted coordinate. The coordinate-sum argument is unchanged, so the target remains shared. There is no averaging of the canonical grade covariance across orientations in this operation.

Exact finite compilation

At each target and prefix, a control specifies a probability law on the source alphabet and a cost. A permitted path chooses at every step a letter in the prescribed law’s support. In the next lemma, every node law and utility must be supplied by an earlier finite strong realization. The lemma turns these realizations into tensor maps when every permitted path ends inside its assigned target windows. It is useful to state it for either alphabet, and with a general coefficient \(\lambda>0\) on the direct-label logarithm. For the six-state score \(D-A+(\beta/3)M\) this coefficient is \(\lambda=1\); for the W score \(\gamma(D-A)+M\) it is \(\lambda=\gamma\).

The exact populations and multinomial entropy estimates use the method of types (Csiszár 1998, sec. II). The proof also establishes the local tensor maps, their uniform auxiliary supply, and nonvanishing of every counted output.

For any affine functional \(\ell\), define the node cost by \(c_v=\ell(q_v)-u_v\). The prefix weights sum to one at each time, so the averaged law in the lemma satisfies \[\frac1n\sum_v w_v\ell(q_v)=\ell(\overline q).\] Thus (37) has the equivalent form \[ u_{\mathrm{out}} \geq\ell(\overline q) +\frac{\lambda H(a)-\mathbb E\sum_{t=1}^n c_t}{n}. \tag{39}\] The expectation denotes the finite sum \(\sum_v w_vc_v\). For the six-state supporting plane fixed above, \(\lambda=1\) and every node cost is nonnegative. To contradict that plane, it is therefore enough to send every permitted path into its window while keeping the expected cost strictly below \(H(a)\). The remaining argument constructs such controls from a failed lower test.

A lower test supplies inexpensive small drifts

At a lower contact, \(\ell\circ\alpha-\varphi\) has a local minimum zero. Thus its first derivative vanishes and \[ Q_0=g_*\cdot D^2\alpha(\mu_0)-D^2\varphi(\mu_0)\succeq0. \tag{40}\] If (35) fails, \(\mathop{\mathrm{Tr}}(Q_0C(\alpha_0))<1\). Choose \(\varepsilon>0\) so small that \[ Q=Q_0+\varepsilon I\succ0, \qquad \tau=\mathop{\mathrm{Tr}}(QC(\alpha_0))<1. \tag{41}\] Taylor’s theorem and \(\varphi\leq h\circ\alpha\) give, after reducing the neighborhood if necessary, \[ 0\leq c(v):=\ell(\alpha(\mu_0+v))-h(\alpha(\mu_0+v)) \leq \frac12v^\top Qv. \tag{42}\] By the definition of the closed attainable set, the law and utility in this display can be approximated simultaneously, to any prescribed positive accuracy, by a finite earlier construction. We postpone these finitely many approximations until the entire control tree has been fixed.

Transform centered grades by \(Q^{1/2}\). A grade \(g\) then gives the increment \(X=Q^{1/2}(g-\mu_0)\). A small prescribed mean \(m\) is obtained by taking the law \(\alpha(\mu_0+Q^{-1/2}m)\). We call these chart laws soft controls; their ideal cost satisfies \[ c(m)\leq |m|^2/2. \tag{43}\] There is a fixed bound \(B>0\) on the magnitude of every increment, and \[ \mathbb E|X|^2\longrightarrow\tau\quad\hbox{as }m\longrightarrow0. \tag{44}\] The limit concerns the second moment, which equals the covariance trace at mean zero.

We also allow exact singleton controls. The point \(\mu_0\) is in the relative interior of the grade convex hull, so there is a \(\kappa>0\) such that for every unit vector \(u\in\mathcal P\), one singleton increment satisfies \(u\cdot X\leq-\kappa\). Its utility is zero. The costs of the finitely many singleton choices have a finite common upper bound \(C_*\).

A control that retains every path

We now construct controls for the bounded increments just described whose cost is smaller than the target-label gain in (39). The terminal guarantee must hold for every permitted path. Soft controls will be made safe for every letter in the entire source alphabet, so later rational approximation cannot create an unsafe new outcome.

The contradiction and the order of limits

Write \(U_\gamma=U^W_\gamma\) for the three-state attainable value.

The following interior-maximum argument is the strict-comparison strategy of viscosity-solution theory (Crandall et al. 1992, sec. 5.C). Its short proof uses the lower-test inequalities just established.

Controlling the supporting-plane term

The lower-test inequality retains \(g\cdot\mathcal L\alpha\) when the chart is not exactly harmonic. Although the supporting supergradient is unknown, concavity and a uniform value bound control this term. The certificate will apply the following estimate where every chart coordinate has a positive lower bound.

The affine chart and the baseline

For \(q=(q_0,q_1,q_2)\) in the probability simplex, set \[ z=\frac{3q_0-1}{2}+\frac{\mathrm i\sqrt3}{2}(q_2-q_1), \qquad q_i=\frac{1+2\operatorname{Re}(\zeta^i z)}3, \qquad \zeta=e^{2\pi\mathrm i/3}. \tag{53}\] The three deterministic laws correspond to \(1,\zeta^2,\zeta\). If \(Z\) takes these values with probabilities \(q_0,q_1,q_2\), respectively, then \(\mathbb EZ=z\), \(\mathbb EZ^2=\bar z\), and \(\mathbb E|Z|^2=1\). Thus the full covariance contraction, with \(\partial_z=(\partial_x-\mathrm i\partial_y)/2\), is \[ \mathcal L_W = (\bar z-z^2)\partial_z^2 +2(1-z\bar z)\partial_z\partial_{\bar z} +(z-\bar z^2)\partial_{\bar z}^2. \tag{54}\] There is no factor \(1/2\) in this formula. Equivalently, in affine simplex coordinates it is \((\mathop{\mathrm{diag}}(q)-qq^{\mathsf T}):D^2\).

Define \[ F_0(q)=(\gamma _0-1)\sum_{i=0}^2\mathop{\mathrm{en}}(q_i) +(2-\gamma _0)\sum_{i=0}^2\mathop{\mathrm{en}}(1-q_i). \tag{55}\] Since \(\mathop{\mathrm{en}}''(t)=-1/t\), the diagonal covariance entries give \[\mathcal L_W\sum_i\mathop{\mathrm{en}}(q_i)=-\sum_i(1-q_i)=-2, \qquad \mathcal L_W\sum_i\mathop{\mathrm{en}}(1-q_i)=-\sum_iq_i=-1.\] Consequently \(\mathcal L_WF_0=-\gamma _0\). On each edge the two entropy sums coincide with the binary entropy. Lemma 7 achieves that entropy by binary separation, with \(D-A\) tending to zero. Both coefficients in (55) are positive. Hence, for \(0<\delta<1\), \((1-\delta)F_0\le U\) on the boundary and \(\mathcal L_W((1-\delta)F_0)>-\gamma _0\) in the interior. The comparison consequence of Corollary 30 and continuity of the values prove, upon letting \(\delta\) decrease to zero, that \[ U(q)\ge F_0(q)\quad\hbox{on the whole simplex}. \tag{56}\]

A polynomial improvement and its domain

Let \[\begin{align*} \rho(\theta)&=\sum_{k=0}^4c_k\cos(3k\theta),\qquad \Omega_W=\{re^{\mathrm i\theta}:0\le r\le\rho(\theta)\}, \tag{57}\\ (c_0,c_1,c_2,c_3,c_4) &=(.28309034,-.05388682,.00841589,.00450821,-.00680398). \end{align*}\] Here and below inequalities on this compact set include its boundary; comparison is applied to its open interior. The proposed improvement is a real polynomial \(H_W\). Its exact specification is short despite its degree. Put \[\begin{align*} (s_0,s_1,s_2,s_3) &=(.0152567903,.0002597033,-.0014351728,-.0017937434),\\ (s_4,s_5,s_6)&=(-.0008593989,-.0002090472,-.0000227468). \end{align*}\] Set \(a_{3k,0}=s_k/(.32)^{3k}\) for \(0\le k\le6\). All other pure coefficients \(a_{j,0},a_{0,j}\) are zero, except the already assigned \(a_{0,0}\). For \(d=0,\ldots,110\), and \(i+j=d\), define \[ a_{i+1,j+1}= \frac{d(d-1)a_{ij}-(i+2)(i+1)a_{i+2,j-1} -(j+2)(j+1)a_{i-1,j+2}} {2(i+1)(j+1)}. \tag{58}\] A negative index denotes a zero coefficient. Every coefficient on the right has degree at most \(d+1\), so this is a finite rational recursion. Finally set \[ H_W(z)=\operatorname{Re}\sum_{i+j\le112}a_{ij}z^i\bar z^j. \tag{59}\]

Here are explicit bounds on this polynomial; their verification uses only rational arithmetic. Put \(R_W=.357\), and, for \(k=0,1,2\), put \[S_k=\sum_{i+j\ge k}|a_{ij}|(i+j)(i+j-1)\cdots(i+j-k+1) R_W^{i+j-k},\] where the empty product is one. The recursion gives \[ S_0<.058178, \qquad S_1<1.490164, \qquad S_2<53.686778. \tag{60}\] For clarity, a finite procedure for checking the residual is as follows. For each \(a_{ij}\), add its four contributions \[\begin{array}{c|c} \text{monomial}&\text{coefficient}\\ \hline z^i\bar z^j&-(i+j)(i+j-1)a_{ij}\\ z^{i-2}\bar z^{j+1}&i(i-1)a_{ij}\\ z^{i+1}\bar z^{j-2}&j(j-1)a_{ij}\\ z^{i-1}\bar z^{j-1}&2ij a_{ij} \end{array}\] and omit negative exponents. Call the resulting coefficients \(b_{ij}\). Equation (58) makes \(b_{ij}=0\) for \(i+j\le110\), exactly. The remaining rational sum satisfies \[ \sum_{i,j}|b_{ij}|R_W^{i+j}<6.739223\cdot10^{-13}<7\cdot10^{-13}. \tag{61}\] This proves \(|\mathcal L_WH_W|<7\cdot10^{-13}\) on \(|z|\le R_W\).

The geometry of the shell has similarly direct bounds. Write \[r_* =\sum_k|c_k|=.35670524,\quad r_1=\sum_k3k|c_k|=.33437745,\quad r_2=\sum_k(3k)^2|c_k|=2.13289155.\] The lower triangle inequality gives \(\rho\ge.20947544>.2\), whereas \(\rho\le r_*<.357\). Formula (53) therefore implies \(q_i>.095\) throughout \(\Omega_W\). For \(z(\theta)=\rho(\theta)e^{\mathrm i\theta}\), \[ |z'|\le r_*+r_1=.69108269, \qquad |z''|\le r_*+2r_1+r_2=3.15835169<3.16, \qquad |q_i''|<2.11. \tag{62}\] Differentiating each monomial in (59) gives \(|(H_W\circ z)''|\le S_2|z'|^2+S_1|z''|<30.348\). One can also verify the needed baseline bound without cancellation. For a single summand \(f(t)=(\gamma _0-1)\mathop{\mathrm{en}}(t)+(2-\gamma _0)\mathop{\mathrm{en}}(1-t)\), on \(.095<t<.572\) we have \(|f'(t)|<2.5\) and \(|f''(t)|<5.1\). These follow, for example, from \(1.32<\gamma _0<1.33\), \(-\log(.095)<2.4\), and \(-\log(.428)<.9\). Using \(|q_i'|\le2|z'|/3\) and \(|q_i''|\le2|z''|/3\) gives \[ \left|\frac{d^2}{d\theta^2} \bigl(F_0(q(\theta))+H_W(z(\theta))\bigr)\right| <49.387<68. \tag{63}\] The slightly larger bound 68 will be used in interpolation.

What is certified by the finite library

We next describe the mathematical objects in the library. A record fixes a finite tree of completion, parity, binary-separation, and side-permutation operations, with rational conditional distributions on its branches. Proposition 15 compiles this hierarchy into a family of finite realizations using growing exact-type populations and efficient GROUP parameters, preserving arbitrary payloads and the canonical bank convention. The utility of a record is the limiting attainable score of this family. Every positive accuracy is achieved with finite supplies, so the record gives a lower bound on the closed value \(U\). The arithmetic below evaluates these laws and limiting utilities; the final strict excess over \(\log3\) will later select an actual finite realization.

Here is an explicit description of its word groups, which is also useful for checking the library independently. Number the W labels \(0,1,2\) and define the partial completion map \[c(0,0)=0,\quad c(0,1)=c(1,0)=c(1,1)=1,\quad c(0,2)=c(2,0)=c(2,2)=2;\] the pairs \((1,2)\) and \((2,1)\) are discarded. A two-position completion has outer label \(c(i,j)\). A three-position completion has outer label \(c(c(i,j)-k\pmod3,r)\), where \(k\in\{0,1,2\}\); an undefined intermediate label discards the word. Its inner label is deterministic. Independent permutations of the three labels are allowed in the two or three positions. These are precisely finite compositions of the completion restriction. For parity on three positions discard the six words with all labels different. A retained word has a majority label and an odd-count label; on a constant word both equal its sole label. Either label can be the outer label and the other the inner label. A nonconstant outer/inner group has three words and a constant group has one. This is the parity restriction proved earlier, followed by two W separations.

Suppose the block length is \(L\in\{2,3\}\). Let \(t_i\) be the outer law, \(v_{ij}\) the inner law conditional on \(i\), and \(C_{ij}\) the law of the retained words in that group. Let \(n(w)\) count the original canonical source labels, obtained by undoing each positional reindexing. The intermediate cyclic rotation changes only the completed-block flag and fiber membership, not these source labels. If the child constructions have limiting utilities \(u_t,u_{v_i}\), the original law and limiting utility are given exactly by \[\begin{align*} q_{\rm out}&=\frac1L\sum_{i,j}t_iv_{ij}\mathbb E_{C_{ij}}n(w), \tag{64}\\ u_{\rm out}&=\frac1L\left(u_t+\sum_it_i u_{v_i} +\sum_{i,j}t_iv_{ij}H(C_{ij})\right). \tag{65}\end{align*}\] For completion the inner utility is zero. The last term is supplied by Proposition 15: once the outer label is direct, resolve the gate refinements in the order of Lemma 14, using each gate’s own pair of knowing sides. The flattened final word need not be readable by one fixed pair. Exact conditional types fix the populations and canonical histograms of every pool, including under the positional permutations, and the entropy chain rule counts the remaining word law once. For parity, after its two labels are direct, the remaining choice is the primitive three-word group of Lemma 12. These are precisely the hypotheses behind the last term of (65). Each auxiliary separation has \(D-A\to0\); hence the limiting utilities of these pure completion/parity records satisfy \(u=M\le H(q)\le\log3\).

The following finite menu protocol specifies the candidates used in the arithmetic check. Its deterministic integer implementation is menu.hpp in the accompanying certificate sources.

1. For weights \(d=(i/64,j/64,1)\) with \(0\le i\le j\le64\), the terminal operation deletes a least-weight label and separates the remaining two, with probabilities proportional to their weights, rounded as specified below. The zero pair uses the deterministic record.

2. The initial record repeats two-position completion twelve times, placing a maximum-weight label first at each step, and ends with this terminal operation. Positive integer weights are renormalized at each recursive call, with a lower bound of one integer unit.

3. Fourteen improvement layers may retain an earlier record or assemble earlier records using two-position completion, three-position completion, or either order of the parity labels above. All positional permutations and the three intermediate cyclic offsets are available. A child call also permits terminal binary separation. Candidate comparison uses \(u+\sum_iq_i\log d_i\); lookup examines the nearby indices within two of the nearest \(64d_i/\max d\) after sorting the weights, and all compatible side permutations. The outer weights in parity may themselves be chosen from the rounded exponentials of such child scores.

4. Each conditional word receives a positive integer weight equal to the rounded product of its positional weights, clamped below by one. The cumulative normalization in (66) fixes its exact conditional law. Append all six side permutations of the selected final records and the three deterministic records.

The preliminary scores that select operation types, the integer roots or exponentials used as search weights, and ties in selection have no mathematical accuracy requirement: they only choose among the explicitly admissible finite trees just described. In particular, a computed score is never used as the utility of a record. Utilities and laws are evaluated anew by (64)–(65). The supplied finite program fixes all these selection choices, including ties; the certificate verifies feasible mixtures of its resulting records. Neither global optimization of the records nor optimality of a mixture is needed for the lower bound.

Arithmetic errors and exact distributions

Let \(B=2^{52}\). For positive integer word weights \(w_1,\ldots,w_m\) set \[ p_j=\frac1B\left( \left\lfloor\frac{B\sum_{k\le j}w_k}{\sum_kw_k}\right\rfloor- \left\lfloor\frac{B\sum_{k<j}w_k}{\sum_kw_k}\right\rfloor\right). \tag{66}\] These probabilities are nonnegative and telescope to one. Zero-probability words are omitted. This formula, not an unrounded idealized weight law, defines every conditional distribution used by a record.

The evaluator represents a real number by an integer divided by \(B\). Multiplication and division truncate toward zero, and an input constant \(x\) is stored as \(\lfloor Bx+1/2\rfloor\). Logs are evaluated by reducing the argument to \(x\in[1,2]\) with powers of two and using \[ \log x=2\sum_{j=0}^{39}\frac{t^{2j+1}}{2j+1} +\varepsilon(x),\qquad t=\frac{x-1}{x+1},\qquad 0\le\varepsilon(x)\le\frac{2\,3^{-81}}{81(1-1/9)}. \tag{67}\] Since \(|t|\le1/3\), summing the geometric propagation of rounding errors in Horner evaluation gives an error below \(7/B\) on \([1,2]\). For a probability represented at scale \(B\), reduction uses at most 52 doublings. Keeping the factor \(p_j\) in \(-p_j\log p_j\), rather than bounding all reduced-log errors by their worst case separately, gives entropy error less than \(400/B\) for any conditional word distribution here (which has at most 27 words). For example, \(\sum_jp_j|h_j|\le1+H(p)/\log2\le1+\log_2 27\), where \(h_j\) is the reduction exponent; the log errors and the at most 27 final product roundings are already less than \(100/B\). The allowance \(400/B\) includes the other normalization and evaluation roundings.

Let \(e_r^{\rm init}\) be the \(\ell^1\) error between the exact law of a record and its stored law after \(r\) initial completion steps, and let \(f_r^{\rm init}\) be its utility error. The terminal binary law is exact at scale \(B\), with utility error at most \(400/B\). In a completion, averaging normalized count vectors contracts the child-law error. There are three groups; rounding the count averages and restoring the missing mass to the first coordinate contributes less than \(15/B\). The outer child utility is divided by two. Perturbing its weights in the conditional entropy term contributes at most \(2e_r^{\rm init}\), and the local entropy and arithmetic errors contribute less than \(250/B\). Thus \[ e_r^{\rm init}\le\frac{15r}{B},\qquad f_r^{\rm init}\le\frac12 f_{r-1}^{\rm init} +2e_r^{\rm init}+\frac{250}{B}. \tag{68}\] At \(r=12\) these give \(e_0\le180/B\) and \(f_0\le1700/B\) for the improvement layers. (The displayed initial recurrence actually gives \(f_{12}^{\rm init}\le1159.991/B\).)

For an improvement layer let \(e_h,f_h\) be uniform errors over its records. A parity assembly combines at most an outer law and an inner law, so their errors total at most \(2e_{h-1}\). There are at most nine groups. The sum of product and count roundings leaves fewer than 21 missing probability units before restoration; adding that mass to one coordinate costs less than \(42/B\) in \(\ell^1\). The two child utility contributions are divided by three, giving coefficient \(2/3\); completion has the smaller coefficient \(1/2\). Inner utilities are at most \(\log3\), and the conditional word entropy is at most \(\log27\). Applying these bounds to (65), with the just obtained law-error allowance, gives the conservative recurrence \[ e_h\le2e_{h-1}+\frac{42}{B},\qquad f_h\le\frac23 f_{h-1}+3e_h+\frac{250}{B}. \tag{69}\] To see that the last fixed allowance is sufficient, the entropy errors contribute at most \(400/(LB)\le200/B\); the at most nine group-weight products, their utility products, the three inner-utility products, and the final division contribute less than \(50/B\) after normalization. For parity, each conditional group actually has at most three words, so the weight-perturbation estimate in (69) has additional slack. Retaining a record from an earlier layer preserves these bounds. At \(h=14\) they give \[ e_{14}\le\frac{3637206}{B}<8.5\cdot10^{-10},\qquad f_{14}<3.635\cdot10^{-9}<10^{-8}. \tag{70}\]

For mixture evaluation, project the stored first two coordinates and utility down to scale \(2^{30}\). A feasible triple of projected library points determines nonnegative barycentric weights by exact determinant ratios. Applying those same weights to the true records gives a genuine attainable law \(\widehat q\). The singleton points are in the library, so every projected simplex target admits a feasible triple. The implementation’s pivot search is used only to locate a triple with a sufficient utility; feasibility is verified by its nonnegative determinant ratios.

The difference between two floor remainders in a first or second coordinate is less than \(2^{-30}\); the third coordinate is their complement. Combining this with (70) gives \(|\widehat q_i-q_i|<2.8\cdot10^{-9}\), including the much smaller error in a shell target’s trigonometric evaluation. We may cap the utility claimed for a mixture at \(K=1.5\). Lemma 33 then bounds its correction loss on the shell by \(1.5(2.8\cdot10^{-9})/.095\). Adding the library utility and projection errors proves the following bounds, also recording the grid bound needed later:

The last two bounds can be checked directly as follows. Store the scaled polynomial coefficients \(a_{ij}R_W^{i+j}\), evaluate in polar coordinates with \(r/R_W<1\), and sum the finitely many roundings. There are 6441 monomials, degree at most 112, and (60) bounds the effects of coordinate error. For cosine, reduce the angle to \([0,\pi]\) and use its degree-48 Taylor polynomial in Horner form. Its Taylor remainder and propagated fixed-point errors total less than \(300/B\). Coefficient rounding, at most 112 radial multiplications, and the two products per monomial give an error well below \(10^{-9}\), including this trigonometric error. Applying (67) to the six entropy terms in (55) gives the stated \(10^{-11}\) allowance.

The finite checks and the continuum conclusion

The finite shell check uses \[ \theta_l=\frac{l\pi}{6480},\qquad 0\le l\le2160. \tag{71}\] At each angle it forms \(r=\rho(\theta_l)\) and the target law by (53), evaluates a feasible library mixture as above, and subtracts the stored values of \(F_0\) and \(H_W\). Thus the finite statement to check is a collection of 2161 integer inequalities: if \(g_l\) is the resulting gap in units of \(B^{-1}\), then \[ \min_l g_l=-4180063084, \qquad 10^6 g_l>-5B\quad(0\le l\le2160). \tag{72}\] In particular the recorded minimum is exactly \(-4180063084/2^{52}\) in utility units, approximately \(-0.928160457\cdot10^{-6}\). This finite arithmetic result is reproducible from the coefficient and menu specifications above and the supplied integer checker. Its mathematical meaning is a lower bound from feasible constructions, with the proved error allowances; it is not a claim that the numerical candidate is an optimizer. Using the conservative threshold \(-5\cdot10^{-6}\) in (72), subtracting the preceding evaluation and exact-law correction allowances, and transporting from rounded targets to exact sample targets gives \[ U(q(\theta_l))-F_0(q(\theta_l))-H_W(z(\theta_l)) >-5.2\cdot10^{-6}. \tag{73}\]

It remains to fill the intervals between these samples; no sampling assumption is made here. If a twice differentiable scalar function has \(|f''|\le M\) on an interval of length \(h\), its difference from its linear interpolant is at most \(Mh^2/8\). Mix the two sample constructions with their linear interpolation weights. Their law is the chord between the two sample laws. By (62), each coordinate differs from the desired curved law by at most \(2.11h^2/8\). Correct this discrepancy using Lemma 33; since \(q_i>.095\), the utility loss is at most \(1.5(2.11/.095)h^2/8\). The interpolation error of \(F_0+H_W\) is at most \(68h^2/8\) by (63). With \(h=\pi/6480\) their total is \[ \left(68+\frac{1.5\cdot2.11}{.095}\right)\frac{h^2}{8} <2.977\cdot10^{-6}<3.1\cdot10^{-6}. \tag{74}\] Both the shell and the polynomial are invariant under rotation by \(2\pi/3\) and conjugation: the recurrence preserves \(i-j\equiv0\pmod3\) and has real coefficients. The value is invariant under label permutations. These symmetries extend the interval \([0,\pi/3]\) to the entire boundary.

At the target exponent \(\beta=1129/500\), we have \(3/\beta>\gamma _0\). Proposition 22 therefore transfers both the baseline and the seed to \(U_{3/\beta}\). Together with Proposition 25, this is the promised attainable lower bound on the five-component face.

The chart and its exact coefficients

Put \(\zeta=\exp(2\pi i/3)\) and \(R=31/25\). For a real polynomial \(P\) on the complex plane define, with subscripts modulo three, \[ r_i(z)=\frac{1+\Re(\zeta^i z)}3,\qquad p_i(z)=P(\zeta^i z),\qquad E_i(z)=r_i(z)+p_i(z)-p_{i+1}(z)-p_{i+2}(z). \tag{76}\] Their six-coordinate sum is one. In the six-state support, their mean satisfies \(\mu_i=1-r_i\). Thus \[z=3r_0-1+i\sqrt3(r_2-r_1)\] is an invertible affine coordinate on the mean plane. Whenever all six coordinates are positive, (76) is a chart to which Theorem 26 applies.

Here is a finite rational definition of \(P\). For integers \(N\geq8\) and \(b\geq1\), put \(Q=2^b\) and \(\operatorname{rnd}(t)=\lfloor t+1/2\rfloor\). Let \[(Z_0,\ldots,Z_7)=(18623,-2696,-2677,194,393,17,1,8),\qquad Z_k=0\ (k\geq8).\] We define symmetric integers \(A_{ij}=A_{ji}\) for \(i+j\leq N\). The pure coefficients are \[A_{0k}=A_{k0}=\operatorname{rnd}(QZ_k/100000).\] Let \(c_{00}=8\), \(c_{10}=c_{01}=2\), \(c_{20}=c_{02}=-1\), and \(c_{11}=-2\), with every other \(c_{ij}\) zero; after computing \(A_{ij}\) set \(C_{ij}=72A_{ij}+Qc_{ij}\). For \(1\leq i\leq j\), in increasing total degree, form the following sum. For \(0\leq x<i\), \(0\leq y<j\), \((x,y)\ne(0,0)\), put \[h=1+y-x\pmod 3,\quad h\in\{0,1,2\},\qquad a=i-x-1+h,\quad c=j-y+1-h,\] and set \[w_0(a,c)=c(c-1),\qquad w_1(a,c)=ac,\qquad w_2(a,c)=a(a-1).\] Then define \[ S_{ij}=\sum_{\substack{0\leq x<i,\ 0\leq y<j\\(x,y)\ne(0,0)}} C_{xy}A_{a,c}w_h(a,c),\qquad A_{ij}=\operatorname{rnd}\left(-\frac{S_{ij}}{C_{00}ij}\right), \qquad A_{ji}=A_{ij}. \tag{78}\] The indices \(a,c\) are nonnegative, and both \(a+c\) and \(x+y\) are smaller than \(i+j\). Thus (78) is a definition by finite recursion. For both choices used here, \(21<C_{00}/Q<22\), so its denominator is positive. Finally put \[ P_{N,b}(z)=2^{-b}\sum_{i+j\leq N}A_{ij}z^i\bar z^j, \qquad P=P_{780,500},\qquad P^{\rm ref}=P_{420,224}. \tag{79}\] The chart used in the proof is defined by \(P\). The smaller polynomial \(P^{\rm ref}\) makes the finite evaluations less expensive; uniform bounds on its difference from \(P\) will transfer those evaluations to the chart. The symmetry of the coefficients makes these polynomials real-valued and invariant under conjugation. Rotation permutes the three functions \(p_i\); it need not fix \(P\) itself.

Uniform residual and polynomial comparisons

The reason for the recursion is most transparent at the coefficient level. For the chart \(P_{N,b}\) form \[\mathcal C(z,\bar z)=\sum_{i,j}(C_{ij}/Q)z^i\bar z^j =36\bigl[r_0(1-r_0)+2P_{N,b}\bigr].\] Write \(\mathcal C^{[s]}\) for the terms whose exponent difference is \(s\) modulo three. Then \[\mathcal L=\mathcal C^{[0]}\partial_z\partial_{\bar z} +\mathcal C^{[2]}\partial_z^2+\mathcal C^{[1]}\partial_{\bar z}^2.\] The coefficient of \(z^{i-1}\bar z^{j-1}\) in \(\mathcal L P_{N,b}\) is \[\frac{C_{00}ijA_{ij}+S_{ij}}{Q^2}.\] Indeed, the three second derivatives give exactly the shifts and factors in (78). A term outside \(x<i\), \(y<j\) has zero derivative factor. Every other coefficient on the right has already been computed. Nearest rounding therefore leaves a defect of absolute value at most \(C_{00}ij/(2Q^2)<36ij/Q\). Reflection handles \(i>j\).

For any polynomial \(F=\sum f_{ij}z^i\bar z^j\), the elementary inequality \[ \sup_{|z|\leq R}|F(z)|\leq\sum_{i,j}|f_{ij}|R^{i+j} \tag{80}\] provides a uniform, rather than sampled, bound. A convenient majorant for all low-degree rounding defects is \[\rho=\sum_{k=2}^N\frac{36(k+1)k^2R^{k-2}}Q.\] For the remaining products put, for \(s=0,1,2\), \[D_{s,k}=\frac{R^k}{Q}\sum_{\substack{a+c=k\\a-c\equiv s\ (3)}}|C_{ac}|, \qquad V_{s,m}=\frac{R^{m-2}}Q\sum_{a+c=m}|A_{ac}|v_s(a,c),\] where \((v_0,v_1,v_2)=(ac,c(c-1),a(a-1))\). A product with covariance degree \(k\) and differentiated chart degree \(m\) has degree \(k+m-2\). Every coefficient outside the recursion is consequently included in \[ \sup_{|z|\leq R}|\mathcal L P_{N,b}(z)| \leq\rho+\sum_{s=0}^2\sum_{k+m>N}D_{s,k}V_{s,m}. \tag{81}\] All terms on the right are nonnegative rational numbers. They can be bounded using integer arithmetic: set \(U=2^{160}\), replace each \(D_{s,k}\) and \(V_{s,m}\) by its upper integer multiple at scale \(U\), round each summand of \(\rho\) upwards at the same scale, and divide the two sums by \(U^2\) and \(U\), respectively. For \(N=780,b=500\) this gives \[ \epsilon:=\sup_{|z|\leq R}|\mathcal L P(z)| <3.328667\cdot10^{-22}<3.329\cdot10^{-22}. \tag{82}\] The exact upper numerator and denominator, as well as the complete coefficients regenerated by (78), form part of the finite certificate. Thus the small low-degree defect is attached to the defined polynomial, not assumed for an arbitrary supplied coefficient list.

For two polynomials, with missing coefficients interpreted as zero, define \[\Delta_a=\sum_{i,j}|P_{ij}-P'_{ij}|R^{i+j}(i+j)^a, \qquad a=0,1,2,\] using \((i+j)^0=1\) also at the constant term. A unit real directional derivative of a monomial costs at most \(i+j\) and a second one at most \((i+j)(i+j-1)\). Hence \[ |P-P'|\leq\Delta_0,\quad \|\nabla(P-P')\|\leq\Delta_1/R,\quad \|D^2(P-P')\|_{\rm op}\leq\Delta_2/R^2. \tag{83}\] Computing the coefficient differences exactly before taking absolute values, and rounding the resulting positive sums upwards, gives the following bounds on the entire closed disk:

Here the subscript denotes truncation by total degree. The same sums with factors \(k\) and \(k(k-1)\) prove, for either full or reference chart, \[ \|\nabla p_i\|<.592,\qquad \|D^2p_i\|_{\rm op}<3.05. \tag{84}\] Truncating either chart at degree 40 changes its value by less than \(.0002\) and its gradient by less than \(.006\). These derivative estimates will control interpolation and root locations; value closeness alone would not suffice.

Geometry of the domain

Work first in the sector \(0\leq\theta\leq\pi/3\), writing \(z=re^{i\theta}\). Define its probability domain by \(r\leq R\) and \(E_1\geq0\). We shall prove that the other five coordinates are uniformly positive there. Rotations and conjugation then provide the full domain \(\Omega\).

From (84), \[ \|\nabla E_i\|<G:=\tfrac13+3(.592)<2.11,\qquad \|D^2E_i\|_{\rm op}<9.15. \tag{85}\] Divide the sector into \(480\) radial and \(480\) angular cells, with centers \[r_j=\frac{R(2j+1)}{960},\qquad \theta_l=\frac{(2l+1)\pi}{2880},\qquad 0\leq j,l<480.\] Evaluate the degree-40 reference chart at these centers, including its radial derivative and unit-tangential derivative \(r^{-1}\partial_\theta\). The following are the exact integer center tests, after division by the arithmetic scale: \[\begin{align*} p_i&\geq.0516\quad(i=0,1,2),& E_0,E_2&\geq.055,& d&\geq.488, \tag{86}\\ E_1<.018&\ \Longrightarrow\ -\partial_rE_1\geq.183 \quad\hbox{and}\quad\|\nabla E_1\|\geq.3208,\\ E_1\geq-.008&\ \Longrightarrow\ (9d-2)^2 \geq18\sum_{i=0}^2(D_i-D_{i+1})^2. \end{align*}\] For completeness, their arithmetic specification uses \(T=2^{45}\), the rational approximation \(3141592653589793238/10^{18}\) to \(\pi\), and sine and cosine series through degree 64 on arguments reduced to \([0,2\pi)\). Every division in these recurrences is rounded down. The Taylor remainder is below \(10^{-30}\); propagation of rounding errors is bounded by \(65e^{2\pi}/T\). Including the argument approximation gives error below \(2\cdot10^{-9}\) in either trigonometric value. There are \(861\) possible chart coefficients through degree 40; their absolute majorant is below \(.921\), and the first-derivative majorant is below \(.592\). Product and summation errors consequently leave a common allowance \(10^{-7}\) for the displayed scalar fields and gradient vectors. These rules specify finite integer evaluations at all \(230400\) centers, and all tests (86) hold.

Let \(b=\pi/2880\). Every point of a cell is within distance \[\delta\leq\sqrt{(R/960)^2+R^2b^2}<.001870298\] of its center. Adding the truncation tails, arithmetic allowance, and Lipschitz variation gives \[\begin{align*} p_i&>.0516-.0002-.592\delta-10^{-7}>.0502926, \tag{87}\\ E_0,E_2&>.055-.0006-G\delta-10^{-7}>.0504548. \end{align*}\] If the true \(E_1\) at a point is at most \(.01\), its truncated center value is below \(.01+.0006+G\delta+10^{-7}<.018\). Thus the derivative tests apply. Using the Hessian variation and the degree-40 gradient tail yields \[\begin{align*} -\partial_rE_1&>.183-.018-9.15\delta-Gb-10^{-7}>.1455857, \tag{88}\\ \|\nabla E_1\|&>.3208-.018-9.15\delta-10^{-7}>.2856866. \end{align*}\] Only the first line needs the term \(Gb\), accounting for rotation of the radial unit vector between the point and the center.

In particular \(-\partial_rE_1>.144\) wherever \(E_1\leq.01\). At the origin, \(E_1=1/3-P(0)>.1471\). Once a ray reaches \(.01\), its value decreases strictly while below that level and cannot cross upwards through it. Consequently each ray has at most one zero. Let \(r_*(\theta)\) be this zero if it lies below \(R\), and \(R\) otherwise. Implicit differentiation on the smooth face and clipping at \(R\) give \[ |r_*'|\leq GR/.144<18.2,\qquad |r_*''|\leq\frac{9.15((r_*')^2+R^2)+2.11(2|r_*'|+R)}{.144}<22000, \tag{89}\] where the second inequality is used only on intervals wholly in a smooth face. The clipped radius is Lipschitz; its second derivative is not used across a face–cap junction.

The eigenvalues of the matrix in (77) are \[9d\ \pm\ 3\sqrt{2\sum_i(D_i-D_{i+1})^2}.\] The center tests give a smaller eigenvalue at least 2; \(d\geq.488\) ensures the required sign before taking square roots. A cell containing a point with \(E_1\geq0\) has computed center \(E_1>-.004546\), so the test is active. Throughout the sector \(r_i\in[-.08,.746667]\), and hence \[\|\nabla D_i\|\leq1.16/3+2(.592)<1.571.\] The change from the truncated center to the full value is less than \(2(.0002)+1.571(.001871)+10^{-7}<.00334\). If all \(D_i\) change by at most \(t\), then \(\|\Delta C\|_{\rm op}\leq15t\): the three coefficients of \(D_i\) in a unit-direction quadratic form are \(3+6\cos(2a+2\pi i/3)\); they sum to 9, at most one is negative, and a negative coefficient has magnitude at most 3. Their absolute sum is at most 15. We conclude \[ \lambda_{\min}(C)>2-15(.00334)>1.949\qquad\hbox{on }\overline\Omega. \tag{90}\] All full/reference differences in (83) fit within the remaining strict slacks, so these conclusions hold for \(P_{780,500}\).

The barrier and the interior inequality

Finite Taylor polynomials, explicit remainder bounds, and subdivision into certified boxes are standard techniques of validated numerics; see (Makino and Berz 2003, sec. 2 and Algorithm 1) and (Solovyev and Hales 2013, sec. 2). We specify the integer arithmetic and all error allowances for the present certificate below.

Let \[\mathcal I=\{(i,j):0\leq j\leq i,\ i+j\leq22,\ i-j\equiv0\pmod3\}.\] The \(52\) exact rational coefficients \(a_{ij}\) in Table 1 define \[ \varphi(z)=\Re\sum_{(i,j)\in\mathcal I}a_{ij}z^i\bar z^j. \tag{91}\] For \(i>j\), the real part gives \(a_{ij}(z^i\bar z^j+z^j\bar z^i)/2\); a diagonal term occurs once. This polynomial is invariant under \(z\mapsto\zeta z\) and conjugation. Its constant term is \(1.098619383270680538\).

The six-component boundary inequality

We apply the three-state seed to a face of the six-component domain, and the matching construction to its circular cap. It is important to keep these two sources of attainable values distinct.

Put \(U=U_{\gamma_0}\), where \(\gamma_0=300000/225925\). Since \(3/\beta>\gamma_0\), Proposition 22 permits us to use this lower parameter in the face estimate of Proposition 25. At \(E_1=0\) define \[ Q=(p_2+E_0,p_0+E_2,p_1),\qquad J=\mathop{\mathrm{en}}(p_2)+\mathop{\mathrm{en}}(p_0)+\mathop{\mathrm{en}}(E_0)+\mathop{\mathrm{en}}(E_2)-\mathop{\mathrm{en}}(Q_0)-\mathop{\mathrm{en}}(Q_1). \tag{99}\] The face lower bound is \[ B_e=\frac{1129}{1500}\bigl(U(Q)+J\bigr). \tag{100}\] At the cap put \(l_h=E_{h+1}+E_{h+2}\). The side-\(h\) marginal is \((1-l_h-p_h,l_h,p_h)\), so Proposition 24 gives \[ B_c=\frac13\sum_{h=0}^2 \bigl[\mathop{\mathrm{en}}(l_h)+\mathop{\mathrm{en}}(p_h)+\mathop{\mathrm{en}}(1-l_h-p_h)\bigr]. \tag{101}\]

The positive inset and the comparison argument

The supporting-covector estimate requires all six probabilities to be bounded away from zero. Set \(\eta=2\cdot10^{-9}\) and replace each active face \(E_i=0\) by \(E_i=\eta\), retaining the cap where it is reached first. Let the resulting domain be \(\Omega_\eta\). It contains the origin, has compact closure, and all six coordinates are at least \(\eta\) there. We now transfer Lemma 38 to its boundary.

On a removed terminal segment of a ray, \(0\leq E_1\leq\eta\) and \(-\partial_rE_1>.144\). Its length is at most \[ \Delta r\leq\eta/.144<1.389\cdot10^{-8}. \tag{110}\] This also handles an original cap endpoint with \(0\leq E_1<\eta\). The five other coordinates remain greater than \(.05\) and each changes by less than \(2.11\Delta r<2.94\cdot10^{-8}\). Write \(\alpha_b\) and \(\alpha_\eta\) for the original and new endpoint laws. With \[\lambda=\max_{i:(\alpha_b)_i>0} \left(1-\frac{(\alpha_\eta)_i}{(\alpha_b)_i}\right)_+,\] the active coordinate contributes nothing, and \(\lambda<2.94\cdot10^{-8}/.05=5.88\cdot10^{-7}\). If \(\lambda>0\), the vector \[s=\frac{\alpha_\eta-(1-\lambda)\alpha_b}{\lambda}\] is a probability distribution. Mix a construction at \(\alpha_b\) with singleton constructions of average law \(s\). Singleton utility is nonnegative, and the original utility is at most \(\log6<2\). The loss is below \(2\lambda<1.18\cdot10^{-6}\). When \(\lambda=0\) no correction is required. The closure of rational mixtures gives the same conclusion for limiting endpoint laws.

To bound the change of the barrier, every point of the inset segment has a face-check sample within angular distance \(h=\pi/(3\cdot65536)\). The band test covers even cap endpoints where the inset becomes active. The radial Lipschitz bound, root error, and inset displacement give total polar-coordinate distance at most \[d_*=19.2h+2\cdot10^{-9}+1.389\cdot10^{-8}<.000307.\] Taylor’s theorem for \(\partial_r\varphi\), using (104), (103), and (105), gives \[|\partial_r\varphi| <2.902+79.002d_*+\frac{1999.002}{2}d_*^2 +\frac{435\cdot10^6}{6}d_*^3<3.\] Thus the barrier changes by less than \(3\Delta r<4.2\cdot10^{-8}\). The two transfer losses total less than \(1.3\cdot10^{-6}\), leaving more than \(4.2\cdot10^{-6}\) slack on the inset boundary. At unchanged cap points there is no loss. Symmetry treats all faces.

Two starting tensors

The second starting tensor is the five-term tensor \(T'\) from (11), obtained from the \(q=1\) Coppersmith–Winograd tensor (Coppersmith and Winograd 1990, sec. 7). We retain its color flags and make the conditional trees explicit. The formulas below give short polynomial witnesses for both starting budgets.

The first base has budget \(R=2\) and support \[\mathsf B=\{100\},\qquad \mathsf A=\{001\},\qquad \mathsf C=\{010\}.\] It is the coefficient of order one in \[(x_0+t x_1)(y_0+t y_1)(z_0+t z_1)-x_0y_0z_0,\] whose constant coefficient is zero. Its conditional trees are trivial.

The second base has budget \(R=3\) and support \[ \mathsf A=\{002,011\},\qquad \mathsf B=\{200,110\},\qquad \mathsf C=\{020\}. \tag{115}\] The triples give indices on \(X,Y,Z\), with unit coefficients. The flag tests are \(z>0\), \(x>0\), and \(y=2\). Within \(\mathsf A\), the choice is read by \(Y,Z\); within \(\mathsf B\), it is read by \(X,Y\).

To verify the budget, put \[P(t)=(x_0+t x_1+t^2x_2) (y_0+t y_1+t^2y_2) (z_0+t z_1+t^2z_2).\] The first coefficient of \(P(t)+P(-t)-2P(0)\) is twice the sum of the six monomials with index sum two; the family has rank at most three. Now give weight one to \(x_1,z_1,y_0,y_2\) and weight zero to all other variables. The term \(101\) has total weight three and the other five terms have weight one. The leading part is exactly (115).

Completion and termination

To terminate, delete one color using its owning flag. The choice between the two surviving colors is read by both their owning sides. Follow it with their conditional trees. This is a readable tree to which 40 applies.

A script consists of a base, a finite list of completions, and a termination pair. Its base-factor count is \[b=\prod_{\text{completions}}m\] (the empty product is one), and its cost before the auxiliary tensors of the readable tree are introduced is \(R^b\). No conditional branch is exempt from this cost.

A dual-exponent witness

Use base two, distinguished side \(X\), and its color \(\mathsf B\). After \(b\) base factors, regard the \(X\)-coordinates as binary words of length \(b\); the logarithmic base cost is \(b\log2\). We seek a final leaf law for which \(X\) is uniform on all these words and \(S=\mathrm H(X)=b\log2\). By 41 and the output-size lower bound, such a law gives \[w\!\left(\min\{1,2T/(b\log2)\}\right)=2.\] The construction will preserve the exact incident-entropy equality while increasing the nonincident entropy \(T\).

To identify what preserves this equality, let \(X\) also denote the random coordinate induced by a leaf law on a readable tree, including a tree conditional on one color. At a node \(\nu\), conditioning means that the path reaches that node, and the conditional mutual information is \[\mathrm I(X;\text{child}\mid\nu) =\mathrm H(X\mid\nu)-\mathrm H(X\mid\text{child},\nu).\] Since a leaf determines \(X\), successive conditioning at the nonterminal nodes telescopes to \[\mathrm H(X)=\sum_\nu\mathbb P(\nu)\, \mathrm I(X;\text{child}\mid\nu).\] At an incident node the child is a function of \(X\) and the prefix, so its mutual information is \(\mathrm H(\text{child}\mid\nu)\). Subtracting these incident contributions gives \[ \mathrm H(X)-S =\sum_{\nu\text{ nonincident}} \mathbb P(\nu)\,\mathrm I(X;\text{child}\mid\nu). \tag{125}\] The terms on the right are nonnegative. Thus \(S=\mathrm H(X)\) precisely when every nonincident choice at a positive-mass node is independent of \(X\), conditional on the preceding choices.

We maintain this equality separately within each color. Partition the binary words into an active set \(P\) and its complement \(Q\), with the following properties:

1. color \(\mathsf B\) permits precisely \(P\), while each other color permits precisely \(Q\);

2. the chosen conditional law of each color makes \(X\) uniform on its permitted set;

3. its conditional incident entropy is exactly the logarithm of that set’s size.

Write \(\rho=|P|/2^b\), and let \(h_i\) be color \(i\)’s nonincident entropy; initially \((\rho,b,h_i)=(1/2,1,0)\).

Terminate by keeping \(\mathsf B\) and the inactive color with larger \(h\), placing mass \(\rho\) on \(\mathsf B\). The incident termination label and the uniform conditional laws make \(X\) uniform on all \(2^b\) binary words. Hence \[ S=b\log2,\qquad T=bD,\qquad D=\frac{\rho h_{\mathsf B}+(1-\rho)\max(h_{\mathsf A},h_{\mathsf C})}{b}. \tag{130}\] By 41 and the size lower bound, \[ \alpha\ge \min\{1,2D/\log2\}. \tag{131}\]

Use the following seven completions: \[ -2,\quad +2,\quad +2,\quad -3,\quad +2,\quad -2,\quad +3. \tag{132}\] A minus sign means center \(\mathsf B\). A plus sign means the inactive color with larger \(h\), with an arbitrary fixed tie choice. The absolute value is the completion size. Resolving the first tie as \(\mathsf A\), the centers are \(\mathsf B,\mathsf A,\mathsf C,\mathsf B,\mathsf C,\mathsf B,\mathsf A\).

For a short certificate, set \(\delta=|h_{\mathsf A}-h_{\mathsf C}|\). A minus step leaves \(D\) unchanged and gives \[\delta'=\frac{m(1-\rho)}{1-\rho^m}\delta.\] At a plus step put \[z=\log\bigl((1+e^{-\delta})^m-1\bigr).\] Substitution in 47 yields \[ \delta'=|z|,\qquad D'=D+\frac{1-\rho'}{mb}\max\{0,z\}. \tag{133}\] Indeed \(h_i\) is the larger inactive entropy, and \(h'_j=mh_i+z\), so the new maximum is \(mh_i+\max\{0,z\}\).

After the first three steps, at \(b=8\), \[\rho_8=1-(3/4)^4,\qquad \delta_8=\log(9/7),\qquad D_8=\frac{0.5625}{4}\log3.\] The two plus steps here have \(z=\log3\) and \(z=\log(7/9)\). The subsequent bounds are \[\begin{array}{c|l} b&\text{certified information}\\ \hline 24& \rho_{24}=\rho_8^3,\quad 0.3194<\rho_{24}<0.3195,\quad 0.348<\delta_{24}<0.354\\ 48& 1-\rho_{48}=(1-\rho_{24})^2>0.463,\quad 0.536<\rho_{48}<0.537,\quad 0.635<z_{48}<0.651\\ 96& \rho_{96}=\rho_{48}^2,\quad \delta_{96}=2\delta_{48}/(1+\rho_{48})<0.86\\ 288& 1-\rho_{288}=(1-\rho_{48}^2)^3>0.360,\quad z_{288}>0.628. \end{array}\] Their elementary verification is given in 12.4. Since \(\log2<0.6932\) and \(\log3>1.098\), \[\begin{align*} \frac{2D_{288}}{\log2} &> \frac{2}{0.6932} \left[ \frac{0.5625\cdot1.098}{4} +\frac{0.463\cdot0.635}{48} +\frac{0.360\cdot0.628}{288} \right]\\ &=\frac{1548637}{3327360}>0.465. \tag{134}\end{align*}\] This proves the dual-exponent conclusion without any approximate equality being used to certify exponent two.

A one-parameter rectangular curve

Use base three, one size-three completion centered on \(\mathsf A\), keep \(\mathsf B,\mathsf C\), and distinguish \(X\). This is the 75-component support of 11; the leaf law below tunes its two balanced outer dimensions and its inner dimension. Every word in \(\{0,1,2\}^3\) occurs on \(X\). For a nonzero word \(x\), its outer color is \(\mathsf B\), and the number of supported leaves in its fiber is \(d(x)=2^{\#\{\text{zero entries of }x\}}\). For the zero word, its outer color is \(\mathsf C\), and \(d(0)=3^3-2^3=19\). The fiber histogram is therefore \[\begin{array}{c|rrrr} d&1&2&4&19\\ \hline \#\{x:d(x)=d\}&8&12&6&1. \end{array}\] The total number of leaves is \(75\).

Give \(x\) probability proportional to \(d(x)^t\), and choose a leaf uniformly within its fiber. Put \[ \begin{split} Z(t)&=8+12\,2^t+6\,4^t+19^t,\\ g(t)&=(\log Z)'(t),\qquad h(t)=\log Z(t)-tg(t). \end{split} \tag{135}\] Then \(\mathrm H(X)=h(t)\) and \(\mathrm H(\text{leaf}\mid X)=g(t)\). In the nonzero branch, the \(\mathsf A/\mathsf B\) pattern and the choices within \(\mathsf B\) are incident to \(X\); the choices within \(\mathsf A\) are hidden on \(Y,Z\). In the zero branch all choices after branching are on \(Y,Z\). The outer \(\mathsf B/\mathsf C\) label is incident to \(X\). To check that the hidden choices do not leak information about \(X\), fix a nonzero outer branch and its \(\mathsf A/\mathsf B\) pattern. Then \(d(x)=2^{\#\mathsf A}\) is constant over that pattern. Each leaf has probability \(d(x)^{t-1}/Z(t)\), so the hidden choices in its \(\mathsf A\)-slots are independent of the remaining \(X\)-coordinates, including after any preceding slot histories. The zero branch has fixed \(X\). The information identity (125) therefore gives precisely \(S=h(t)\), \(T=g(t)\). Its base cost is \(3^3\), and 41 gives \[ w\!\left(\frac{2g(t)}{h(t)}\right) \le\frac{6\log3}{h(t)} . \tag{136}\] Here \(w(k)=W(1,k,1)\) can also be read for \(k>1\); we use only aspect ratios in \([0,1]\).

At \(t=2/3\), write \(u=2^{2/3}\), \(v=19^{2/3}\). Then \[g=\frac{12u(1+u)\log2+v\log19}{8+12u+6u^2+v}.\] Cubing verifies \[1.58739<u<1.58742,\qquad 7.1203<v<7.1205,\qquad 49.2878<Z<49.2890.\] Using the logarithm bounds below gives \[1.11844<g<1.11856,\qquad 3.1519<h<3.1522.\] In particular \[\frac{2g}{h}> \frac{2\cdot1.11844}{3.1522}>0.709,\qquad \frac{6\log3}{h}< \frac{6\cdot1.0987}{3.1519}<2.092 .\] Monotonicity proves \(w(0.709)<2.092\).

A finite-family square witness

Use base three and the completions \[(\mathsf B,2),\quad(\mathsf A,3),\quad(\mathsf C,2),\quad (\mathsf B,2),\quad(\mathsf A,3),\] then keep \(\mathsf B,\mathsf C\). The number of original factors is \(b=72\). Let \(d_i\) be the number of conditional monomials of color \(i\). Initially \((d_{\mathsf B},d_{\mathsf A},d_{\mathsf C})=(2,2,1)\). A size-\(m\) completion at \(i\) updates counts to \[d_i^m\quad\text{at }i,\qquad (d_i+d_j)^m-d_i^m\quad\text{at }j\ne i.\] After three steps the vector is \((20691584,13993344,10144225)\). After four it is \[(428141648429056,\;774902581936128,\;522705468255425) \ \ge\ 10^{12}(428,774,522)\] coordinatewise. The final sum of the kept counts is \[N=2995461856366867388223311649574852466276480577,\] and in particular \[ N\ge 10^{36} (1202^3+1296^3-2\cdot774^3)>2.95\cdot10^{45}. \tag{137}\] The substitution of lower counts is legitimate: the polynomial \((a+b)^3+(a+c)^3-2a^3\) has nonnegative coefficients.

Under the uniform leaf law, the sum of the three pair rates is \(\log N\). Averaging over permutations balances all three at \(\log N/3\). Thus 40 gives \[w(1)\le \frac{3\cdot72\log3}{\log N} <\frac{216\cdot1.0987}{1.0817+45\cdot2.3025} <2.267.\]

The three constructions above yield their stated bounds once the following elementary enclosures are verified.

Elementary interval verification

For \(1\le y\le2\), put \(s=(y-1)/(y+1)\). The logarithm series has the rational enclosure \[ 2\sum_{j=0}^7\frac{s^{2j+1}}{2j+1} \le\log y\le 2\sum_{j=0}^7\frac{s^{2j+1}}{2j+1} +\frac{2s^{17}}{17(1-s^2)}. \tag{138}\] It follows by summing the positive series for \(2\operatorname{arctanh}s\) and bounding its tail geometrically. For a positive rational \(x\), write \(x=2^a y\) with \(1\le y\le2\) and use \(\log x=a\log2+\log y\). Rational substitution in (138) gives \[\begin{array}{c|c} x&\text{bounds for }\log x\\ \hline 2&(0.69314,\;0.69316)\\ 3&(1.098,\;1.0987)\\ 19&(2.9444,\;2.9445)\\ {[49.2878,49.2890]}&(3.89765,\;3.89772)\\ 9/7&(0.250,\;0.252)\\ 10&>2.3025\\ 2.95&>1.0817. \end{array}\] For the dual witness, \[\delta_{24}= \frac{3(1-\rho_8)}{1-\rho_8^3}\log(9/7);\] the displayed bounds for \(\rho_{24}\) and \(\delta_{24}\) now use only rational arithmetic. Alternating Taylor bounds through degrees six and seven give \[e^{-0.354}>0.701,\qquad e^{-0.348}<0.707,\qquad e^{-0.86}>0.4225.\] Consequently the logarithm series at \[(1+0.701)^2-1,\quad (1+0.707)^2-1,\quad (1+0.4225)^3-1\] proves \(0.635<z_{48}<0.651\) and \(z_{288}>0.628\). Also \[\delta_{96}<\frac{2\cdot0.651}{1+0.536}<0.86.\] The remaining \(\rho\) inequalities are direct rational powers. This verifies every inequality used in (134). The cube-root brackets and the expression for \(g\) similarly verify the curve certificate.

For reference only, evaluation of the exact formulas gives \[\begin{array}{c|c} \text{quantity}&\text{approximate value}\\ \hline 2D_{288}/\log2&0.466101554898\\ 2g(2/3)/h(2/3)&0.709698932519\\ 6\log3/h(2/3)&2.091251835621\\ 216\log3/\log N&2.266187438999. \end{array}\] The proofs above rely on the rational inequalities, not these decimal approximations. The accompanying certificate scripts reproduce the finite support/count calculations and all stated rational enclosures. In a fresh writable copy of verification/certificates/, the command python3 checks/run_checks.py uses integer and rational arithmetic from the Python standard library; its three checkers separately verify the numerical inequalities, finite supports and counts, and declared baseline data. The optional numerical diagnostics are not used in these certificates.

A separator preserved by the baseline operations

Let \[ q_*=0.45,\qquad v_p=\frac{p-2}{1-q_*},\qquad u_p=1-\frac{q_*v_p}{2},\qquad 2<p\le2.258. \tag{139}\] Then \(0<v_p\le u_p\le1\). For a triple with smallest coordinate \(c\), put \[ P_p(a,b,c)=u_p(a+b)+v_pc. \tag{140}\] Equivalently, without ordering the coordinates, \[P_p(a,b,c) =u_p(a+b+c)+(v_p-u_p)\min(a,b,c),\] the maximum of the three linear forms that assign \(v_p\) to one coordinate and \(u_p\) to the other two.

For any additional old input it suffices to check the plane at \(p=2.258\) together with the usual size bound. Indeed, after ordering, \[P_p(a,b,c)=a+b+v_p\bigl(c-q_*(a+b)/2\bigr).\] If the parenthesis is nonnegative, this increases with \(p\). Otherwise it is at most the size bound \(a+b\).

For shapes \((1,\ell,1)\), the test at \(p=2.258\) is \[ P_{2.258}(1,\ell,1)= \begin{cases} 2+\dfrac{0.258}{0.55}(\ell-0.45),&0\le\ell\le1,\\[2mm] u_{2.258}(1+\ell)+v_{2.258},&\ell\ge1. \end{cases} \tag{141}\] If \(\ell\le0.45\), or \(\ell\ge2/0.45-1\), it already follows from the size bound. Between those regimes the following downward roundings of the published entry values suffice. They are bounds on the reported costs, not lower bounds on matrix-multiplication exponents. \[\begin{array}{c|rrrrrrrr} \ell&.50&.527\text{--}.528&.55&.60&.65,.70& .75,.80&.85,.90,.95&1\\ \hline \text{entry at least}&2.04&2.05&2.06&2.09&2.12&2.18&2.24&2.36 \end{array}\] \[\begin{array}{c|rrrrr} \ell&1.10,1.20&1.50&2&2.50&3\\ \hline \text{entry at least}&2.44&2.71&3.16&3.60&4.05. \end{array}\] For example, the newer entries at \(\ell=.50,.60,.70\) are \(2.042776,2.092351,2.152770\), respectively (Alman et al. 2025). All displayed roundings satisfy (141) by substitution. The other entries either lie in the automatic size-bound region or are covered by these grouped tests. It follows from 49 that every estimate generated by \(\mathcal B_p\) remains on or above \(P_p\).

The strict improvement interval

The endpoint at one is excluded because the comparison uses the same square point on both sides. By [thm:square], \(w(1)<2.258\), so 50 applies at \(p=2.258\) and proves strict improvement over \(\mathcal B_{2.258}\) throughout \(0.321334<k<1\). If a more precise old exponent-two endpoint is supplied, the same statement uses that endpoint in place of the rounded table entry. No strict improvement is asserted where the baseline already gives two.

There is also a comparison using only the constructions in \(\mathcal F_7\). Interpolate their three proved points \[(0.465,2),\qquad(0.709,2.092),\qquad(1,2.267).\] Against the numerical \(p=2.258\) separator, the comparisons at \(k=0.465,0.709,0.93\) are \[\begin{array}{c|ccc} k&0.465&0.709&0.93\\ \hline \text{new line}&2&2.092&2.224903780\ldots\\ \text{separator}&2.007036363\ldots&2.121494545\ldots& 2.225163636\ldots . \end{array}\] Both differences are affine on the intervening segments. The smallest endpoint margin is greater than \(0.0002598\); these inequalities also follow directly from rational arithmetic. Thus this finite family improves that numerical baseline through \(k=0.93\), in addition to the flat-range improvement.

A sufficient test for further old estimates

The table comparison can be extended without evaluating a large nonconvex parameter program, provided the extra input estimates satisfy an explicit condition. Let \(f\) be the convex upper-bound envelope from such old estimates before adding the new square point. Suppose \[ f(.50)\ge2.035,\qquad f(.60)\ge2.087, \tag{143}\] and include the known estimates \[f(.40)\le2.010,\quad f(.50)\le2.043,\quad f(.60)\le2.093,\quad f(.70)\le2.154.\] Condition (143) concerns the specified envelope of estimates. The published record values alone do not prove it for every possible untabulated parameter choice.

This is a sufficient inclusion rule for further baseline inputs, not a claim about all future analyses of the source tensors. For an enlarged baseline, 50 gives strict improvement wherever that baseline exceeds two in \(0<k<1\). The comparison with \(\mathcal B_{2.258}\) uses the proved dual-exponent witness together with [thm:square]; the extension in 51 still requires (143). The finite-family numerical bounds were established independently in 12.

Inputs and source identity.

The directory verification/certificate/ contains the 52 exact decimal coefficients of the barrier, both integer coefficient charts, all numerical generators and checkers, and their reference outputs. The packet manifest records the size and SHA-256 of every source and input file. The README describes the package, and the supplemental checker verifies the additional arithmetic bounds used in this manuscript.

The two chart hashes are

qP420_gmp:
7dc037ea127cece2216f3219eeeca4cdab0288319a10111a78d272586b776f0b
qP780_gmp:
f23c0480f1109509545fdd17bb4de81602f50952411554b337105defbe7a070c

The barrier coefficient file, inputs/newc22, has SHA-256

41d42a58936b9da0f01a98a24fc4e998a00b83c9f4032a4ae166b7ef11073912

The working-copy path substitutions made by the driver are recorded separately from the source hashes. They change input locations and compiler selection, not arithmetic formulas or thresholds.

Running the check.

A standard run requires Python 3.10 or later, a POSIX system supporting fork, a C++17 compiler with signed 128-bit integer support and UndefinedBehaviorSanitizer, and the GMP C++ library for chart generation. A preflight checks the additional assumptions of a 64-bit long and arithmetic right shift of signed negative integers. Assertions must remain enabled. From verification/certificate/, run

python3 reproduce.py \
  --cxx 'g++ -fsanitize=undefined -fno-sanitize-recover=all' \
  --work-dir ../../certificate-run
python3 verify_manuscript_bounds.py --work-dir ../../certificate-run

A compatible Clang installation may be selected instead. The commands make no network requests or package installations. They write into a new output directory and refuse to overwrite an existing run or supplemental report. The optional flag --reuse-charts uses the supplied chart bytes after hash verification; omitting it regenerates both charts.

This distinction matters mathematically. The low-degree residual calculation uses the rounding-defect bound for the coefficient recurrence. Matching a stored hash alone does not independently establish that recurrence. Both full charts were regenerated with GMP integer arithmetic, with fail-fast undefined-behavior checks, and found to agree byte-for-byte with the supplied inputs. Separate small-degree comparisons also matched the GMP generator against the Python recurrence. The computation of the residual and chart differences then uses exact integer upper bounds.

Finite coverage.

The complete run passed all stages listed below. The preserved command records include compiler flags, exit codes, source substitutions, hashes, and logs.

The finite tensor examples check selected identities; their general forms are proved earlier. For the interior run, the sector identifiers were independently checked to be exactly \(0,\ldots,127\), without omissions or duplicates. Each saved sector-input hash agreed with the corresponding reference hash, and every checker process returned success. The interval checker rejects an unresolved box at its maximum depth rather than accepting it.

The reproduced boundary output is

h -4180063084
b 0 65536 amb 6 terms 7250 edge 128315602072 cap 152568202355

In particular, the actual edge-sample minimum is \[\frac{128315602072}{2^{52}}>28.49\cdot10^{-6}.\] The boundary proof uses this stronger measured minimum when paying its conservative endpoint and displacement allowances. It does not replace it by the checker’s weaker acceptance threshold \(12\cdot10^{-6}\). A supplemental execution also asserted that each endpoint gap used in a nonambiguous boundary interval had actually been evaluated; its full output was unchanged.

The interface with the analytic estimates.

The rational certificate gives \[\varepsilon<3.329\cdot10^{-22},\qquad \frac{6\varepsilon}{2\cdot10^{-9}}<10^{-12},\qquad \varphi(0)-\log 3>7.0946\cdot10^{-6}.\] The logarithm comparison uses a finite positive series for \(2\operatorname{atanh}(1/2)\) and an exact geometric remainder. The physical fourth-derivative coefficient sum is also checked exactly to be less than \(435\cdot10^6\).

The final-summary program takes the analytic interior margin \(9.8\cdot10^{-8}\), boundary margin \(5.5\cdot10^{-6}\), and inset cost \(1.3\cdot10^{-6}\) as inputs; it does not prove those estimates. The supplemental program verify_manuscript_bounds.py explicitly records this interface, checks the actual boundary minimum and the exact allowance subtractions, and rechecks the complete interior-sector identities and hashes. The justification of each allowance, and hence of the continuum conclusion, is the analytic argument of 35. These programs are not a proof-assistant formalization and do not claim a practical matrix-multiplication implementation.