\documentclass[11pt]{amsart}

\usepackage{amsmath,amssymb,amsthm}
\usepackage[margin=1.1in]{geometry}
\usepackage{array}
\usepackage{booktabs,longtable}
\usepackage{microtype}
\usepackage{xurl}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage[hidelinks]{hyperref}
\hypersetup{pdftitle={Improved sum-difference inequalities in abelian groups},
  pdfauthor={Logan J. Kleinwaks}}
\setlength{\emergencystretch}{2em}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}

\numberwithin{equation}{section}

\newcommand{\N}{\mathbb{N}}
\newcommand{\Z}{\mathbb{Z}}
\newcommand{\R}{\mathbb{R}}
\newcommand{\e}{\mathrm{e}}
\newcommand{\lamI}{\lambda_\infty}
\newcommand{\lsup}{\lambda_*}
\newcommand{\Hb}{\mathbf{H}}
\newcommand{\cmi}[3]{(#1,#2\,\|\,#3)}
\newcommand{\lean}[1]{\texttt{#1}}
\DeclareMathOperator{\supp}{supp}

\title[Improved sum--difference inequalities]{Improved sum--difference inequalities in abelian groups}
\author{Logan J. Kleinwaks}
\subjclass[2020]{11B30, 11B75, 94A17}
\keywords{Sumsets, difference sets, Shannon entropy, non-Shannon inequalities, formal verification}

\date{First version: September 28, 2026; Version 1.1: October 6, 2026}

\begin{document}

\begin{abstract}
For all finite subsets $X,Y$ of an abelian group, we prove
\[
 |X-Y|\le |X+Y|^{\lamI},\qquad
 \lamI=\frac{9451\e-3286}{5378\e+787}=1.454277448906\ldots,
\]
improving the classical exponent $3/2$. We also prove that a universal
two-set exponent $\lambda$ over the integers implies an upper bound
$2-1/\lambda$ for the Gyarmati--Hennecart--Ruzsa constant, the supremum $\theta^*$ of $t$ such that $|A-B|\gg|A+B|^t$ and $|A+B|\ll|A|$ for arbitrarily large $A,B\subset\Z$.
Consequently,
\[
 \theta^*\le\frac{13524\e-7359}{9451\e-3286}=1.312373302115\ldots,
\]
improving their bound $4/3$. The first argument combines a coupling with
distinct differences, entropy inequalities for independent sums, a finite
certificate using non-Shannon inequalities, and an explicit limiting
certificate with weights $\int_0^1t(1-t)^k\e^t\,dt$. The transfer uses
localisation and the Pl\"unnecke--Ruzsa inequality over a sequence of scales.
The proofs are formalised in Lean~4.
\end{abstract}

\maketitle

\section{Formal verification and use of AI}
The mathematical results in Theorems~\ref{thm:pair}--\ref{thm:transfer},
Corollary~\ref{cor:theta}, and the lemmas and propositions used in
their proofs have counterparts in the accompanying Lean~4
formalisation. Appendix~\ref{app:lean} gives the correspondence and
explains the representation of finite laws. The reference environment
is \texttt{leanprover/lean4:v4.28.0}, with Mathlib revision
\texttt{8f9d9cff6bd728b17a24e163c9402775d9e6a365}.
The headline proofs use only \texttt{propext},
\texttt{Classical.choice} and \texttt{Quot.sound}.
They use neither unproved auxiliary statements nor
\texttt{native\_\allowbreak{}decide}. See \cite{Lean,Mathlib} for Lean and Mathlib.

All mathematical formalisation was performed by Aristotle
(Harmonic), which also simplified the formalisation under the
author's instructions. Research and proof derivation were performed
using Aristotle, GPT-6 Astra, and GPT-5.6 Sol. The author wrote the
research-loop instructions; additional research instructions were
generated by GPT-6 Astra and GPT-5.6 Sol. Aristotle wrote the initial
manuscript under the author's instructions. The manuscript was
revised by GPT-6 Astra under the author's instructions and by the
author. \emph{The author contributed no deep problem-specific insight, the results were obtained through the author's work on more general mathematical research loops.} The author is responsible for the final text and the claims
made in it.

\section{Proof outline and main results}\label{sec:outline}

\subsection{Proof outline}
There are two independent arguments. The first transfers an inequality
$|X-Y|\le |X+Y|^\lambda$ to the small-sumset setting. For
$|A+B|\le K|A|$, write $s=|A+B|$, $d=|A-B|$ and $M_h=|hB-hB|$.
A maximal packing by translates of $hB-hB$ decomposes $A$ into pieces
on which the pair inequality can be combined with a cardinality bound.
Controlling the overlap of the corresponding sumsets gives
\begin{equation}\label{eq:onescale}
 dM_h\le sM_{4h}^{\,2-1/\lambda}\qquad(h\ge1).
\end{equation}
Multiplying these estimates over $h=1,4,\ldots,4^{J-1}$ and using
$M_{4^J}\le K^{2\cdot4^J}|A|$ gives
$d\le C(K,J)s^{2-1/\lambda+1/J}$. Letting $J\to\infty$ bounds the
admissible exponent by $2-1/\lambda$. This is Part~I, in
\S\ref{sec:transfer}.

The second argument establishes the pair inequality. Choose
$\Gamma\subset X\times Y$ with exactly one representative for each
difference, and let $(X_1,Y_1)$ be uniform on $\Gamma$. Then
$X_1-Y_1$ determines the pair and
\[
 L:=H(X_1,Y_1)=\log|X-Y|.
\]
For its marginal laws $\mu,\nu$, put
$h(i,j)=H(\mu^{*i}*\nu^{*j})$ and $S=\log|X+Y|$.
Entropy inequalities for independent sums make $h$ nonnegative,
nondecreasing, and concave in each coordinate. The representative
property gives the additional links
\[
 L+h(i,j)\le h(i+1,j)+h(i,j+1),
 \qquad h(1,1)\le S.
\]
These inequalities retain only the marginal laws. To exploit the
dependence in $(X_1,Y_1)$, we introduce a second independent copy and
apply Shannon inequalities and ten instances of the non-Shannon
families of Mat\'u\v{s} and Csirmaz--Csirmaz to integer linear forms
in the four coordinates. Their exact weighted sum, followed by
symmetrisation, gives
\begin{align*}
 22882L\le {}&5820S+8694h(1,1)\\
             &+11645\bigl(h(1,0)+h(0,1)\bigr)
              +685\bigl(h(2,0)+h(0,2)\bigr).
\end{align*}
The finite certificate is given in \S\ref{sec:lemmaA}; the entropy
setup and the two known non-Shannon families are in \S\ref{sec:entropy}.

The remaining step is an inequality for real arrays satisfying these
conditions. We prove it by an inductive certificate whose weights are
\[
 w_k=\int_0^1t(1-t)^k\e^t\,dt,\qquad
 w_{k+2}=(k+4)w_{k+1}-(k+1)w_k.
\]
This recurrence cancels the interior terms, while $w_k\to0$ controls
the remainder. Since $w_0=1$ and $w_1=3-\e$, the limiting coefficients
are explicit:
\[
 (21512\e+3148)L\le(37804\e-13144)S.
\]
This yields $L\le\lamI S$ and proves the pair inequality. The array
argument is in \S\ref{sec:grid}, and the two parts are assembled in
\S\ref{sec:assembly}.

\subsection{Main results}
For finite subsets of an abelian group, write
$A\pm B=\{a\pm b:a\in A,\ b\in B\}$, and let $hB$ denote the
$h$-fold sumset, with $0B=\{0\}$. We use the following precise
formulation of the exponent in Gyarmati, Hennecart, and Ruzsa
\cite[(5)]{GHR}. A real number $t$ is \emph{admissible} if $t>1$ and
for every $K>1$ there is $c=c(K)>0$ such that for every $n_0\in\N$
there exist finite $A,B\subset\Z$ with $B\ne\varnothing$, $|A|\ge n_0$ and
\begin{equation}\label{eq:adm}
 |A+B|\le K|A|,\qquad |A-B|\ge c|A+B|^t.
\end{equation}
Let $\theta^*$ be the supremum of the admissible exponents, with the
convention $\sup\varnothing=0$. This is the
Gyarmati--Hennecart--Ruzsa exponent, denoted $C_{3a}$ in the
\href{https://teorth.github.io/optimizationproblems/constants/3a.html}{Optimization Constants in Mathematics GitHub repository}.

Define the unrestricted integer pair exponent by
\begin{equation}\label{eq:lsup}
 \lsup=\inf\{\lambda\in\R:
 |X-Y|\le|X+Y|^\lambda\text{ for all finite }X,Y\subset\Z\}.
\end{equation}
The set of exponents in \eqref{eq:lsup} contains $2$, and each of
its elements is at least $1$. The classical inequality recorded in
\cite[\S1]{GHR} gives $\lsup\le3/2$.

\begin{theorem}[two-set inequality]\label{thm:pair}
For every abelian group $G$ and finite $X,Y\subset G$,
\[
 |X-Y|\le|X+Y|^{\lamI},\qquad
 \lamI=\frac{9451\e-3286}{5378\e+787}=1.454277448906\ldots.
\]
\end{theorem}

\begin{theorem}[transfer]\label{thm:transfer}
If $|X-Y|\le|X+Y|^\lambda$ for every finite $X,Y\subset\Z$, then
$\theta^*\le2-1/\lambda$. Consequently,
$\theta^*\le2-1/\lsup$.
\end{theorem}

\begin{corollary}\label{cor:theta}
\[
 \theta^*\le 2-\frac1{\lamI}
 =\frac{13524\e-7359}{9451\e-3286}=1.312373302115\ldots.
\]
\end{corollary}

Theorem~\ref{thm:pair} has no multiplicative constant and imposes
no torsion or cardinality restriction on $G$. Replacing $Y$ by $-Y$
also gives $|X+Y|\le|X-Y|^{\lamI}$. Theorem~\ref{thm:transfer}
with $\lambda=3/2$ recovers $\theta^*\le4/3$.

\subsection{Prior work and the contribution of the proof}
Gyarmati, Hennecart, and Ruzsa \cite[Corollary~3]{GHR} proved
$|A-B|\le K^{2/3}|A+B|^{4/3}$ under $|A+B|\le K|A|$.
Their result gives the previous upper bound $4/3$ for $\theta^*$.
The unrestricted two-set problem must be distinguished from the
single-set inequality $|X-X|\le|X+X|^{4/3}$ of Freiman and Pigarev,
recalled in \cite[\S1]{GHR}. The simplex construction of
Hennecart, Robert, and Yudin \cite{HRY} yields
$\lsup\ge\log(1+\sqrt2)/\log2$; see also \cite[\S2]{GHR}.

The transfer uses Ruzsa's maximal-packing argument \cite{Ru99}
and the Pl\"unnecke--Ruzsa inequality, for which we use the form
in \cite[Theorem~1.2]{Pet12}. The entropy approach belongs to the
theory developed by Ruzsa \cite{Ru09}, Tao \cite{Tao10}, and
Madiman, Marcus, and Tetali \cite{Mad08,MMT12}. In particular, the
submodularity inequality for independent sums is due to Madiman
\cite{Mad08}; its discrete abelian-group form also appears in
\cite[Corollary~2.6]{MMT12}.

The non-Shannon inequalities used here are existing inequalities
of Mat\'u\v{s} \cite{Mat07} and Csirmaz--Csirmaz \cite{CC}.
Both are reproduced explicitly in \cite[Theorem~22 and (31)]{CC}.
Their proofs use the conditional-copy construction originating
in Zhang--Yeung \cite{ZY98} and developed systematically by
Dougherty, Freiling, and Zeger \cite{DFZ11}.
The contributions here are the multiscale transfer, the specific
two-copy entropy certificate, and its combination with the limiting
array certificate. No new general information inequality is asserted.

\section{Part I: the transfer}\label{sec:transfer}

All sets in this section are finite subsets of an abelian group, except where
the group is explicitly specialised to $\Z$.

\begin{lemma}[reduction to $K=2$]\label{lem:window}
Let $C>0$ and $r\in\R$. Suppose that $|A-B|\le C|A+B|^{r}$ for all nonempty $A,B\subset\Z$ with
$|A+B|\le2|A|$. Then every admissible $\theta$ satisfies $\theta\le r$.
\end{lemma}

\begin{proof}
Apply \eqref{eq:adm} with $K=2$. It gives $c>0$ and pairs with $|A+B|\ge|A|\ge n_0$ and
$c|A+B|^{\theta}\le|A-B|\le C|A+B|^{r}$. If $\theta>r$, this fails once
$|A+B|^{\theta-r}>C/c$.
\end{proof}

Taking $K=2$ suffices to bound the admissible exponents. The estimates
below retain $K$ until this final application.

\begin{lemma}[packing]\label{lem:packing}
Let $D$ be finite and nonempty. There is $T\subset A$ such that the translates $t+D$ $(t\in T)$
are pairwise disjoint and every $a\in A$ satisfies $a-t\in D-D$ for some $t\in T$.
\end{lemma}

\begin{proof}
Take $T\subset A$ of maximal cardinality with disjoint translates. If $a\in A\setminus T$ had
$a-t\notin D-D$ for all $t\in T$, then $a+D$ would be disjoint from every $t+D$, contradicting
maximality; elements of $T$ are covered by $t=a$.
\end{proof}

\begin{lemma}[localisation]\label{lem:local}
Let $D$ be finite and nonempty and $\lambda\ge1$. Suppose that $|X-B|\le|X+B|^{\lambda}$ for every
$X\subset A$ contained in a translate of $D-D$. Then
\[
  |A-B|\,|D|\le |D-D-B|^{1-1/\lambda}\,|A+B|\,|D-D+D-B|.
\]
\end{lemma}

\begin{proof}
Let $T$ be as in Lemma~\ref{lem:packing} and assign each $a\in A$ to one $t\in T$ with
$a-t\in D-D$; let $A_t$ be the set of elements assigned to $t$. Then $A-B=\bigcup_t(A_t-B)$.
Since $A_t-B\subset t+(D-D-B)$ we have $|A_t-B|\le U:=|D-D-B|$, and by hypothesis
$|A_t-B|\le|A_t+B|^\lambda$. For $x>0$, $x\le U$ and $x\le v^\lambda$ imply
$x=x^{1-1/\lambda}x^{1/\lambda}\le U^{1-1/\lambda}v$;
the same bound is immediate for $x=0$, so
\[
  |A-B|\le\sum_{t\in T}|A_t-B|\le U^{1-1/\lambda}\sum_{t\in T}|A_t+B| .
\]
Let $w\in A+B$, and let $T_w$ be the set of $t$ with $w\in A_t+B$. If $w=a+b$ with $a\in A_t$ and
$a-t=y-z$ ($y,z\in D$), then $t+D=w+(z-y+D-b)\subset w+(D-D+D-B)$. The translates $t+D$,
$t\in T_w$, are disjoint, so $|T_w|\,|D|\le|D-D+D-B|$. Summing over $w\in A+B$ gives
$|D|\sum_t|A_t+B|\le|A+B|\,|D-D+D-B|$.
\end{proof}

\begin{lemma}[one scale]\label{lem:onescale}
Let $B\ne\varnothing$ and $\lambda\ge1$, and suppose that $|X-B|\le|X+B|^\lambda$ for every
$X\subset A$. Write $M_h=|hB-hB|$. Then for every $h\ge1$,
\[
  |A-B|\,M_h\le M_{4h}^{\,2-1/\lambda}\,|A+B| .
\]
\end{lemma}

\begin{proof}
Apply Lemma~\ref{lem:local} with $D=hB-hB$. Then $D-D-B=2hB-(2h+1)B$ and
$D-D+D-B=3hB-(3h+1)B$. Since $B\neq\varnothing$, $|mB-nB|$ is nondecreasing in $m$ and $n$, so
both sets have at most $M_{4h}$ elements.
\end{proof}

\begin{proposition}[multi-scale inequality]\label{prop:multiscale}
Let $A,B$ be nonempty with $|A+B|\le K|A|$, let $\lambda\ge1$, and suppose that
$|X-B|\le|X+B|^\lambda$ for every $X\subset A$. Then for every $J\in\N$
\[
  |A-B|^J\le |A+B|^J\,\bigl(K^{2\cdot4^J}|A|\bigr)^{1+J(1-1/\lambda)} .
\]
\end{proposition}

\begin{proof}
Put $d=|A-B|$, $s=|A+B|$ and $m_j=M_{4^j}$. We show by induction on $j$ that
$d^j m_0\le s^j m_j^{\,1+j(1-1/\lambda)}$. The case $j=0$ is equality. For the step, Lemma
\ref{lem:onescale} with $h=4^j$ gives $d\,m_j\le m_{j+1}^{2-1/\lambda}s$, and $m_j\le m_{j+1}$
gives $m_j^{\,j(1-1/\lambda)}\le m_{j+1}^{\,j(1-1/\lambda)}$; multiplying,
\[
  d^{j+1}m_0\le s^j\,(d\,m_j)\,m_j^{\,j(1-1/\lambda)}\le s^{j+1}m_{j+1}^{\,1+(j+1)(1-1/\lambda)} .
\]
Finally $m_0=|B-B|\ge1$, and the Pl\"unnecke--Ruzsa inequality
$|mB-nB|\le(|A+B|/|A|)^{m+n}|A|$ \cite[Theorem~1.2]{Pet12} gives $m_J\le K^{2\cdot4^J}|A|$.
\end{proof}

\begin{proof}[Proof of Theorem~\ref{thm:transfer}]
Suppose $|X-Y|\le|X+Y|^\lambda$ for all finite $X,Y\subset\Z$. Then $\lambda\ge1$ (take
$X=\{0\}$, $Y=\{0,1\}$). Let $J\ge1$ and let $A,B\subset\Z$ be nonempty with $|A+B|\le2|A|$.
Proposition~\ref{prop:multiscale} with $K=2$, together with $|A|\le|A+B|=s$, gives after taking
$J$-th roots
\[
  |A-B|\le s\,(2^{2\cdot4^J}s)^{(1+J(1-1/\lambda))/J}=C_J\,s^{\,2-1/\lambda+1/J}.
\]
By Lemma~\ref{lem:window} every admissible $\theta$ satisfies $\theta\le2-1/\lambda+1/J$ for all
$J\ge1$, hence $\theta\le2-1/\lambda$, and $\theta^\ast\le2-1/\lambda$ (this is also true when
there is no admissible exponent, since $2-1/\lambda\ge1>0$).

For the second statement, apply the first to $\lambda=2$ to get $\theta^\ast\le3/2$. If
$\theta^\ast>2-1/\lsup$, then $\lsup<1/(2-\theta^\ast)$, so some $\lambda$ in the set
\eqref{eq:lsup} satisfies $\lambda<1/(2-\theta^\ast)$, that is $2-1/\lambda<\theta^\ast$,
contradicting the first statement.
\end{proof}

\begin{remark}
At a single scale the ratio $M_{4h}/M_h$ implicit in \eqref{eq:onescale} need not be bounded in
terms of $K$. Over the scales $4^j$ the product of these ratios telescopes to at most
$K^{2\cdot4^J}|A|$, and the $J$-th root turns this loss into a constant times $s^{1/J}$.
\end{remark}

\section{Entropy: the coupling, the grid, and non-Shannon inequalities}\label{sec:entropy}

\subsection{Notation}
All random variables are finitely supported and defined on a common finite probability space;
$H$ denotes Shannon entropy with natural logarithms, and $H(U_1,\dots,U_r)$ the joint entropy.
For finitely supported probability measures $\alpha,\beta$ on an abelian group $G$, $\alpha*\beta$
is the law of $U+V$ with $U\sim\alpha$, $V\sim\beta$ independent, and $H(\alpha)$ is the entropy of
$\alpha$. We use the following facts.
\begin{itemize}
\item[(E1)] If $U$ takes values in a finite set $S$, then $H(U)\le\log|S|$.
\item[(E2)] $H(U)=H(V)$ if $U$ and $V$ are functions of each other; $H(f(U))\le H(U)$;
  $H(U,V)=H(U)+H(V)$ if $U,V$ are independent.
\item[(E3)] Submodularity: $H(U,W)+H(V,W)\ge H(U,V,W)+H(W)$.
\item[(E4)] For independent $U,V$: $H(U)\le H(U+V)$.
\item[(E5)] (Madiman \cite{Mad08}) For independent $U,V,W$:
  $H(U+V+W)+H(V)\le H(U+V)+H(V+W)$.
\end{itemize}
(E4) follows from $H(U)+H(V)=H(U+V,V)\le H(U+V)+H(V)$. For (E5), apply (E3) to the joint
variables $(U,V+W)$ and $(U+V,W)$, both of which determine $U+V+W$ and which together determine
$(U,V,W)$: this gives $H(U,V,W)+H(U+V+W)\le H(U,V+W)+H(U+V,W)$, and independence turns it into
(E5).

\subsection{The coupling and the grid}

\begin{lemma}[coupling]\label{lem:coupling}
For finite $X,Y\subset G$ there is $\Gamma\subset X\times Y$ with $|\Gamma|=|X-Y|$ such that
distinct elements of $\Gamma$ have distinct differences $x-y$.
\end{lemma}

\begin{proof}
Choose one representative pair for each $z\in X-Y$.
\end{proof}

Fix such a $\Gamma$, assume
$X,Y\ne\varnothing$, and let $(X_1,Y_1)$ be uniform on $\Gamma$. Let $\mu,\nu$ be the laws of $X_1$ and
$Y_1$, and put
\[
  L=\log|\Gamma|=\log|X-Y|,\qquad S=\log|X+Y|,\qquad h(i,j)=H(\mu^{*i}*\nu^{*j})\quad(i,j\in\N).
\]

\begin{lemma}[coupled Ruzsa triangle inequality]\label{lem:link}
For every finitely supported law $\omega$ on $G$,
$L+H(\omega)\le H(\mu*\omega)+H(\nu*\omega)$. In particular
\[
  L+h(i,j)\le h(i+1,j)+h(i,j+1)\qquad(i,j\in\N).
\]
\end{lemma}

\begin{proof}
Let $W\sim\omega$ be independent of $(X_1,Y_1)$. Since $(X_1+W)-(Y_1+W)=X_1-Y_1$ determines
$(X_1,Y_1)$, the map $(X_1,Y_1,W)\mapsto(X_1+W,Y_1+W)$ is injective on the support. Hence
$L+H(W)=H(X_1,Y_1,W)=H(X_1+W,Y_1+W)\le H(X_1+W)+H(Y_1+W)$. Take $\omega=\mu^{*i}*\nu^{*j}$.
\end{proof}

This is the entropy analogue of Ruzsa's inequality $|X-Y||W|\le|X+W||Y+W|$ for the specific
coupling $\Gamma$.

\begin{lemma}[grid concavity]\label{lem:grid}
For all $i,j\in\N$:
\begin{gather*}
 h(i+2,j)+h(i,j)\le2h(i+1,j),\qquad h(i,j+2)+h(i,j)\le2h(i,j+1),\\
 h(i,j)\le h(i+1,j),\qquad h(i,j)\le h(i,j+1),\qquad h(i,j)\ge0,\qquad h(1,1)\le S.
\end{gather*}
\end{lemma}

\begin{proof}
Concavity is (E5) with $U,W$ two independent copies of $\mu$ (respectively $\nu$) and
$V\sim\mu^{*i}*\nu^{*j}$: $H(\alpha*\alpha*\beta)+H(\beta)\le2H(\alpha*\beta)$. Monotonicity is (E4).
Finally $\mu^{*1}*\nu^{*1}$ is supported on $X+Y$, so $h(1,1)\le S$ by (E1).
\end{proof}

Only unit steps of (E5) are needed: Lemma~\ref{lem:grid} is the only information about $h$ used,
besides Lemma~\ref{lem:link} and Corollary~\ref{cor:Asym}.

\subsection{Two copies and linear forms}\label{subsec:forms}
Let $(X_2,Y_2)$ be an independent copy of $(X_1,Y_1)$, and write $\mathbf{V}=(X_1,Y_1,X_2,Y_2)$.
For $c\in\Z^4$ write $c\cdot\mathbf V=c_1X_1+c_2Y_1+c_3X_2+c_4Y_2$, and for a finite list $F$ of
vectors in $\Z^4$ put $\Hb[F]=H\bigl((c\cdot\mathbf V)_{c\in F}\bigr)$. We denote the forms by their
values (so $\Hb[X_1+Y_2,\,Y_1-Y_2]$ is the joint entropy of these two forms), and a
parenthesised list of forms is regarded as one joint variable. The following rules hold.
\begin{itemize}
\item[(R1)] ($\Z$-span.) If every form of $F'$ is an integer combination of forms of $F$ and
  conversely, then $\Hb[F]=\Hb[F']$.
\item[(R2)] (Coupling.) If $X_k-Y_k$ is an integer combination of forms of $F$ ($k=1$ or $2$),
  then $\Hb[F]=\Hb[F,X_k,Y_k]$, since $x-y$ determines $(x,y)$ on $\Gamma$.
\item[(R3)] (Exchange.) $\Hb[F]$ is unchanged if $(X_1,Y_1)$ and $(X_2,Y_2)$ are exchanged in all
  forms.
\item[(R4)] (Independence.) If the forms of $F_1$ involve only $X_1,Y_1$ and those of $F_2$ only
  $X_2,Y_2$, then $\Hb[F_1,F_2]=\Hb[F_1]+\Hb[F_2]$.
\item[(R5)] $\Hb[X_k,Y_k]=L$ for $k=1,2$, and $\Hb[\varnothing]=0$.
\item[(R6)] (Bridge.) A single form with coefficients in $\{0,1\}$, involving at most one
  variable from each copy, has entropy $h(i,j)$, where $i$ (resp.~$j$) is the number of $X$'s
  (resp.~$Y$'s): e.g.\ $\Hb[X_1]=h(1,0)$, $\Hb[X_1+X_2]=h(2,0)$, $\Hb[X_1+Y_2]=\Hb[Y_1+X_2]=h(1,1)$,
  $\Hb[Y_1+Y_2]=h(0,2)$.
\item[(R7)] (Support.) $\Hb[X_1+Y_1]\le S$, since $X_1+Y_1\in X+Y$.
\end{itemize}
Rules (R1)--(R2) are applications of (E2), (R3) holds because the two copies are
independent and identically distributed, and (R4) is the independence of the copies. The identifications used to rewrite lists of forms are certified by
(R1)--(R3); independence and the identifications with $L$ and $h$ use
(R4)--(R6). Integer coefficients are essential: division by an integer
would not be valid in an arbitrary abelian group. The formalisation
searches for integer witnesses to mutual determination and verifies
each witness (Appendix~\ref{app:lean}); it does not assume completeness
of that search. The inequality (R7) is the only inequality that relates the
dependent sum $X_1+Y_1$ to $|X+Y|$; the grid only sees sums of independent variables.

\subsection{Non-Shannon inequalities}\label{subsec:nonshannon}
For jointly distributed $a,b,c$ write $\cmi abc=H(a,c)+H(b,c)-H(a,b,c)-H(c)$ and
$(a,b)=\cmi ab\varnothing$, and let
\[
  [abcd]=-(a,b)+\cmi abc+\cmi abd+(c,d)
\]
be the Ingleton expression, with the convention of \cite[\S2]{CC}. For five jointly distributed variables $a,b,c,d,z$ and
$k\in\N$ put
\begin{align*}
\mathsf M_k[abcd]&=\cmi bza+k\bigl([abcd]+\cmi azb+\cmi abz\bigr)+\tbinom k2\bigl(\cmi acb+\cmi abc\bigr),\\
\mathsf C_k[abcd]&=\cmi abz+k\bigl([abcd]+\cmi azb+\cmi bza\bigr)+\tbinom k2\bigl(\cmi acb+\cmi bca\bigr),
\end{align*}
and let $\mathsf M_k[acbd]$, $\mathsf C_k[acbd]$ be the same expressions with $[abcd]$ replaced by
$[acbd]$ (and no other change).

\begin{theorem}[{Mat\'u\v{s} \cite{Mat07}; see \cite[Theorem~22]{CC}}]\label{thm:matus}
$\mathsf M_k[abcd]\ge0$ and $\mathsf M_k[acbd]\ge0$ for all $k\in\N$.
\end{theorem}

\begin{theorem}[{Csirmaz--Csirmaz \cite[(31)]{CC}}]\label{thm:companion}
$\mathsf C_k[abcd]\ge0$ and $\mathsf C_k[acbd]\ge0$ for all $k\in\N$.
\end{theorem}

For $k=1$ and $z=d$, $\mathsf M_1[abcd]$ is a permutation of the
Zhang--Yeung inequality \cite{ZY98} (see
Remark~\ref{rem:cuts}). Both theorems are re-proved in the formalisation, by induction on $k$ from
one common lemma.

\begin{lemma}[copy lemma \cite{ZY98,DFZ11}]\label{lem:copy}
For $a,b,c,d,z$ there are $a',b',c',d',z'$ on a finite probability space such that
$(a',b',c',d')$ has the law of $(a,b,c,d)$, $(a',b',z')$ has the law of $(a,b,z)$, and
$\cmi{(c',d')}{z'}{(a',b')}=0$.
\end{lemma}

\begin{proof}
Retain the marginal law of $(a,b,c,d)$ and, conditionally on $(a,b)$,
sample $z'$ independently of $(c,d)$ with the conditional law of $z$
given $(a,b)$. Equivalently, on pairs of original sample points with
the same $(a,b)$-value, use the weight $p(\omega)p(\omega')/p_{a,b}(a,b)$.
Fibres of zero mass contribute zero. This preserves the two stated
marginals and gives the required conditional independence.
\end{proof}


The formal proof of $\mathsf M_{k+1}$ applies the case $k$, with the other Ingleton variant, to
$(a',c',b',d',z')$ and adds finitely many Shannon inequalities and the conditional independence
\cite[proof of Theorem~22]{CC}. For $\mathsf C_{k+1}$ it applies the case $k$ to the joint variables
$\bigl((a',z'),(b',z'),(c',z'),(d',z'),(c',z')\bigr)$, following the second proof of Theorem~16 and the subsequent remark in \cite{CC}.

\section{The two-copy inequality}\label{sec:lemmaA}

\begin{proposition}[two-copy inequality]\label{prop:A}
In the setting of \S\ref{sec:entropy},
\[
  194497\,L\le 49470\,S+73899\,h(1,1)+99532\,h(1,0)+98433\,h(0,1)+4986\,h(2,0)+6659\,h(0,2).
\]
\end{proposition}

\begin{proof}
The inequality is the sum, with the positive integer weights listed, of the 27 Shannon
inequalities and the support inequality of Table~\ref{tab:shannon} and of the ten non-Shannon
inequalities of Table~\ref{tab:cuts}, after every entropy has been rewritten with (R1)--(R6). Each
Shannon row is an instance of (E3), written as a conditional mutual information of joint
variables; each row of Table~\ref{tab:cuts} is an instance of Theorem~\ref{thm:matus} or
\ref{thm:companion} in which each of $a,b,c,d,z$ is a single form or a pair of forms, so that each
of the joint entropies of the five-variable expression is an $\Hb[F]$. After rewriting, 49
distinct joint entropies $\Hb[F]$ occur besides $L$, $S$ and the $h(i,j)$. Their coefficients
cancel, apart from those that (R4)--(R6) turn into multiples of $L$ and of
$h(1,0),h(0,1),h(2,0),h(0,2),h(1,1)$. The sum is exactly the stated inequality.
\end{proof}

The cancellation is an exact calculation over the integers. The
formal proof supplies each row separately and ends with their explicit
weighted sum. Tables~\ref{tab:shannon} and \ref{tab:cuts} give all the
inequality rows; the remaining operations are the entropy identities
(R1)--(R6). Thus the certificate can be checked without reproducing
the search that found its coefficients.

\begin{table}[ht]
\small
\caption{Shannon rows and the support row of Proposition~\ref{prop:A}. Each entry
$I(A;C\mid B)=H(A,B)+H(B,C)-H(A,B,C)-H(B)\ge0$ is an instance of (E3); an empty condition means
$B=\varnothing$. Row names are those of the formal proof.}\label{tab:shannon}
\begin{tabular}{@{}lll@{}}
\toprule
row & inequality & weight\\
\midrule
s116 & $I(Y_2\,;\,Y_1+X_2)$ & 21105 \\
s117 & $I(Y_2\,;\,X_1-X_2)$ & 9814 \\
s118 & $I(Y_2\,;\,X_1)$ & 17442 \\
s119 & $I(Y_2\,;\,X_1+X_2)$ & 4986 \\
s120 & $I(Y_2\,;\,X_1+Y_1)$ & 26370 \\
s121 & $I((X_2,Y_2)\,;\,X_1-Y_1-X_2)$ & 16965 \\
s122 & $I((X_2,Y_2)\,;\,X_1-Y_1+Y_2)$ & 12564 \\
s123 & $I((X_2,Y_2)\,;\,X_1)$ & 11708 \\
s124 & $I((X_2,Y_2)\,;\,(X_1,Y_1,Y_2)\mid Y_2)$ & 1304 \\
s125 & $I((X_2,Y_2)\,;\,(X_1+Y_1,X_2)\mid X_2)$ & 4896 \\
s126 & $I(X_2\,;\,Y_1-Y_2)$ & 7764 \\
s127 & $I(X_2\,;\,Y_1+Y_2)$ & 6659 \\
s128 & $I(X_2\,;\,X_1+Y_2)$ & 16839 \\
s129 & $I(X_2\,;\,X_1+Y_1)$ & 23100 \\
s130 & $I(Y_1-Y_2\,;\,(X_1,X_2))$ & 2376 \\
s131 & $I(Y_1+X_2\,;\,X_1+X_2+Y_2)$ & 18522 \\
s132 & $I(Y_1+X_2\,;\,X_1+Y_1+Y_2)$ & 26001 \\
s133 & $I(X_1-X_2\,;\,(Y_1,Y_2))$ & 4016 \\
s134 & $I((Y_1,Y_2)\,;\,(X_1+X_2+Y_2,Y_1-Y_2)\mid Y_1-Y_2)$ & 3564 \\
s135 & $I((Y_1+X_2,Y_2)\,;\,(X_1+X_2,Y_1+X_2-Y_2)\mid Y_1+X_2-Y_2)$ & 2277 \\
s136 & $I((Y_1+X_2,Y_2)\,;\,(X_1,Y_1+X_2+Y_2)\mid Y_1+X_2+Y_2)$ & 2520 \\
s137 & $I((X_1,Y_1,Y_2)\,;\,(X_1,Y_1+Y_2,X_2)\mid (X_1,Y_1+Y_2))$ & 748 \\
s138 & $I((X_1+Y_1+X_2,Y_2)\,;\,(X_1,Y_1+X_2)\mid X_1+Y_1+X_2)$ & 2376 \\
s139 & $I((X_1,X_2)\,;\,(X_1-X_2,Y_1+X_2+Y_2)\mid X_1-X_2)$ & 6024 \\
s140 & $I((X_1+Y_2,X_2)\,;\,(X_1-X_2+Y_2,Y_1+Y_2)\mid X_1-X_2+Y_2)$ & 4149 \\
s141 & $I((Y_1-Y_2,X_2+Y_2)\,;\,(X_1+Y_2,Y_1-Y_2)\mid Y_1-Y_2)$ & 6576 \\
s142 & $I((X_1+Y_2,X_2+Y_2)\,;\,(X_1-X_2,Y_1+X_2)\mid X_1-X_2)$ & 7806 \\
\midrule
r143 & $S-H(X_1+Y_1)\ge0$ \quad (R7) & 49470 \\
\bottomrule
\end{tabular}
\end{table}

\begin{table}[ht]
\small
\caption{The ten non-Shannon rows of Proposition~\ref{prop:A}: instances of
Theorem~\ref{thm:matus} ($\mathsf M_k$) and Theorem~\ref{thm:companion} ($\mathsf C_k$), with the
arguments $(a,b,c,d,z)$.}\label{tab:cuts}
\begin{tabular}{@{}l>{\raggedright\arraybackslash}p{11.2cm}r@{}}
\toprule
row & instance & weight\\
\midrule
cut144 & $\mathsf M_1[abcd]$: $a=(X_1+Y_2,Y_1-Y_2)$, $b=(X_1-X_2,Y_1+X_2)$, $c=(X_1-X_2+Y_2,Y_1+X_2-Y_2)$, $d=z=(X_1,Y_1)$ & 4794 \\
cut145 & $\mathsf C_2[acbd]$: $a=(X_1,Y_1-Y_2)$, $b=(X_1+Y_2,Y_1-Y_2)$, $c=z=(X_1+X_2+Y_2,Y_1-Y_2)$, $d=X_1+Y_1+X_2-Y_2$ & 1188 \\
cut146 & $\mathsf M_3[abcd]$: $a=X_2$, $b=X_1+Y_1+X_2$, $c=Y_1+X_2$, $d=X_1+X_2$, $z=Y_1+X_2-Y_2$ & 1146 \\
cut147 & $\mathsf C_2[acbd]$: $a=(X_1-X_2,Y_1)$, $b=(X_1-X_2,Y_1+X_2)$, $c=z=(X_1-X_2,Y_1+X_2+Y_2)$, $d=X_1+Y_1-X_2+Y_2$ & 2008 \\
cut148 & $\mathsf C_3[acbd]$: $a=X_1+Y_1+X_2$, $b=Y_1+X_2-Y_2$, $c=z=X_2$, $d=X_1+X_2$ & 516 \\
cut149 & $\mathsf M_3[abcd]$: $a=Y_1$, $b=Y_1+X_2+Y_2$, $c=Y_1+X_2$, $d=Y_1+Y_2$, $z=X_1-Y_1-X_2$ & 1506 \\
cut150 & $\mathsf M_3[abcd]$: $a=Y_2$, $b=X_1+Y_1+Y_2$, $c=z=X_1-X_2+Y_2$, $d=Y_1+Y_2$ & 963 \\
cut151 & $\mathsf M_3[acbd]$: $a=X_1$, $b=X_1-Y_1+Y_2$, $c=(X_1+X_2+Y_2,Y_1)$, $d=X_1+X_2$, $z=X_1+X_2+Y_2$ & 396 \\
cut152 & $\mathsf M_3[acbd]$: $a=Y_1$, $b=X_1-Y_1-X_2$, $c=(X_1,Y_1+X_2+Y_2)$, $d=Y_1+Y_2$, $z=Y_1+X_2+Y_2$ & 420 \\
cut153 & $\mathsf M_3[abcd]$: $a=Y_1+X_2$, $b=X_1-Y_1+Y_2$, $c=z=Y_1$, $d=Y_1+X_2-Y_2$ & 153 \\
\bottomrule
\end{tabular}
\end{table}

\begin{remark}[structure of the certificate]\label{rem:cuts}
In six of the ten rows $z$ coincides with $d$ (cut144) or with $c$ (cut145, cut147, cut148,
cut150, cut153), so these are four-variable inequalities. Writing
$\mathsf M^{(4)}_s(a,b,c,d)=\cmi bca+s[abcd]+\binom{s+1}2(\cmi acb+\cmi abc)$ for Mat\'u\v{s}'s
four-variable family \cite{Mat07}, whose case $s=1$ is the Zhang--Yeung inequality \cite{ZY98}, a
direct expansion gives $\mathsf M_1[abcd]|_{z=d}=\mathsf M^{(4)}_1(a,b,d,c)$,
$\mathsf C_s[acbd]|_{z=c}=\mathsf M^{(4)}_s(c,a,b,d)$ for $s=2,3$, and
$\mathsf M_3[abcd]|_{z=c}=\mathsf M^{(4)}_3(a,b,c,d)$. Each of the four arguments of cut144
determines $X_1+Y_1$. Only cut146, cut149, cut151 and cut152 involve five distinct variables. The coefficients were obtained by a finite linear-programming search.
Their validity here is established by the displayed certificate and does not
depend on optimality of that search.
\end{remark}

\begin{corollary}[symmetric two-copy inequality]\label{cor:Asym}
\[
  22882\,L\le 5820\,S+8694\,h(1,1)+11645\,\bigl(h(1,0)+h(0,1)\bigr)+685\,\bigl(h(2,0)+h(0,2)\bigr).
\]
\end{corollary}

\begin{proof}
The set $\Gamma'=\{(-y,-x):(x,y)\in\Gamma\}\subset(-Y)\times(-X)$ again has distinct differences,
$|\Gamma'|=|\Gamma|$ and $|(-Y)+(-X)|=|X+Y|$. Its marginals are the reflections of $\nu$ and $\mu$,
and reflection preserves entropy, so the array attached to $\Gamma'$ is $h'(i,j)=h(j,i)$.
Proposition~\ref{prop:A} for $\Gamma'$ is Proposition~\ref{prop:A} for $\Gamma$ with
$h(i,j)$ replaced by $h(j,i)$. Adding the two inequalities and dividing by $17$ gives the claim.
\end{proof}

\section{The grid lemma}\label{sec:grid}

\begin{proposition}[grid lemma]\label{prop:grid}
Let $h:\N^2\to\R$ and $L,S\in\R$ satisfy, for all $i,j\in\N$,
\begin{itemize}
\item[(G1)] $h(i+2,j)+h(i,j)\le2h(i+1,j)$ and $h(i,j+2)+h(i,j)\le2h(i,j+1)$;
\item[(G2)] $h(i,j)\le h(i+1,j)$, $h(i,j)\le h(i,j+1)$, and $h(i,j)\ge0$;
\item[(G3)] $L+h(i,j)\le h(i+1,j)+h(i,j+1)$;
\item[(G4)] $h(1,1)\le S$;
\item[(G5)] $22882\,L\le 5820\,S+8694\,h(1,1)+11645\,(h(1,0)+h(0,1))+685\,(h(2,0)+h(0,2))$.
\end{itemize}
Then $(21512\e+3148)\,L\le(37804\e-13144)\,S$.
\end{proposition}

The proof occupies the rest of this section.

\subsection{Symmetrisation}
The array $g(i,j)=\frac12(h(i,j)+h(j,i))$ is symmetric and satisfies (G1)--(G4). Concavity of $g$
in $i$ uses concavity of $h$ in both variables, and the link of $g$ at $(0,j)$ is the average of
the links of $h$ at $(0,j)$ and $(j,0)$. Condition (G5) becomes
\begin{equation}\label{eq:G5sym}
  22882\,L\le5820\,S+8694\,g(1,1)+23290\,g(0,1)+1370\,g(0,2).
\end{equation}
From now on we use only: $g$ is symmetric; $i\mapsto g(i,j)$ is concave and nondecreasing for each
$j$; $g\ge0$; the links $\ell_j:=g(1,j)+g(0,j+1)-g(0,j)-L\ge0$; $g(1,1)\le S$; and
\eqref{eq:G5sym}.

\subsection{The weights}
For $m,k\in\N$ let $B(m,k)=\int_0^1t^m(1-t)^k\e^t\,dt\ge0$ and $w_k=B(1,k)$.

\begin{lemma}\label{lem:weights}
$w_0=1$, $w_1=3-\e$, and for all $k\in\N$:
\begin{itemize}
\item[(i)] $w_{k+2}=(k+4)w_{k+1}-(k+1)w_k$;
\item[(ii)] $0\le w_{k+1}\le w_k$ and $2w_{k+1}\le w_k+w_{k+2}$;
\item[(iii)] $w_k\le1/(k+1)$;
\item[(iv)] $(k+1)w_{k+1}\le(k+3)w_{k+2}$.
\end{itemize}
\end{lemma}

\begin{proof}
Integration by parts gives $B(0,k+1)=(k+1)B(0,k)-1$, $B(0,0)=\e-1$, $B(1,0)=1$, and
$B(m,k)=B(m,k+1)+B(m+1,k)$ gives $w_k=1-kB(0,k)$. These imply $w_1=3-\e$ and (i). Next
$w_k-w_{k+1}=B(2,k)\ge0$ and $w_k-2w_{k+1}+w_{k+2}=B(3,k)\ge0$. From $B(0,k+1)\ge0$ we get
$(k+1)B(0,k)\ge1$, hence (iii). Finally (iv) is the convexity in (ii) at $k+1$ combined with (i).
\end{proof}

The integral representation supplies both the recurrence needed for
cancellation and the decay needed to pass to the limit. In particular,
$w_1=3-\e$ accounts for the occurrence of $\e$ in the final exponent.

\subsection{Row inequalities}
For $f:\N\to\R$ let $\tau_m(f)=mf(1)-(m-1)f(0)-f(m)$, the defect at $m$ of the chord through
$(0,f(0))$ and $(1,f(1))$.

\begin{lemma}\label{lem:rows}
Let $f$ be concave, i.e.\ $f(k+2)+f(k)\le2f(k+1)$. Then for all $m\in\N$: $\tau_m(f)\ge0$,
$(m+1)\tau_{m+1}(f)\le m\,\tau_{m+2}(f)$, and
\[
  w_{m+1}\,\tau_{m+2}(f)\le w_{m+2}\,\tau_{m+4}(f).
\]
\end{lemma}

\begin{proof}
With $\delta_k=f(k+1)-f(k)$ nonincreasing, $\tau_{m+1}=\sum_{k=1}^{m}(\delta_0-\delta_k)$ is a sum of
$m$ nonnegative, nondecreasing terms. Hence $\tau_{m+1}\ge0$, and averages over longer initial segments are larger. For $m\ge1$ this gives
$\tau_{m+1}/m\le\tau_{m+2}/(m+1)$; the case $m=0$ follows from $\tau_1=0$. Applying this twice gives
$(m+3)\tau_{m+2}\le(m+1)\tau_{m+4}$. Multiplying by Lemma~\ref{lem:weights}(iv),
$(m+1)w_{m+1}\le(m+3)w_{m+2}$, gives the last claim.
\end{proof}

\subsection{The certificate}
Put
\[
  \kappa=\frac{\e-1}{24660},\qquad N=1+21512\,\kappa,\qquad \Lambda=\e+13144\,\kappa ,
\]
so that $24660\,N=21512\e+3148$ and $24660\,\Lambda=37804\e-13144$.

\begin{lemma}\label{lem:invariant}
For every $m\in\N$,
\begin{equation}\label{eq:inv}
  (N-w_{m+2})\,L\le\Lambda S+(w_{m+1}-w_{m+2})\,g(0,m+3)-w_{m+1}\,g(m+2,m+3).
\end{equation}
\end{lemma}

\begin{proof}
Write $\tau^{(j)}_m=\tau_m(g(\cdot,j))$. For $m=0$ (where $w_1=3-\e$ and $w_2=11-4\e$) the
difference of the two sides of \eqref{eq:inv} equals
\begin{multline*}
 (\e-2-1370\kappa)\,\ell_1+(3\e-8)\,\ell_2+w_0\,\tau^{(1)}_2+w_1\,\tau^{(2)}_3
 +(\e+7324\kappa)\,(S-g(1,1))\\
 +\kappa\,\bigl(5820S+8694g(1,1)+23290g(0,1)+1370g(0,2)-22882L\bigr),
\end{multline*}
using $g(2,1)=g(1,2)$ and $g(3,2)=g(2,3)$ in $\tau^{(1)}_2=2g(1,1)-g(0,1)-g(2,1)$ and
$\tau^{(2)}_3=3g(1,2)-2g(0,2)-g(3,2)$. All coefficients are positive: for example,
$2.7<\e<2.8$ gives $0<\kappa<10^{-4}$ and
$\e-2-1370\kappa>0$, and each
bracket is nonnegative by the links, Lemma~\ref{lem:rows}, $g(1,1)\le S$ and \eqref{eq:G5sym}.

For the step from $m$ to $m+1$, add to \eqref{eq:inv} the link $\ell_{m+3}\ge0$ with weight
$w_{m+2}-w_{m+3}\ge0$ and the row inequality
$w_{m+2}\tau^{(m+3)}_{m+4}-w_{m+1}\tau^{(m+3)}_{m+2}\ge0$ of Lemma~\ref{lem:rows}. By the
recurrence $w_{m+3}=(m+5)w_{m+2}-(m+2)w_{m+1}$ and the symmetry $g(m+4,m+3)=g(m+3,m+4)$, the
terms in $g(1,m+3)$ and $g(0,m+3)$ cancel and the result is \eqref{eq:inv} for $m+1$.
\end{proof}

The choice of $\kappa$ is forced: it is the unique value for which the coefficient of $g(0,1)$ in
the base combination vanishes. The row inequalities with weights $w_{j-2},w_{j-1}$ and the links
with weights $w_{j-1}-w_j$, $j\ge3$, form the dual certificate; for every finite truncation the
remainder is the last two terms of \eqref{eq:inv}.

\begin{proof}[Proof of Proposition~\ref{prop:grid}]
By monotonicity $g(m+2,m+3)\ge g(0,m+3)\ge0$, and $w_{m+1}\ge w_{m+2}\ge0$, so the last two terms of
\eqref{eq:inv} add up to at most $-w_{m+2}\,g(0,m+3)\le0$. Hence $(N-w_{m+2})L\le\Lambda S$ for all
$m$. If $L\le0$ the claim follows from $\Lambda S\ge\Lambda g(1,1)\ge0$. If $L>0$, let $m\to\infty$
and use $w_{m+2}\le1/(m+3)$: this gives $NL\le\Lambda S$, and multiplying by $24660$ gives the
claim.
\end{proof}

\section{Proofs of Theorem~\ref{thm:pair} and Corollary~\ref{cor:theta}}\label{sec:assembly}

\begin{proof}[Proof of Theorem~\ref{thm:pair}]
If $X$ or $Y$ is empty, both sides vanish. Otherwise take $\Gamma$ as in Lemma~\ref{lem:coupling}
and $h,L,S$ as in \S\ref{sec:entropy}. Lemma~\ref{lem:grid} gives (G1), (G2) and (G4),
Lemma~\ref{lem:link} gives (G3), and Corollary~\ref{cor:Asym} gives (G5). By
Proposition~\ref{prop:grid},
\[
  (21512\e+3148)\log|X-Y|\le(37804\e-13144)\log|X+Y| ,
\]
that is $|X-Y|\le|X+Y|^{\lamI}$, since
$(37804\e-13144)/(21512\e+3148)=(9451\e-3286)/(5378\e+787)$.
\end{proof}

\begin{proof}[Proof of Corollary~\ref{cor:theta}]
By Theorem~\ref{thm:pair} with $G=\Z$, $\lamI$ belongs to the set in \eqref{eq:lsup}, so
$\lsup\le\lamI$. By Theorem~\ref{thm:transfer}, $\theta^\ast\le2-1/\lsup\le2-1/\lamI$, and
$2-1/\lamI=(13524\e-7359)/(9451\e-3286)$.
\end{proof}

\appendix

\section{The formal proof}\label{app:lean}

The accompanying repository consists of the twenty proof modules listed
below, the manuscript, and build and publication metadata. Its mathematical
namespace is \lean{SumsDifferences}; subsidiary namespaces include
\lean{MultiScale}, \lean{ConverseAmplification}, \lean{CoupledEntropy},
\lean{CoupledForms}, \lean{NonShannon}, \lean{GridClosedForm}, and
\lean{ClosedForm}. Module names in the table omit their common prefix
\lean{SumDifference} and the extension \lean{.lean}.

The reference toolchain is \lean{leanprover/lean4:v4.28.0}, and the
Mathlib commit is
\begin{center}
\texttt{8f9d9cff6bd728b17a24e163c9402775d9e6a365}.
\end{center}
The additive-combinatorial input taken from Mathlib is the
Pl\"unnecke--Ruzsa inequality
\lean{pluennecke\_\allowbreak{}ruzsa\_\allowbreak{}inequality\_\allowbreak{}nsmul\_\allowbreak{}sub\_\allowbreak{}nsmul\_\allowbreak{}add}.
The finite entropy theory is developed in
\lean{FinEntropy}, \lean{JointEntropy}, \lean{CondEntropy},
\lean{EntropyEquality}, \lean{EntropyCompute}, and \lean{ProductLaw}.
Group-valued laws are represented by elements of the group algebra
$\R[G]$ with nonnegative coefficients of total mass one; multiplication
is convolution. Thus $\lean{ent}$ and $\lean{pushEntropy}$ denote the
ordinary Shannon entropies used in the paper.

The theorem \lean{pair\_\allowbreak{}ceiling\_\allowbreak{}entropic} is polymorphic in a type
$G$ equipped with \lean{AddCommGroup G}. Its auxiliary
\lean{DecidableEq G} instance supplies equality decisions for finite
sets and imposes no mathematical restriction, since classical logic
provides such an instance for every $G$. Cardinalities are coerced
to $\R$, and exponentiation is real exponentiation. Empty sets are
included. The definition \lean{Admissible} has exactly the quantifiers
in \eqref{eq:adm}; \lean{theta} is its real supremum, with
$\operatorname{sSup}\varnothing=0$. No lower-bound construction is
required to prove the upper bound on this supremum.

\medskip
\noindent
{\small
\begin{longtable}{@{}>{\raggedright\arraybackslash}p{2.6cm}>{\raggedright\arraybackslash}p{7.5cm}>{\raggedright\arraybackslash}p{4.6cm}@{}}
\toprule
paper & Lean declaration & module\\
\midrule
\endfirsthead
\toprule
paper & Lean declaration & module\\
\midrule
\endhead
\eqref{eq:adm}, $\theta^\ast$ & \lean{Admissible}, \lean{theta} & \lean{ThetaDefs}\\
\eqref{eq:lsup} & \lean{pairCeilingExponents}, \lean{lamSup} & \lean{ThetaMultiScaleCore}\\
Lemma~\ref{lem:window} & \lean{admissible\_\allowbreak{}le\_\allowbreak{}of\_\allowbreak{}rpow\_\allowbreak{}bound} & \lean{ThetaLocalization}\\
Lemma~\ref{lem:packing} & \lean{exists\_\allowbreak{}translate\_\allowbreak{}packing} & \lean{ThetaLocalization}\\
Lemma~\ref{lem:local} & \lean{card\_\allowbreak{}sub\_\allowbreak{}mul\_\allowbreak{}card\_\allowbreak{}le\_\allowbreak{}localized\_\allowbreak{}const} & \lean{ThetaLocalization}\\
Lemma~\ref{lem:onescale} & \lean{card\_\allowbreak{}sub\_\allowbreak{}mul\_\allowbreak{}le\_\allowbreak{}scale} & \lean{ThetaMultiScaleCore}\\
Proposition~\ref{prop:multiscale} & \lean{card\_\allowbreak{}sub\_\allowbreak{}pow\_\allowbreak{}mul\_\allowbreak{}le\_\allowbreak{}telescope}, \lean{card\_\allowbreak{}sub\_\allowbreak{}pow\_\allowbreak{}le\_\allowbreak{}multiscale} & \lean{ThetaMultiScaleCore}\\
Theorem~\ref{thm:transfer} & \lean{one\_\allowbreak{}le\_\allowbreak{}of\_\allowbreak{}pair\_\allowbreak{}ceiling}, \lean{admissible\_\allowbreak{}le\_\allowbreak{}of\_\allowbreak{}pairCeiling\_\allowbreak{}multiscale\_\allowbreak{}J}, \lean{admissible\_\allowbreak{}le\_\allowbreak{}of\_\allowbreak{}pairCeiling\_\allowbreak{}multiscale}, \lean{theta\_\allowbreak{}le\_\allowbreak{}of\_\allowbreak{}pair\_\allowbreak{}ceiling}, \lean{theta\_\allowbreak{}le\_\allowbreak{}two\_\allowbreak{}sub\_\allowbreak{}inv\_\allowbreak{}lamSup} & \lean{ThetaMultiScaleCore}\\
(E4), (E5), (E1) & \lean{ent\_\allowbreak{}le\_\allowbreak{}ent\_\allowbreak{}mul}, \lean{ent\_\allowbreak{}madiman}, \lean{ent\_\allowbreak{}mul\_\allowbreak{}le\_\allowbreak{}log\_\allowbreak{}card} & \lean{EntropySumsetCalculus}\\
Lemma~\ref{lem:coupling} & \lean{exists\_\allowbreak{}coupling} & \lean{CoupledEntropyCore}\\
Lemma~\ref{lem:link} & \lean{coupled\_\allowbreak{}link}, \lean{link} & \lean{EntropySumsetCalculus}, \lean{CoupledEntropyCore}\\
Lemma~\ref{lem:grid} & \lean{ent\_\allowbreak{}concave\_\allowbreak{}step}, \lean{grid\_\allowbreak{}concave} & \lean{CoupledEntropyCore}\\
$\Hb[F]$, (R1)--(R7) & \lean{HL}, \lean{Det.gen}, \lean{HL\_\allowbreak{}eq\_\allowbreak{}of\_\allowbreak{}det}, \lean{HL\_\allowbreak{}swap}, \lean{HL\_\allowbreak{}indep}, \lean{HL\_\allowbreak{}pair1/2}, \lean{HL\_\allowbreak{}X1}, \dots, \lean{HL\_\allowbreak{}X1Y1\_\allowbreak{}le} & \lean{LinearFormsEntropy}\\
identities via (R1)--(R3) & \lean{HL\_\allowbreak{}eq\_\allowbreak{}norm} & \lean{LinearFormsNormalForm}\\
Lemma~\ref{lem:copy} & \lean{copy\_\allowbreak{}step} & \lean{MatusInequality}, \lean{CopyLemma}\\
Theorem~\ref{thm:matus} & \lean{matus\_\allowbreak{}ineq} & \lean{MatusInequality}\\
Theorem~\ref{thm:companion} & \lean{companion\_\allowbreak{}ineq} & \lean{CompanionInequality}\\
pairs of forms as variables & \lean{HS\_\allowbreak{}eq\_\allowbreak{}HL2} & \lean{LinearFormsPairs}\\
Proposition~\ref{prop:A} & \lean{CoupledForms.two\_\allowbreak{}copy\_\allowbreak{}ineq} & \lean{ThetaTwoCopyLemma}\\
Corollary~\ref{cor:Asym} & \lean{CoupledForms.two\_\allowbreak{}copy\_\allowbreak{}ineq\_\allowbreak{}sym} & \lean{ThetaClosedFormBound}\\
Lemma~\ref{lem:weights} & \lean{GridClosedForm.Z\_\allowbreak{}zero}, \lean{Z\_\allowbreak{}one}, \lean{Z\_\allowbreak{}rec}, \lean{Z\_\allowbreak{}succ\_\allowbreak{}le}, \lean{Z\_\allowbreak{}convex}, \lean{Z\_\allowbreak{}le}, \lean{Z\_\allowbreak{}weight} & \lean{ThetaGridClosedForm}\\
Lemma~\ref{lem:rows} & \lean{tau\_\allowbreak{}nonneg}, \lean{tau\_\allowbreak{}ratio}, \lean{tau\_\allowbreak{}two}, \lean{psi\_\allowbreak{}nonneg} & \lean{ThetaGridClosedForm}\\
Lemma~\ref{lem:invariant} & \lean{inv\_\allowbreak{}base}, \lean{inv\_\allowbreak{}step}, \lean{inv\_\allowbreak{}all} & \lean{ThetaGridClosedForm}\\
Proposition~\ref{prop:grid} & \lean{grid\_\allowbreak{}closed\_\allowbreak{}sym}, \lean{grid\_\allowbreak{}closed\_\allowbreak{}form} & \lean{ThetaGridClosedForm}\\
Theorem~\ref{thm:pair} & \lean{ClosedForm.log\_\allowbreak{}card\_\allowbreak{}le\_\allowbreak{}of\_\allowbreak{}coupling\_\allowbreak{}closed}, \lean{pair\_\allowbreak{}ceiling\_\allowbreak{}entropic} & \lean{ThetaClosedFormBound}\\
Corollary~\ref{cor:theta} & \lean{lamSup\_\allowbreak{}le\_\allowbreak{}closed\_\allowbreak{}form}, \lean{theta\_\allowbreak{}le\_\allowbreak{}closed\_\allowbreak{}form} & \lean{ThetaClosedFormBound}\\
\bottomrule
\end{longtable}}

\medskip
\noindent\emph{Differences of presentation.} Lemmas~\ref{lem:local}--\ref{lem:onescale} and
Proposition~\ref{prop:multiscale} are formalised with an additional constant $C>0$ in the
hypothesis $|X-B|\le C|X+B|^\lambda$; the paper uses $C=1$, as does the formal proof of
Theorem~\ref{thm:transfer}. The pair exponent is formalised directly by the infimum
\eqref{eq:lsup}; no alternative characterisation of it is used.

\medskip
\noindent\emph{The certificate of Proposition~\ref{prop:A}.} Each of the 76 rows (Tables
\ref{tab:shannon} and \ref{tab:cuts}, the identities (R4)--(R6), 24 further identifications by (R1)--(R3) and
$\Hb[\varnothing]=0$) is a separate lemma, and the proposition is closed by
\lean{linear\_\allowbreak{}combination} with the integer weights of the tables.
The identifications of lists of forms use \lean{HL\_\allowbreak{}eq\_\allowbreak{}norm}; independence and the
identifications with $L$ and $h$ are proved separately. For the former,
a computable test finds integer witnesses for
the mutual determination of two lists of forms (allowing (R2) and (R3)), the kernel re-checks
these witnesses with \lean{decide}, and the lemma \lean{Det.gen} turns them into an equality of
entropies. The search procedure is not trusted; only the re-check enters the proof. The published Lean source contains the complete certificate;
no external data file or search program is a proof input.

\medskip
\noindent\emph{Axioms.} The commands
\begin{quote}\small
\lean{\#print axioms SumsDifferences.theta\_le\_closed\_form}\\
\lean{\#print axioms SumsDifferences.pair\_ceiling\_entropic}
\end{quote}
report \lean{propext}, \lean{Classical.choice} and \lean{Quot.sound} only.

\begin{thebibliography}{99}

\bibitem{CC} E.~P.~Csirmaz and L.~Csirmaz,
\emph{Information inequalities for five random variables},
Computation \textbf{14} (2026), no.~2, article~42.
Extended version: \href{https://arxiv.org/abs/2512.23316v2}{arXiv:2512.23316v2}.
References to numbered results are to this version.
\url{https://doi.org/10.3390/computation14020042}.

\bibitem{DFZ11} R.~Dougherty, C.~Freiling, and K.~Zeger,
\emph{Non-Shannon information inequalities in four random variables},
2011. \href{https://arxiv.org/abs/1104.3602}{arXiv:1104.3602}.

\bibitem{GHR} K.~Gyarmati, F.~Hennecart, and I.~Z.~Ruzsa,
\emph{Sums and differences of finite sets},
Funct. Approx. Comment. Math. \textbf{37} (2007), 175--186.
\href{https://gyarmatikati.web.elte.hu/publ/sumdiffv.pdf}{Author manuscript}.
\url{https://doi.org/10.7169/facm/1229618749}.

\bibitem{HRY} F.~Hennecart, G.~Robert, and A.~Yudin,
\emph{On the number of sums and differences},
Ast\'erisque \textbf{258} (1999), 173--178.
\url{https://www.numdam.org/item/AST_1999__258__173_0/}.

\bibitem{Mad08} M.~Madiman, \emph{On the entropy of sums},
Proc. IEEE Information Theory Workshop, Porto, 2008, 303--307.
\href{https://www.stat.yale.edu/~mm888/Pubs/2008/ITW-sums08.pdf}{Author manuscript}.
\url{https://doi.org/10.1109/ITW.2008.4578674}.

\bibitem{MMT12} M.~Madiman, A.~W.~Marcus, and P.~Tetali,
\emph{Entropy and set cardinality inequalities for partition-determined functions},
Random Structures Algorithms \textbf{40} (2012), 399--424.
\href{https://arxiv.org/abs/0901.0055}{arXiv:0901.0055}.

\bibitem{Mat07} F.~Mat\'u\v{s}, \emph{Infinitely many information inequalities},
Proc. IEEE International Symposium on Information Theory, Nice, 2007, 41--44.
\url{https://doi.org/10.1109/ISIT.2007.4557201}.
The five-variable family used here, with a proof, is reproduced in
\cite[Theorem~22]{CC}.

\bibitem{Mathlib} The mathlib Community, \emph{The Lean mathematical library},
Proc. 9th ACM SIGPLAN International Conference on Certified Programs and Proofs,
2020, 367--381.
\href{https://arxiv.org/abs/1910.09336}{arXiv:1910.09336}.
The Mathlib~4 revision used here is
\href{https://github.com/leanprover-community/mathlib4/tree/8f9d9cff6bd728b17a24e163c9402775d9e6a365}{8f9d9cff6bd728b17a24e163c9402775d9e6a365}.

\bibitem{Lean} L.~de~Moura and S.~Ullrich,
\emph{The Lean 4 theorem prover and programming language},
Automated Deduction---CADE~28, Lecture Notes in Comput. Sci. \textbf{12699},
Springer, 2021, 625--635.
\url{https://lean-lang.org/papers/lean4.pdf}.

\bibitem{Pet12} G.~Petridis,
\emph{New proofs of Pl\"unnecke-type estimates for product sets in groups},
Combinatorica \textbf{32} (2012), 721--733.
\href{https://arxiv.org/abs/1101.3507v3}{arXiv:1101.3507v3}.

\bibitem{Ru99} I.~Z.~Ruzsa, \emph{An analog of Freiman's theorem in groups},
Ast\'erisque \textbf{258} (1999), 323--326.
\url{https://www.numdam.org/item/AST_1999__258__323_0/}.

\bibitem{Ru09} I.~Z.~Ruzsa, \emph{Sumsets and entropy},
Random Structures Algorithms \textbf{34} (2009), 1--10.
\url{https://doi.org/10.1002/rsa.20248}.

\bibitem{Tao10} T.~Tao, \emph{Sumset and inverse sumset theory for Shannon entropy},
Combin. Probab. Comput. \textbf{19} (2010), 603--639.
Revised preprint, titled \emph{Sumset and inverse sumset theorems for Shannon entropy}:
\href{https://arxiv.org/abs/0906.4387v5}{arXiv:0906.4387v5}.

\bibitem{ZY98} Z.~Zhang and R.~W.~Yeung,
\emph{On characterization of entropy function via information inequalities},
IEEE Trans. Inform. Theory \textbf{44} (1998), 1440--1452.
\url{https://www.cs.cornell.edu/courses/cs783/2007fa/papers/ZYnonShannon.pdf}.

\end{thebibliography}
\end{document}