A LOWER BOUND FOR THE FILLING AREA OF THE CIRCLE

Introduction

Let $S^1_{2\pi} = \mathbb{R}/2\pi\mathbb{Z}$ carry its intrinsic length metric

An isometric filling of $S^1_{2\pi}$ is a compact connected Riemannian surface $M$ with one boundary component and an arclength parametrization $\gamma:S^1_{2\pi}\longrightarrow\partial M$ such that

Here $d_M$ is the intrinsic Riemannian distance on $M$. Equivalently, one may require the left-hand side to be at least the right-hand side: the reverse inequality follows by using a shorter boundary arc.

Gromov’s filling area conjecture asserts that every orientable isometric filling of $S^1_{2\pi}$ has area at least $2\pi$; a hemisphere attains this value [4]. The distinction between fixed and unrestricted topology is essential. Classical results establish filling minimality for the disk and for further classes of surfaces [1, 5]. The present paper concerns all orientable fillings, with no bound on their genus.

By scaling, the corresponding bound for a circle of arbitrary length $L>0$ is

We do not claim that $\rho_*$ is optimal.

Recent universal estimates use discrete methods [2], Fourier coefficients of boundary distance functions [3], and calibrations of polyhedral fillings in maximum norm spaces [6]. The estimate above is larger than the universal orientable lower bounds established in those papers. Our construction also uses distance coordinates and piecewise constant alternating forms. Its additional ingredients are refinement confined to endpoint bands, inheritance between different numbers of anchors, and a norm estimate for positive combinations of two coefficient systems. Laurent polynomials allow selected matrix norm bounds to exploit the fact that the tangent space has dimension two.

The proof has an analytic part and a finite arithmetic part. We prove the boundary integral formula for the actual step functions by Lipschitz Stokes, and justify the reduction to finitely many distance profiles, including profiles on grid lines. We then give the precise integer and rational tests for the coefficient arrays in the electronic supplement. No numerical optimization or earlier certificate is needed to verify these data. The theorem is a computer-assisted inequality; the supplement forms part of its finite proof.

Distance coordinates and boundary integrals

Let $M$ be a compact connected oriented Riemannian surface with one boundary component. We assume that an arclength parametrization $\gamma:\mathbb{R}/2\pi\mathbb{Z}\longrightarrow\partial M$, compatible with the boundary orientation, satisfies

Here the distance on the right is the length of the shorter circular arc. The usual filling condition with $\ge$ in (4) is equivalent to this condition: the reverse inequality follows by using a boundary arc as a path in $M$.

Fix an integer $n\ge2$, put $h=\pi/n$ and $\alpha_i=ih$, and define

We extend the indices by $F_{i+n}=-F_i$ and $X_{i+n}=-X_i$. Each $F_i$ is 1-Lipschitz. Applying the reverse triangle inequality to the two distances in (5) gives $\lvert F_{i+1}-F_i\rvert\le h$, including the last inequality with $F_n=-F_0$. Consequently $X=(X_0,\ldots,X_{n-1})$ takes its values in the polytope

For $0\le i<j<n$ and $k=j-i$, summation along the two complementary chains of consecutive indices gives

Summation over a chain of length $n$ also gives $\lvert x_i\rvert\le n/2$. Write

Thus $(X_i,X_j)(M)\subset\mathcal{R}_{n,j-i}$.

On the boundary, (4) yields

The pair $(X_i,X_j)$ maps the positively oriented boundary of $M$ onto $\mathcal{R}_{n,k}$ once, with positive orientation. Indeed, the parameters $\alpha_i,\alpha_j,\alpha_i+\pi,\alpha_j+\pi$ give, in that order, the four corners

Between consecutive parameters the two coordinates are affine, with successive directions $(-1,1),(-1,-1),(1,-1),(1,1)$. These are the four edges of the rectangle in counterclockwise order.

We shall integrate forms with coefficients that are constant on finitely many rectangles. The following elementary version of Stokes’ theorem also addresses the level sets on which such coefficients jump.

The boundary calculation (2.7) identifies the last integral with

The planar formula in Lemma 2.1 makes this $\int_{\mathcal{R}_{n,j-i}} \mathbf{1}_I(s)\mathbf{1}_J(t)\,ds\,dt$, as asserted. □

Let

be a finite grid. For $1\leq k<n$, let $f_k$ have the constant value $c_{k,a,b}$ on $\mathcal{R}_{n,k}\cap(I_a\times I_b)$. Set $f_k(s,t)=0$ if $s$ or $t$ is a grid value. At an edge or corner of $\mathcal{R}_{n,k}$ the cell value is retained unless one of its coordinates is a grid value. Define the measurable two-form

and its boundary action

Proposition 2.2 immediately gives

There are $n-k$ pairs with separation $k$, which accounts for that factor in (2.13). Both the coefficients and the action may be signed. The formula is unchanged if all the anchors $\alpha_i$ are translated by the same circular parameter.

Bounds for alternating forms

For a real skew-symmetric $n\times n$ matrix $W$, with upper entries $w_{ij}$, define

This is the comass on the product of $n$ Euclidean unit disks. It is a norm on skew-symmetric matrices, is invariant under conjugation by a signed permutation matrix, and satisfies the triangle inequality. These properties follow directly by changing the vectors $(a_i,b_i)$ in (3.1).

The matrix of a coefficient system $f$ at $x\in\mathcal{E}_n$ is

At a differentiability point of the distance coordinates, choose a positively oriented orthonormal basis $e_1,e_2$ and put $a_i=dF_i(e_1)$, $b_i=dF_i(e_2)$. Since $F_i$ is 1-Lipschitz, $a_i^2+b_i^2\leq1$, and

It follows that any uniform upper bound $U>0$ for $\lVert W_f(x)\rVert_{\mathrm{disc}}$, $x\in\mathcal{E}_n$, gives

Indeed, (3.3) gives $\Omega_f\leq U\,dA$ almost everywhere, and (2.14) evaluates its integral. We use two finite criteria for bounding the norm (3.1).

Proof. The diagonal entries $d_i$ of $D$ are nonnegative by (22). With $z=a+\mathrm{i}b$, one has

For vectors in the unit disks this gives $a^{\mathsf T}Wb\leq\operatorname{tr}D$. Replacing $b$ by $-b$ gives the opposite inequality. The real quadratic form of (23) at $(a,b)$ is twice the displayed Hermitian quadratic form, which proves the equivalence. □

Write $\mathbb{T}=\{z\in\mathbb{C}:|z|=1\}$, and set

Proof. For fixed values of the other coordinates, $C_W$ is a real linear function of $z_i\in\mathbb{R}^2$. Its maximum on a closed disk is attained on its boundary, unless the function is constant, in which case any boundary point has the same value. Starting with a maximizer on the compact product of disks, replace the coordinates successively by such boundary maximizers. This proves the first assertion. Complex conjugation changes the sign of $C_W$, so its maximum also equals the maximum of its absolute value. Finally, multiplication of all coordinates by the same unit complex number leaves $C_W$ unchanged. □

Proof. For $z\in\mathbb{T}^{n-1}$, every $z^\nu$ has absolute value one. Hence

Subtracting the nonnegative sum of squares in (25) proves the stated upper bound for $\widetilde{C}_W$ on the torus. Lemma 3.2 proves (27) on the full product of disks. Only the inequality is extended to the disks; the Laurent identity is used on the torus. □

The identity in (3.8) has a finite exact meaning. If $p(z)=\sum_{\alpha}c_{\alpha}z^{\alpha}$, then on the torus

Thus the identity can be checked coefficient by coefficient using Gaussian rational arithmetic. In particular a conjugate pair $(u+iv)z^{\nu}+(u-iv)z^{-\nu}$ contributes $2u\operatorname{Re}z^{\nu}-2v\operatorname{Im}z^{\nu}$. Both propositions allow coefficients of either sign.

Finite partitions and refinement

Symmetry and finite coverage

Assume that the grid (14) is centrally symmetric: $g_{N-a}=-g_a$. Then $-I_a=I_{a^*}$, where $a^*=N-1-a$. We use coefficient systems satisfying

Each equality is read on the corresponding pair rectangle. The maps $(s,t)\mapsto(t,s)$ and $(s,t)\mapsto(-s,-t)$ preserve $\mathcal{R}_{n,k}$, whereas $(s,t)\mapsto(t,-s)$ maps it onto $\mathcal{R}_{n,n-k}$.

Define the signed permutation matrices $Q$, $R$ by

They preserve $\mathcal{E}_n$. The identities (4.1) imply

For the first identity, entries not crossing the last coordinate are immediate. The remaining upper entries satisfy

which is precisely the sign obtained when the order of the two matrix indices is reversed. For the second identity all upper entries reverse order, and the symmetry $f_k(s,t)=f_k(t,s)$ gives the common minus sign. It follows from (3.1) that the norm is constant on the orbits generated by $Q$, $R$. Here $Q^{2n}=R^2=1$ and $RQR=Q^{-1}$, so there are finitely many transformations. A simultaneous linear combination of coefficient systems obeying (4.1) has the same covariance, using the same transformation for every summand.

Call a label tuple $\mathbf{a}=(a_0,\ldots,a_{n-1})$ admissible if

The associated matrix has upper entries $c_{j-i,a_i,a_j}$. In this definition admissibility asserts only the displayed pairwise conditions.

Proof. Let $x$ be such a point. For every $i<j$, the point $(x_i,x_j)$ lies in the open rectangle $I_{a_i}\times I_{a_j}$ and the closed rectangle $\mathcal{R}_{n,j-i}$. A sufficiently small neighborhood of this point inside the open rectangle meets the interior of $\mathcal{R}_{n,j-i}$ in positive area. This remains true if the point lies on an edge or corner of $\mathcal{R}_{n,j-i}$, since the latter is a nondegenerate convex rectangle. Thus (4.4) holds. The matrix is constant on the indicated box, restricted to $\mathcal{E}_n$. The transformations $Q$, $R$ permute the admissible boxes, by the pair-rectangle symmetries above, and (4.3) preserves the norm. ∎

The finite set in Lemma 4.1 can be enumerated by assigning labels successively and, after every assignment, retaining in each remaining coordinate only the labels compatible with every previous one in (31). Induction on the assigned prefix shows that this procedure lists every admissible tuple. Some listed boxes may have empty intersection with $\mathcal{E}_n$; including their matrices imposes additional inequalities and preserves the conclusion of the lemma.

For $0 < \delta< n/2$ define the endpoint band

Suppose $\pm(n/2-\delta) \in G$. Every open cell is then either inside or outside the corresponding one-dimensional endpoint band. Call a tuple affected if one of its cells is in that band. Any affected tuple can be carried by a power of $Q$ to a tuple whose first cell is in $(-n/2,-n/2+\delta)$. Indeed, move an endpoint coordinate to the first position and use $Q^n=-1$ if its sign is positive. Hence every affected orbit has such a representative; its lexicographically least representative also has its first cell in this initial group of cells. This justifies restricting the first label when enumerating the affected orbits.

Dyadic refinement

Dyadic refinement. Let $f$ be a coefficient system for $m$ anchors. For $n=2m$, define its refinement by

If the parent grid is $G_m$, choose a child grid $G_{2m}$ satisfying

The refinement is constant on the open child cells. In the following identities all coordinate profiles avoid their respective grids.

For $x \in\mathcal{E}_{2m}$ put

Both belong to $\mathcal{E}_m$: each difference is the sum of two consecutive differences divided by two, including the final difference with the antiperiodic convention. By (34), if $x$ avoids the child grid, both profiles avoid the parent grid. Ordering the even coordinates before the odd coordinates gives

where $\simeq$ denotes conjugation by that permutation matrix. In particular

The even child distance coordinates are the parent coordinates, and the odd ones are parent coordinates with all anchors translated by $\pi/(2m)$. The normalized child coordinates are twice the corresponding parent coordinates. Formula (33) therefore gives the average of these two parent forms. Their actions are equal, by (17) and the translation observation following it, and hence

This equality also follows directly from (16), using $\mathcal{R}_{2m,2k}=2\mathcal{R}_{m,k}$ and the factor $1/2$ in (33). The zero values assigned on the extra child grid lines do not change the action. On $M$ the corresponding differentials vanish almost everywhere on those levels, by Lemma 2.1.

A child system may differ from a positive multiple $r\mathcal{D}f$ inside an endpoint band. More precisely, require its coefficient of a pair with both coordinates in $[-n/2+\delta,n/2-\delta]$ to agree with $r\mathcal{D}f$, whenever the two coordinates avoid the child grid. Then (36), multiplied by $r$, holds for every profile outside $B_{n,\delta}$ that avoids the child grid. Profiles inside the band are covered by the affected tuples. The qualification about avoiding the grid is necessary when a refinement introduces extra grid values; we remove it after completing the recursive estimates.

If a parent coefficient is $p/T_{\mathrm{old}}$, a child coefficient is $q/T_{\mathrm{new}}$, and $r=K/T_{\mathrm{new}}$, then the required agreement on an unchanged cell of even separation is precisely

On unchanged cells of odd separation the child coefficient is zero. Thus this part of the refinement condition can be checked by integer multiplication.

Positive combinations through several refinements

Let $n_\ell=2^\ell n_0$ for $0\leq\ell\leq L$. For each source $s\in\{1,\ldots,S\}$, suppose that $f^{(\ell)}$ is a coefficient system at level $\ell$. At a fixed level all sources use the same grid $G_\ell$ and satisfy (28). Assume $2G_{\ell-1}\subset G_\ell$. At levels $\ell\geq1$, choose endpoint bands $B_\ell=B_{n_\ell,\delta_\ell}$ whose thresholds are grid values, and positive constants $r_{s,\ell}$, so that outside $B_\ell$ the child system agrees with $r_{s,\ell}\mathcal{D}f^{(\ell-1)}$ in the sense just specified. Write $W_s^{(\ell)}=W_{f_s^{(\ell)}}$.

For nonnegative numbers $\mu_1,\ldots,\mu_S$, put

An empty product is one. Thus, for three levels, the weights are $\mu_s$ at level 2, $\mu_sr_{s,2}$ at level 1, and $\mu_sr_{s,2}r_{s,1}$ at level 0.

Proof. We prove the assertion at every level by induction, working throughout with profiles off the corresponding grids. At level 0 it is Lemma 4.1. At a higher level, an affected profile has an affected admissible tuple, so the asserted bound is one of the premises. At a profile outside $B_\ell$, coefficient inheritance and $\beta_s^{(\ell)}r_{s,\ell}=\beta_s^{(\ell-1)}$ give

The parity profiles belong to $E_{n_{\ell-1}}$ and avoid its grid. The induction hypothesis bounds both blocks by $U$, so (37) bounds their average by $U$. The two parity profiles may correspond to different tuples; the common bound $U$ applies to both. Finally, the simultaneous covariance in (30) proves the assertion about representatives. ∎

The premises have two useful finite forms. If a certified upper bound $u_{s,\ell,\mathbf{a}}$ is available for the matrix of source $s$ at a required tuple $\mathbf{a}$, the triangle inequality gives the bound

for the mixture at that tuple. One may instead apply Proposition 3.3 directly to the matrix $\sum_s\beta_s^{(\ell)}W_s^{(\ell)}(\mathbf{a})$. This second certificate must refer to this exact weighted matrix, with all summands evaluated at the same tuple. Either bound can be used for each tuple, and any common upper bound for the resulting finite list serves as $U$. The factors $1/2$ occur in the averages (42); they are not additional factors in (43).

Values on the grids

We now extend the estimate at the finest level to all profiles. The following argument applies to either type of matrix certificate and to their positive combinations.

Proof. The polytope $\mathcal{E}_n$ is full dimensional, since its defining inequalities are strict at the origin. Its interior is dense in it, and removing finitely many coordinate hyperplanes leaves a dense set. Thus every $x\in\mathcal{E}_n$ is a limit of profiles avoiding $G$. For such a profile $y$ sufficiently close to $x$, every coordinate of $x$ outside $G$ and the corresponding coordinate of $y$ lie in the same open cell. The submatrix on those indices is therefore the prescribed one at $x$. Given vectors in the unit disks for all indices, replace those indexed by grid coordinates of $x$ by zero. Evaluating $W(y)$ on the resulting vectors is exactly the same as evaluating the extended $W(x)$ on the original vectors. The former is bounded in absolute value by $U$. Taking the maximum proves the assertion.*

Apply Lemma 4.3 once to the finest mixture in Proposition 4.2. All ancestor estimates have already been established off their grids, since the grids are nested as in (34). The extension is the coefficient convention in (15). On the preimage of any grid value of $X_i$, $dF_i=0$ almost everywhere; hence this convention also gives the required pulled-back form when such a level set has positive area. There is no need to assume that these preimages have measure zero.

By linearity of the boundary action, the integral of the resulting finest form is

Consequently, if $U>0$, the complete finite set of premises in Proposition 4.2 yields

Every quantity on the right is determined by finitely many cell areas, coefficient values, and matrix certificates. When the grid values, coefficients, and certificate entries are rational, the cell areas in (16) are rational, and all remaining assertions reduce to the finite matrix and rational inequalities in the two certificate criteria.

The rational certificate

We now specify the finite data used in the proof. The two collections of coefficients will be denoted by $a=1,2$. Each collection has three levels, with $n=14,28,56$. These levels are parts of a single construction. All integers and rational arrays in this section are supplied in the electronic supplement. At a fixed level $n$, abbreviate $R_{n,k}$ to $R_k$.

Grids and coefficient arrays

Put

The numbers of open intervals are 28, 36, 56, respectively. In particular, $2G_{14}\subset G_{28}$ and $2G_{28}\subset G_{56}$. The endpoint band has width 2 at each of the last two levels.

For a grid $G_n=\{t_0<\cdots<t_N\}$, write $I_u=(t_u,t_{u+1})$. The coefficient classes are the equivalence classes of triples $(k,u,v)$, $1\leq k<n$, for which $\operatorname{Area}(R_k\cap(I_u\times I_v))>0$, under

Each class is represented by its lexicographically least triple. The list of these representatives in lexicographic order is denoted by $\mathcal{K}_n$. The supplement supplies the integer vector $(p_{a,n,\kappa})_{\kappa\in\mathcal{K}_n}$. On a pair cell with class $\kappa$, the coefficient is

As in the preceding sections, incident coefficients are set to zero on coordinate grid lines. The resulting form is denoted by $\Omega_{a,n}$.

The positive integers used for normalization and inheritance are as follows.

$a$	$n$	$K_{a,n}$	$T_{a,n}$
1	14	100000000	100000344
1	28	1250004300000000	1250009954439084
1	56	31250248860977100000000	31251408412709010636800
2	14	100000000	100001194
2	28	5000059700000000	5000141045182364
2	56	125003526129559100000000	125100260860029607051264

For $n=28,56$, put $r_{a,n}=K_{a,n}/T_{a,n}$. On every pair cell outside the endpoint band, the coefficient vectors satisfy the following integer identities. If $k$ is odd, then $p_{a,n,\kappa}=0$. If $k$ is even and $\kappa'$ is the parent cell class obtained by replacing $(k,s,t)$ with $(k/2,s/2,t/2)$, then

The containment of grids in (45) makes the parent class unambiguous on every open child cell. Thus, away from the finest grid, $\Omega_{a,n}$ agrees outside its endpoint band with $r_{a,n}$ times the average of the two rotated parent forms.

The sizes of the arrays and the complete coverage counts are

$n$	$\#\mathcal{K}_n$	Changed classes	Inherited classes	Rooted boxes	Matrix patterns
14	346	346	0	2975284	53538
28	1382	176	1206	69474	29640
56	8092	162	7930	30856	14590

At the first level, all compatible boxes are enumerated. At the last two levels, rooted boxes means compatible boxes whose first coordinate lies in the negative endpoint band. The symmetry argument in the preceding section covers every affected box from these rooted boxes. The same ordered pattern arrays are used for $a=1$ and $a=2$.

A pattern records the index in $\mathcal{K}_n$ of the class of each pair $(i,j)$, with $i<j$ and pairs in lexicographic order. For each admissible box, take the lexicographically least such vector under the cyclic and reversed orders of its vertices. The covariance identities (30) justify these operations. Duplicate vectors are removed, and the distinct vectors are sorted lexicographically. This defines the ordered pattern array used below.

Matrix and polynomial witnesses

For a stored pattern $\tau$, let $P_{a,n,\tau}$ be the real skew-symmetric matrix whose upper entries are the corresponding $p_{a,n,\kappa}$. The data include positive integers $d_{a,n,\tau,0},\ldots,d_{a,n,\tau,n-1}$ satisfying

Consequently, the norm of this pattern of $\Omega_{a,n}$ is bounded by

At level 56, selected bounds are reduced by the Laurent-polynomial criterion proved above, for the same coefficients $p_{a,56,\kappa}/T_{a,56}$. There are sixteen such certificates for $a=1$, and eight for $a=2$. In this notation $b_{a,56,\tau}$ will mean the smaller of the diagonal bound and the polynomial bound when a polynomial certificate is supplied. The coefficients of the form are unchanged.

Set

For $n=56,28,14$, define

A first bound for a pattern at level $n$ is

For eighty-four specified patterns, the supplement gives a polynomial certificate directly for the mixed matrix

Of these certificates, sixty-four belong to level 14 and twenty to level 28. For each certificate, the target edge weights are compared, as rational numbers, with (53) before its bound is used. Let $\widehat{B}_{n,\tau}$ be the smaller of $B_{n,\tau}$ and this additional bound, when present, and let $\widehat{B}_{n,\tau}=B_{n,\tau}$ otherwise.

Proof. All tests in this proposition are finite integer or rational computations. We describe the tests and their mathematical justification; the complete arrays and executable implementations accompany the paper.

First compute the area of every $R_k \cap(I_u \times I_v)$. Start with the closed rectangle $[t_u,t_{u+1}] \times[t_v,t_{v+1}]$, and successively intersect it with the four half-planes

All vertices remain rational. At an edge from $x$ to $y$ meeting $L(z)=c$, the new vertex is

The shoelace formula gives its area exactly. A pair of labels is compatible if and only if this area is positive. These tests also reconstruct every coefficient key and the boundary weights

To enumerate boxes, choose the coordinate labels in order. After assigning label $u_i$, delete from the domain of every later coordinate $j$ the labels incompatible with $(u_i,u_j)$. A branch is discarded only if a domain is empty. At level 14 every initial domain consists of all labels. At levels 28 and 56, only the first domain is restricted to the negative endpoint band. This gives every all-pairs-compatible box in the relevant rooted set by induction on the number of assigned coordinates. Reduce the boxes and their coefficient patterns by the signed symmetries, discard duplicate patterns, and compare with the supplied arrays. This yields the counts in the table. The coverage lemma shows why this computation suffices for all actual distance profiles, without assuming joint realizability of every enumerated box.

For each unchanged coefficient, locate the containing parent cell after dividing its endpoints by two and check (5.4) by integer multiplication. The numbers of identities checked at levels 28 and 56 are 1206 and 7930, respectively, in each collection.

The matrix tests are performed on the actual integer entries. Two exact tests are used. Write $H = 2\operatorname{diag}(d) + iP$. The first test constructs a Gaussian rational matrix $L$ for the normalized matrix $A = H/K$, where $K = K_{a,n} > 0$, and proves

At level 14, the same test instead uses a real rational Gram factor for the real representation of $H/(2K)$. Denominators are cleared before every comparison. Indeed, for a Hermitian matrix $R$, the estimate $2\lvert z_i\rvert\lvert z_j\rvert\le\lvert z_i\rvert^2 + \lvert z_j\rvert^2$ proves

Thus (57) proves strict positivity of the normalized matrix, and hence of $H$. The real Gram test has the same implication.

The second test uses the real symmetric representation

An exact Schur complement may first eliminate positive principal blocks; every zero entry required for a block separation is checked in $\mathcal{H}$ itself. For the remaining rational symmetric matrices, clear a positive common denominator and perform fraction-free elimination. With $p_{-1} = 1$, the elimination step is

Every division is required to be exact and every pivot strictly positive. The determinant identity underlying elimination identifies these pivots with successive leading principal minors. Their positivity is equivalent to a positive diagonal in the $LDL^{\mathsf{T}}$ decomposition. The Schur-complement identity then proves positivity of the original matrix. The trace tests in (49) are integer sums. Both methods pass for every matrix in the table. The fraction-free elimination is evaluated directly with Python integers at level 14, and with FLINT at levels 28 and 56.

A failed numerical Gram proposal is never accepted. The programs then use exact elimination or an exact characteristic-polynomial test. For a real symmetric matrix $S$, strict positivity of every coefficient of $\det(tI + S)$ implies $S \succ0$: the polynomial has no zero for $t \ge0$, while a nonpositive eigenvalue of $S$ would give such a zero. All matrices in the present data pass the Gram criterion itself.

For completeness, the polynomial test has the following integer form. Write its Gaussian rational polynomials with common denominator $D_{\mathrm{pol}} > 0$, and its rational target edge weights with common denominator $D_{\mathrm{wt}} > 0$. Set $q = \operatorname{lcm}(D_{\mathrm{pol}}^2, D_{\mathrm{wt}})$. Direct convolution of the integer polynomial coefficients gives

where the coordinate $z_0$ has been fixed to $1$, $b_0$, $b_{\nu}$, $c_{\nu}$ are integers and $\mathcal{V}$ contains one representative of each nonzero exponent pair $\{\nu,-\nu\}$. The rational upper bound checked by the program is

For an integer $m \ge0$, the ceiling square root is determined by integer comparisons: it is $\lfloor\sqrt{m}\rfloor$ when $m$ is a square and $\lfloor\sqrt{m}\rfloor+1$ otherwise. Thus no floating-point inequality enters (5.16). The two supplied polynomial implementations independently expand every square and obtain the same bound. The phase-to-disk lemma makes this a bound for the required two-dimensional norm.

Finally, compare all grids, keys and patterns directly, form the rational weights (5.7), and compute every $\widehat{B}_{n,\tau}$. Their maximum is exactly (5.10). It is attained at pattern 646 of level 28, with patterns indexed from zero as in the supplied arrays. The action is independently computed from (5.12):

This gives (5.11), and the boundary integral identity gives the final assertion.

Completion of the proof

Proof of Theorem 1.1. Use the level-56 distance functions, with

First suppose that the level-56 profile avoids its grid. At a profile in the level-56 endpoint band, its pattern is covered by Proposition 5.1, and $|\Omega(e_1,e_2)|\le U$. Outside that band, the inheritance identities express this form as the average of two rotated level-28 mixed forms with weights $c_{a,28}$. Each of the two level-28 profiles either lies in its endpoint band, where its mixed budget is at most $U$, or lies outside the band. In the latter case, inheritance expresses the corresponding mixed form as the average of two rotated level-14 mixed forms with weights $c_{a,14}$. All level-14 profiles are covered. The triangle inequality for each average therefore gives the common bound $U$ on every off-grid profile. The zero-coordinate extension lemma extends it to grid profiles. For the actual distance functions, all omitted rows have zero differential almost everywhere on their corresponding grid level sets. Hence

The boundary integral identity and (5.11) give

Exact rational simplification using (5.6), (5.10) and (5.11) yields

This proves the asserted inequality.

Appendix A. Exact reproduction and decimal enclosures

The electronic supplement is part of the finite certificate. It contains the six matrix data files, the two lists of source polynomial bounds, the eighty-four mixed polynomial bounds, and all verification programs. The file proof/certificate_manifest.json identifies each base array by its source index $a$ and level $n$, and records the file identities of all finite data. In the base JSON files, coefficient_numerators stores the vector $p$, diagonal_numerators stores the rows $d$, and scaling_numerator is $T$. The auxiliary integer $K$ is the field denominator at level 14, and coefficient_denominator at levels 28 and 56. The entry point proof/verify_all.py regenerates the profile coverage and performs all matrix, polynomial, inheritance and final-budget tests. The original numerical optimization is not needed for this verification. Python with NumPy and python-flint, together with a C++17 compiler, suffices. Every acceptance test is an exact integer or rational comparison; fixed-width products are used only with explicit bounds preventing overflow. Floating-point linear algebra is used only to propose a Gram factor that is subsequently checked exactly.

The following order makes the dependencies explicit:

1. Recompute all clipped pair areas and the complete level-14 coverage; verify both level-14 matrix collections.

2. Recompute the level-28 coverage, exact inherited coefficients, and every level-28 matrix; repeat at level 56.

3. Expand all 108 Gaussian polynomial certificates in two independent implementations and compare every target edge with its actual rational coefficient.

4. Compare the two collections’ profile arrays, compute all 97768 mixed budgets, and recompute the boundary action and $\rho_\ast$.

Successful verification therefore uses the finite arrays themselves, rather than a record that a previous computation succeeded.

The displayed decimal can also be enclosed using rational arithmetic. For $q > 1$, put

For even $N$, the alternating-series estimate gives

Machin’s identity

then gives rational lower and upper bounds for $\pi$. With $N = 64$, squaring these positive bounds and multiplying by the positive rational number $\rho_\ast$ proves

The supplement includes this integer check.

References

Zhili College, Tsinghua University, Beijing 100084, China

Email address: [email protected]