\documentclass[11pt]{article} \usepackage[T1]{fontenc} \usepackage[margin=1in]{geometry} \usepackage{amsmath,amssymb,amsthm,mathtools} \usepackage{microtype} \usepackage[hidelinks]{hyperref} \hypersetup{pdftitle={A Counterexample to Affine-Subspace Union Stability under Small Deletions},pdfauthor={Yuran Xiu},pdfkeywords={affine subspaces, Boolean cube, union stability, trimming, resolution over parities, proof complexity}} \newtheorem{theorem}{Theorem}[section] \newtheorem{lemma}[theorem]{Lemma} \newtheorem{corollary}[theorem]{Corollary} \theoremstyle{definition} \newtheorem{remark}[theorem]{Remark} \newcommand{\F}{\mathbb F} \newcommand{\codim}{\operatorname{codim}} \newcommand{\code}[1]{\texttt{\small\detokenize{#1}}} \title{A Counterexample to Affine-Subspace Union\\Stability under Small Deletions} \author{Yuran Xiu\\IIIS, Tsinghua University\\\texttt{xiuyr23@mails.tsinghua.edu.cn}} \date{15 October 2026} \begin{document} \maketitle \begin{abstract} We construct a family of affine coordinate subspaces of $\F_2^N$ whose union is the entire space, but for which deleting a $1/N$ fraction from each member removes a fraction larger than $N^{-c}$ from the union, for every fixed $c>0$ and arbitrarily large $N$. Each subspace has codimension $\log_2 N$, and the family has at most $2N^2$ members. The construction uses all monochromatic coordinate conditions of size $k$ on $2k$ distinguished coordinates, where $N=2^k$, and deletes their common intersection with the middle Hamming layer. The exact global loss is $\binom{2k}{k}/4^k$. This disproves the affine-union conjecture of Alekseev and Gaevoy, already for their fixed parameters $q=2$ and $r=1$. The all-exponent, arbitrarily-large-dimension counterexample has been formalized and checked in Lean~4. \end{abstract} \section{Introduction} If a small fraction of the points is deleted from each member of a covering family, how much of its union can disappear? Without structural assumptions, local retention says little about the union: the deleted points can be exactly those whose memberships have small multiplicity. We show that this remains an obstruction even when all the original sets are affine subspaces of small codimension and their union is the whole Boolean cube. Alekseev and Gaevoy proposed the following stability assertion in their study of polynomial-depth lower bounds for resolution over parities, denoted $\operatorname{Res}(\oplus)$~\cite[Conjectures~1.4 and~4.2]{AG26}. For fixed constants $r,q>0$, suppose affine subspaces $\Phi_1,\ldots,\Phi_m\subseteq\F_2^N$ have codimension at most $(\log N)^q$, and their union has size at least $2^{N-1}$. For arbitrary subsets $\Phi_i'\subseteq\Phi_i$ satisfying \begin{equation}\label{eq:local-conj} |\Phi_i'|\geq(1-N^{-r})|\Phi_i|, \end{equation} the proposed conclusion is \begin{equation}\label{eq:global-conj} \left|\bigcup_i\Phi_i'\right| \geq(1-N^{-rc})\left|\bigcup_i\Phi_i\right| \end{equation} for some positive constant $c$ depending only on $q$. We disprove this assertion for $r=1$ and $q=2$. \begin{theorem}\label{thm:main} For every real $c>0$ and every integer $N_0$, there exist an integer $N\geq\max\{1,N_0\}$ and a finite family of affine subspaces $\Phi_i\subseteq\F_2^N$, with subsets $\Phi_i'\subseteq\Phi_i$, such that \begin{enumerate} \item $\bigcup_i\Phi_i=\F_2^N$; \item $\codim\Phi_i\leq(\log N)^2$ for every $i$, with $\log$ the natural logarithm; \item $|\Phi_i'|=(1-1/N)|\Phi_i|$ for every $i$; \item $\left|\bigcup_i\Phi_i'\right|<(1-N^{-c})2^N$. \end{enumerate} The same family also satisfies the codimension bound $(\log_2N)^2$. It can be chosen with at most $2N^2$ members. \end{theorem} The theorem excludes every uniform positive exponent, even if it may depend on both $r$ and $q$, and even if the assertion is required only in sufficiently large dimensions. The construction is elementary: coordinate subcubes and central binomial coefficients suffice. Its consequence is the failure of the stated auxiliary combinatorial conjecture. It does not refute an unconditional proof-complexity lower bound, nor does it establish a new $\operatorname{Res}(\oplus)$ lower bound. \section{A cover by coordinate subspaces} Fix an integer $k\geq2$ and set $N=2^k$. Since $2k\leq2^k$, we may distinguish the first $2k$ coordinates of $\F_2^N$. Write $U=\{1,\ldots,2k\}$. For every $k$-element subset $S\subseteq U$ and every $b\in\F_2=\{0,1\}$, define \begin{equation}\label{eq:subspaces} \Phi_{S,b}=\{x\in\F_2^N:x_i=b\text{ for every }i\in S\}. \end{equation} There are $m=2\binom{2k}{k}\leq2\cdot2^{2k}=2N^2$ indexed members. Let the deleted set be the middle layer on the distinguished coordinates: \begin{equation}\label{eq:bad} B=\left\{x\in\F_2^N:\left|\{i\in U:x_i=1\}\right|=k\right\}. \end{equation} Coordinates outside $U$ are unrestricted. In every member of the family delete the same ambient set: \begin{equation}\label{eq:trim} \Phi'_{S,b}=\Phi_{S,b}\setminus B. \end{equation} \begin{lemma}\label{lem:dimension} Each $\Phi_{S,b}$ is an affine subspace of codimension $k$ and cardinality $2^{N-k}$. \end{lemma} \begin{proof} The coordinate projection $\pi_S:\F_2^N\to\F_2^S$ is a surjective linear map. Its fiber over the constant vector $b$ is a translate of $\ker\pi_S$, and is exactly~\eqref{eq:subspaces}. Rank-nullity gives $\dim\ker\pi_S=N-k$. Alternatively, the coordinates in $S$ are fixed and each of the other $N-k$ coordinates is free, which also gives the cardinality. \end{proof} \begin{lemma}\label{lem:cover} The family in~\eqref{eq:subspaces} covers $\F_2^N$. \end{lemma} \begin{proof} Among $2k$ Boolean coordinates, either at least $k$ are one or at least $k$ are zero. Choose a $k$-element subset of positions with that common value. The input belongs to its corresponding $\Phi_{S,b}$. \end{proof} \section{Exact local and global losses} \begin{lemma}[Local deletion]\label{lem:local} For every index $(S,b)$, \[ |\Phi_{S,b}\cap B|=2^{N-2k},\qquad |\Phi'_{S,b}|=(1-2^{-k})|\Phi_{S,b}|. \] \end{lemma} \begin{proof} When $b=1$, the $k$ coordinates of $S$ already supply all the ones allowed in $U$ by~\eqref{eq:bad}. Thus every coordinate in $U\setminus S$ must be zero. When $b=0$, the $k$ remaining coordinates of $U\setminus S$ must all be one. In either case all $2k$ distinguished coordinates are determined, and the other $N-2k$ coordinates are free. Dividing by the count in Lemma~\ref{lem:dimension} gives the deletion fraction $2^{N-2k}/2^{N-k}=2^{-k}$. Subtracting from one proves the retention identity. \end{proof} \begin{lemma}[Global deletion]\label{lem:global} The retained union is $\F_2^N\setminus B$, and its missing fraction is \begin{equation}\label{eq:loss} \delta_k:=\frac{|B|}{2^N}=\frac{\binom{2k}{k}}{4^k} \geq\frac{1}{2k+1}. \end{equation} \end{lemma} \begin{proof} Set difference by a fixed set distributes over unions, so Lemma~\ref{lem:cover} and~\eqref{eq:trim} give \[ \bigcup_{S,b}\Phi'_{S,b} =\left(\bigcup_{S,b}\Phi_{S,b}\right)\setminus B =\F_2^N\setminus B. \] There are $\binom{2k}{k}$ choices for the one positions in $U$, followed by $2^{N-2k}$ choices outside $U$. This proves the equality in~\eqref{eq:loss}. For the inequality, the binomial coefficients in row $2k$ attain their maximum at $k$. This follows, for $j1, \] and from symmetry for $j>k$. Their sum is $2^{2k}=4^k$, so $4^k\leq(2k+1)\binom{2k}{k}$, as required. \end{proof} The two loss estimates explain the obstruction. A point in the middle layer belongs to exactly two members: the all-one condition on its $k$ one positions and the all-zero condition on its $k$ zero positions. Deleting the whole middle layer is inexpensive within every individual subspace. Because the deletion is shared by all members, no surviving member restores a deleted point to the union. \section{Arbitrarily large counterexamples} \begin{lemma}\label{lem:parameters} For every $c>0$ and every $N_0$, an integer $k\geq2$ can be chosen so that \begin{equation}\label{eq:parameters} 2^k\geq N_0,\qquad k\leq(k\log2)^2,\qquad 2^{ck}>2k+1. \end{equation} \end{lemma} \begin{proof} The first condition holds for all sufficiently large $k$. The second holds once $k\geq1/(\log2)^2$. For the last condition, put $a=2^c=1+d$ with $d>0$. By the binomial theorem, for integers $k\geq2$, \[ a^k\geq\binom{k}{2}d^2=\frac{k(k-1)d^2}{2}. \] The quadratic expression on the right is greater than $2k+1$ for all sufficiently large $k$. Thus all three conditions can be met simultaneously. \end{proof} \begin{proof}[Proof of Theorem~\ref{thm:main}] Choose $k$ from Lemma~\ref{lem:parameters}, let $N=2^k$, and use the family~\eqref{eq:subspaces} with retained subsets~\eqref{eq:trim}. The inequality $2k\leq2^k$ holds at $k=2$ and persists by induction: if it holds at $k\geq2$, then $2(k+1)\leq4k\leq2^{k+1}$. Hence the distinguished coordinates exist. Lemma~\ref{lem:cover} gives the full union. By Lemma~\ref{lem:dimension} and the parameter choice, \[ \codim\Phi_{S,b}=k\leq(k\log2)^2=(\log N)^2. \] Also $k\leq k^2=(\log_2N)^2$. Lemma~\ref{lem:local} gives the exact local retained fraction $1-2^{-k}=1-1/N$. Finally, Lemma~\ref{lem:global} and the strict last inequality in~\eqref{eq:parameters} imply \[ \delta_k\geq\frac1{2k+1}>2^{-ck}=N^{-c}. \] Thus the retained union has size $(1-\delta_k)2^N<(1-N^{-c})2^N$. The bound $m\leq2N^2$ was established immediately after the construction. \end{proof} \begin{corollary}\label{cor:false} Conjectures~1.4 and~4.2 of~\cite{AG26}, with arbitrary retained subsets as stated there, fail for $q=2$ and $r=1$. \end{corollary} \begin{proof} For any proposed positive exponent $c$, Theorem~\ref{thm:main} meets the codimension and local-retention hypotheses. Its original union is the entire cube, so it also meets the half-cube union hypothesis. Its retained union strictly violates~\eqref{eq:global-conj} with $r=1$. Since $N_0$ is arbitrary, restricting the conjecture to sufficiently large $N$ does not avoid the counterexample. \end{proof} \paragraph{Scope of the obstruction.} The retained sets in this example are arbitrary subsets of affine subspaces, exactly as permitted in the conjecture. They are not required to be affine. The result does not address modified assertions imposing additional structure on those sets or changing the ambient dimension parameter. In particular, the extra unrestricted coordinates are part of the actual ambient space; the dimension in the deletion tolerance $1/N$ is the same $N$ used in the codimension hypothesis. \section{Formal verification} The formal construction uses actual affine subspaces of \code{Fin N -> ZMod 2}. A coordinate projection is proved surjective, and its fibers are represented as translates of its kernel. Rank-nullity proves that their codimension is $k$. Thus affine dimension is part of the checked statement, rather than inferred only from a set's cardinality. The development proves the counts of the coordinate fibers, the local deleted intersections, and the middle layer. It also proves that the original union is the full space and that the retained union is precisely the complement of the middle layer. Its final predicate \code{AffineUnion.TrimmingFailure} includes retained-subset containment, the local fraction, the half-cube hypothesis, the strict global failure, and both natural- and binary-logarithm codimension bounds. The declaration \begin{center}\code{AffineUnion.counterexample_all_c}\end{center} gives a failure for every positive real $c$ above every prescribed ambient threshold. The separate declaration \code{no_uniform_trimming_exponent} rules out even an exponent accompanied by an arbitrary eventual dimension threshold. These declarations formalize Theorem~\ref{thm:main}'s stability failure and Corollary~\ref{cor:false}. The supplementary family-size observation $m\leq2N^2$ is proved in the exposition and is not needed by the formal counterexample predicate. Verification used Lean~4.27.0 and mathlib commit \begin{center}\code{a3a10db0e9d66acbebf76c5e6a135066525ac900}.\end{center} The saved formal artifact includes its pinned dependency manifest, source hashes, successful independent rebuild logs, and transitive axiom reports. From the formal project's \texttt{lean} directory, the commands \begin{verbatim} lake exe cache get lake build lake env lean ParentAudit.lean \end{verbatim} use the saved toolchain and manifest. A separate saved rebuild script also checks dependency revisions and recompiles the local source into a fresh build. The accepted declarations depend only on \code{propext}, \code{Classical.choice}, and \code{Quot.sound}. There are no admitted lemmas, extra mathematical axioms, native decision procedures, or unchecked external certificates. The independent rebuild reused the pinned Lean compiler and dependency caches; it did not rebuild Lean or mathlib in full. \begin{thebibliography}{9} \bibitem{AG26} Yaroslav Alekseev and Nikita Gaevoy. \newblock New Polynomial-Depth Res(+) Lower Bounds. \newblock \emph{Electronic Colloquium on Computational Complexity}, Report TR26-007, 2026. \newblock \url{https://eccc.weizmann.ac.il/report/2026/007/}. Conjectures~1.4 and~4.2. \end{thebibliography} \end{document}