\documentclass[12pt,a4paper,reqno]{amsart}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage[a4paper,margin=27mm]{geometry}
\usepackage{amsmath,amssymb,mathtools,booktabs,enumitem,needspace}
\usepackage{microtype}
\usepackage[hidelinks]{hyperref}
\hypersetup{
 pdftitle={A lower bound for the filling area of the circle},
 pdfauthor={Qiyue Tang},
 pdfsubject={An exact universal lower bound for orientable isometric fillings},
 pdfkeywords={filling area, boundary distance, calibration, exact certificate}
}
\numberwithin{equation}{section}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}
\newcommand{\R}{\mathbb R}
\newcommand{\C}{\mathbb C}
\newcommand{\Z}{\mathbb Z}
\newcommand{\Q}{\mathbb Q}
\newcommand{\ii}{\mathrm i}
\newcommand{\Area}{\operatorname{Area}}
\newcommand{\tr}{\operatorname{tr}}
\newcommand{\diag}{\operatorname{diag}}
\newcommand{\calE}{\mathcal E}
\newcommand{\calR}{\mathcal R}
\newcommand{\eps}{\varepsilon}
\title[A lower bound for the filling area of the circle]{A lower bound for the filling area of the circle}
\author{Qiyue Tang}
\address{Zhili College, Tsinghua University, Beijing 100084, China}
\email{tangqy24@mails.tsinghua.edu.cn}
\date{November 9, 2026}
\subjclass[2020]{53C23, 53C20, 49Q20}
\keywords{Filling area, boundary distance, calibration, exact certificate}
\begin{document}
\begin{abstract}
We prove that every compact connected orientable Riemannian surface
isometrically filling the circle of length \(2\pi\) has area at least
\(6.06571278970403721852\). The exact bound is a specified rational
multiple of \(\pi^2\), and no restriction is imposed on the genus.
The proof uses alternating forms built from antipodal distance
differences. Finite partitions of the distance profiles, a three-level
inheritance construction, and positive combinations of two coefficient
systems reduce the norm estimate to rational matrix and Laurent-polynomial
certificates. We give the geometric reduction and all exact verification
criteria. Complete finite data and independent arithmetic checks
accompany the paper.
\end{abstract}
\maketitle

\section{Introduction}

Let \(S^1_{2\pi}=\R/2\pi\Z\) carry its intrinsic length metric
\[
 d_{S^1}(s,t)=\min_{m\in\Z}|s-t+2m\pi|.
\]
An \emph{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
\begin{equation}\label{eq:filling}
 d_M(\gamma(s),\gamma(t))=d_{S^1}(s,t)
 \qquad(s,t\in S^1_{2\pi}).
\end{equation}
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 \cite{Gromov}. The distinction between fixed and unrestricted
topology is essential. Classical results establish filling minimality
for the disk and for further classes of surfaces
\cite{BCIK,Ivanov}. The present paper concerns all orientable fillings,
with no bound on their genus.

\begin{theorem}\label{thm:main}
Let \(M\) be a compact connected orientable Riemannian surface with exactly
one boundary component. Suppose that an arclength parametrization of
its boundary satisfies \eqref{eq:filling}. Then
\begin{equation}\label{eq:mainbound}
                     \Area(M)\geq \rho_*\pi^2,
\end{equation}
where
\begin{equation}\label{eq:rho}
 \rho_*=
 \frac{2003451650178971284257400112098931034076276719384090896484375}
      {3259843634129750064586400053851596684985686473853019071267024}.
\end{equation}
In particular,
\[
                     \Area(M)>6.06571278970403721852.
\]
\end{theorem}

By scaling, the corresponding bound for a circle of arbitrary length
\(L>0\) is
\[
                          \Area(M)\geq\frac{\rho_*}{4}L^2.
\]
We do not claim that \(\rho_*\) is optimal.

Recent universal estimates use discrete methods \cite{BW}, Fourier
coefficients of boundary distance functions \cite{CLZ}, and calibrations
of polyhedral fillings in maximum norm spaces \cite{Zust}. 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.


% Purely geometric sections.  The main statement and the exact certificate
% data are supplied in the surrounding paper.  All labels have prefix geo:.

\section{Distance coordinates and boundary integrals}
\label{geo:sec-distance}

Let $M$ be a compact connected oriented Riemannian surface with one boundary
component.  We assume that an arclength parametrization
$\gamma\colon\mathbb R/2\pi\mathbb Z\longrightarrow\partial M$, compatible
with the boundary orientation, satisfies
\begin{equation}
 d_M(\gamma(s),\gamma(t))=d_{\mathbb R/2\pi\mathbb Z}(s,t).
 \label{geo:boundary-distance}
\end{equation}
Here the distance on the right is the length of the shorter circular arc.
The usual filling condition with $\geq$ in
\eqref{geo:boundary-distance} is equivalent to this condition: the reverse
inequality follows by using a boundary arc as a path in $M$.

Fix an integer $n\geq2$, put $h=\pi/n$ and $\alpha_i=ih$, and define
\begin{equation}
 F_i(p)=\frac{d_M(p,\gamma(\alpha_i+\pi))
                   -d_M(p,\gamma(\alpha_i))}{2},
 \qquad X_i(p)=\frac{F_i(p)}h,
 \quad 0\leq i<n.
 \label{geo:distance-coordinates}
\end{equation}
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 \eqref{geo:distance-coordinates} gives
$|F_{i+1}-F_i|\leq h$, including the last inequality with $F_n=-F_0$.
Consequently $X=(X_0,\ldots,X_{n-1})$ takes its values in the polytope
\begin{equation}
 \mathcal E_n=
 \{x\in\mathbb R^n:|x_{i+1}-x_i|\leq1\ (0\leq i<n),\ x_n=-x_0\}.
 \label{geo:profile-polytope}
\end{equation}
For $0\leq i<j<n$ and $k=j-i$, summation along the two complementary
chains of consecutive indices gives
\begin{equation}
 |x_i-x_j|\leq k,\qquad |x_i+x_j|\leq n-k
 \quad(x\in\mathcal E_n).
 \label{geo:pair-constraints}
\end{equation}
Summation over a chain of length $n$ also gives $|x_i|\leq n/2$.
Write
\begin{equation}
 \mathcal R_{n,k}=\{(s,t)\in\mathbb R^2:
             |s-t|\leq k,\ |s+t|\leq n-k\},\qquad 1\leq k<n.
 \label{geo:pair-rectangle}
\end{equation}
Thus $(X_i,X_j)(M)\subset\mathcal R_{n,j-i}$.

On the boundary, \eqref{geo:boundary-distance} yields
\begin{equation}
 F_i(\gamma(s))=\frac\pi2-d_{\mathbb R/2\pi\mathbb Z}(s,\alpha_i).
 \label{geo:boundary-coordinate}
\end{equation}
The pair $(X_i,X_j)$ maps the positively oriented boundary of $M$ onto
$\partial\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
\begin{equation}
 \left(\frac n2,\frac n2-k\right),\quad
 \left(\frac n2-k,\frac n2\right),\quad
 \left(-\frac n2,-\frac n2+k\right),\quad
 \left(-\frac n2+k,-\frac n2\right).
 \label{geo:boundary-corners}
\end{equation}
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.

\begin{lemma}\label{geo:lipschitz-stokes}
If $u,v$ are Lipschitz functions on $M$, then
\begin{equation}
 \int_Mdu\wedge dv=\int_{\partial M}u\,dv.
 \label{geo:stokes}
\end{equation}
For an interval $I=(a,b)$, let
\[
 P_I(t)=\min\{\max\{t-a,0\},b-a\}.
\]
Then
\begin{equation}
 d(P_I\circ u)=\mathbf1_I(u)\,du
 \quad\hbox{almost everywhere on }M.
 \label{geo:clamp-chain-rule}
\end{equation}
\end{lemma}

\begin{proof}
A Lipschitz function has zero differential almost everywhere on any one
of its level sets.  To see this in a coordinate chart, consider a point
where the function is differentiable and the level set has density one.
A nonzero differential would be bounded away from zero, relative to the
distance from the point, in a cone of positive relative measure.
Differentiability would then put that cone outside the level set near
the point, a contradiction.  The differentiation and density theorems
prove the assertion.  The ordinary chain rule away from the two levels
$a,b$, together with this assertion on those levels, proves
\eqref{geo:clamp-chain-rule}.

For completeness, extend $u,v$ in boundary charts, mollify, and combine
the local approximations with a smooth partition of unity.  This gives
smooth functions $u_\varepsilon,v_\varepsilon$ converging uniformly and
strongly in $W^{1,2}$ to $u,v$, with bounded Lipschitz constants.
Stokes' theorem holds for each pair of smooth approximations.  Its left
side converges by the Cauchy--Schwarz inequality.  On the closed boundary,
integration by parts gives
\begin{align*}
 \left|\int_{\partial M}u_\varepsilon\,dv_\varepsilon
             -\int_{\partial M}u\,dv\right|
 &\leq \|u_\varepsilon-u\|_\infty
                    \operatorname{Var}_{\partial M}(v_\varepsilon)\\
 &\quad+\|v_\varepsilon-v\|_\infty
                    \operatorname{Var}_{\partial M}(u).
\end{align*}
The right side tends to zero.  This proves \eqref{geo:stokes} without
requiring convergence of the boundary derivatives.  The same argument
proves the planar formula on a polygon; alternatively, that case follows
by smoothing the two functions and applying Green's theorem.
\end{proof}

\begin{proposition}\label{geo:cell-integral}
For open bounded intervals $I,J\subset\mathbb R$ and $0\leq i<j<n$,
\begin{equation}
 \int_M\mathbf1_I(X_i)\mathbf1_J(X_j)\,dF_i\wedge dF_j
 =h^2\operatorname{Area}\bigl(\mathcal R_{n,j-i}\cap(I\times J)\bigr).
 \label{geo:exact-cell-integral}
\end{equation}
\end{proposition}

\begin{proof}
Apply Lemma~\ref{geo:lipschitz-stokes} to
$P_I(X_i),P_J(X_j)$.  The left side of
\eqref{geo:exact-cell-integral}, divided by $h^2$, is
\[
 \int_Md(P_I(X_i))\wedge d(P_J(X_j))
 =\int_{\partial M}P_I(X_i)\,d(P_J(X_j)).
\]
The boundary calculation \eqref{geo:boundary-corners} identifies the last
integral with
\[
 \int_{\partial\mathcal R_{n,j-i}}P_I(s)\,d(P_J(t)).
\]
The planar formula in Lemma~\ref{geo:lipschitz-stokes} makes this
$\int_{\mathcal R_{n,j-i}}\mathbf1_I(s)\mathbf1_J(t)\,ds\,dt$,
as asserted.
\end{proof}

Let
\begin{equation}
\begin{gathered}
 G=\{g_0<g_1<\cdots<g_N\},\qquad
 g_0=-n/2,\quad g_N=n/2,\\
 I_a=(g_a,g_{a+1})\qquad(0\leq a<N)
\end{gathered}
 \label{geo:grid}
\end{equation}
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
\begin{equation}
 \Omega_f=\sum_{0\leq i<j<n}
             f_{j-i}(X_i,X_j)\,dF_i\wedge dF_j
 \label{geo:step-form}
\end{equation}
and its boundary action
\begin{equation}
 A_n(f)=\frac1{n^2}\sum_{k=1}^{n-1}(n-k)
       \sum_{a,b=0}^{N-1}c_{k,a,b}\,
          \operatorname{Area}\bigl(\mathcal R_{n,k}\cap(I_a\times I_b)\bigr).
 \label{geo:action}
\end{equation}
Proposition~\ref{geo:cell-integral} immediately gives
\begin{equation}
 \int_M\Omega_f=\pi^2A_n(f).
 \label{geo:action-integral}
\end{equation}
There are $n-k$ pairs with separation $k$, which accounts for that factor
in \eqref{geo:action}.  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.

\section{Bounds for alternating forms}
\label{geo:sec-comass}

For a real skew-symmetric $n\times n$ matrix $W$, with upper entries
$w_{ij}$, define
\begin{equation}
 \|W\|_{\mathrm{disc}}
 =\max_{a_i^2+b_i^2\leq1}
       \left|a^{\mathsf T}Wb\right|
 =\max_{a_i^2+b_i^2\leq1}
       \left|\sum_{i<j}w_{ij}(a_i b_j-a_j b_i)\right|.
 \label{geo:disc-comass}
\end{equation}
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 \eqref{geo:disc-comass}.

The matrix of a coefficient system $f$ at $x\in\mathcal E_n$ is
\begin{equation}
 (W_f(x))_{ij}=f_{j-i}(x_i,x_j)\quad(i<j),
 \qquad (W_f(x))_{ji}=-(W_f(x))_{ij}.
 \label{geo:coefficient-matrix}
\end{equation}
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
\begin{equation}
 \Omega_f(e_1,e_2)=a^{\mathsf T}W_f(X)b.
 \label{geo:tangent-evaluation}
\end{equation}
It follows that any uniform upper bound $U>0$ for
$\|W_f(x)\|_{\mathrm{disc}}$, $x\in\mathcal E_n$, gives
\begin{equation}
 \operatorname{Area}(M)\geq\frac{\pi^2A_n(f)}U.
 \label{geo:area-principle}
\end{equation}
Indeed, \eqref{geo:tangent-evaluation} gives $\Omega_f\leq U\,dA$
almost everywhere, and \eqref{geo:action-integral} evaluates its integral.

We use two finite criteria for bounding the norm
\eqref{geo:disc-comass}.

\Needspace{9\baselineskip}
\begin{proposition}\label{geo:diagonal-certificate}
Let $D$ be a real diagonal matrix.  If
\begin{equation}
 D+\frac{\mathrm i}{2}W\succeq0,
 \label{geo:hermitian-condition}
\end{equation}
then $\|W\|_{\mathrm{disc}}\leq\operatorname{tr}D$.
Condition~\eqref{geo:hermitian-condition} is equivalent to positive
semidefiniteness of the real symmetric matrix
\begin{equation}
 \begin{pmatrix}2D&-W\\ W&2D\end{pmatrix}.
 \label{geo:real-block-condition}
\end{equation}
\end{proposition}

\begin{proof}
The diagonal entries $d_i$ of $D$ are nonnegative by
\eqref{geo:hermitian-condition}.  With $z=a+\mathrm i b$, one has
\[
 z^*\left(D+\frac{\mathrm i}{2}W\right)z
   =\sum_i d_i(a_i^2+b_i^2)-a^{\mathsf T}Wb\geq0.
\]
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
\eqref{geo:real-block-condition} at $(a,b)$ is twice the displayed
Hermitian quadratic form, which proves the equivalence.
\end{proof}

Write $\mathbb T=\{z\in\mathbb C:|z|=1\}$, and set
\begin{equation}
 C_W(z)=\sum_{i<j}w_{ij}\operatorname{Im}(\overline z_i z_j).
 \label{geo:phase-polynomial}
\end{equation}

\begin{lemma}\label{geo:torus-disks}
The maximum of $C_W$ on the product of closed unit disks equals its
maximum on $\mathbb T^n$, and both equal $\|W\|_{\mathrm{disc}}$.
The latter maximum may be taken over the subtorus $z_0=1$.
\end{lemma}

\begin{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.
\end{proof}

\begin{proposition}\label{geo:laurent-certificate}
Let $W$ have rational entries.  Put
\[
 \widetilde C_W(z_1,\ldots,z_{n-1})=C_W(1,z_1,\ldots,z_{n-1}).
\]
Suppose that Gaussian rational Laurent polynomials
$p_1,\ldots,p_q$ satisfy, on $\mathbb T^{n-1}$, the identity
\begin{equation}
 \widetilde C_W(z)+\sum_{\ell=1}^q|p_\ell(z)|^2
 =a_0+\sum_{\nu\in H}
       \bigl(r_\nu\operatorname{Re}z^\nu
                   +s_\nu\operatorname{Im}z^\nu\bigr),
 \label{geo:laurent-identity}
\end{equation}
where $a_0,r_\nu,s_\nu\in\mathbb Q$ and $H$ contains at most one
representative of each nonzero pair $\{\nu,-\nu\}\subset\mathbb Z^{n-1}$.
If $t_\nu\in\mathbb Q$ satisfy
\begin{equation}
 t_\nu\geq0,\qquad t_\nu^2\geq r_\nu^2+s_\nu^2,
 \label{geo:residual-bound}
\end{equation}
then
\begin{equation}
 \|W\|_{\mathrm{disc}}\leq a_0+\sum_{\nu\in H}t_\nu.
 \label{geo:laurent-upper}
\end{equation}
\end{proposition}

\begin{proof}
For $z\in\mathbb T^{n-1}$, every $z^\nu$ has absolute value one.  Hence
\[
 r_\nu\operatorname{Re}z^\nu+s_\nu\operatorname{Im}z^\nu
 \leq\sqrt{r_\nu^2+s_\nu^2}\leq t_\nu.
\]
Subtracting the nonnegative sum of squares in
\eqref{geo:laurent-identity} proves the stated upper bound for
$\widetilde C_W$ on the torus.  Lemma~\ref{geo:torus-disks} proves
\eqref{geo:laurent-upper} on the full product of disks.  Only the
inequality is extended to the disks; the Laurent identity is used on
the torus.
\end{proof}

The identity in \eqref{geo:laurent-identity} has a finite exact meaning.
If $p(z)=\sum_\alpha c_\alpha z^\alpha$, then on the torus
\[
 |p(z)|^2=\sum_{\alpha,\beta}
                   c_\alpha\overline c_\beta z^{\alpha-\beta}.
\]
Thus the identity can be checked coefficient by coefficient using
Gaussian rational arithmetic.  In particular a conjugate pair
$(u+\mathrm i v)z^\nu+(u-\mathrm i v)z^{-\nu}$ contributes
$2u\operatorname{Re}z^\nu-2v\operatorname{Im}z^\nu$.
Both propositions allow coefficients of either sign.

\section{Finite partitions and refinement}
\label{geo:sec-refinement}

\subsection{Symmetry and finite coverage}

Assume that the grid \eqref{geo:grid} is centrally symmetric:
$g_{N-a}=-g_a$.  Then $-I_a=I_{a^*}$, where $a^*=N-1-a$.
We use coefficient systems satisfying
\begin{equation}
 \begin{split}
 f_k(s,t)&=f_k(t,s)=f_k(-s,-t),\\
 f_k(s,t)&=f_{n-k}(t,-s).
 \end{split}
 \label{geo:coefficient-symmetries}
\end{equation}
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
\begin{equation}
 Qx=(x_1,\ldots,x_{n-1},-x_0),\qquad
 Rx=(x_{n-1},\ldots,x_0).
 \label{geo:signed-generators}
\end{equation}
They preserve $\mathcal E_n$.  The identities
\eqref{geo:coefficient-symmetries} imply
\begin{equation}
 W_f(Qx)=QW_f(x)Q^{\mathsf T},\qquad
 W_f(Rx)=-RW_f(x)R^{\mathsf T}.
 \label{geo:matrix-symmetries}
\end{equation}
For the first identity, entries not crossing the last coordinate are
immediate.  The remaining upper entries satisfy
\[
 f_{n-1-i}(x_{i+1},-x_0)=f_{i+1}(x_0,x_{i+1}),
\]
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 \eqref{geo:disc-comass} 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
\eqref{geo:coefficient-symmetries} has the same covariance, using the
same transformation for every summand.

Call a label tuple $\mathbf a=(a_0,\ldots,a_{n-1})$ \emph{admissible}
if
\begin{equation}
 \operatorname{Area}\bigl(
    \mathcal R_{n,j-i}\cap(I_{a_i}\times I_{a_j})\bigr)>0
 \quad\hbox{for every }0\leq i<j<n.
 \label{geo:admissible-labels}
\end{equation}
The associated matrix has upper entries $c_{j-i,a_i,a_j}$.
In this definition admissibility asserts only the displayed pairwise
conditions.

\begin{lemma}\label{geo:coverage}
Every point of $\mathcal E_n$ whose coordinates avoid $G$ belongs to a
box $I_{a_0}\times\cdots\times I_{a_{n-1}}$ with admissible label tuple.
Consequently a norm bound for the matrices of all admissible tuples
implies the same bound for all such points.  One matrix from each orbit
under \eqref{geo:signed-generators} suffices.
\end{lemma}

\begin{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 \eqref{geo:admissible-labels} 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
\eqref{geo:matrix-symmetries} preserves the norm.
\end{proof}

The finite set in Lemma~\ref{geo:coverage} 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 \eqref{geo:admissible-labels}.  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
\begin{equation}
 \mathcal B_{n,\delta}
 =\{x\in\mathcal E_n:\max_i|x_i|>n/2-\delta\}.
 \label{geo:endpoint-band}
\end{equation}
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.

\subsection{Dyadic refinement}

Let $f$ be a coefficient system for $m$ anchors.  For $n=2m$, define its
refinement by
\begin{equation}
 (\mathcal Df)_k(s,t)=
 \begin{cases}
   \dfrac12 f_{k/2}(s/2,t/2),&k\ \text{even},\\[3pt]
   0,&k\ \text{odd}.
 \end{cases}
 \label{geo:refinement}
\end{equation}
If the parent grid is $G_m$, choose a child grid $G_{2m}$ satisfying
\begin{equation}
 2G_m\subset G_{2m}.
 \label{geo:nested-grids}
\end{equation}
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
\begin{equation}
 x^{(0)}=\tfrac12(x_0,x_2,\ldots,x_{2m-2}),\qquad
 x^{(1)}=\tfrac12(x_1,x_3,\ldots,x_{2m-1}).
 \label{geo:parity-profiles}
\end{equation}
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 \eqref{geo:nested-grids}, if $x$
avoids the child grid, both profiles avoid the parent grid.
Ordering the even coordinates before the odd coordinates gives
\begin{equation}
 W_{\mathcal Df}(x)
 \simeq\frac12
 \begin{pmatrix}W_f(x^{(0)})&0\\0&W_f(x^{(1)})\end{pmatrix},
 \label{geo:refinement-matrix}
\end{equation}
where $\simeq$ denotes conjugation by that permutation matrix.  In
particular
\begin{equation}
 \|W_{\mathcal Df}(x)\|_{\mathrm{disc}}
 \leq\frac12\bigl(\|W_f(x^{(0)})\|_{\mathrm{disc}}
                    +\|W_f(x^{(1)})\|_{\mathrm{disc}}\bigr).
 \label{geo:refinement-bound}
\end{equation}

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~\eqref{geo:refinement} therefore gives the
average of these two parent forms.  Their actions are equal, by
\eqref{geo:action-integral} and the translation observation following it,
and hence
\begin{equation}
 A_{2m}(\mathcal Df)=A_m(f).
 \label{geo:action-inheritance}
\end{equation}
This equality also follows directly from \eqref{geo:action}, using
$\mathcal R_{2m,2k}=2\mathcal R_{m,k}$ and the factor $1/2$ in
\eqref{geo:refinement}.  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~\ref{geo:lipschitz-stokes}.

A child system may differ from a positive multiple $r\mathcal Df$
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 Df$, whenever the two coordinates avoid the child grid.
Then \eqref{geo:refinement-matrix}, multiplied by $r$, holds for every
profile outside $\mathcal 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
\begin{equation}
 q(2T_{\mathrm{old}})=Kp.
 \label{geo:integer-inheritance}
\end{equation}
On unchanged cells of odd separation the child coefficient is zero.
Thus this part of the refinement condition can be checked by integer
multiplication.

\subsection{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_s^{(\ell)}$ is a coefficient
system at level $\ell$.  At a fixed level all sources use the same grid
$G_\ell$ and satisfy \eqref{geo:coefficient-symmetries}.  Assume
$2G_{\ell-1}\subset G_\ell$.  At levels $\ell\geq1$, choose endpoint
bands $\mathcal B_\ell=\mathcal B_{n_\ell,\delta_\ell}$ whose thresholds
are grid values, and positive constants $r_{s,\ell}$, so that outside
$\mathcal B_\ell$ the child system agrees with
$r_{s,\ell}\mathcal Df_s^{(\ell-1)}$ in the sense just specified.
Write $W_s^{(\ell)}=W_{f_s^{(\ell)}}$.

For nonnegative numbers $\mu_1,\ldots,\mu_S$, put
\begin{equation}
 \beta_s^{(\ell)}=\mu_s\prod_{q=\ell+1}^{L}r_{s,q},
 \qquad
 M_\ell(x)=\sum_{s=1}^S\beta_s^{(\ell)}W_s^{(\ell)}(x).
 \label{geo:recursive-mixture}
\end{equation}
An empty product is one.  Thus, for three levels, the weights are
$\mu_s$ at level $2$, $\mu_s r_{s,2}$ at level $1$, and
$\mu_s r_{s,2}r_{s,1}$ at level $0$.

\begin{proposition}\label{geo:recursive-bound}
Suppose that $U\geq0$ bounds $\|M_0\|_{\mathrm{disc}}$ on every
admissible tuple of level $0$, and bounds $\|M_\ell\|_{\mathrm{disc}}$
on every affected admissible tuple of each level $1\leq\ell\leq L$.
Then
\begin{equation}
 \|M_L(x)\|_{\mathrm{disc}}\leq U
 \label{geo:off-grid-recursive-bound}
\end{equation}
for every $x\in\mathcal E_{n_L}$ whose coordinates avoid $G_L$.
In each premise it suffices to check one common symmetry representative
of the tuple for all sources.
\end{proposition}

\begin{proof}
We prove the assertion at every level by induction, working throughout
with profiles off the corresponding grids.  At level $0$ it is
Lemma~\ref{geo:coverage}.  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 $\mathcal B_\ell$, coefficient
inheritance and
$\beta_s^{(\ell)}r_{s,\ell}=\beta_s^{(\ell-1)}$ give
\begin{equation}
 M_\ell(x)\simeq\frac12
 \begin{pmatrix}
   M_{\ell-1}(x^{(0)})&0\\
   0&M_{\ell-1}(x^{(1)})
 \end{pmatrix}.
 \label{geo:mixture-inheritance}
\end{equation}
The parity profiles belong to $\mathcal E_{n_{\ell-1}}$ and avoid its
grid.  The induction hypothesis bounds both blocks by $U$, so
\eqref{geo:refinement-bound} 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
\eqref{geo:matrix-symmetries} proves the assertion about representatives.
\end{proof}

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
\begin{equation}
 \sum_{s=1}^S\beta_s^{(\ell)}u_{s,\ell,\mathbf a}
 \label{geo:triangle-budget}
\end{equation}
for the mixture at that tuple.  One may instead apply
Proposition~\ref{geo:laurent-certificate} 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
\eqref{geo:mixture-inheritance}; they are not additional factors in
\eqref{geo:triangle-budget}.

\subsection{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.

\begin{lemma}\label{geo:grid-extension}
Let $W(x)$ be a finite step matrix field on the part of $\mathcal E_n$
whose coordinates avoid a grid $G$.  Suppose its $(i,j)$ entry depends
only on the cells of $x_i,x_j$, also when the pair lies on an edge of
$\mathcal R_{n,j-i}$.  Suppose $\|W(x)\|_{\mathrm{disc}}\leq U$ there.
At an arbitrary $x\in\mathcal E_n$, retain these cell values for pairs
of coordinates outside $G$, and set to zero every row and column whose
coordinate belongs to $G$.  The extended matrix still satisfies
$\|W(x)\|_{\mathrm{disc}}\leq U$.
\end{lemma}

\begin{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.
\end{proof}

Apply Lemma~\ref{geo:grid-extension} once to the finest mixture in
Proposition~\ref{geo:recursive-bound}.  All ancestor estimates have
already been established off their grids, since the grids are nested
as in \eqref{geo:nested-grids}.  The extension is the coefficient
convention in \eqref{geo:step-form}.  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
\[
                    \pi^2\sum_s\mu_s A_{n_L}(f_s^{(L)}).
\]
Consequently, if $U>0$, the complete finite set of premises in
Proposition~\ref{geo:recursive-bound} yields
\begin{equation}
 \operatorname{Area}(M)\geq
 \frac{\pi^2}{U}\sum_{s=1}^S\mu_s A_{n_L}(f_s^{(L)}).
 \label{geo:recursive-area-bound}
\end{equation}
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 \eqref{geo:action} are rational, and all
remaining assertions reduce to the finite matrix and rational
inequalities in the two certificate criteria.

\section{The rational certificate}\label{sec: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 \(\mathcal R_{n,k}\) to \(R_k\).

\subsection{Grids and coefficient arrays}

Put
\begin{align}
G_{14}&=\{-4,-3,\ldots,4\}\nonumber\\
&\quad{}\cup
 \left\{\pm\frac92,\ \pm5,\ \pm\frac{21}4,\ \pm\frac{11}2,\
 \pm\frac{23}4,\ \pm6,\ \pm\frac{25}4,\ \pm\frac{13}2,\
 \pm\frac{27}4,\ \pm7\right\},                                      \label{eq:grids}\\
G_{28}&=2G_{14}\cup\{-14,-13,\ldots,14\},\nonumber\\
G_{56}&=\{-28,-27,\ldots,28\}.\nonumber
\end{align}
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
\begin{equation}\label{eq:keyclass}
\begin{split}
(k,u,v),\ &(k,v,u),\ (k,\bar u,\bar v),\ (k,\bar v,\bar u),\\
(n-k,v,\bar u),\ &(n-k,\bar u,v),\
(n-k,\bar v,u),\ (n-k,u,\bar v),
\end{split}
\qquad \bar u=N-1-u.
\end{equation}
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
\begin{equation}\label{eq:actualcoef}
                 f_{a,n,k}(s,t)=\frac{p_{a,n,\kappa}}{T_{a,n}}.
\end{equation}
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.
\begin{center}
\small
\begin{tabular}{ccrr}
\toprule
\(a\)&\(n\)&\(K_{a,n}\)&\(T_{a,n}\)\\
\midrule
1&14&\(100000000\)&\(100000344\)\\
1&28&\(1250004300000000\)&\(1250009954439084\)\\
1&56&\(31250248860977100000000\)&\(31251408412709010636800\)\\
\midrule
2&14&\(100000000\)&\(100001194\)\\
2&28&\(5000059700000000\)&\(5000141045182364\)\\
2&56&\(125003526129559100000000\)&\(125100260860029607051264\)\\
\bottomrule
\end{tabular}
\end{center}
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
\begin{equation}\label{eq:integerinherit}
 2T_{a,n/2}\,p_{a,n,\kappa}
       =K_{a,n}\,p_{a,n/2,\kappa'}.
\end{equation}
The containment of grids in \eqref{eq:grids} 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.

\Needspace{8\baselineskip}
The sizes of the arrays and the complete coverage counts are
\begin{center}
\small
\begin{tabular}{rrrrrr}
\toprule
\(n\)&\(\#\mathcal K_n\)&Changed classes&
Inherited classes&Rooted boxes&Matrix patterns\\
\midrule
14&346&346&0&\(2975284\)&\(53538\)\\
28&1382&176&1206&\(69474\)&\(29640\)\\
56&8092&162&7930&\(30856\)&\(14590\)\\
\bottomrule
\end{tabular}
\end{center}
At the first level, all compatible boxes are enumerated. At the last
two levels, \emph{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 \eqref{geo:matrix-symmetries} justify these operations.
Duplicate vectors are removed, and the distinct vectors are sorted
lexicographically. This defines the ordered pattern array used below.

\subsection{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
\begin{equation}\label{eq:integerwitness}
 2\operatorname{diag}(d_{a,n,\tau})+\ii P_{a,n,\tau}\succ0,
 \qquad
 \sum_i d_{a,n,\tau,i}\leq T_{a,n}.
\end{equation}
Consequently, the norm of this pattern of \(\Omega_{a,n}\) is bounded by
\[
            b_{a,n,\tau}
              =\frac{\sum_i d_{a,n,\tau,i}}{T_{a,n}}.
\]
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
\begin{equation}\label{eq:mixtureweights}
 \mu_1=\frac{23108519759}{10^{12}},\qquad
 \mu_2=\frac{976891480241}{10^{12}},\qquad
 \mu_1+\mu_2=1.
\end{equation}
For \(n=56,28,14\), define
\begin{equation}\label{eq:scaledweights}
\begin{split}
 c_{a,56}&=\mu_a,\\
 c_{a,28}&=\mu_a r_{a,56},\\
 c_{a,14}&=\mu_a r_{a,56}r_{a,28}.
\end{split}
\end{equation}
A first bound for a pattern at level \(n\) is
\begin{equation}\label{eq:trianglebudget}
               B_{n,\tau}=\sum_{a=1}^{2}c_{a,n}b_{a,n,\tau}.
\end{equation}
For eighty-four specified patterns, the supplement gives a polynomial
certificate directly for the mixed matrix
\begin{equation}\label{eq:mixedmatrix}
       W_{n,\tau}
          =\sum_{a=1}^{2}\frac{c_{a,n}}{T_{a,n}}P_{a,n,\tau}.
\end{equation}
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
\eqref{eq:mixedmatrix} 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.

\begin{proposition}\label{prop:finitecertificate}
The arrays in the electronic supplement satisfy the following statements.
\begin{enumerate}[label=\textup{(\roman*)},leftmargin=*]
\item The exact pair-cell tests and the signed symmetries give the complete
pattern sets counted above. Corresponding grids, coefficient keys, and
ordered patterns of the two collections are identical.
\item Every unchanged coefficient satisfies \eqref{eq:integerinherit}.
Every one of the \(195536\) matrices in the two collections satisfies
\eqref{eq:integerwitness}.
\item All \(108\) Laurent certificates have their stated rational upper
bounds and the exact target coefficients specified above.
\item The maximum of the \(97768\) final mixed budgets is
\begin{equation}\label{eq:exactU}
 U=\frac{29105746733301339862378571909389256115943629230830527422027}
          {29128486995944537460708185972236383400000000000000000000000}.
\end{equation}
\item The boundary action factors of the two level-\(56\) forms are
\begin{equation}\label{eq:actions}
\begin{split}
 A_1&=\frac{76814122456010519630747}{125005633650836042547200},\\
 A_2&=\frac{2151061404035391032035211}{3502807304080828997435392}.
\end{split}
\end{equation}
so that \(\int_M\Omega_{a,56}=\pi^2 A_a\) for every filling under
consideration.
\end{enumerate}
\end{proposition}

\begin{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
\[
 s-t\leq k,\quad t-s\leq k,\quad
 s+t\leq n-k,\quad -s-t\leq n-k.
\]
All vertices remain rational. At an edge from \(x\) to \(y\) meeting
\(L(z)=c\), the new vertex is
\[
                x+\frac{c-L(x)}{L(y)-L(x)}(y-x).
\]
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
\begin{equation}\label{eq:actionweights}
 m_{n,\kappa}
   =\sum_{k=1}^{n-1}(n-k)
       \sum_{\substack{u,v\\ [k,u,v]=\kappa}}
             \operatorname{Area}(R_k\cap(I_u\times I_v)).
\end{equation}

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 \eqref{eq:integerinherit} 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)+\ii P\).
The first test constructs a Gaussian rational matrix \(L\) for the
normalized matrix \(A=H/K\), where \(K=K_{a,n}>0\), and proves
\begin{equation}\label{eq:dominance}
 (A-LL^*)_{ii}>
 \sum_{j\ne i}
 \left(\left|\operatorname{Re}(A-LL^*)_{ij}\right|
       +\left|\operatorname{Im}(A-LL^*)_{ij}\right|\right).
\end{equation}
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|z_i||z_j|\leq |z_i|^2+|z_j|^2\) proves
\[
 z^*Rz\geq
 \sum_i\left(R_{ii}-\sum_{j\ne i}|R_{ij}|\right)|z_i|^2.
\]
Thus \eqref{eq:dominance} 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
\begin{equation}\label{eq:realrepresentation}
             \mathcal H=
             \begin{pmatrix}2\operatorname{diag}(d)&-P\\
                             P&2\operatorname{diag}(d)\end{pmatrix}.
\end{equation}
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
\[
 M^{(r+1)}_{ij}
   =\frac{p_r M^{(r)}_{ij}
            -M^{(r)}_{ir}M^{(r)}_{rj}}{p_{r-1}},
 \qquad p_r=M^{(r)}_{rr}.
\]
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 \eqref{eq:integerwitness} 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\geq0\), 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_{\rm pol}>0\), and its rational target edge weights with common
denominator \(D_{\rm wt}>0\).
Set \(q=\operatorname{lcm}(D_{\rm pol}^2,D_{\rm wt})\).
Direct convolution of the integer
polynomial coefficients gives
\begin{equation}\label{eq:integersos}
 q\left(\widetilde C_W(z)+\sum_\ell|p_\ell(z)|^2\right)
   =b_0+\sum_{\nu\in\mathcal V}
          \bigl(b_\nu\operatorname{Re}z^\nu+
                c_\nu\operatorname{Im}z^\nu\bigr),
 \qquad z\in\mathbb T^{n-1},
\end{equation}
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
\begin{equation}\label{eq:isqrtbound}
       \frac{b_0+\sum_{\nu\in\mathcal V}
                \left\lceil\sqrt{b_\nu^2+c_\nu^2}\right\rceil}{q}.
\end{equation}
For an integer \(m\geq0\), 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 \eqref{eq:isqrtbound}. 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 \eqref{eq:scaledweights}, and compute every
\(\widehat B_{n,\tau}\). Their maximum is exactly \eqref{eq:exactU}.
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 \eqref{eq:actionweights}:
\begin{equation}\label{eq:integeraction}
       A_a=\frac{1}{56^2T_{a,56}}
                \sum_{\kappa\in\mathcal K_{56}}
                    m_{56,\kappa}p_{a,56,\kappa}.
\end{equation}
This gives \eqref{eq:actions}, and the boundary integral identity gives
the final assertion.
\end{proof}

\subsection{Completion of the proof}

\begin{proof}[Proof of Theorem~\ref{thm:main}]
Use the level-\(56\) distance functions, with
\[
                         \Omega=\mu_1\Omega_{1,56}+
                                  \mu_2\Omega_{2,56}.
\]
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~\ref{prop:finitecertificate}, and
\(|\Omega(e_1,e_2)|\leq 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
\[
                         |\Omega(e_1,e_2)|\leq U
                         \quad\text{almost everywhere on }M.
\]
The boundary integral identity and \eqref{eq:actions} give
\[
 U\operatorname{Area}(M)
       \geq\int_M\Omega
       =\pi^2(\mu_1A_1+\mu_2A_2).
\]
Exact rational simplification using \eqref{eq:mixtureweights},
\eqref{eq:exactU} and \eqref{eq:actions} yields
\[
                       \frac{\mu_1A_1+\mu_2A_2}{U}=\rho_*.
\]
This proves the asserted inequality.
\end{proof}

\appendix
\section{Exact reproduction and decimal enclosures}\label{app:reproduction}

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 \texttt{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, \texttt{coefficient\_numerators} stores the vector
\(p\), \texttt{diagonal\_numerators} stores the rows \(d\), and
\texttt{scaling\_numerator} is \(T\).
The auxiliary integer \(K\) is the field \texttt{denominator} at level
\(14\), and \texttt{coefficient\_denominator} at levels \(28\) and \(56\).
The entry point \texttt{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 \texttt{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:
\begin{enumerate}[label=\arabic*.,leftmargin=*]
\item Recompute all clipped pair areas and the complete level-\(14\)
coverage; verify both level-\(14\) matrix collections.
\item Recompute the level-\(28\) coverage, exact inherited coefficients,
and every level-\(28\) matrix; repeat at level \(56\).
\item Expand all \(108\) Gaussian polynomial certificates in two
independent implementations and compare every target edge with its
actual rational coefficient.
\item Compare the two collections' profile arrays, compute all \(97768\)
mixed budgets, and recompute the boundary action and \(\rho_*\).
\end{enumerate}
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
\[
 S_N(q)=\sum_{j=0}^{N-1}\frac{(-1)^j}{(2j+1)q^{2j+1}}.
\]
For even \(N\), the alternating-series estimate gives
\[
 S_N(q)<\arctan(1/q)<
 S_N(q)+\frac{1}{(2N+1)q^{2N+1}}.
\]
Machin's identity
\[
                    \pi=16\arctan(1/5)-4\arctan(1/239)
\]
then gives rational lower and upper bounds for \(\pi\).
With \(N=64\), squaring these positive bounds and multiplying by the
positive rational number \(\rho_*\) proves
\[
       6.06571278970403721852
           <\rho_*\pi^2<
       6.06571278970403721853.
\]
The supplement includes this integer check.


\begin{thebibliography}{99}

\bibitem{BCIK}
V.~Bangert, C.~B.~Croke, S.~V.~Ivanov and M.~G.~Katz,
\emph{Filling area conjecture and ovalless real hyperelliptic surfaces},
Geom. Funct. Anal. \textbf{15} (2005), no.~3, 577--597.
\href{https://doi.org/10.1007/s00039-005-0517-8}{doi:10.1007/s00039-005-0517-8}.

\bibitem{BW}
J.~Briggs and C.~Wells,
\emph{A discrete view of Gromov's filling area conjecture},
preprint (2026),
\href{https://arxiv.org/abs/2602.17859v1}{arXiv:2602.17859v1}.

\bibitem{CLZ}
L.~Chen, X.~Li and Y.~Zhong,
\emph{A Fourier approach to Gromov's filling area conjecture},
preprint (2026),
\href{https://arxiv.org/abs/2609.08251v1}{arXiv:2609.08251v1}.

\bibitem{Gromov}
M.~Gromov,
\emph{Filling Riemannian manifolds},
J. Differential Geom. \textbf{18} (1983), no.~1, 1--147.
\href{https://doi.org/10.4310/jdg/1214509283}{doi:10.4310/jdg/1214509283}.

\bibitem{Ivanov}
S.~Ivanov,
\emph{Filling minimality of Finslerian \(2\)-discs},
Proc. Steklov Inst. Math. \textbf{273} (2011), 176--190.
\href{https://doi.org/10.1134/S0081543811040079}{doi:10.1134/S0081543811040079}.

\bibitem{Zust}
R.~Z\"ust,
\emph{Examples of absolutely minimal polyhedral chains in maximum norm spaces},
preprint (2026),
\href{https://arxiv.org/abs/2610.29593v1}{arXiv:2610.29593v1}.

\end{thebibliography}
\end{document}