\documentclass[11pt]{amsart}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage{amsmath,amssymb,amsthm}
\usepackage[margin=1in]{geometry}
\usepackage[expansion=false]{microtype}
\usepackage{xurl}
\usepackage[hidelinks]{hyperref}
\hypersetup{pdfauthor={Ricardo Pinho},
 pdftitle={An explicit finite cylinder cover of the regular tetrahedron saving 3.86e-4 below the half-area bound},
 pdfsubject={Metric geometry; cylinder coverings},
 pdfkeywords={math.MG, math.CO, regular tetrahedron, exact certificate}}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newcommand{\R}{\mathbb R}
\newcommand{\Amin}{A_{\min}}
\newcommand{\conv}{\operatorname{conv}}
\newcommand{\area}{\operatorname{area}}
\newcommand{\proj}{\operatorname{proj}}
\title[An explicit finite cylinder cover of the regular tetrahedron]{An explicit finite cylinder cover of the regular tetrahedron saving $3.86\times10^{-4}$ below the half-area bound}
\author{Ricardo Pinho}
\thanks{Independent researcher.}
\email{pinho.ricardo@gmail.com}
\date{15 October 2026}
\subjclass[2020]{52A40, 52C17}
\keywords{Cylinder covering, regular tetrahedron, exact rational certificate}
\begin{document}
\begin{abstract}
We give an explicit cover of a regular tetrahedron by $4096$ cylinders with compact triangular perpendicular bases. The sum of their base areas, divided by the tetrahedron's minimum orthogonal projection area, lies in
$[0.499613830783714148,\,0.499613830783714149)$.
Thus the saving below $1/2$ exceeds $0.000386169216285851$.
The construction uses a finite tilt in the angular-sector framework of OpenAI's September 2026 preprint and rationally specified radial cutoffs. Coverage is certified by exact linear-programming dual witnesses, and independently verified by exhaustive rational polyhedron clipping. We describe the geometric reduction, the certificate obligations, and reproducible verification of the full closed tetrahedron and the perpendicular base areas. No optimality is asserted.
\end{abstract}
\maketitle

\section{Introduction and result}
A cylinder in Euclidean three-space is $B+\R u$, where $u$ is a unit vector and $B\subset u^\perp$ is a measurable set of finite planar area. For a convex body $K$, put
\[
 \Amin(K)=\min_{\|u\|=1}\area(\proj_{u^\perp}K),\qquad
 C(\mathcal C;K)=\frac{\sum_i\area(B_i)}{\Amin(K)}.
\]
The half-area question asks whether every finite cylinder cover has $C\geq1/2$.
It is related to Bang's plank theorem \cite{bang}: the total width of a plank cover is at least the body's minimum width. The classical two-cylinder tetrahedral example has $C=1/2$; its attribution to Bang is recorded in \cite[Introduction]{bezdek-litvak}.
The distinct directionwise cost is
\[
 R(\mathcal C;K)=\sum_i\frac{\area(B_i)}{\area(\proj_{u_i^\perp}K)}\leq C(\mathcal C;K).
\]
Bezdek and Litvak proved $R\geq1/3$ in dimension three, and $R\geq1$ for ellipsoids \cite[Theorem 3.1]{bezdek-litvak}. Bezdek and Khan formulated the proposed bound $R\geq1/2$ as the 1-Codimensional Cylinder Covering Conjecture \cite[Definition 3 and Conjecture 4.13]{bezdek-khan}.

OpenAI \cite[Theorem 1.1]{angular} constructed finite triangular-cylinder covers of a regular tetrahedron with
\begin{equation}\label{eq:prior}
 C=\tfrac12-\tfrac{13}{6000}\varepsilon^2+E,\qquad
 |E|\leq2\varepsilon^4,\qquad 0<\varepsilon\leq\tfrac1{2000},
\end{equation}
using $2\lceil2/\varepsilon^2\rceil$ cylinders. At $\varepsilon=1/2000$ this gives $16\,000\,000$ cylinders and guaranteed saving
$13/24\,000\,000\,000-1/8\,000\,000\,000\,000>5.4154\times10^{-10}$.
The companion preprints develop ruled-set approximation \cite{ruled}, slope-field perturbations \cite{slope}, and triangular approximation of radial sweeps \cite{radial}.
Our contribution is a concrete, exactly certified finite-tilt instance within the angular-sector framework, with optimized rational cutoffs and a substantially larger explicit saving.

\begin{theorem}\label{thm:main}
Every regular tetrahedron of positive edge length admits a cover by $4096$ cylinders with compact nondegenerate triangular perpendicular bases for which
\begin{equation}\label{eq:bound}
 0.499613830783714148\ \leq\ C\ <\ 0.499613830783714149.
\end{equation}
In particular, $1/2-C>0.000386169216285851$ and $R<1/2$.
\end{theorem}
The data and certificate at the revision specified in Section~\ref{sec:data} are part of the explicit construction. The proof below reduces the theorem to finitely many rational identities and inequalities verified by the accompanying checkers. Similarities preserve $C$, so one scale suffices.

\section{The construction}
Use rational coordinates $(x,y,t)$ for the physical point $(x,y,\sqrt2t)$, with metric $dx^2+dy^2+2dt^2$. Set
\begin{equation}\label{eq:K}
 K=\{(x,y,t): |x|\leq1-t,\ |y|\leq t\}.
\end{equation}
Its vertices are $(\pm1,0,0)$ and $(0,\pm1,1)$ in these coordinates; all physical edges have length $2$.
For a physical unit vector $u$, summing the absolute scalar products with the four facet area vectors and dividing by two gives
\[
 \area(\proj_{u^\perp}K)
 =\max(\sqrt2|u_x|,|u_z|)+\max(\sqrt2|u_y|,|u_z|).
\]
Indeed those area vectors are $(0,\pm\sqrt2,-1)$ and $(\pm\sqrt2,0,1)$.
Writing $U=\max(|u_x|,|u_z|/\sqrt2)$ and $V=\max(|u_y|,|u_z|/\sqrt2)$, we have $(U+V)^2\geq u_x^2+u_y^2+u_z^2=1$. Equality is attained along the $x$ axis, so $\Amin(K)=\sqrt2$.

Put
\begin{equation}\label{eq:parameters}
 n=2048,\quad \tau=\frac9{20},\quad q_j=-1+\frac{2j}{n}\ (0\leq j\leq n),\quad
 \phi(q)=\frac{1-q^2}{4}\left(1-\frac{q^2}{200}+\frac{27q^4}{1250}\right).
\end{equation}
For $l=q_j$, $r=q_{j+1}$, define the secant parameters
\[
 \alpha_j=\frac{r\phi(l)-l\phi(r)}{r-l},\qquad
 \beta_j=\frac{\phi(l)-\phi(r)}{r-l}.
\]
The positive rational node radii $R_j$, satisfying $R_j=R_{n-j}$, are specified in \texttt{cover.json}. They are recovered from the $t$ coordinates of the nonzero vertices in the lower family. Adjacent triangles share the same node radius. Define
\begin{align*}
 P_j&=\conv\{(0,0,0),(0,q_jR_j,R_j),(0,q_{j+1}R_{j+1},R_{j+1})\},\\
 Q_j&=\conv\{(0,0,1),(q_jR_j,0,1-R_j),(q_{j+1}R_{j+1},0,1-R_{j+1})\},\\
 v_j&=(1,\tau\alpha_j,\tau\beta_j),\qquad
 w_j=(-\tau\alpha_j,1,\tau\beta_j).
\end{align*}
Our cylinders are $L_j=P_j+\R v_j$ and $U_j=Q_j+\R w_j$, for $0\leq j<n$. The axis vectors need not be unit: normalizing them leaves their real spans unchanged. The intercept triangles are oblique; the charged bases are their orthogonal projections perpendicular to their axes. Projection preserves the cylinder as a set and gives compact nondegenerate triangles.

An ordinary Euclidean rational export is obtained by the similarity
\begin{equation}\label{eq:similarity}
 F(x,y,t)=(x+y,x-y,2t-1).
\end{equation}
It multiplies physical squared lengths and areas by $2$. The exported tetrahedron has vertices $(1,1,-1)$, $(-1,-1,-1)$, $(1,-1,1)$, $(-1,1,1)$ and minimum projection area $2\sqrt2$. All its axes, intercept vertices and perpendicular vertices are rational. For each exported axis $a$, the latter are computed as $p-a(p\cdot a)/(a\cdot a)$. The file \texttt{cover\_euclidean.json} lists them explicitly.

\section{Why the certificate proves coverage}
\subsection{Angular selection}
For $L_j$, writing $a=\tau\alpha_j$, $b=\tau\beta_j$, projection along the axis to $x=0$ sends a point to $(0,y_0,t_0)=(0,y-ax,t-bx)$. Its angular conditions are
$l t_0\leq y_0\leq r t_0$. They imply $t_0\geq0$ because $l<r$.
The side planes can therefore be written
\[
 y=q_jt+\tau\phi(q_j)x,\qquad
 y=q_{j+1}t+\tau\phi(q_{j+1})x,
\]
since $\alpha_j-q_j\beta_j=\phi(q_j)$ at both endpoints.
For a point of $K$, the sequence of right-hand boundary heights starts at $-t\leq y$ and ends at $t\geq y$. Select the first subsequent height at least $y$; this brackets $y$ by adjacent heights and selects a lower angular wedge. This finite first-crossing argument does not require monotonicity of the heights.
For the upper family the corresponding heights are
$q_j(1-t)-\tau\phi(q_j)y$; they bracket $x$ between $-(1-t)$ and $1-t$ and select an upper wedge in the same way.

\subsection{Radial exclusion}
For any intercept triangle with ordered vertices $p_0,p_1,p_2$ and axis $v$, form the three normals
$(p_j-p_i)\times v$, one for each edge, orienting each so the remaining vertex satisfies its inequality strictly. Nonzero scalar products at those vertices prove transversality. The resulting three inequalities describe exactly the triangular cylinder: two angular side faces and one radial face. All coefficients are rational; no Euclidean square roots are required for set membership.

For an angular pair $(j,k)$ let its lower and upper radial membership inequalities be $a_L\cdot p\leq b_L$ and $a_U\cdot p\leq b_U$ (each normalized by a positive rational factor). Form a system in $z=(x,y,t,\delta)$ consisting of the four inequalities defining $K$, the four angular inequalities, and
\begin{equation}\label{eq:radial}
 -a_L\cdot p+\delta\leq-b_L,\qquad
 -a_U\cdot p+\delta\leq-b_U.
\end{equation}
Write these ten inequalities as $Az\leq d$. If a point belongs to both selected wedges but neither cylinder, both radial faces fail strictly. Taking $\delta$ to be the smaller positive failure gives a feasible $z$ with $\delta>0$.

For each checked pair the certificate specifies at most four row indices. The checker solves for the supported multipliers $\lambda$ exactly and verifies
\begin{equation}\label{eq:dual}
 \lambda\geq0,\qquad \lambda^{T}A=(0,0,0,1),\qquad \lambda^{T}d\leq0.
\end{equation}
Thus every feasible point satisfies $\delta=\lambda^TAz\leq\lambda^Td\leq0$, excluding simultaneous strict failure. This argument is elementary weak duality and does not assume a numerical optimizer is correct.

The isometry $S(x,y,t)=(-y,x,1-t)$ maps $L_j$ to $U_{n-1-j}$ and $U_j$ to $L_j$; the checker verifies the vertex sets and parallel axes exactly. Hence the pair transformation is $(j,k)\mapsto(k,n-1-j)$. Its orbits have size four: a fixed point of its square would require $j=n-1-j$, impossible for even $n$. The checker verifies one representative of each orbit and completeness of the representative list. There are $n^2=4\,194\,304$ pairs and $n^2/4=1\,048\,576$ certificates. The final artifact uses only witnesses of the form \eqref{eq:dual}.

Every point of $K$ has a wedge in each family. If uncovered, it would contradict the corresponding dual bound. This proves coverage of the whole closed tetrahedron, with no exception for boundary points.

\section{Area and computer verification}\label{sec:verification}
For rational coordinate edge vectors $e,f$ of an intercept triangle and rational axis $v$, the normalized perpendicular area is
\begin{equation}\label{eq:area}
 \frac{\area(B)}{\sqrt2}
 =\frac{|\det(e,f,v)|}{2\sqrt{v_x^2+v_y^2+2v_t^2}}.
\end{equation}
This follows by transforming to physical coordinates and taking the scalar product of the triangle's area vector with the unit axis. In the two symmetric families it gives
\begin{equation}\label{eq:sum}
 C=\sum_{j=0}^{n-1}\frac{(2/n)R_jR_{j+1}}
 {\sqrt{1+\tau^2(\alpha_j^2+2\beta_j^2)}}.
\end{equation}
The primary checker encloses each reciprocal square root by rational numbers $k/10^{30}$ and $(k+1)/10^{30}$, using integer square roots and checking the bounding inequalities exactly. Summing rational bounds proves \eqref{eq:bound}. It also verifies the Euclidean export, perpendicularity, equality of intercept and projected cylinders, and exact agreement of squared normalized areas. SHA-256 checks bind the certificate and export to the cover file.

\paragraph{Two verification methods.}
The standard-library checker \texttt{verify.py} reconstructs the halfspaces by cross products, checks angular matching and the symmetry, and verifies all dual witnesses using \texttt{fractions.Fraction}. The separately developed checker in \texttt{independent\_check/} uses FLINT rationals and does not read the dual certificate. It reconstructs the planes and checks angular selection, then clips $K$ by both angular wedges and both closed radial-failure halfspaces for every one of the $4\,194\,304$ pairs, without a symmetry reduction. Each surviving failure polytope has dimension less than three (or is empty).

Discarding lower-dimensional pieces is sufficient: a point outside a finite union of closed cylinders has an open uncovered neighborhood. Even if the point is on $\partial K$, that neighborhood contains interior points of $K$. Avoiding the finitely many angular planes gives a point strictly inside both selected wedges and strictly outside both radial faces. Its pair failure polytope would then contain an open ball, contradicting the exact clipping result. The independent area routine computes each squared Euclidean base area as a rational cross-product norm and encloses the sum of square roots using Arb at $192$ bits.

\paragraph{Controls and reproduction.}
The primary controls check the exact two-cylinder cost $1/2$ and reject broken angular matching, a missing certificate record, invalid dual support, inward radial perturbation, and a corrupted perpendicular base. The independent controls exhibit a rational uncovered point after removing one cylinder or halving its intercept triangle about its tip. These are explicit holes in the modified covers, not just rejected sufficient certificates.
From the pinned repository, with Python and \texttt{python-flint} installed, run:
\begin{verbatim}
python verify.py cover.json certificate.json.gz \
    --euclidean cover_euclidean.json --output verification.json
python test_verifier.py
cd independent_check
python independent.py --areas-only
python cells.py --workers 1
python controls.py
\end{verbatim}
Assertions must remain enabled (do not use Python's \texttt{-O} option).
The rerun used Python 3.12.13, python-flint 0.9.0 (FLINT 3.6.0), and one computational worker on an Apple silicon Mac. The complete primary verification took 98.4 seconds, the independent area check took 0.34 seconds, and exhaustive independent coverage checking took 1142.9 seconds. These are elapsed times from the present rerun, including input loading; runtime depends on the machine.

Exact certificates and interval arithmetic establish the inequalities; floating-point search tolerances and coverage sampling play no role in verification.

\section{Remarks and limitations}
The rational radii originate in numerical optimization, but the theorem concerns only the shipped finite data. The tilt $\tau=9/20$ is fixed: the asymptotic error estimate \eqref{eq:prior} is not applied at this tilt. The angular compatibility mechanism comes from \cite{angular}; the result here is a quantitative explicit instance, not a new resolution of the underlying conjecture.
A saving of $10^{-3}$ was not achieved. Neither optimality of this cover nor minimality of its cylinder count is proved. No priority claim is made. The inequality $R\leq C$ transfers the strict half-bound failure to the directionwise formulation; affine invariance of $R$ does not preserve this numerical $C$ bound for arbitrary tetrahedra.

\section{Data availability}\label{sec:data}
The complete rational data, compressed certificate and both checker implementations are available at
\url{https://github.com/rpinho/tetrahedron-cylinder-cover}, revision
\nolinkurl{a73f6955cdd97b4184081e03581bb6cb6190c33b}.
The defining files are \texttt{cover.json}, \texttt{cover\_euclidean.json} and \texttt{certificate.json.gz}; the radii and all cylinder vertices and axes are thereby specified without rounding. The primary-source preprints cited below were checked at revision \nolinkurl{1581d4cbdd69a0faf34b2089614fe2a814316a6a} of \texttt{openai/math}, accessed 15 October 2026.

\section*{AI assistance}
The search, the exact certificates and the checkers were developed with AI coding assistants (OpenAI Codex and Claude) under the author's direction, and the text was drafted with AI assistance. The author directed the work and reviewed the construction and results but has not verified every step by hand; correctness rests on the exact certificates, which are checked by two independent exact-arithmetic verifiers in the linked repository.

\bibliographystyle{amsplain}
\bibliography{refs}
\end{document}