\documentclass[11pt,reqno]{amsart} \usepackage[T1]{fontenc} \usepackage{lmodern} \usepackage{amsmath,amssymb,amsthm,mathtools} \usepackage[a4paper,margin=1in]{geometry} \usepackage{booktabs,tabularx,array} \usepackage{microtype} \usepackage{xcolor} \usepackage[ colorlinks=true, linkcolor=blue, citecolor=blue, urlcolor=blue, bookmarksnumbered=true, pdfdisplaydoctitle=true ]{hyperref} \usepackage{enumitem} \usepackage{longtable} \setlength{\emergencystretch}{2em} \numberwithin{equation}{section} \newcommand{\one}{\mathbf 1} \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{\Q}{\mathbb Q} \newcommand{\Z}{\mathbb Z} \newcommand{\Vol}{\operatorname{Vol}_4} \newcommand{\conv}{\operatorname{conv}} \newcommand{\Ufour}{U_4^{(1)}} \newcommand{\KU}{K_U} \newcommand{\RM}{K_{\mathrm{RM}}} \newcommand{\Bfive}{\mathcal B_5} \newcommand{\PAMO}{P_{\mathrm{AMO}}^{(1)}} \newcommand{\Mfour}{M_4^{(1)}} \newcommand{\Tsep}{\frac{4437}{20000}} \title[Volume comparison for constant-width bodies]{Volume Computation and Comparison for Four-Dimensional Bodies of Constant Width} \author{Hangang Wang} \date{October 26, 2026. Preprint.} \subjclass[2020]{Primary 52A38; Secondary 52A20, 52-08} \keywords{Bodies of constant width, four-dimensional volume, certified comparison, interval arithmetic} \thanks{\textbf{Affiliations.} China University of Geosciences (Wuhan), China (home institution); University of Manitoba, Canada (visiting research institution; Mitacs Globalink Research Intern, 2026).} \thanks{\textbf{Acknowledgements.} Most of this work was completed during the author's 2026 Mitacs Globalink Research Internship at the University of Manitoba. The author gratefully acknowledges Mitacs for its support and thanks Professor Andriy Prymak for supervising the project and for his generous guidance in developing more effective research and learning methods.} \thanks{\textbf{AI assistance and manuscript preparation.} The research was conducted by the author under the supervision of Professor Andriy Prymak. The initial manuscript was primarily written by the author. AI tools subsequently assisted with the organization, revision, and editorial refinement of the final manuscript, as well as selected mathematical arguments, auxiliary checks, and code development. OpenAI's \emph{GPT-5.6 Sol, GPT-6 Sol, and Astra} were used for mathematical and computational assistance, while Claude provided limited editorial assistance with the \LaTeX{} manuscript. Codex assisted with final \LaTeX{} editing and source-file packaging. The author takes responsibility for the mathematical content and conclusions.} \thanks{\textbf{Human review and verification.} The author has reviewed, checked, and understood all parts of the manuscript, including the mathematical arguments, computational methods, and the validation logic supporting the certified numerical results. The scope of computational certificate checking and reproduction is documented in Appendix~\ref{app:repro} and the accompanying repository. This statement does not imply that every full-scale production computation was independently rerun, nor does it claim formal verification or independent peer review.} \hypersetup{pdftitle={Volume Computation and Comparison for Four-Dimensional Bodies of Constant Width},pdfauthor={Hangang Wang}} \begin{document} \begin{abstract} We compute and compare the volumes of explicit four-dimensional bodies of constant width one. The original five-entry comparison consists of the simplex-symmetric projection body $U_4$, the canonical raised Meissner pair, the canonical raise of $U_3$, the body $\mathcal B_5$, and $M_4$. We combine exact geometric formulas, numerical integration, interval enclosures and inscribed rational polytopes to obtain a certified strict ordering of their volumes. We also compare $U_4$ with the direct four-dimensional AMO peabody. The two raised Meissner bodies are proved noncongruent but exactly equal in volume. An introductory account explains why different constructions benefit from different computational methods, and distinguishes approximate volume estimates from inequalities certified by exact or outward-rounded arithmetic. \end{abstract} \maketitle \section{Introduction}\label{sec:introduction} A body has constant width one if the distance between its two parallel supporting hyperplanes is one in every direction. The Blaschke--Lebesgue problem asks how small its volume can be. This note concerns a finite comparison in dimension four: which of several explicit constructions has the smallest volume? It does not assert a global minimizer among all four-dimensional bodies of constant width. In dimension three, the minimum-volume problem remains open \cite[Section~14.2]{MMO}. The two classical, noncongruent Meissner bodies have the same width-one volume, approximately $0.419860046$, and are conjectured to minimize volume; see \cite[Section~8.3.3]{MMO} and \cite{KW}. The tetrahedrally symmetric body $U_3$ has slightly larger volume \cite{ABPR}. A recent preprint proves the universal lower bound $1651/4000=0.41275$ for width-one bodies \cite[Theorem~1.1]{Jiang2026}; this still leaves a gap to the Meissner volume. The five entries in the original comparison are the projection body $\Ufour$ \cite{ABPR}, the canonical raises of the two Meissner bodies \cite{KW,LRO} (counted as one volume class), the canonical raise $\KU$ of $U_3^{(1)}$ \cite{ABPR,LRO}, the body $\Bfive$ \cite{MRP}, and $\Mfour$ \cite{ABNPR}. The direct four-dimensional peabody $\PAMO$ \cite{AMO4} is included as an additional comparison. The two raised Meissner representatives are different bodies: we prove that they are noncongruent and nevertheless have exactly the same volume. All volumes below use width one; changing width by a factor $w$ changes four-dimensional volume by $w^4$. \subsection{Main results} We use the rational separator \begin{equation}\label{eq:T} T=\Tsep=0.22185. \end{equation} \begin{theorem}[Certified comparison]\label{thm:main-separator} For the width-one constructions defined in Section~\ref{sec:prelim}, \begin{equation}\label{eq:five-chain} \Vol(\Ufour)<\Vol(\RM)<\Vol(\KU)<\Vol(\Bfive)<\Vol(\Mfour), \end{equation} where $\Vol(\RM)=\Vol(K_F)=\Vol(K_V)$. Moreover, \begin{equation}\label{eq:main-separator} \Vol(\Ufour)0.2220978270$ & Certified inner fan \\ \bottomrule \end{tabularx} \end{table} The approximate AMO volume is $0.2244750148$, suggesting a position between Body~5 and $M_4$. We do not use that approximate placement in the certified chain. Nor does being the smallest in this finite list imply that $U_4$ minimizes volume among all constant-width bodies: its volume-decreasing deformations are the subject of a separate manuscript. \paragraph{Guide to the paper.} Section~\ref{sec:prelim} specifies the constructions. Sections~\ref{sec:U4} and~\ref{sec:RM} explain the $U_4$ integral and the raised Meissner pair. Section~\ref{sec:certificates} describes the certified endpoints and Section~\ref{sec:main-proof} assembles them. The appendices contain the angular calculations, the optional common-fan construction, membership certificates, and reproducibility information. \section{Preliminaries and the candidate bodies}\label{sec:prelim} \subsection{Support functions and constant width} Let $K\subset\R^n$ be a convex body. Its support function is \[ h_K(u)=\max_{x\in K}\langle x,u\rangle, \qquad u\in S^{n-1}. \] The width in direction $u$ is $h_K(u)+h_K(-u)$. Hence $K$ has constant width $w$ if \begin{equation}\label{eq:cw} h_K(u)+h_K(-u)=w \end{equation} for every $u\in S^{n-1}$. We use width one throughout. A width-$w$ body is the intersection of all radius-$w$ balls centered at its points, \begin{equation}\label{eq:ball-intersection} K=\bigcap_{a\in K}\overline B(a,w); \end{equation} see \cite[Theorem~6.1.4]{MMO}. This description is repeatedly used in the endpoint certificates below. \subsection{Canonical dimension raising} Let $H\subset\R^n$ be an affine hyperplane and let $K_0\subset H$ be a width-one body. For the canonical choice of the auxiliary set in the construction of Lachand--Robert and Oudet \cite[Theorem~4.1]{LRO}, define \begin{align} K_+(K_0)&=H_+\cap\bigcap_{q\in K_0}\overline B(q,1),\label{eq:Kplus}\\ K_-(K_0)&=H_-\cap\bigcap_{x\in K_+(K_0)}\overline B(x,1),\label{eq:Kminus} \end{align} and \begin{equation}\label{eq:raise} \mathcal R(K_0)=K_+(K_0)\cup K_-(K_0). \end{equation} Then $\mathcal R(K_0)$ has constant width one and \begin{equation}\label{eq:section} \mathcal R(K_0)\cap H=K_0. \end{equation} If $H=\R^{n-1}\times\{0\}$, the positive half has the graph description \begin{equation}\label{eq:height} K_+(K_0)=\{(y,s):y\in K_0,\ 0\le s\le(1-F_{K_0}(y)^2)^{1/2}\}, \qquad F_{K_0}(y)=\max_{q\in K_0}\|y-q\|. \end{equation} \subsection{The simplex-symmetric bodies \texorpdfstring{$M_n$}{Mn} and \texorpdfstring{$U_n$}{Un}} For $x\in\R^n$, let $x_+,x_-$ be its coordinatewise positive and negative parts. The width-two body of \cite{ABNPR} is \begin{equation}\label{eq:Mn} M_n^{(2)}= \left\{x:\ \|x_+\|^2+(\|x_-\|+\sqrt2)^2\le4\right\}. \end{equation} Let $H_n=\mathbf1^\perp\subset\R^{n+1}$ and let $P_n$ be the orthogonal projection onto $H_n$. The body \begin{equation}\label{eq:Un} U_n^{(2)}=P_n(M_{n+1}^{(2)}) \end{equation} has constant width two and the full symmetry group of a regular $n$-simplex \cite{ABPR}. We write \[ U_n^{(1)}=\frac12U_n^{(2)}, \qquad M_n^{(1)}=\frac12M_n^{(2)}. \] The other comparison bodies are denoted by \[ \KU=\mathcal R(U_3^{(1)}), \qquad \Bfive, \qquad \PAMO, \qquad \Mfour. \] Here $\Bfive$ is the width-one normalization of the body constructed in \cite{MRP}, and $\PAMO$ is the width-one normalization of the direct four-dimensional focal-quadric peabody of \cite{AMO4}. \section{The volume of \texorpdfstring{$U_4$}{U4}}\label{sec:U4} We record the analytic reduction used for the $U_4$ upper bound in Theorem~\ref{thm:main-separator}. Work first in width two. Let \[ H_4=\left\{u\in\mathbb R^5:\sum_{i=1}^5u_i=0\right\}, \qquad S(H_4)=H_4\cap S^4. \] For $u\in S(H_4)$ set \[ r(u)=\|u_+\|, \qquad s(u)=\|u_-\|, \qquad m(u)=\sum_{u_i>0}u_i. \] Since $\|u\|=1$, one has $r^2+s^2=1$. The support function of the width-two projection body is \begin{equation}\label{eq:U4-support} H(u)= \begin{cases} \sqrt2\,r(u),&r(u)\ge s(u),\\[0.2em] 2-\sqrt2\,s(u),&r(u)\le s(u). \end{cases} \end{equation} Let \[ D=\{u\in S(H_4):r(u)\ge s(u)\}. \] On a sign cell in $D$ with $k$ positive coordinates, put \[ B=\nabla^2_{S^3}(\sqrt2 r)+\sqrt2 r I. \] \begin{proposition}[Curvature-radius spectrum]\label{prop:U4-spectrum} For $k\ge2$, the eigenvalues of $B$ on the tangent space are \[ \underbrace{\alpha,\ldots,\alpha}_{k-2},\quad \beta_k, \quad\underbrace{0,\ldots,0}_{4-k}, \] where \begin{equation}\label{eq:alpha-beta} \alpha=\frac{\sqrt2}{r}, \qquad \beta_k=\frac{\sqrt2\bigl((5-k)r^2+m^2\bigr)}{5r^3}. \end{equation} For $k=1$, $B=0$. \end{proposition} \begin{proof} Let $P$ be the positive coordinate set and let $A_P$ be coordinate projection onto $P$ followed by orthogonal projection to $H_4$. The homogeneous first-branch support function is $F_P(x)=\sqrt2\langle A_Px,x\rangle^{1/2}$. Its Euclidean Hessian restricted to the tangent space is \[ \frac{\sqrt2}{r}\left(A_P-\frac{A_Pu\otimes A_Pu}{r^2}\right). \] The spectrum of $A_P$ on $H_4$ is \[ 1^{[k-1]},\qquad \frac{5-k}{5},\qquad 0^{[4-k]}. \] The zero-sum directions supported on $P$ and orthogonal to $u$ give $k-2$ copies of $\alpha$, while the projections of $\ker A_P$ onto $u^\perp$ give $4-k$ zero eigenvalues. Indeed the homogeneous Hessian annihilates both $\ker A_P$ and $u$, and $u\notin\ker A_P$, so projection onto $u^\perp$ is injective on this kernel. The remaining eigenvalue is determined by the trace and equals $\beta_k$ in \eqref{eq:alpha-beta}. \end{proof} If $u\in D$, then $k\le3$ almost everywhere. Indeed, if four coordinates were positive, the unique negative coordinate would have magnitude $m$ and hence $s=m>r$ in the interior of the sign cell. Thus $\det B=0$ almost everywhere on $D$. For a width-two body the antipodal curvature-radius operator is $2I-B$. Put \[ \Delta_k(u)=\det(2I-B(u)). \] Proposition~\ref{prop:U4-spectrum} gives \begin{equation}\label{eq:Deltas} \Delta_1=8, \qquad \Delta_2=4(2-\beta_2), \qquad \Delta_3=2(2-\alpha)(2-\beta_3). \end{equation} Pairing antipodal directions in the support-volume formula \cite[Section~5.1]{Schneider} and then scaling from width two to width one yields \begin{equation}\label{eq:U4-spherical} \Vol(\Ufour) =\frac1{64}\sum_{k=1}^3 \int_{D\cap\{\#\{u_i>0\}=k\}} (2-\sqrt2 r(u))\Delta_k(u)\,d\sigma(u). \end{equation} The coefficient $1/64=(1/4)\,2^{-4}$ combines the four-dimensional support-volume factor with the change from width two to width one. The integral can be reduced to one one-dimensional and two two-dimensional integrals. On a fixed sign cell with $k$ positive and $l=5-k$ negative coordinates, write \[ u=(p,-q),\qquad p=\frac{m}{k}\mathbf1_k+\xi, \qquad q=\frac{m}{l}\mathbf1_l+\eta, \] with $\xi\perp\mathbf1_k$ and $\eta\perp\mathbf1_l$. Put \[ z=m\sqrt{\frac5{kl}}, \qquad x=\|\xi\|, \qquad y=\|\eta\|. \] The variable $z$ measures the common mean component of the two coordinate groups; $x,y$ measure fluctuations within them. Thus $\theta$ below allocates the remaining squared norm between these fluctuation spaces. Then $z^2+x^2+y^2=1$. For $k=2,3$ write \[ x=\sqrt{1-z^2}\cos\theta, \qquad y=\sqrt{1-z^2}\sin\theta, \qquad 0\le\theta\le\frac\pi2. \] The remaining angular integrations are positivity measures \[ A_j(t)=\sigma_{j-2}\{\omega\in S(\mathbf1_j^\perp):\omega_i\ge-t\ \text{for all }i\}. \] With \[ m=z\sqrt{\frac{k(5-k)}5}, \qquad r^2=\frac{5-k}{5}z^2+(1-z^2)\cos^2\theta, \] the exact reduction is \begin{equation}\label{eq:U4-I123} \Vol(\Ufour)=I_1+I_2+I_3, \end{equation} where \begin{equation}\label{eq:I1} I_1= \frac5{64}\int_{\sqrt{5/8}}^1 8\left(2-\frac{2\sqrt2}{\sqrt5}z\right) \sqrt{1-z^2}\, A_4\!\left(\frac{z}{2\sqrt5\sqrt{1-z^2}}\right)\,dz, \end{equation} and, for $k=2,3$, \begin{equation}\label{eq:Ik} I_k=\frac{\binom5k}{64} \int_0^1\int_0^{\pi/2} \mathbf1_{\{r^2\ge1/2\}} x^{k-2}y^{3-k} A_k\!\left(\frac{m}{kx}\right) A_{5-k}\!\left(\frac{m}{(5-k)y}\right) (2-\sqrt2r)\Delta_k(r,m)\,d\theta\,dz. \end{equation} The piecewise formulas for $A_2,A_3,A_4$ in Appendix~\ref{app:angular-v3} produce finitely many algebraic subdomains. Splitting along those boundaries before interval evaluation removes the discontinuous indicator from the validated quadrature. Directed Arb arithmetic on the resulting finite family gives the enclosure \eqref{eq:U4-current}. The analytic reduction \eqref{eq:U4-I123} is exact; interval arithmetic enters only in the final evaluation. \section{The two canonical raised Meissner bodies}\label{sec:RM} Let $A,B,C,D$ be the vertices of a centered regular tetrahedron of edge length one. For the coordinate witnesses below take \[ A=\tfrac1{2\sqrt2}(1,1,1),\quad B=\tfrac1{2\sqrt2}(1,-1,-1),\quad C=\tfrac1{2\sqrt2}(-1,1,-1),\quad D=\tfrac1{2\sqrt2}(-1,-1,1). \] Their Gram relations are \begin{equation}\label{eq:tet-gram} X\cdot Y= \begin{cases} 3/8,&X=Y,\\ -1/8,&X\ne Y, \end{cases} \qquad X,Y\in\{A,B,C,D\}. \end{equation} Let $\Gamma_{XY}$ be the short circular edge of the Reuleaux tetrahedron joining $X$ and $Y$. The two Meissner types may be described by preserving respectively the three arcs \begin{equation}\label{eq:EF-EV} E_F=\{AB,AC,AD\}, \qquad E_V=\{BC,BD,CD\}. \end{equation} Their canonical raises are $K_F=\mathcal R(M_F)$ and $K_V=\mathcal R(M_V)$. \subsection{Noncongruence}\label{subsec:RM-noncongruence} The section identity \eqref{eq:section} shows at once that $K_F$ and $K_V$ are different subsets in the fixed raising coordinates, because $M_F\ne M_V$. To rule out an arbitrary ambient Euclidean congruence, we use a finite rigidity argument. Set \begin{equation}\label{eq:E} E=(0,0,0,\sqrt{5/8}). \end{equation} The five points $A,B,C,D,E$ form a regular four-simplex of edge length one contained in both $K_F$ and $K_V$. Let \[ O=E/5. \] Its circumradius is $\sqrt{2/5}$. \begin{lemma}[Circumsphere rigidity]\label{lem:circum-rigidity} For $K\in\{K_F,K_V\}$ the unique minimum circumball is \[ \overline B_4(O,\sqrt{2/5}), \] and \begin{equation}\label{eq:contact} K\cap\partial B_4(O,\sqrt{2/5})=\{A,B,C,D,E\}. \end{equation} \end{lemma} \begin{proof} Both raised bodies have diameter one. Jung's theorem in dimension four gives radius at most $\sqrt{2/5}$, while the contained regular four-simplex already has that circumradius. The center is unique. Indeed, if $P_1,\dots,P_5$ are the simplex vertices, then \[ \frac15\sum_{i=1}^5\|P_i-c\|^2=\frac25+\|c-O\|^2. \] Hence a radius-$\sqrt{2/5}$ ball containing the simplex is centered at $O$. Write $v_i=P_i-O$. Then \[ \sum_i v_i=0, \qquad \|v_i\|^2=\frac25, \qquad v_i\cdot v_j=-\frac1{10}\quad(i\ne j), \] and \[ \sum_i v_iv_i^{\mathsf T}=\frac12I_4. \] Let $x\in K$ lie on the circumsphere and put $w=x-O$. Since every $P_i$ belongs to the diameter-one body $K$, \[ \|w-v_i\|\le1, \] so $a_i:=w\cdot v_i\ge-1/10$. Moreover \[ \sum_i a_i=0, \qquad \sum_i a_i^2=\frac12\|w\|^2=\frac15. \] With $b_i=a_i+1/10\ge0$, one has \[ \sum_i b_i=\frac12, \qquad \sum_i b_i^2=\frac14. \] Thus \[ 0=(\sum_i b_i)^2-\sum_i b_i^2=2\sum_{i1, \qquad \Delta_1=\frac98+\frac{3\sqrt5-\sqrt{30}-\sqrt6}{16}>1. \] The certificates are \begin{center} \begin{tabular}{c|c|c|c} \toprule $\rho$ & $p_\rho\in K_F$ & $q_\rho\in K_V$ & $\|T_\rho(p_\rho)-q_\rho\|^2$\\ \midrule $\mathrm{id}$ & $P_{AB}$ & $P_{CD}$ & $\Delta_0$\\ $(DE)$ & $P_{AB}$ & $U_{DC}$ & $\Delta_1$\\ $(AB)$ & $P_{AB}$ & $P_{CD}$ & $\Delta_0$\\ $(AB)(DE)$ & $U_{DB}$ & $P_{BC}$ & $\Delta_1$\\ $(ABCDE)$ & $U_{DB}$ & $P_{BD}$ & $\Delta_1$\\ $(AEDCB)$ & $U_{AB}$ & $P_{BC}$ & $\Delta_1$\\ $(AE)$ & $U_{AC}$ & $P_{BD}$ & $\Delta_1$\\ \bottomrule \end{tabular} \end{center} If $T_\rho(K_F)=K_V$, then both $T_\rho(p_\rho)$ and $q_\rho$ would lie in the diameter-one body $K_V$, contradicting the last column. We have proved: \begin{theorem}\label{thm:RM-noncong} The two canonical raised Meissner bodies are not congruent: \[ K_F\not\cong K_V. \] \end{theorem} \subsection{Equality of volume: the positive half}\label{subsec:RM-positive} For $0\le\rho\le1$ define the common four-vertex lens \begin{equation}\label{eq:Qrho} Q_\rho=\bigcap_{Z\in\{A,B,C,D\}}B_3(Z,\rho). \end{equation} For a tetrahedral edge $XY$, define the arc defect \begin{equation}\label{eq:Dxy} D_{XY}(\rho)=\{x\in Q_\rho:\ \max_{p\in\Gamma_{XY}}\|x-p\|>\rho\}. \end{equation} If $E$ is a set of edges, put \begin{equation}\label{eq:SErho} S_E(\rho)=Q_\rho\setminus\bigcup_{e\in E}D_e(\rho). \end{equation} By \eqref{eq:height}, the horizontal slice at height $s\ge0$ of the canonical raise is \begin{equation}\label{eq:slice-positive} K_{M,+}\cap\{x_4=s\} =S_{E_M}(\sqrt{1-s^2})\times\{s\}, \qquad M\in\{M_F,M_V\}. \end{equation} Write a point in barycentric coordinates \[ x=\lambda_AA+\lambda_BB+\lambda_CC+\lambda_DD, \qquad \lambda_A+\lambda_B+\lambda_C+\lambda_D=1. \] From \eqref{eq:tet-gram}, \begin{equation}\label{eq:x-X} \|x-X\|^2 =\frac12\sum_Z\lambda_Z^2+\frac12-\lambda_X. \end{equation} Define \begin{equation}\label{eq:crho} c_\rho(x)=\frac12\sum_Z\lambda_Z^2+\frac12-\rho^2. \end{equation} Then \begin{equation}\label{eq:Q-bary} x\in Q_\rho\quad\Longleftrightarrow\quad \lambda_X\ge c_\rho(x)\quad\text{for every }X. \end{equation} \begin{lemma}\label{lem:defect-negative} If $x\in D_{XY}(\rho)$, then $\lambda_X<0$ and $\lambda_Y<0$. \end{lemma} \begin{proof} By symmetry take $XY=AB$. A point $p\in\Gamma_{AB}$ has barycentric coordinates with $\mu_C=\mu_D=-a$, $a\ge0$. Put \[ \theta_A=\mu_A+a, \qquad \theta_B=\mu_B+a. \] The circular parametrization gives \[ 0\le\theta_A,\theta_B\le1, \qquad \theta_A+\theta_B=1+4a. \] Using the Gram relations one obtains \begin{equation}\label{eq:gap} \rho^2-\|x-p\|^2 =\theta_A\lambda_A+\theta_B\lambda_B-c_\rho(x). \end{equation} If $\lambda_A\ge0$, the right side is nonnegative in all three possible cases $\lambda_B\ge0,c_\rho\le0$, $\lambda_B\ge0,c_\rho>0$, and $\lambda_B<0$, using respectively positivity, \eqref{eq:Q-bary}, and $c_\rho\le\lambda_B$. Thus no $AB$ arc constraint can fail. The same argument with $A,B$ interchanged proves the claim. \end{proof} \begin{lemma}\label{lem:two-negative} If $x\in Q_\rho$ with $0\le\rho\le1$, at most two barycentric coordinates of $x$ are negative. \end{lemma} \begin{proof} If, say, $\lambda_A,\lambda_B,\lambda_C<0$, then $\lambda_D>1$ and $\sum_Z\lambda_Z^2>1$. Hence $c_\rho(x)>1-\rho^2\ge0$, contradicting \eqref{eq:Q-bary} for a negative coordinate. \end{proof} \begin{corollary}\label{cor:defects-disjoint} The six sets $D_e(\rho)$ are pairwise disjoint. \end{corollary} \begin{proof} For adjacent edges, Lemma~\ref{lem:defect-negative} would force at least three negative barycentric coordinates; for opposite edges it would force all four. Both contradict Lemma~\ref{lem:two-negative}. \end{proof} Define \[ C(\rho)=Q_\rho\setminus\bigcup_eD_e(\rho), \] where the union is over all six tetrahedral edges. Then \begin{align} S_{E_F}(\rho)&=C(\rho)\,\dot\cup\,D_{BC}(\rho)\,\dot\cup\,D_{BD}(\rho)\,\dot\cup\,D_{CD}(\rho),\label{eq:SF}\\ S_{E_V}(\rho)&=C(\rho)\,\dot\cup\,D_{AB}(\rho)\,\dot\cup\,D_{AC}(\rho)\,\dot\cup\,D_{AD}(\rho).\label{eq:SV} \end{align} The tetrahedral symmetry group is transitive on the six edges and preserves $Q_\rho$, so all six defects have equal volume. Equations \eqref{eq:SF}--\eqref{eq:SV} therefore give equal three-dimensional slice volumes for every $s$. Fubini yields \begin{equation}\label{eq:positive-equality} \Vol(K_{F,+})=\Vol(K_{V,+}). \end{equation} \subsection{Equality of volume: the negative half}\label{subsec:RM-negative} Lift the positive slice decomposition to four-dimensional defect towers: \[ C^+=\{(x,s):0\le s\le1,\ x\in C(\sqrt{1-s^2})\}, \] \[ D_e^+=\{(x,s):0\le s\le1,\ x\in D_e(\sqrt{1-s^2})\}. \] Thus, up to null boundaries, \[ K_{F,+}=C^+\,\dot\cup\,D_{BC}^+\,\dot\cup\,D_{BD}^+\,\dot\cup\,D_{CD}^+, \] \[ K_{V,+}=C^+\,\dot\cup\,D_{AB}^+\,\dot\cup\,D_{AC}^+\,\dot\cup\,D_{AD}^+. \] For $S\subset\R^4$ put \[ \mathcal B(S)=\bigcap_{x\in S}B_4(x,1), \] and define \begin{equation}\label{eq:L0} L_0=\{x_4\le0\}\cap\mathcal B(C^+), \end{equation} \begin{equation}\label{eq:Fe} F_e=L_0\setminus\mathcal B(D_e^+). \end{equation} Then \begin{align} K_{F,-}&=L_0\setminus(F_{BC}\cup F_{BD}\cup F_{CD}),\label{eq:KFminus}\\ K_{V,-}&=L_0\setminus(F_{AB}\cup F_{AC}\cup F_{AD}).\label{eq:KVminus} \end{align} We prove that the six forbidden regions are pairwise disjoint. The quantity $\mu_{XY}$ below is the minimum of a barycentric linear expression along the retained arc. The function $U_R$ is a squared height: it describes the top of a vertical fibre of the relevant tower, where distance from a point in the negative half is largest. For an edge $XY$ and negative numbers $\xi,\zeta$, set \begin{equation}\label{eq:mu} \mu_{XY}(\xi,\zeta) =-\frac12\left(\xi+\zeta+\sqrt{9\xi^2+6\xi\zeta+9\zeta^2}\right). \end{equation} The arc-gap minimization used in the positive-half proof gives \begin{equation}\label{eq:min-gap} \min_{p\in\Gamma_{XY}}(\theta_X(p)\lambda_X+\theta_Y(p)\lambda_Y) =\mu_{XY}(\lambda_X,\lambda_Y) <\min\{\lambda_X,\lambda_Y\} \end{equation} when $\lambda_X,\lambda_Y<0$. For a barycentric vector $\lambda$ of sum one and an endpoint $R\in\{X,Y\}$ of minimal coordinate, define \begin{equation}\label{eq:UR} U_R(\lambda)=\frac12-\frac12\sum_Z\lambda_Z^2+\lambda_R =1-\frac12\|\lambda-e_R\|^2. \end{equation} If $U_R(\lambda)\ge0$, the corresponding point \[ p_R(\lambda)=(x(\lambda),\sqrt{U_R(\lambda)}) \] is the top of the relevant defect tower branch. For a lower point, distance to a fixed vertical fibre increases with height, so every lower violation is witnessed at such a top. \begin{lemma}[Opposite-edge sign]\label{lem:opposite-edge} If $z=(y(\eta),-\tau)\in F_{XY}$ and $ZW$ is the edge opposite to $XY$, then \[ \eta_Z<0,\qquad \eta_W<0. \] \end{lemma} \begin{proof} We prove the contrapositive for $Z$. Assume $\eta_Z\ge0$. Consider a defect-top branch with \[ \lambda_X\le\lambda_Y<0, \qquad \lambda_X=-a, \quad \lambda_Y=-b, \quad a\ge b>0, \] and active endpoint $R=X$. The condition $U_X(\lambda)\ge0$ implies the reserve inequalities \begin{equation}\label{eq:reserve} \lambda_Z>3b, \qquad \lambda_W>3b. \end{equation} Indeed, if $\lambda_Z\le3b$, writing $a=b+u$ and $\lambda_Z=3b-v$ with $u,v\ge0$, the sum-one condition gives $\lambda_W=1+u-b+v$ and direct expansion yields $\|\lambda-e_X\|^2>2$, contradicting $U_X\ge0$. Set \[ d_Z=e_X+e_Y-3e_Z+e_W, \qquad \lambda(t)=\lambda+td_Z, \qquad 0\le t\le b. \] The sum of coordinates and the active $X$-branch are preserved. By \eqref{eq:reserve}, the opposite coordinates remain nonnegative. At $t=b$ one has $\lambda_Y(b)=0$, hence the terminal top lies in the common core $C^+$ by Lemma~\ref{lem:defect-negative}. Moreover \[ \frac{d}{dt}U_X(\lambda(t))=4\lambda_Z(t)>0. \] For the lower point $z$, the squared distance to the branch top is \[ \Psi_X(\lambda;z) =\frac12\sum_R\eta_R^2+\tau^2+\frac12+(e_X-\eta)\cdot\lambda +2\tau\sqrt{U_X(\lambda)}. \] Since $(e_X-\eta)\cdot d_Z=4\eta_Z\ge0$, the distance does not decrease as the path moves toward the terminal core top. The terminal top belongs to $C^+$ and $z\in L_0$, so its distance from $z$ is at most one. Therefore the original top is also at distance at most one, contradicting $z\in F_{XY}$. The same argument applies to $W$ and to the branch with active endpoint $Y$. \end{proof} \begin{corollary}\label{cor:Fe-disjoint} The six forbidden regions $F_e$ are pairwise disjoint. \end{corollary} \begin{proof} A point of $L_0$ projects to a point of a lens $Q_{\sqrt{1-\tau^2}}$, so Lemma~\ref{lem:two-negative} allows at most two negative barycentric coordinates. If two forbidden regions correspond to adjacent edges, Lemma~\ref{lem:opposite-edge} forces at least three negative coordinates; if they correspond to opposite edges, it forces all four. Both cases are impossible. \end{proof} The tetrahedral group preserves $C^+$ and $L_0$ and acts transitively on the six edges. Hence the six forbidden regions have equal four-dimensional volume. Equations \eqref{eq:KFminus}--\eqref{eq:KVminus} and Corollary~\ref{cor:Fe-disjoint} give \begin{equation}\label{eq:negative-equality} \Vol(K_{F,-})=\Vol(K_{V,-}). \end{equation} Combining \eqref{eq:positive-equality} and \eqref{eq:negative-equality} proves the second half of Theorem~\ref{thm:RM-pair-intro}. \begin{theorem}\label{thm:RM-equal} The two canonical raised Meissner bodies have exactly equal four-dimensional volume: \[ \Vol(K_F)=\Vol(K_V). \] Together with Theorem~\ref{thm:RM-noncong}, they are noncongruent equal-volume bodies of constant width one. \end{theorem} \section{Validated volume certificates}\label{sec:certificates} \subsection{Upper bound for \texorpdfstring{$U_4$}{U4}} For the separator theorem, the available uniform-grid Arb record already gives the sufficient enclosure \begin{equation}\label{eq:U4-bound} 0.2218338853720453<\Vol(\Ufour)<0.2218382994641744T. \end{equation} Qhull supplies a candidate tetrahedron list. Membership is checked separately against complete circular arcs and negative-half inner balls. The boundary audit checks distinct, nondegenerate tetrahedra; incidence two at every triangle; a connected facet-dual graph; cyclic edge links; and connected vertex links of Euler characteristic two. Together these checks give a closed connected PL three-manifold, rather than merely a list of positive determinants. Integer orientation tests verify local convexity at all $814553$ edges; the recorded run has no unsupported planar edge links. The finite realization is bounded, so Rybnikov's local-to-global theorem \cite[Theorem~8]{Rybnikov} identifies it as a convex boundary. An exact positive barycentric witness places the origin inside, and determinant summation gives \eqref{eq:RM-lower}. An independent validated outer computation gives \begin{equation}\label{eq:RM-upper} \Vol(\RM)\le0.222595179568435. \end{equation} \subsection{How the raised-body upper bounds are certified} For a unit ball centred at $c$ and containing the origin, the radial upper root in a unit direction $u$ is \[ R_c(u)=c\cdot u+\sqrt{(c\cdot u)^2+1-\|c\|^2}. \] If the raised body is contained in that ball, its radial function is at most $R_c$. On the positive half, centres come from the complete defining arcs; on the negative half they are certified points of the positive half. Choosing one valid centre on each parameter box is sufficient. Taking a finite set of constraints enlarges the intersection, so it yields an upper bound even when the selected centre is not the true active centre. In a spatial symmetry chamber use \[ D=1+a^2(1+s^2),\qquad u_\pm=\left(\frac{2q(1,a,as)}{(1+q^2)\sqrt D}, \ \pm\frac{1-q^2}{1+q^2}\right), \] with $(a,s,q)\in[0,1]\times[-1,1]\times[0,1]$. Here $v=(1,a,as)/\sqrt D$ is a spatial unit direction and $q=\tan(\phi/2)$, where $u_\pm=(\sin\phi\,v,\pm\cos\phi)$. The area factors are \[ d\sigma_2(v)=\frac{a}{D^{3/2}}\,da\,ds,\qquad \sin^2\phi\,d\phi=\frac{8q^2}{(1+q^2)^3}\,dq. \] The first follows by differentiating $v$ and taking its cross product; the second follows from the half-angle identities. The box integrand has the form \[ F=\frac{\kappa R_c(u_\pm)^4aq^2}{D^{3/2}(1+q^2)^3}. \] Here $\kappa=48$ for the $24$ spatial chamber images of $K_U$. For the raised Meissner body four signed chamber representatives are integrated separately, each with $\kappa=12$ for six permutation images. Thus $\kappa=24\cdot8/4=48$ or $6\cdot8/4=12$, respectively. On a box with side lengths $\ell_a,\ell_s,\ell_q$, two-point Gauss quadrature in each variable gives \[ \int_B F\le Q_B^\uparrow+ \frac{\ell_s\ell_q\ell_a^5M_a+ \ell_a\ell_q\ell_s^5M_s+\ell_a\ell_s\ell_q^5M_q}{4320}, \qquad M_j\ge\sup_B|\partial_j^4F|. \] The constant is the one-dimensional two-point Gauss remainder constant. Telescoping the three integrations and using positive quadrature weights gives the displayed estimate. Interval Taylor arithmetic bounds the fourth derivatives on the whole box. Nodes, square roots, centres, Jacobians, weights and additions are enclosed outwards; enclosing only the final sum would not suffice. The dyadic box upper endpoints are accumulated with integer arithmetic, and the box tree is checked to cover its domain. The recorded hardened upper sums are \[ \begin{aligned} U_F&=\frac{538202119804071468248419}{2417851639229258349412352} <0.222595179568435,\\ U_U&=\frac{2155448166585847858684765}{9671406556917033397649408} <0.222868116845350. \end{aligned} \] These are the endpoints used in the present comparison, replacing the earlier displayed upper estimates in the working record. \subsection{Raised \texorpdfstring{$U_3$}{U3} and Body 5} The hardened comparison certificate for the canonical raise of $U_3$ gives \begin{equation}\label{eq:KU-bounds} 0.222628250<\Vol(\KU)\le0.222868116845350. \end{equation} The independent directed-rounding certificate for Body 5 gives, with endpoints rounded outwards, \begin{equation}\label{eq:B5-bounds} 0.222877646477730<\Vol(\Bfive)<0.222991176426990. \end{equation} Consequently \begin{equation}\label{eq:RM-KU-B5} \Vol(\RM)<\Vol(\KU)<\Vol(\Bfive). \end{equation} Indeed, the adjacent certified separations are \[ 0.222595179568435 <0.222628250 \] and \[ 0.222868116845350 <0.222877646477730. \] \paragraph{Geometry behind the other two enclosures.} The raised-$U_3$ lower certificate uses a cap-and-chamber simplicial fan at mesh $n=80$, with $800442$ endpoint records per half. Positive-half endpoints satisfy all six elliptical arc constraints, including the interval interpolation error between tested arc parameters. Negative-half endpoints satisfy rigorous witness-ball inequalities. Integer ray determinants and rational radii then give a lower volume sum. This inner construction is distinct from the common fan in Appendix~\ref{sec:fan}. In the final compact record each endpoint is $s v/2^{42}$, with integer $s$ and a prescribed integer ray $v$; the arc grid has $2048$ intervals. The older \texttt{n80} JSON uses interval determinants and reports a different endpoint. It is not the source of the final bound \eqref{eq:KU-bounds}. The quartic/Bernstein adapter in Appendix~\ref{sec:adapters} belongs to the common-fan route, not to this sampled-arc certificate. For Body~5, the divergence theorem writes volume as a sum over the parametrized boundary pieces: \[ \Vol(K)=\frac14\int_{\partial K}\langle x,n(x)\rangle\,dS(x). \] Using the boundary strata generated by the six spherical patches, four inherited apex arcs, six new base arcs, four base vertices and the apex, respectively, the signed flux decomposition is \begin{equation}\label{eq:B5-flux} \Vol(\Bfive)=\tfrac14\bigl( 6I_f+4I_a+6I_b+4I_v+I_E\bigr). \end{equation} The $I$'s are outward-normal fluxes over the corresponding smooth boundary pieces, not the lower-dimensional generating strata themselves. Their boundaries have zero surface measure. Appendix~\ref{app:body5} gives a representative kernel and the apex remainder bound; the supplementary code supplies all transformed kernels. The recorded certificate uses a $64\times64$ face grid, $1024$ subintervals on each of two arc types, a $128\times128$ base-vertex grid, and a truncated moment calculation with a bounded tail for the remaining apex term. Basic binary64 operations are expanded outwards; square-root endpoints are checked by exact rational squaring, and arctangent and $\pi$ are enclosed by explicit series. Thus the deterministic point estimate $0.2229277265$ is supplemented by the enclosure \eqref{eq:B5-bounds}. \subsection{\texorpdfstring{$M_4$}{M4}} For width one, \begin{equation}\label{eq:M4-exact} \Vol(\Mfour) =\frac{\pi}{32}\bigl[(24-11\sqrt2)\pi-24\bigr] \approx0.2480396734. \end{equation} The common rational fan already gives the independent lower certificate \begin{equation}\label{eq:M4-common} L_{M_4,3}=0.233244525156270\ldots>T. \end{equation} \subsection{The AMO peabody} A separate interval-domain computation places the width-one AMO body near \[ \Vol(\PAMO)\approx0.22447501476943. \] More importantly for the common method, the uniform level-$5$ certificate contains $87552$ rays and $524288$ cells and has independent-verifier value \begin{equation}\label{eq:AMO-k5} L_{\mathrm{AMO},5}=0.222097827053789\ldots>T. \end{equation} Hence \[ \Vol(\Ufour)T\\\hline \Bfive&0.221864682307840&\text{yes}\\ \KU&0.219885140191584&\text{no}\\ \RM&0.219660269719997&\text{no}. \end{array} \] Together with $M_4$ and AMO, Body~5 thus has a common-fan lower bound above $T$. The two raised entries do not cross $T$ in this computation; their completed comparisons use the body-specific certificates above. Refining a directional mesh does not enlarge a fixed family of interior witness balls. Consequently a modest fan bound does not contradict a sharper lower bound obtained with a different inner construction. \section{Proof of the comparison theorem}\label{sec:main-proof} \begin{proof}[Proof of Theorem~\ref{thm:main-separator}] Equation \eqref{eq:U4-bound} gives $\Vol(\Ufour)-t$ for all four coordinates, then the limiting configuration at first contact has three coordinates equal to $-t$ and the fourth equal to $3t$; the unit-norm condition is $12t^2=1$, equivalently $c=1/3$. For $c\ge1/3$ there are no positive-area triple cap intersections. Two caps intersect precisely when their angular radius $\alpha=\arccos c$ satisfies $2\alpha\ge\gamma$, where $\gamma=\arccos(-1/3)$ is the tetrahedral center distance. Since \[ \cos(\gamma/2)=\sqrt{\frac{1+\cos\gamma}{2}}=\frac1{\sqrt3}, \] pairwise lenses occur exactly for $c<1/\sqrt3$. It remains to compute the area $L(c)$ of one pairwise lens. Let $1/3\le c\le1/\sqrt3$. Spherical trigonometry for the triangle formed by the two cap centers and one intersection point gives \[ \phi= \arccos\!\left(\frac{\sqrt2c}{\sqrt{1-c^2}}\right), \qquad \psi= \arccos\!\left(\frac{c^2+1/3}{1-c^2}\right). \] Each boundary arc is an arc of a small circle of Euclidean radius $\sqrt{1-c^2}$ and has length $2\phi\sqrt{1-c^2}$. With the orientation induced from the lens, its geodesic curvature has magnitude $c/\sqrt{1-c^2}$. Hence the two boundary arcs contribute total geodesic curvature $4c\phi$. The two corner contributions in Gauss--Bonnet reduce to the angle term $2\psi$, and since the unit sphere has Gaussian curvature one, Gauss--Bonnet yields \begin{equation}\label{eq:lens-v3} L(c)=2\psi-4c\phi =2\arccos\!\left(\frac{c^2+1/3}{1-c^2}\right) -4c\arccos\!\left(\frac{\sqrt2c}{\sqrt{1-c^2}}\right). \end{equation} Inclusion--exclusion now gives \[ A_4(t) =4\pi-4\cdot2\pi(1-c)+6L(c) =8\pi c-4\pi+6L(c) \] for $1/3\le c<1/\sqrt3$. When $1/\sqrt3\le c<1$ the lenses are absent, so $A_4(t)=8\pi c-4\pi$; for $c\ge1$ all forbidden caps are empty and $A_4(t)=4\pi$. This proves the piecewise formula used in the main text. \section{A common rational simplicial-fan lower bound}\label{sec:fan} \subsection{The cross-polytope fan} Let \begin{equation}\label{eq:C4} C_4=\conv\{\pm e_1,\pm e_2,\pm e_3,\pm e_4\}\subset\R^4. \end{equation} Its boundary has sixteen tetrahedral facets \[ \conv\{\varepsilon_1e_1,\varepsilon_2e_2,\varepsilon_3e_3,\varepsilon_4e_4\}, \qquad \varepsilon_i\in\{\pm1\}. \] The positive hull of each facet is the corresponding orthant. Hence the cones over these sixteen facets cover $\R^4$ and have pairwise disjoint interiors. Each tetrahedron is refined by the standard edge-midpoint subdivision. If its vertices are $v_1,v_2,v_3,v_4$, insert the six edge midpoints $m_{ij}=(v_i+v_j)/2$. The four corner tetrahedra are separated from a central octahedron; splitting the octahedron along one fixed opposite-vertex diagonal gives four further tetrahedra. Thus each parent tetrahedron is replaced by eight children. On a common face of two parent tetrahedra, the induced subdivision is the same triangular midpoint subdivision, so the refined triangulation is conforming. After $k$ refinements, every boundary vertex has denominator $s_k=2^k$. Write a ray vertex as $\widetilde u_i=u_i/s_k$ with $u_i\in\Z^4$. The cones over the refined tetrahedra again form a complete simplicial fan. \begin{proposition}[Fan counts]\label{prop:fan-count} Let $V_k,E_k,F_k$ denote the number of vertices, edges, and tetrahedra in the level-$k$ triangulation of $\partial C_4$. Then \[ V_0=8,\qquad E_0=24,\qquad F_0=16, \] and \begin{equation}\label{eq:fan-rec} V_{k+1}=V_k+E_k, \qquad F_{k+1}=8F_k, \qquad E_k=V_k+F_k. \end{equation} Consequently \[ \begin{array}{c|r|r} k&V_k&F_k\\\hline 2&192&1024\\ 3&1408&8192\\ 4&11008&65536\\ 5&87552&524288\\ 6&699392&4194304. \end{array} \] \end{proposition} \begin{proof} Every old edge contributes one new midpoint vertex and no other new vertices are created, giving $V_{k+1}=V_k+E_k$. Each old tetrahedron gives eight children. For a triangulation of $S^3$, every triangular face belongs to exactly two tetrahedra, so $f_2=2F_k$. Euler's relation $V_k-E_k+f_2-F_k=0$ gives $E_k=V_k+F_k$. \end{proof} \subsection{The determinant identity} The four-dimensional cross-polytope has volume \begin{equation}\label{eq:C4-volume} \Vol(C_4)=\frac{2^4}{4!}=\frac{16}{24}. \end{equation} Because the coned refined tetrahedra partition $C_4$, \begin{equation}\label{eq:det-audit} \sum_{C=(i_1,i_2,i_3,i_4)} \left|\det(u_{i_1},u_{i_2},u_{i_3},u_{i_4})\right| =16s_k^4. \end{equation} This identity is an exact audit of the reconstructed fan. It is not, by itself, a substitute for proving that an arbitrary list of cells is a conforming triangulation; coverage and non-overlap come from the recursive construction above. \subsection{Certified radial endpoints and the lower bound} Let $K\subset\R^4$ be a convex body containing the origin. Let $A:\R^4\to\R^4$ be the linear chart used for the body and set $J=|\det A|$. Fix an integer denominator $D$. On each fan ray choose an integer radius $r_i\ge0$ and define \begin{equation}\label{eq:endpoint} p_i=A\left(\frac{r_i}{Ds_k}u_i\right). \end{equation} Assume that every $p_i$ has been rigorously certified to belong to $K$. \begin{proposition}[Exact inscribed-simplex bound]\label{prop:inscribed-bound} For every fan cell $C=(i_1,i_2,i_3,i_4)$, \[ \conv\{0,p_{i_1},p_{i_2},p_{i_3},p_{i_4}\}\subset K. \] The interiors of these simplices are pairwise disjoint, and \begin{equation}\label{eq:LK} L_K= \frac{J}{24(Ds_k)^4} \sum_C \left|\det(u_{i_1},u_{i_2},u_{i_3},u_{i_4})\right| \prod_{j=1}^4 r_{i_j} \le\Vol(K). \end{equation} \end{proposition} \begin{proof} Each simplex is contained in $K$ by convexity. It is also contained in the cone over the corresponding fan cell, and distinct cone interiors are disjoint. Formula \eqref{eq:LK} is the exact four-simplex determinant formula summed over the cells. \end{proof} When $J\in\Q$, \eqref{eq:LK} is rational. If $L_K=N/Q$, the comparison $L_K>T$ is the integer inequality \begin{equation}\label{eq:integer-threshold} 20000N-4437Q>0. \end{equation} When $J$ contains a fixed quadratic radical, the sign is first determined and the final comparison is reduced to an integer inequality after squaring. No rounded decimal is proof data. \subsection{Uniform and adaptive refinements} The preceding construction is the uniform refinement. The adaptive variant refines selected leaf tetrahedra, together with the conforming closure required on shared faces. The verifier reconstructs the resulting nonuniform simplicial complex from the refinement tree, checks face matching, and repeats the same determinant audit. Proposition~\ref{prop:inscribed-bound} then applies without change. The adaptive strategy affects efficiency, not the proof kernel. \section{Exact endpoint certificates}\label{sec:adapters} The fan and determinant calculation are common to all bodies. Only the proof of $p_i\in K$ depends on the geometry of the candidate. \subsection{\texorpdfstring{$M_4$}{M4}} Membership in $M_4$ follows directly from the Cartesian description \eqref{eq:Mn}. After fixing the sign pattern of the rational endpoint and clearing denominators, the inequality becomes an exact integer comparison. No root isolation or floating convex-hull computation is required. \subsection{Raised Meissner body} For the positive half, the preserved-edge description gives three circular-arc constraints. For a circular parametrization $\gamma(t)=c+a\cos t+b\sin t$ with $a\perp b$ and $\|a\|=\|b\|=R$ on a closed parameter interval, \[ \|x-\gamma(t)\|^2 =\|x-c\|^2+R^2-2(x-c)\cdot(a\cos t+b\sin t). \] Thus the maximum distance on the arc is attained at an endpoint or at a stationary point of this elementary trigonometric expression. All three preserved arcs must satisfy the radius-one constraint. Replacing this conjunction by an ``at least one arc'' test is not conservative; it accepts exterior points. For the negative half, the certificate uses the rigorously contained finite union \begin{equation}\label{eq:RM-negative-witness} L_-= \{x_4\le0\}\cap \bigcup_m B_4\left(m,1-\sqrt{\frac58+\|m\|^2}\right), \end{equation} with rational witness centers $m$. Endpoint inclusion is therefore reduced to exact ball inequalities. The equal-volume theorem of Section~\ref{sec:RM} transfers every strict lower bound proved for one canonical raised Meissner representative to the other. \subsection{Raised \texorpdfstring{$U_3$}{U3}} Each positive-half boundary arc is an ellipse of the form \[ \gamma(t)=A\cos t+B\sin t, \qquad 0\le t\le\frac\pi2. \] The substitution \begin{equation}\label{eq:qparam} q=\tan(t/2), \qquad 0\le q\le1, \end{equation} covers the complete arc, with $q=0$ and $q=1$ corresponding to its endpoints. After clearing denominators, every radius-one constraint becomes an integer quartic inequality \begin{equation}\label{eq:quartic} P(q)\ge0\qquad(0\le q\le1). \end{equation} This is an alternative adapter for the common fan of Appendix~\ref{sec:fan}; it is not the interpolation test used by the specialized $n=80$ certificate. Writing $P$ in the Bernstein basis certifies positivity whenever all Bernstein coefficients are nonnegative. If this fails on $[0,1]$, exact dyadic de Casteljau subdivision produces two child intervals and the test is repeated. A fixed depth guard returns failure rather than an uncertified acceptance. The negative half uses the separately frozen rigorous inner model from the earlier raised-$U_3$ certificate. \subsection{Body 5} The boundary description of \cite{MRP} splits the relevant support problem into six spherical patches. On each patch the radial support maximum is attained among a finite set of at most seven candidates. In the coefficient chart used for the certificate the volume Jacobian is $1/4$, while the support comparisons lie in $\Q(\sqrt5)$. Their signs are decided exactly by separating the rational and $\sqrt5$ parts and, only after checking the sign needed for squaring, reducing to integer inequalities. \subsection{The direct AMO peabody} The construction in \cite{AMO4} gives a complete boundary assembled from pair, triple, and cap pieces; it does not provide a global membership oracle. The endpoint certificate therefore starts from a rigorous boundary witness rather than pretending that the boundary parametrization itself is a membership test. Let $G$ be the barycenter of the regular four-simplex. By simplex symmetry the Chebyshev center is $G$, and the constant-width relation together with Jung's inequality gives the rational inball \begin{equation}\label{eq:AMO-inball} B(G,1/3)\subset\PAMO. \end{equation} The following elementary lemma converts a boundary enclosure into an interior certificate. \begin{lemma}[Inward shrink]\label{lem:inward-shrink} Let $B(G,r_0)\subset K$, let $x\in K$, and suppose $\|x-c\|\le\rho$. For $0\le\lambda\le1$, \begin{equation}\label{eq:shrink-ball} B\bigl(G+\lambda(c-G),(1-\lambda)r_0-\lambda\rho\bigr)\subset K \end{equation} whenever the displayed radius is nonnegative. In particular, a rational point $p$ belongs to $K$ if \begin{equation}\label{eq:shrink-test} \|p-[G+\lambda(c-G)]\|+\lambda\rho\le(1-\lambda)r_0. \end{equation} \end{lemma} \begin{proof} For every $y\in B(G,r_0)$, convexity gives $(1-\lambda)y+\lambda x\in K$. The image of the inball is $B(G+\lambda(x-G),(1-\lambda)r_0)$. Replacing the unknown $x$ by its enclosure center $c$ loses at most $\lambda\rho$ in radius, which yields \eqref{eq:shrink-ball}. \end{proof} In the centered chart $G=0$ and $r_0=1/3$, the implemented test is \begin{equation}\label{eq:AMO-test} \|p-\lambda c\|+\lambda\rho\le\frac{1-\lambda}{3}. \end{equation} The term $\lambda\rho$ is essential. The spherical-cap branch also requires an exact component check excluding the remote positive component; the finite branch-and-bound audit closes on the component containing the regular-simplex direction. \section{Boundary integration and the apex remainder for Body 5} \label{app:body5} The coordinates used for these kernels are those of \cite{MRP}: $A_i=e_i/\sqrt2$ and $E=\varphi(A_1+\cdots+A_4)/2$, with $\varphi=(1+\sqrt5)/2$. All normals in \eqref{eq:B5-flux} are outward. In this coordinate origin the apex flux is negative; it must not be replaced by its absolute value. \subsection{A representative face kernel and the quadrature error} Put $z_0=-1/\sqrt3$, $z_1=(\varphi-1)/\sqrt3$, and, on $[0,1]^2$, \[ z=z_0+(z_1-z_0)x,\quad b=\frac{1+\sqrt3z}{\sqrt6\sqrt{1-z^2}},\quad q_0=\frac{b}{\sqrt{1-b^2}},\quad q=q_0+(1-q_0)y. \] The face contribution used in the validator is $I_f=\int_{[0,1]^2}f_f$, where \[ f_f(x,y)= \frac{2(z_1-z_0)(1-q_0)}{1+q^2} \left[J_0-\left(\frac{\sqrt3}{2}+\frac z2\right)J_c\right], \quad J_0=\frac{5\pi}{12}-\frac{3\sqrt3}{4},\quad J_c=\frac{11}{12}-\frac{\sqrt3\pi}{6}. \] Integrating in $y$ recovers the angular factor $\pi/2-2\arcsin b$, which explains this transformation. In the code, \texttt{f\_face2}, \texttt{f\_apex\_arc}, \texttt{f\_base\_arc} and \texttt{f\_base\_vertex} give $I_f,I_a,I_b,I_v$, respectively, by integration over unit intervals or squares. Their grids are $64^2,1024,1024,128^2$. For a rectangle of area $A$ and half-widths $h_x,h_y$, a midpoint Taylor enclosure has error at most \[ A\left(\frac{h_x^2}{6}\sup|f_{xx}|+ \frac{h_y^2}{6}\sup|f_{yy}|+ \frac{h_xh_y}{4}\sup|f_{xy}|\right). \] Indeed, the linear terms integrate to zero; integrating the absolute second-order remainder gives the displayed factors. The one-dimensional version is $\ell^3\sup|f''|/24$. Interval automatic differentiation bounds these derivatives over the complete cell, including the parameter maps. \subsection{An exact moment expansion for the apex} Let $\Delta_3=\{\lambda_i\ge0:\sum_{i=1}^4\lambda_i=1\}$, with measure $d\lambda_1d\lambda_2d\lambda_3$ after eliminating $\lambda_4$; thus $\int_{\Delta_3}1=1/6$. With $s=\sum_i\lambda_i^2$, $R=\sqrt{(1+s)/2}$ and $c=(5+\sqrt5)/8$, \begin{equation}\label{eq:B5-apex-integral} I_E=\frac{\sqrt5}{4}\int_{\Delta_3}(R^{-4}-cR^{-5})\,d\lambda. \end{equation} To see the constants, put $v_i=E-A_i$. Then $v_i\cdot v_j=(1+\delta_{ij})/2$, $|\det(v_1,\ldots,v_4)|=\sqrt5/4$ and $E\cdot v_i=c$. For $w=\sum_i\lambda_i v_i$ the boundary point is $E-w/R$, its outward normal is $-w/R$, and the spherical Jacobian is $(\sqrt5/4)R^{-4}$. This gives \eqref{eq:B5-apex-integral}. Set $a_0=13/8$, $q_*=3/13$ and \[ M_j=\frac{j!}{(2j+3)!} \sum_{m_1+\cdots+m_4=j}\prod_{i=1}^4\frac{(2m_i)!}{m_i!}, \qquad \mu_k=\sum_{j=0}^k\binom{k}{j}(-5/8)^{k-j}M_j. \] These are the exact moments of $s^j$ and $(s-5/8)^k$ by the Dirichlet monomial formula. Since $1/4\le s\le1$, $|(s-5/8)/a_0|\le q_*$. Define \[ S_1^{(K)}=\sum_{k=0}^{K}(-1)^k(k+1)\mu_k/a_0^k,\qquad S_2^{(K)}=\sum_{k=0}^{K}(-1)^k\frac{(5/2)_k}{k!}\mu_k/a_0^k. \] Then \eqref{eq:B5-apex-integral} equals \[ \frac{\sqrt5}{4} \left[4a_0^{-2}(S_1^{(K)}+\varepsilon_1) -c\,2^{5/2}a_0^{-5/2}(S_2^{(K)}+\varepsilon_2)\right], \] where, for $n=K+1$, \[ |\varepsilon_1|\le \frac{q_*^n((n+1)-nq_*)}{6(1-q_*)^2},\qquad |\varepsilon_2|\le \frac{(5/2)_nq_*^n}{6n!\,[1-q_*(n+5/2)/(n+1)]}. \] The first bound sums an arithmetico-geometric tail; for the second, successive absolute terms have ratio at most $q_*(n+5/2)/(n+1)<1$. The production value $K=20$ gives $|\varepsilon_1|<2.046\cdot10^{-13}$ and $|\varepsilon_2|<7.393\cdot10^{-13}$. Combining this bound with the four quadrature enclosures in \eqref{eq:B5-flux}, using outward arithmetic throughout, gives \eqref{eq:B5-bounds}. \section{Certificate index and reproducibility}\label{app:repro} A replay must check input schemas and hashes, geometric membership, nonoverlap or convexity, and the final exact or outward-rounded sum. A floating candidate, a stored success flag, and a matching hash do not replace these checks. The common fan is reconstructed from its refinement rule; its final threshold test is the integer comparison \eqref{eq:integer-threshold}. \begin{table}[ht] \centering\small \caption{Proof dependencies and the status of the accompanying review archive. Full filenames, hashes, commands and logs are in \texttt{CERTIFICATES.md}.} \label{tab:certificate-index} \begin{tabularx}{\textwidth}{@{}lXX@{}} \toprule ID & Conclusion and record & Review-archive status\\ \midrule U4-G & Uniform-grid enclosure \eqref{eq:U4-bound}; Arb grid manifest & Source and exact endpoint records available\\ U4-S & Sharper hybrid enclosure \eqref{eq:U4-current}; adaptive six-decimal record & New production certificate, completed checkpoint and log available; local audit passed\\ RM-L & Inner-polytope bound \eqref{eq:RM-lower}; membership and PL boundary checks & Compact data and exact membership/convexity verifier available\\ R-C & Two raised-body upper bounds and the final $n=80$ lower bound \eqref{eq:KU-bounds} & Recovered source/data; complete fresh replay passed\\ B5 & Boundary enclosure \eqref{eq:B5-bounds} & Standalone source and component records available\\ FAN & Common-fan thresholds, including \eqref{eq:AMO-k5} & Code archive, level-5 records and AMO log available\\ \bottomrule \end{tabularx} \end{table} \paragraph{Distinct certificate versions.} U4-G uses $60$-digit uniform integration; U4-S uses $50$-digit hybrid refinement. The older \nolinkurl{raised_u3_certified_simplicial_lower_n80.json} differs from R-C's rational-ray record in \nolinkurl{Manitoba_full_comparison_certificates_20260929_v2.zip}: \texttt{certify\_comparison.py}, \texttt{raised\_comparison\_compact.npz} and \texttt{rm\_lower.npz} (checker digest prefix \texttt{b3aadabd3843}). The new U4-S \nolinkurl{u4_6dp_adaptive_certificate.json}, supplied on October~21, 2026, has digest prefix \texttt{a5b0a863c50d}; its completed checkpoint has prefix \texttt{5ccfe5a3c878}. The historical JSON with prefix \texttt{b787db8a5fad} remains unrecovered. The supplement preserves full hashes and the original returned files. \paragraph{Scope of the present draft.} The R-C source and both NPZ inputs match their recorded SHA-256 hashes. A complete replay on October~16, 2026 reproduced all four exact bounds; its rational-ray $U_3$ lower bound differs from the older interval-determinant record. For U4-S, the returned log records a complete adaptive run of about $83$ minutes. A local audit checks hashes, checkpoint counters, exact imported endpoints and aggregation; a local checkpoint replay recomputes the six one-dimensional integrals and total. Both passed, without repeating the adaptive two-dimensional integration. Enclosure~\eqref{eq:U4-current} lies inside $(0.2218355,0.2218365)$, certifying rounding to $0.221836$ at six decimals, but not seven. The computational audits and replays described above establish the documented scope of numerical certificate checking and reproduction. The author's human review and understanding of the manuscript are declared separately on the first page. In particular, the complete adaptive two-dimensional production run was not independently repeated. \paragraph{Code and data availability.} Code, compact data and certificates are available at \href{https://github.com/WangHangang/4d-constant-width-certificates}{\nolinkurl{WangHangang/4d-constant-width-certificates}}. For this revision, use commit \href{https://github.com/WangHangang/4d-constant-width-certificates/tree/5d69e0be6ea17ea2f8e458543ab5e308b31d0dd9}{\texttt{5d69e0be6ea1}}, directory \texttt{manuscript1/}. Its \texttt{CERTIFICATES.md} maps the claims to their inputs and replay scope. The original large raised-Meissner datasets have a separately linked Zenodo archive. For U4-S, the supplement's \nolinkurl{docs/U4_S_RETURN_AUDIT.md} gives the provenance, audit scope and commands for checkpoint replay or a fresh adaptive run. \section{Exact threshold arithmetic}\label{app:integer} For a rational common-fan lower bound $L=N/Q$, the separator test is \eqref{eq:integer-threshold}. For the raised Meissner exact lower bound \eqref{eq:RM-lower}, both sides are positive and \[ \frac{S\sqrt2}{192D^4}>\frac{4437}{20000} \] is equivalent to \[ 2(20000S)^2>(4437\cdot192D^4)^2, \] where \[ S=36415211368949752100591187, \qquad D=1048576. \] Thus the strict comparison is an integer statement once the inner-polytope containment has been certified. \enlargethispage{2\baselineskip} \begin{thebibliography}{99} \bibitem{ABNPR} A.~Arman, A.~Bondarenko, F.~Nazarov, A.~Prymak and D.~Radchenko, \emph{Small volume bodies of constant width}, International Mathematics Research Notices 2025 (2025), no.~4, rnaf020, \href{https://doi.org/10.1093/imrn/rnaf020}{doi:10.1093/imrn/rnaf020}. \bibitem{ABPR} A.~Arman, A.~Bondarenko, A.~Prymak and D.~Radchenko, \emph{Small volume bodies of constant width with tetrahedral symmetries}, SIGMA 21 (2025), 109, \href{https://doi.org/10.3842/SIGMA.2025.109}{doi:10.3842/SIGMA.2025.109}. \bibitem{AMO4} I.~Arelio, L.~Montejano and D.~Oliveros, \emph{A four-dimensional peabody of constant width}, Mathematika 71 (2025), e70014. \bibitem{Jiang2026} Y.~Jiang, \emph{A $0.41275$ lower bound for the three-dimensional Blaschke--Lebesgue problem}, preprint, arXiv:2610.13964v1, 2026, \url{https://arxiv.org/abs/2610.13964v1}. \bibitem{KW} B.~Kawohl and C.~Weber, \emph{Meissner's mysterious bodies}, The Mathematical Intelligencer 33 (2011), 94--101. \bibitem{LRO} T.~Lachand--Robert and E.~Oudet, \emph{Bodies of constant width in arbitrary dimension}, Math. Nachr. 280 (2007), 740--750. \bibitem{MMO} H.~Martini, L.~Montejano and D.~Oliveros, \emph{Bodies of Constant Width: An Introduction to Convex Geometry with Applications}, Birkh\"auser, Cham, 2019, \href{https://doi.org/10.1007/978-3-030-03868-7}{doi:10.1007/978-3-030-03868-7}. \bibitem{MRP} M.~G.~Mercado--Flores, M.~Raggi and E.~Rold\'an--Pensado, \emph{A four-dimensional body of constant width}, Mathematika 72 (2026), e70113. \bibitem{Rybnikov} K.~Rybnikov, \emph{An efficient local approach to convexity testing of piecewise-linear hypersurfaces}, Comput. Geom. 42 (2009), 147--172. \bibitem{Schneider} R.~Schneider, \emph{Convex Bodies: The Brunn--Minkowski Theory}, 2nd expanded ed., Cambridge University Press, 2014. \end{thebibliography} \end{document}