diff e0711ba..bf73b08 mutually_unbiased_bases_dim6_v2.txt
diff --git a/mutually_unbiased_bases_dim6_v2.txt b/mutually_unbiased_bases_dim6_v2.txt
index 5e0611b..1c6383b 100644
--- a/mutually_unbiased_bases_dim6_v2.txt
+++ b/mutually_unbiased_bases_dim6_v2.txt
@@ -20,12 +20,10 @@
\usepackage[nameinlink,noabbrev]{cleveref}
\crefname{section}{Section}{Sections}
\crefname{appendix}{Appendix}{Appendices}
-\hypersetup{colorlinks=true,linkcolor=blue!45!black,citecolor=blue!45!black,urlcolor=blue!45!black,
- pdftitle={The maximum number of mutually unbiased bases in dimension six},
- pdfauthor={OpenAI}}
+\hypersetup{colorlinks=true,linkcolor=blue!45!black,citecolor=blue!45!black,urlcolor=blue!45!black}
\newcommand{\C}{\mathbb C}
\newcommand{\R}{\mathbb R}
-\newtheorem{theorem}{Theorem}[section]
+\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
@@ -42,123 +40,75 @@
\AddToHook{env/corollary/before}{\theoremspace}
\AddToHook{env/definition/before}{\theoremspace}
\AddToHook{env/remark/before}{\theoremspace}
-\numberwithin{equation}{section}
\setlist{itemsep=3pt,topsep=5pt}
\lstset{basicstyle=\ttfamily\small,breaklines=true,columns=fullflexible,keepspaces=true,showstringspaces=false}
\emergencystretch=1em
-\title{The maximum number of mutually unbiased bases\\in dimension six}
-\author{OpenAI}
-\date{September 24, 2026}
\begin{document}
-\maketitle
-\begin{abstract}
-We prove that the maximum number of mutually unbiased orthonormal bases
-in $\C^6$ is three, resolving Zauner's dimension-six MUB conjecture.
-The upper bound is computer-assisted: under the stated binary64 arithmetic
-and compiler conditions, a complete execution of the documented verification
-pipeline excludes four arbitrary complex bases.
-\end{abstract}
-\tableofcontents
-
-% =====================================================================
-\section*{How to read this paper}
-\addcontentsline{toc}{section}{How to read this paper}
% =====================================================================
+The result is one geometric statement. In complex six-dimensional space
+$\C^6$ there are three mutually unbiased orthonormal bases, and no four.
+In symbols, $N(6)=3$.
-This paper proves exactly one geometric statement: in the complex
-$6$-dimensional space $\C^6$ you can find three mutually unbiased
-orthonormal bases, but you cannot find four. That is the whole result.
-Call it ``$N(6) = 3$.''
-
-The proof is long because modern mathematics often needs a computer to
-check finitely many things, and a computer proof is only a proof if you
-can rule out every possible bug, rounding error, and missed case. Most
-of the paper is spent on \emph{certifying}: showing that every test
-the computer runs has a strict safety margin, so that ordinary
-floating-point arithmetic cannot turn a real solution into a spurious
-``not found.''
+The proof is long for an honest reason. Some of modern geometry ends in
+a finite check, and a finite check counts as a proof only when every
+possible bug, rounding error, and missed case is excluded. So most of
+the work is \emph{certification}: every test the computer runs carries a
+strict safety margin, so that ordinary floating-point arithmetic cannot
+turn a true solution into a spurious ``not found.''
-If you are a high-school student with a strong taste for geometry, here
-is the entire strategy in six bullet points. Do not worry if some
-symbols look unfamiliar at first; the point is the shape of the idea.
+The strategy fits in six steps.
\begin{enumerate}
-\item \textbf{Rotate the first basis away.} Any unitary transformation
- makes any basis look like the standard basis. After this rotation, the
- second basis must be the columns of $H/\sqrt 6$, where $H$ is a
- $6\times 6$ matrix with all entries of modulus $1$ and $HH^* = 6I$.
- Such $H$ has a name: a \emph{complex Hadamard matrix}. The question
- ``can we add two more bases?''
- becomes
- ``which $H$ admit two extra MUB bases?''
-
-\item \textbf{Use symmetry to pin down $H$.} Multiply rows of $H$ by
- phases and columns of $H$ by phases; the question is unchanged. Choose
- these phases so that the first row and column of $H$ are $1$. Then $H$
- is determined by $9$ real phase parameters (the remaining entries of
- the first row and column) plus a $4\times 4$ block of unknown phases
- (the lower-right block of $H$).
-
-\item \textbf{Cover the seed.} The $9$ seed phases, as the true $H$
- varies, sweep out some subset of the $9$-torus. We cover that subset
- by finitely many balls of small radius ($0.0320001$ in cycle units).
- This is the \emph{seed cover}, Section~\ref{sec:seed}.
-
-\item \textbf{Complete and refine (Stages A and B).} For each seed ball,
- look at all possible ways to fill in the $4\times 4$ block. Because
- the first three blocks of $H$ are already pinned, the $4\times4$ block
- is forced to satisfy a set of Hadamard equations that compress down
- to a $2\times 2$ unitary matrix $V\in U(2)$. We cover $U(2)$ by finitely
- many boxes (Stage A), and then refine each box into small
- \emph{phase balls} where the actual solution set lives (Stage B).
- This is the hardest geometry in the paper, Sections~\ref{sec:completion}
- and \ref{sec:phase-cover} and \ref{sec:refinement}.
-
-\item \textbf{Exclude two extra bases (Stage C).} Fix one phase ball for
- $H$. Any vector that is unbiased to both the standard basis and
- $H/\sqrt 6$ must have the form $e(\beta)/\sqrt 6$. A small phase-bin
- search covers all such vectors by small \emph{vector balls}. Now imagine
- two more bases: six of their vectors are pairwise orthogonal, and every
- cross pair is unbiased. These conditions become edges of two graphs on
- the vector balls, and the required pattern is two disjoint six-cliques
- with every cross edge present. A finite search rules that pattern out.
- This is Section~\ref{sec:exclusion}.
-
-\item \textbf{Account for everything.} The complete execution of the
- above four stages, on a $2026$ computer with a specific build and a
- specific set of numeric margins, is documented in
- Section~\ref{sec:execution} and Appendix~\ref{sec:rounding}. The finite
- chain covers every possible $H$ up to the allowed symmetries, and each
- local test is either a sound exclusion or an honest failure (which
- would be reported, not hidden). The computer never guesses.
+\item \textbf{Remove the first basis.} A unitary change of coordinates
+ sends any orthonormal basis to the standard one. The second basis is
+ then the column set of $H/\sqrt6$, where every entry of $H$ has modulus
+ $1$ and $HH^*=6I$. Such $H$ is a \emph{complex Hadamard matrix}, and
+ the question becomes: which $H$ admit two further unbiased bases?
+
+\item \textbf{Pin down the phase freedom.} Multiplying rows and columns
+ of $H$ by phases changes nothing. Phases are chosen so that the first
+ row and column of $H$ are $1$, after which $H$ is fixed by nine real
+ phase parameters, the rest of the first row and column, together with a
+ $4\times4$ block of unknown phases.
+
+\item \textbf{Cover the seed.} Those nine parameters trace a subset of
+ the nine-torus, and finitely many balls of radius $0.0320001$, measured
+ in cycles, cover it. This is the seed cover.
+
+\item \textbf{Complete and refine.} For a seed ball, the $4\times4$
+ block must satisfy Hadamard equations that compress to a single
+ $V\in U(2)$. Finitely many boxes cover $U(2)$, and each box refines
+ into small phase balls holding the actual solution set. This is the
+ hardest geometry in the argument.
+
+\item \textbf{Exclude two further bases.} Take one phase ball for $H$.
+ Every vector unbiased to both the standard basis and $H/\sqrt6$ has the
+ form $e(\beta)/\sqrt6$, and a phase-bin search covers them all by small
+ vector balls. Two further bases would need twelve of those balls: six
+ pairwise orthogonal in one group, six in the other, with all $36$ cross
+ pairs unbiased. Those conditions are edges of two graphs, and a finite
+ search rules out the required pair of six-cliques.
+
+\item \textbf{Account for everything.} The execution of these four
+ stages on a 2026 machine, with a fixed build and fixed numeric margins,
+ is recorded together with the certified margins. The finite chain
+ reaches every possible $H$ up to the allowed symmetries, and each local
+ test either excludes soundly or fails openly. Nothing is guessed.
\end{enumerate}
-\textbf{How to use this document.}
-Section~\ref{sec:introduction} is the mathematical introduction: the
-definition of MUBs, the main theorem, the historical context, and the
-easy lower bound (three bases exist, by a tensor-product construction).
-The next five sections then prove the hard direction (four bases are
-impossible), one geometric layer at a time. Section~\ref{sec:execution}
-records what the computer actually did. Appendix~\ref{sec:rounding}
-proves that the arithmetic in each numerical test has strict,
-checkable margins.
-
-\textbf{A note on style (formality).}
-Throughout, all sets of phase coordinates are closed. All balls,
-ellipsoids, and boxes are closed balls, ellipsoids, and boxes. Their
-overlaps and their repeated overlap with the phase representatives are
-harmless: a repeated cover can only weaken an exclusion, never omit a
-true solution. A ``small ball'' always means the same thing: the set of
-phase matrices within a certain Frobenius norm. A numerical center is
-a proposed best guess; it need not itself be an exact Hadamard matrix.
-Every conclusion is drawn from a necessary-condition inequality that
-has been verified on a whole ball, not from the residual size at the
-proposed center.
+\textbf{Formality.} All sets of phase coordinates are closed, as are all
+balls, ellipsoids, and boxes. Overlaps, and repeated overlap with phase
+representatives, are harmless: duplication weakens an exclusion but
+never omits a solution. ``Small ball'' always means the phase matrices
+within a stated Frobenius norm. A numerical center is a proposal and
+need not be an exact Hadamard matrix. Every conclusion comes from a
+necessary-condition inequality verified on a whole ball, not from the
+residual at a proposed center.
% =====================================================================
-\section{Introduction}\label{sec:introduction}
+\medskip\noindent\textbf{Introduction.}
% =====================================================================
Two orthonormal bases $\mathcal B$ and $\mathcal C$ of $\C^d$ are
@@ -172,16 +122,16 @@ unbiased family of orthonormal bases in $\C^d$. The main result is:
\begin{theorem}[Computer-assisted]\label{thm:main}
Under the binary64 arithmetic and compiler conditions stated in
-Appendix~\ref{sec:rounding}, the execution documented in
-Section~\ref{sec:execution} certifies that there are no four pairwise
+the certified arithmetic, the execution documented in
+ certifies that there are no four pairwise
mutually unbiased orthonormal bases in $\C^6$. Consequently
$N(6)=3$.
\end{theorem}
The upper bound is the hard direction. The lower bound (three bases
-exist) is an explicit computation, Section~\ref{subsec:lower}.
+exist) is an explicit computation, .
-\subsection{MUBs, Hadamard matrices, and the shape of the problem}
+\medskip\noindent\textbf{MUBs, Hadamard matrices, and the shape of the problem.}
Fixing one basis by a common unitary transformation costs nothing; every
family can be moved so that the first member is the standard basis. Then
@@ -202,78 +152,108 @@ known family: the second basis is completely unconstrained, and the
argument handles complex Hadamard matrices outside all previously
studied families.
-\subsection{Historical context}
+\medskip\noindent\textbf{Historical context.}
-Mutually unbiased bases describe projective measurements in which any
+Mutually unbiased bases describe projective measurements in which a
state drawn from one basis gives a uniformly random outcome in any
-other basis. This finite-dimensional complementarity appears in
-Schwinger's unitary-operator framework~\cite{Schwinger1960Unitary}.
-Ivanovi\'c developed the state-determination problem and the
-prime-dimensional construction~\cite{Ivanovic1981StateDetermination}.
-Wootters and Fields proved the statistical optimality of maximal MUB
-sets and constructed them whenever $d$ is a prime power
-\cite{WoottersFields1989}. General dimension satisfies $N(d)\le d+1$,
-with an operator-space proof given by
-Bandyopadhyay et al.~\cite{BandyopadhyayEtAl2002}.
-
-Dimension $6$ is the smallest dimension that is neither a prime power
-nor a small even number covered by other constructions, and so it is the
-first genuinely open case. A tensor-product construction gives three
-bases in $\C^6$ (see~\cite[Section 4]{KlappeneckerRotteler2004} and
-Section~\ref{subsec:lower} below). Zauner's dimension-six conjectures
-(from his 1991 diploma thesis~\cite{Zauner1991Diploma} and its doctoral
-sequel~\cite{Zauner1999}, translated in~\cite{Zauner2011}) assert that
-three is the maximum; the equation $N(6)=3$ is stated explicitly as
-Conjecture~1 of~\cite[Section 4]{KlappeneckerRotteler2004}. A recent
-review of the composite-dimension setting is~\cite{McNultyWeigert2026Review}.
-
-Several complementary approaches developed the dimension-six problem
-before the present proof. Grassl proved that the standard--Fourier pair
-cannot extend to four bases~\cite[Theorem 2]{Grassl2004SICMUB6}.
-Bengtsson et al.\ studied the landscape of order-six Hadamard families
-and their unbiased vectors~\cite{BengtssonEtAl2007MUBHadamard}.
-Numerical searches by Butterley--Hall~\cite{ButterleyHall2007Numerical}
-and by Brierley--Weigert~\cite{BrierleyWeigert2008} supplied evidence
-for the conjecture. Brierley--Weigert also enumerated unbiased vectors
-for specific Hadamards using algebraic equations~\cite{BrierleyWeigert2009};
-their Section~3.4 gives rigorous approximation bounds for exact input
-matrices, but their Section~4.3 explains why rounding coefficients
-in sampled non-affine families prevents a complete cover by that method.
-
-The closest antecedent of the present proof is the certified
-discretization of Jaming, Matolcsi, M\'ora, Sz\"oll\H osi and Weiner.
-They proved that the standard basis together with any member of the
-two-parameter Fourier family cannot extend to four
-bases~\cite[Theorem 1.4]{JamingEtAl2009}; their Section~3 introduces the
-combination of closed phase intervals, rigorous error bounds,
-subdivision, and exhaustive compatibility tests that we push further
-here. Jaming--Matolcsi--M\'ora subsequently formulated the unrestricted
-discretization program~\cite[Sections 2--4]{JamingMatolcsiMora2010}. The
-present proof completes an exhaustive cover of \emph{arbitrary} second
-bases, with a finite search that has rigorous error bounds.
-
-Recent lines of work are complementary, not overlapping. Matolcsi et
-al.~\cite[Section 4]{MatolcsiEtAl2026} study triplets of MUBs under
-conjectural sufficient conditions. C\'ardenes Wuttig and
-Tindall~\cite[Section VI]{CardenesWuttigTindall2026Classification}
-classify order-six Hadamard matrices, but do not decide their MUB
-extendibility. Only the two combined results in this paper (the finite
-cover and the local exclusion, together with the execution and the
-arithmetic contract of Theorem~\ref{execute:finite-theorem}) give an
-unconditional upper bound.
-
-\subsection{The strategy at a glance}\label{subsec:strategy}
+other. Schwinger placed this complementarity inside his calculus of
+unitary operator bases in 1960 (Proc. Nat. Acad. Sci. USA 46, 570--579).
+Ivanovi\'c raised the state-determination problem and gave the
+prime-dimensional construction in 1981 (J. Phys. A 14, 3241--3245).
+Wootters and Fields proved that a complete set of such bases is
+statistically optimal for state determination and built one whenever
+the dimension is a prime power (Ann. Physics 191, 363--381, 1989).
+Every dimension obeys $N(d)\le d+1$, and the short operator-space proof
+is due to Bandyopadhyay, Boykin, Roychowdhury and Vatan (Algorithmica
+34, 512--528, 2002).
+
+{\small\url{https://www.pnas.org/doi/10.1073/pnas.46.4.570}}
+
+{\small\url{https://doi.org/10.1088/0305-4470/14/12/019}}
+
+{\small\url{https://www.sciencedirect.com/science/article/pii/0003491689903229}}
+
+{\small\url{https://arxiv.org/pdf/quant-ph/0103162}}
+
+Dimension six is the first case that is neither a prime power nor a
+small even dimension settled by other constructions. A tensor-product
+construction already yields three bases in $\C^6$, tensoring a qubit
+pair with a qutrit triple; that is Section~4 of the Klappenecker and
+R\"otteler study of MUB constructions. Zauner conjectured in his 1991
+Vienna Diplomarbeit that three is the maximum, the same statement
+reappears in his doctoral thesis, and it is Conjecture~1 of the
+Klappenecker--R\"otteler paper. A survey of the composite-dimension
+setting is due to McNulty and Weigert.
+
+{\small\url{https://arxiv.org/pdf/quant-ph/0309120}}
+
+{\small\url{https://www.gerhardzauner.at/documents/gzdiplthd.pdf}}
+
+{\small\url{https://arxiv.org/pdf/2410.23997}}
+
+Four attacks ran alongside. Grassl proved that the standard basis
+together with any member of the two-parameter Fourier family cannot
+extend to four bases, Theorem~2 of his dimension-six note. Bengtsson,
+Bruzda, Ericsson and \.Zyczkowski mapped the order-six Hadamard
+families and the unbiased vectors they carry. Butterley and Hall, and
+independently Brierley and Weigert, produced the numerical evidence
+that no four bases exist. Brierley and Weigert also enumerated the
+unbiased vectors of individual Hadamards through algebraic equations:
+Section~3.4 of that work gives rigorous approximation bounds for exact
+input matrices, and Section~4.3 explains why rounding coefficients in
+sampled non-affine families blocks a complete cover by that route.
+Raynal, Lu and Englert sharpened the numerical side by maximising the
+average distance between four bases and finding the maximum strictly
+below unity, with a two-parameter family of three bases attaining it.
+
+{\small\url{https://arxiv.org/pdf/quant-ph/0406175}}
+
+{\small\url{https://arxiv.org/pdf/math.OA/0609076}}
+
+{\small\url{https://arxiv.org/pdf/0901.4051}}
+
+{\small\url{https://arxiv.org/pdf/1103.1025}}
+
+The closest antecedent is the certified discretization of Jaming,
+Matolcsi, M\'ora, Sz\"oll\H osi and Weiner. They proved that the
+standard basis together with any member of the two-parameter Fourier
+family cannot extend to four bases, Theorem~1.4 of their 2009 paper,
+and their Section~3 introduces closed phase intervals, rigorous error
+bounds, subdivision, and exhaustive compatibility tests. Jaming,
+Matolcsi and M\'ora then set out the unrestricted discretization
+programme in Sections~2--4 of their survey. Those four devices carry
+the finite search throughout: what is added is exhaustive coverage of
+arbitrary second bases, with every error bounded.
+
+{\small\url{https://arxiv.org/pdf/0902.0882}}
+
+{\small\url{https://arxiv.org/pdf/1201.0640}}
+
+Two recent lines of work are complementary rather than overlapping.
+Matolcsi, Matszangosz, Varga and Weiner study triplets of MUBs under
+conjectural sufficient conditions, Section~4 of their preprint.
+C\'ardenes Wuttig and Tindall classify order-six Hadamard matrices
+completely and leave MUB extendibility open. Only the combination of a
+finite cover of all second bases with the local exclusion, executed
+under a certified arithmetic contract, yields an unconditional upper
+bound.
+
+{\small\url{https://arxiv.org/pdf/2503.14752}}
+
+{\small\url{https://arxiv.org/pdf/2608.18053}}
+
+\medskip\noindent\textbf{The strategy at a glance.}
The proof has five layers, each of which strictly refines the previous
one and preserves every exact candidate solution.
\begin{enumerate}
-\item \textbf{Seed cover (Section~\ref{sec:seed}).}
+\item \textbf{Seed cover.}
Row and column rephasings and transpositions place any $H$ into a
standard form with $9$ free phases. A symmetry reduction plus
necessary interval tests cover the possible values of these nine
phases by finitely many seed balls (radius $0.0320001$ in cycle units).
-\item \textbf{Completion (Section~\ref{sec:completion}).}
+\item \textbf{Completion.}
In a block decomposition of $H$ with row and column sizes $2+4$, the
seed pins down the upper-left, upper-right and lower-left blocks. The
lower-right $4\times 4$ block is the only remaining unknown. At any
@@ -285,15 +265,15 @@ one and preserves every exact candidate solution.
$U(2)$ therefore accounts for every feasible completion, and uniform
Taylor bounds within each cell either exclude the cell or place all
its exact completions in a certified phase ball
- (Sections~\ref{sec:completion} and~\ref{sec:phase-cover}).
-\item \textbf{Refinement (Section~\ref{sec:refinement}).}
+ ( and~\ref{sec:phase-cover}).
+\item \textbf{Refinement.}
Each phase ball carries numerical tangent directions and a rigorous
residual-identity estimate; covering the tangent coordinates while
keeping the residual bound yields smaller balls that still cover
every exact solution. No manifold parametrization is used, and the
estimates remain valid even when the proposed center is not an exact
Hadamard matrix.
-\item \textbf{Exclusion (Section~\ref{sec:exclusion}).}
+\item \textbf{Exclusion.}
For a final phase ball, a small phase-bin search covers every vector
unbiased to both the standard basis and $H/\sqrt6$ by closed vector
balls. These vector balls become vertices of two graphs, one for
@@ -301,7 +281,7 @@ one and preserves every exact candidate solution.
remove only impossible edges. Two additional MUB bases would require
two disjoint six-cliques with all $36$ cross edges present; that
pattern is ruled out by finite search.
-\item \textbf{Execution certificate (Section~\ref{sec:execution}).}
+\item \textbf{Execution certificate.}
A complete run of the four programs, on a specific build and platform,
accounts for every seed, every refined ball, and every initially
unresolved record. Nothing is left open: a record that is not
@@ -315,7 +295,7 @@ the argument is a chain of strictly finer covers; each exclusion uses
only a \emph{necessary} condition with a \emph{certified} margin; and no
step in the chain ever relies on a floating-point center being exact.
-\subsection{The elementary lower bound}\label{subsec:lower}
+\medskip\noindent\textbf{The elementary lower bound.}
The lower bound uses only the tensor-product construction. We give it
explicitly so the reader can see that attainment of three bases is
@@ -364,7 +344,7 @@ modulus $(1/2)(1/3)=1/6$. Thus the three bases are mutually unbiased,
and $U_0=I_6$.
\end{proof}
-\subsection{A Lie-algebra consequence}
+\medskip\noindent\textbf{A Lie-algebra consequence.}
An orthonormal basis $\mathcal B$ of $\C^6$ determines its Cartan
subalgebra $\mathfrak h_{\mathcal B}$ of traceless matrices that are
@@ -385,35 +365,41 @@ adjoint condition.
\begin{corollary}[Adjoint-closed Cartan subalgebras]
\label{cor:adjoint-cartan}
Under the arithmetic and compiler conditions of
-Appendix~\ref{sec:rounding}, using the complete execution documented in
-Section~\ref{sec:execution} as in Theorem~\ref{thm:main}, the maximum
+the certified arithmetic, using the complete execution recorded above
+and certified in Theorem~\ref{thm:main}, the maximum
number of pairwise Killing-orthogonal Cartan subalgebras of
$\mathfrak{sl}_6(\C)$ that are all closed under the standard adjoint
$X\mapsto X^*=\overline X^{\,T}$ is three.
\end{corollary}
\begin{proof}
-By~\cite[Theorem 5.2]{BoykinSitharamTiepWocjan2005}, such collections
-of Cartan subalgebras correspond to collections of mutually unbiased
-orthonormal bases of the same cardinality. Theorem~\ref{thm:main} gives
-the upper bound under its stated contract, and
+By Theorem 5.2 of Boykin, Sitharam, Tiep and Wocjan, such collections of
+Cartan subalgebras correspond one-to-one to collections of mutually
+unbiased orthonormal bases of the same cardinality. Theorem~\ref{thm:main}
+gives the upper bound under its stated contract, and
Lemma~\ref{lem:three-mub-six} gives attainment.
\end{proof}
+{\small\url{https://arxiv.org/pdf/quant-ph/0506089}}
+
% =====================================================================
-\section{Equivalences and an exhaustive seed cover}
+\medskip\noindent\textbf{Equivalences and an exhaustive seed cover.}
\label{sec:seed}
% =====================================================================
-The goal of this section is the first layer of the cover: replace every
-possible second basis by one of finitely many nine-phase seed balls. The
-strategy (closed phase discretization plus necessary compatibility tests)
-follows \cite[Section 3]{JamingEtAl2009} and
-\cite[Sections 2--3]{JamingMatolcsiMora2010}; what is new is the specific
-symmetry reduction and shared-coordinate estimate that prove completeness
-of this exact cover.
+The first layer of the cover replaces every possible second basis by one
+of finitely many nine-phase seed balls. The strategy, closed phase
+discretization plus necessary compatibility tests, follows Section 3 of
+Jaming, Matolcsi, M\'ora, Sz\"oll\H osi and Weiner. The unrestricted
+programme is set out in Sections 2--3 of the later survey by Jaming,
+Matolcsi and M\'ora. What is new is the specific symmetry reduction and
+shared-coordinate estimate that prove completeness of this exact cover.
+
+{\small\url{https://arxiv.org/pdf/0902.0882}}
+
+{\small\url{https://arxiv.org/pdf/1201.0640}}
-Throughout we use phases in cycles and write $e(t)=\exp(2\pi i t)$
+Throughout, phases are in cycles and $e(t)=\exp(2\pi i t)$
entrywise. Matrix indices run $0,\ldots,5$, entries are stored in
row-major order with $(i,j)$ in position $6i+j$, and the Hermitian inner
product is $\langle u,v\rangle=\sum_j\overline{u_j}v_j$. Vectors and
@@ -422,7 +408,7 @@ norms are induced Euclidean unless noted. An angle is in radians only
when explicitly stated.
% ---------------------------------------------------------------
-\subsection{Equivalences and phase gauges}
+\medskip\noindent\textbf{Equivalences and phase gauges.}
% ---------------------------------------------------------------
\begin{definition}\label{seed:extendibility}
@@ -494,7 +480,7 @@ a legitimate phase representative; no rounded decision at a half-integer
is claimed to be uniquely preferred.
% ---------------------------------------------------------------
-\subsection{A symmetry arrangement for nine phases}
+\medskip\noindent\textbf{A symmetry arrangement for nine phases.}
% ---------------------------------------------------------------
The \emph{gap} of a finite circular multiset is its largest circular
@@ -627,7 +613,7 @@ For a $Y$ tuple it sorts a copy solely for this computation, preserving
the stored shared-first ordering.
% ---------------------------------------------------------------
-\subsection{Vanishing-sum filters and the shared displacement}
+\medskip\noindent\textbf{Vanishing-sum filters and the shared displacement.}
% ---------------------------------------------------------------
For either of the two lists $x$ or $y$, let $u=(u_0,\ldots,u_4)$ be its
@@ -667,7 +653,7 @@ residual direction and in directions perpendicular to the five
unit-exponential columns. Since the inequality holds for every real
direction, their numerical construction need not reproduce any
prescribed exact direction. One-sided margins for evaluating the
-residuals and supports are established in Appendix~\ref{sec:rounding}.
+residuals and supports are established in the certified arithmetic.
In grid units $h=N\Delta$, write
\begin{equation}\label{seed:grid-error}
@@ -706,7 +692,7 @@ these constraints using the shared column direction and directions
perpendicular to the other four columns; here $t=s$ for $X$ and $t=0$
for $Y$. It skips divisors of magnitude below $10^{-6}$, which only
removes a constraint. Numerator and endpoint margins enlarge the
-computed intervals (Appendix~\ref{sec:rounding}). The pair is rejected
+computed intervals (the certified arithmetic). The pair is rejected
only when the two intervals are strictly disjoint; a common endpoint is
retained.
@@ -719,10 +705,10 @@ tails and applies \texttt{sumok}. The program \texttt{covout} matches
the shared bin, applies the second gap inequality, and intersects the
shared displacement intervals. So every discarded exact solution would
violate one of these necessary conditions. Numerical gap comparisons
-include outward slack (Appendix~\ref{sec:rounding}).
+include outward slack (the certified arithmetic).
% ---------------------------------------------------------------
-\subsection{Certified reuse of seed centers}
+\medskip\noindent\textbf{Certified reuse of seed centers.}
% ---------------------------------------------------------------
The nine seed coordinates, before moving the selected column, are
@@ -789,7 +775,7 @@ right side of~\eqref{seed:dual-formula}. Validity of a proposal is
independent of how it was generated and of the accuracy of the
heuristic linear solve; only finite components of magnitude at most
$10^4$ are used. Its evaluation replaces $1.25\pi/N$ by the larger
-$1.251\pi/N$ and adds a final support margin; Appendix~\ref{sec:rounding}
+$1.251\pi/N$ and adds a final support margin; the certified arithmetic
proves the resulting bound is conservative.
Set $R=0.032$. For a proposed previous center, \texttt{testBucket} first
@@ -814,12 +800,12 @@ stage. Centers retained earlier for the same $X$ tuple are handled
identically, with the first five components of $k$ zero.
% ---------------------------------------------------------------
-\subsection{The exhaustive seed cover proposition}
+\medskip\noindent\textbf{The exhaustive seed cover proposition.}
% ---------------------------------------------------------------
\begin{proposition}[Exhaustive seed cover]\label{seed:cover}
For a completed execution of the specified \texttt{covout} traversal
-under the arithmetic conditions of Appendix~\ref{sec:rounding}, the
+under the arithmetic conditions of the certified arithmetic, the
written rational midpoint centers, equipped with their recorded selected
positions, cover the seed coordinates of every exact complex Hadamard
matrix up to the equivalences of Lemma~\ref{seed:equivalences}, by
@@ -853,7 +839,7 @@ centers are tried can only cause further midpoint insertions; retained
centers remain and are included in the output.
The common selected-position permutation preserves all these distances.
-Appendix~\ref{sec:rounding} bounds the joint error of the nine binary
+the certified arithmetic bounds the joint error of the nine binary
midpoint phases by less than $10^{-14}$, so the triangle inequality
permits the enlarged radius $0.0320001$. The centers need not themselves
satisfy the exact Hadamard equations; their balls cover the necessary
@@ -861,7 +847,7 @@ seed coordinates of all exact solutions.
\end{proof}
% =====================================================================
-\section{Completion over a fixed seed ball}
+\medskip\noindent\textbf{Completion over a fixed seed ball.}
\label{sec:completion}
% =====================================================================
@@ -869,12 +855,12 @@ This section reduces "complete the seed phase ball to a full dephased
Hadamard matrix" to a covering of the $2\times 2$ unitary group $U(2)$.
The reference frames are fixed at the seed center; the center itself is
not assumed to be an exact Hadamard matrix. All statements are first
-proved in exact real and complex arithmetic; Appendix~\ref{sec:rounding}
+proved in exact real and complex arithmetic; the certified arithmetic
replaces each inequality by an outward-computed version with a certified
margin.
% ---------------------------------------------------------------
-\subsection{Seed blocks and fixed complementary frames}
+\medskip\noindent\textbf{Seed blocks and fixed complementary frames.}
% ---------------------------------------------------------------
Fix the stored seed center and take its binary phase coordinates as
@@ -969,14 +955,14 @@ certify that these choices are well defined. A failed frame check leaves
the seed unresolved and never excludes it.
% ---------------------------------------------------------------
-\subsection{A unitary associated to every feasible completion}
+\medskip\noindent\textbf{A unitary associated to every feasible completion.}
% ---------------------------------------------------------------
The polar decomposition associates a unitary with any nonsingular square
matrix, and its nearest-unitary property in unitarily invariant norms is
-classical~\cite[Theorem 1]{FanHoffman1955}; see also
-\cite[Theorem 1.1 and Corollary 2.3]{Higham1986Polar}. Here the
-compressed completion has an explicit positive defect.
+classical: Theorem 1 of Fan and Hoffman, and Theorem 1.1 with Corollary
+2.3 of Higham's 1986 study. Here the compressed completion has an
+explicit positive defect.
\begin{lemma}[Polar comparison]\label{completion:polar}
For a feasible completion let $Y=K_C^*D'K_B$. Then
@@ -1025,12 +1011,12 @@ proves~\eqref{completion:polar-bound}.
The inequality $q<6$ is checked using outward bounds; in the specified
parameter range the stronger $q<.32$ follows from the accepted frame
-checks and the seed radius (Section~\ref{sec:rounding}). Hence every
+checks and the seed radius. Hence every
feasible completion of an accepted seed ball is assigned at least one
$V\in U(2)$.
% ---------------------------------------------------------------
-\subsection{The unitary cells and their Taylor bounds}
+\medskip\noindent\textbf{The unitary cells and their Taylor bounds.}
% ---------------------------------------------------------------
\begin{lemma}[A closed covering of $U(2)$]\label{completion:unitary-cover}
@@ -1114,7 +1100,7 @@ angular derivatives assembled by \texttt{uc::init} and
\texttt{uc::initDeriv}.
% ---------------------------------------------------------------
-\subsection{Comparison with a cell center}
+\medskip\noindent\textbf{Comparison with a cell center.}
% ---------------------------------------------------------------
For the fixed seed and unitary cell define
@@ -1212,7 +1198,7 @@ $\sqrt6$.
\end{proof}
% ---------------------------------------------------------------
-\subsection{A uniform linearization remainder}
+\medskip\noindent\textbf{A uniform linearization remainder.}
% ---------------------------------------------------------------
Let $E_1,B_1,C_1$ be the seed first variations: at a varied entry,
@@ -1325,7 +1311,7 @@ and moving parts of \texttt{block::setup}, \texttt{makeD}, and
\texttt{makeJ}.
% ---------------------------------------------------------------
-\subsection{Necessary flatness and separating inequalities}
+\medskip\noindent\textbf{Necessary flatness and separating inequalities.}
% ---------------------------------------------------------------
We have bounded the total block displacement $Z=D'-D$ by $z$ and its
@@ -1442,18 +1428,18 @@ Stage A path is \texttt{Asearch::testA}; the auxiliary
\texttt{Usearch::test} and \texttt{scalar} routines do not supply
additional exclusion tests for this run. The actual norm and
directional comparisons include the margins proved in
-Appendix~\ref{sec:rounding}.
+the certified arithmetic.
% ---------------------------------------------------------------
-\subsection{Finite recursion and unresolved cells}
+\medskip\noindent\textbf{Finite recursion and unresolved cells.}
% ---------------------------------------------------------------
\begin{proposition}[Completion coverage conditional on successful
termination]\label{completion:recursion}
Fix a seed ball whose frame and bound constructions are certified.
Suppose every final unitary cell is either excluded by a certified
-necessary-condition test or covered by a certified phase ball as in
-Section~\ref{sec:phase-cover}. Then those phase balls cover every
+necessary-condition test or covered by a certified phase ball, as in
+the certified arithmetic. Then those phase balls cover every
feasible Hadamard completion of the seed ball, up to the equivalences
of the phase-ball certificates. The Stage A recursion establishes
exactly this if it terminates with zero unresolved cells.
@@ -1499,11 +1485,11 @@ remainder; these conditions are part of the computational obligation.
They do not follow from the local inequalities alone.
% =====================================================================
-\section{Certified phase balls and their atlas}
+\medskip\noindent\textbf{Certified phase balls and their atlas.}
\label{sec:phase-cover}
% =====================================================================
-This section converts a cell retained by Section~\ref{sec:completion}
+This section converts a cell retained by
into a ball of real phase matrices. For a center $P$, $e(P)$ need not be
an exact Hadamard matrix; the certificates control the center's residual
and the displacement of every exact solution inside the ball. Phase
@@ -1515,7 +1501,7 @@ lies in $\operatorname{ran}\Pi$. All vector norms are Euclidean, phase
matrix norms are Frobenius, and stars on real matrices mean transpose.
% ---------------------------------------------------------------
-\subsection{Residual and Root certificates}
+\medskip\noindent\textbf{Residual and Root certificates.}
\label{sec:root-certificate}
% ---------------------------------------------------------------
@@ -1535,7 +1521,7 @@ notation is
\end{equation}
The factor $2\pi i$ from differentiation cancels the denominator
in~\eqref{phase:residual}. These are the residual and full derivative in
-\texttt{buildH::gen} (in \texttt{patchx.cpp}).
+\texttt{buildH::gen}.
\begin{definition}[Root certificate]\label{phase:root-data}
A \texttt{Root} consists of a stored real center $P$, a stored real
@@ -1592,7 +1578,7 @@ constant-rank or manifold hypothesis on the exact solution set is used.
\end{remark}
% ---------------------------------------------------------------
-\subsection{Constructing Root certificates}
+\medskip\noindent\textbf{Constructing Root certificates.}
% ---------------------------------------------------------------
The construction uses an auxiliary real map $M:\R^{30}\to\R^{36}$ that
@@ -1739,15 +1725,15 @@ possibly inexact $P+v$.
\end{proof}
The combination of a numerical factorization with a checked Gram defect
-is standard in verified matrix-norm estimation; compare
-\cite{Rump2011VerifiedSingularValues}. The bounds are derived from the
-displayed residual identities and the source-specific arithmetic
-estimates, including the error in the proposed tangent frame.
+is standard in verified matrix-norm estimation, as in Rump's 2011
+study of verified singular-value bounds. The bounds come from the
+displayed residual identities and the certified arithmetic estimates,
+including the error in the proposed tangent frame.
-\begin{proposition}[Certificates produced by the source]
+\begin{proposition}[Certificates from the direct checks]
\label{phase:stored-root-certificate}
A successful call to \texttt{buildH::patch} under the arithmetic
-conditions of Appendix~\ref{sec:rounding}
+conditions of the certified arithmetic
certifies~\eqref{phase:root-basic},
\eqref{phase:projector-certificate}, and a valid remainder constant $C$
in the sense of Definition~\ref{phase:root-data}.
@@ -1755,8 +1741,8 @@ in the sense of Definition~\ref{phase:root-data}.
\begin{proof}
The direct checks, not the accuracy of the proposed eigendecomposition,
-establish the assertion. The source proposes an approximate horizontal
-basis and a splitting of the $25$-coordinate horizontal Jacobian.
+establish the assertion. An approximate horizontal basis is proposed
+together with a splitting of the $25$-coordinate horizontal Jacobian.
Eigenvalues below $.64$ propose columns of $T$; the rest propose factors
$H_V,L_V$ for $M$. Every accepted factor entry has magnitude at most
$2$, and at most $25$ columns occur. More than $10$ proposed $T$ columns
@@ -1766,36 +1752,36 @@ Certified absolute row sums of the column Grams of $H_V,L_V$ bound their
squared operator norms. The bound $\mathtt{mnorm}$ also includes the
difference between the accumulated stored $M$ and the exact product
$H_VL_V^*$. The required additions and the $2.1\cdot 10^{-11}$
-Frobenius bound on this difference are proved in
-Section~\ref{round:root}. Thus $\mathtt{mnorm}$ bounds the actual
-stored map, and the first choice in Lemma~\ref{phase:remainder-constants}
+Frobenius bound on this difference are proved in the certified
+arithmetic. Thus $\mathtt{mnorm}$ bounds the actual stored map, and the
+first choice in Lemma~\ref{phase:remainder-constants}
supplies a certified $C$.
-For the optional tensor improvement the source forms the row Gram
-\eqref{phase:tensor-gram} and proposes a real change of basis $U$ with a
-checked upper $\beta$ for $\|U^*U-I\|$. If $\beta<.1$ then
-$\|U^{-1}\|^2\le 1/(1-\beta)$. A certified absolute-row-sum bound $r$
-for $U^*(\mathcal S\mathcal S^*)U$ gives
+For the optional tensor improvement the row Gram
+\eqref{phase:tensor-gram} is formed, and a real change of basis $U$ is
+proposed with a checked upper $\beta$ for $\|U^*U-I\|$. If
+$\beta<.1$ then $\|U^{-1}\|^2\le 1/(1-\beta)$. A certified absolute row
+sum bound $r$ for $U^*(\mathcal S\mathcal S^*)U$ gives
$\|\mathcal S\|^2\le r/(1-\beta)$. This uses congruence by an
invertible matrix, not assumed orthogonal diagonalization. The second
choice in Lemma~\ref{phase:remainder-constants}, with the one-sided
-margins in Section~\ref{round:root}, gives the alternative $C$. Both
+margins certified alongside it, gives the alternative $C$. Both
are upper bounds, so their minimum is allowed.
-Finally the source evaluates the full $36$-coordinate identity
-in~\eqref{phase:projector-certificate}, not just its proposed horizontal
-form. The padded Frobenius residual gives $\mathtt{id}$. Corresponding
-checks on $T^*T-I$, $(I-\Pi)T$, $F(P)$ give the basic bounds, and the
-stored $\mathtt{n0}$ is an upper bound for
-$\mathtt{mnorm}\,\mathtt{froot}$. Section~\ref{round:root} proves the
-one-sided error estimates for all these checks and records their
+Finally the full $36$-coordinate identity
+in~\eqref{phase:projector-certificate} is evaluated, not just its
+proposed horizontal form. The padded Frobenius residual gives
+$\mathtt{id}$. Corresponding checks on $T^*T-I$, $(I-\Pi)T$ and $F(P)$
+give the basic bounds, and the stored $\mathtt{n0}$ is an upper bound
+for $\mathtt{mnorm}\,\mathtt{froot}$. The certified arithmetic proves
+the one-sided error estimates for all these checks and records their
acceptance thresholds. Replacing operator norms by Frobenius norms only
-enlarges the bounds,
-so Proposition~\ref{phase:root-bounds} applies to every successful call.
+enlarges the bounds, so Proposition~\ref{phase:root-bounds} applies to
+every successful call.
\end{proof}
% ---------------------------------------------------------------
-\subsection{Transport and alignment}
+\medskip\noindent\textbf{Transport and alignment.}
% ---------------------------------------------------------------
Callbacks in \texttt{variants} select a real $6\times 6$ signed
@@ -1853,17 +1839,17 @@ Lemma~\ref{seed:equivalences}.
The standard \texttt{dephase} and \texttt{wrap} operations produce the
integer choices in $\Delta$; the exact $\Delta$ used in the arguments
-below is the ideal one, and Section~\ref{sec:rounding} bounds the
+below is the ideal one, and bounds the
computed vs.\ ideal difference.
% ---------------------------------------------------------------
-\subsection{Displacement bounds for a retained cell}
+\medskip\noindent\textbf{Displacement bounds for a retained cell.}
% ---------------------------------------------------------------
Fix a retained cell. Its seed displacement satisfies $\|s\|\le R_s$, its
angular box satisfies $|\theta_a|\le h$, $1\le a\le 4$, and
$Z=D'-D$ has $\|Z\|_F\le z$ and $\|Z-\mathcal J(s,\theta)\|_F\le E_r$ as
-in Section~\ref{sec:completion}. Let $\mathcal I_s=(7,8,9,10,11,13,19,25,31)$
+in . Let $\mathcal I_s=(7,8,9,10,11,13,19,25,31)$
denote the nine seed indices, and $\mathcal I_D$ the sixteen lower-right
indices $(i,j)$ with $2\le i,j\le 5$. The first row and column have zero
raw displacement.
@@ -1914,7 +1900,7 @@ The subtraction $10^{-6}$ from each computed magnitude gives $\mathtt{mi}$
and the upper reciprocal
$\mathtt{invmag}_j=1/(m_j-10^{-6})+10^{-9}$. The ratio has $10^{-7}$ added
and the final arc quantities each have $10^{-8}$ added.
-Section~\ref{sec:rounding} shows these numbers have the one-sided
+ shows these numbers have the one-sided
properties of Lemma~\ref{phase:arc-bounds} for the ideal comparison
block. Failure of any check means failure to cover this cell by this
route, not an exclusion of the cell.
@@ -1974,8 +1960,8 @@ further: the seed coordinates in $u$ are exactly $s$, and the identity
$\|u\|^2=\|s\|^2+\|d\|^2$ gives~\eqref{phase:raw-displacement}.
The stored center $P_0$ differs from an exact solution by
$\epsilon+u/(2\pi)$ up to integer entries. Dephasing an exact phase matrix
-changes $P_0$ by less than $2\cdot 10^{-6}$ cycles per entry, as proved in
-Section~\ref{round:candidate}.
+changes $P_0$ by less than $2\cdot 10^{-6}$ cycles per entry, as proved
+in the certified arithmetic.
\end{proof}
\begin{lemma}[A direct displacement bound]
@@ -2011,7 +1997,7 @@ add $\|\Pi\epsilon\|\le\|\epsilon\|$ by the triangle inequality.
\end{proof}
% ---------------------------------------------------------------
-\subsection{Ellipsoid tangent bounds}
+\medskip\noindent\textbf{Ellipsoid tangent bounds.}
% ---------------------------------------------------------------
Partition $X=(X_s,X_\theta)$, and let $T_s,T_D$ be the rows of $T$
@@ -2106,21 +2092,21 @@ Lemma~\ref{phase:ellipsoid-norm}. Two valid tangent bounds are
\label{phase:tangent-direct}
\end{align}
-\paragraph{Numerical realization.} In \texttt{covercompute},
+\textbf{Numerical realization.} In \texttt{covercompute},
\texttt{off} is the computed $2\pi T^*\Delta$; \texttt{AB} is the
computed $T^*X$; \texttt{U} holds the $16$ corners. The covariance uses
the stored \texttt{AB} coefficients and charges their ideal-coefficient
-error separately outside the ellipsoid. Section~\ref{sec:rounding} gives
+error separately outside the ellipsoid. gives
$\|\widehat A-T^*X\|<1.5\cdot 10^{-5}$,
$\|(s,\theta)\|<.226$, so this substitution costs less than
$3.4\cdot 10^{-6}$ radians. For both covariance choices a diagonal
$10^{-7}I$ is added. The inverses in the second choice are certified
-upper \texttt{invmag} values. Section~\ref{sec:rounding} proves PSD
+upper \texttt{invmag} values. proves PSD
domination of the exact covariance expressions in the stored-coefficient
model.
% ---------------------------------------------------------------
-\subsection{Bootstrap and local coverage}
+\medskip\noindent\textbf{Bootstrap and local coverage.}
% ---------------------------------------------------------------
\begin{proposition}[Finite improvement of a certified radius]
@@ -2148,7 +2134,7 @@ strict improvements preserve the conclusion at the stopping point.
\end{proof}
% ---------------------------------------------------------------
-\subsection{Atlas merge of certified balls}
+\medskip\noindent\textbf{Atlas merge of certified balls.}
% ---------------------------------------------------------------
For a recorded phase ball, the \texttt{Atlas} stores the Root $(P,T)$, the
@@ -2181,7 +2167,7 @@ equivalence, so it contains the aligned representative. Inflate to
$r_P\vee d_{PQ}+r_Q$ and add the outward allowance.
\end{proof}
-The implementation in \texttt{atlas.cpp} uses \texttt{mapH} for $\Phi$.
+The implementation uses \texttt{mapH} for $\Phi$.
Its two index arrays are genuine permutations. In \texttt{variants}, the
leading two row indices are distinct and \texttt{complement} supplies
the other four. The six column labels remain attached to six distinct
@@ -2202,9 +2188,9 @@ maps need not be a canonical invariant.
\texttt{Atlas::find} computes an explicit wrapped dephased difference,
projects it, and evaluates its norm. On success it adds $10^{-7}$ to the
-computed norm, exceeding the dephasing/projection errors certified in
-Section~\ref{sec:rounding}. \texttt{Atlas::add} grows the selected radius
-to at least the incoming radius plus this distance, with another
+computed norm, exceeding the dephasing and projection errors certified
+by the arithmetic bounds above. \texttt{Atlas::add} grows the selected
+radius to at least the incoming radius plus this distance, with another
$10^{-8}$ added and a separate $2\cdot 10^{-8}$-margin comparison to the
cap. It remains valid when an alternative map found by \texttt{variants}
supplied the distance; only existence of that allowed map is needed.
@@ -2236,7 +2222,7 @@ every merge preserves their solution sets up to equivalence
overlapping assignments are harmless.
\end{proof}
-\paragraph{Finite bounds.} The control flow has explicit finite bounds.
+\textbf{Finite bounds.} The control flow has explicit finite bounds.
Before filtering, the nondecreasing five-bin lists for the seed cover
number at most $\binom{116}{5}=160{,}389{,}488$, and for any fixed shared
bin the four ordered tail bins number at most
@@ -2257,7 +2243,7 @@ successful. The local candidate list uses \texttt{topK=4} in an array of
size~$8$.
% =====================================================================
-\section{Refining the phase-ball cover}
+\medskip\noindent\textbf{Refining the phase-ball cover.}
\label{sec:refinement}
% =====================================================================
@@ -2265,7 +2251,7 @@ Stage B replaces a finite collection of certified phase balls by balls of
a smaller prescribed radius. Centers need not be exact Hadamard matrices,
and no regularity assumption on the Hadamard locus is made. The tangent
coordinates used below organize an exhaustive search; the normal
-estimates from Section~\ref{sec:phase-cover} control the remaining
+estimates from control the remaining
directions. A phase matrix is identified with a vector in $\R^{36}$;
stars mean real transpose; $\mathcal V=\operatorname{im}\Pi$ is the
horizontal subspace.
@@ -2283,7 +2269,7 @@ therefore sufficient even when different parts use different
arrangements of the same matrix.
% ---------------------------------------------------------------
-\subsection{Certified relations between centers}
+\medskip\noindent\textbf{Certified relations between centers.}
% ---------------------------------------------------------------
For a Root at $P$ denote its stored tangent matrix $T:\R^k\to\R^{36}$
@@ -2416,7 +2402,7 @@ $d^2=\|h'\|^2\le n_Q(d)^2+(1+o_Q)\|S^*h'\|^2$.
\end{proof}
% ---------------------------------------------------------------
-\subsection{Uniform iteration without contraction}
+\medskip\noindent\textbf{Uniform iteration without contraction.}
% ---------------------------------------------------------------
The relation estimates yield a useful upper iteration without requiring
@@ -2462,7 +2448,7 @@ stopping preserve the conclusion.
\end{proof}
% ---------------------------------------------------------------
-\subsection{The rho search for usable tangent thresholds}
+\medskip\noindent\textbf{The rho search for usable tangent thresholds.}
% ---------------------------------------------------------------
Fix a certified parent Root $P,T$ and a reference center $Q,S$ (an atlas
@@ -2529,7 +2515,7 @@ check aborts. Thus even an unfavorable rounded reevaluation cannot
silently assign a box to a sphere too small to contain it.
% ---------------------------------------------------------------
-\subsection{Exhaustive grid in tangent coordinates}
+\medskip\noindent\textbf{Exhaustive grid in tangent coordinates.}
% ---------------------------------------------------------------
For every parent solution in the parent record,
@@ -2544,7 +2530,7 @@ and chooses
L=\left\lceil E/w+0.500001\right\rceil,\qquad n=2L+1,
\]
with the stated rounded evaluation. The arithmetic of
-Section~\ref{sec:rounding} ensures that the outer endpoints
+ ensures that the outer endpoints
$\pm(L+1/2)w$ contain $[-E_P,E_P]$.
For $u\in\R^k$ and $h\ge 0$ write
@@ -2556,7 +2542,7 @@ union contains $[-E_P,E_P]^k$, so every tangent vector
in~\eqref{refine:tangent-range} belongs to at least one base box. All
intervals are closed; grid boundaries are included.
-\subsection{Blocker induction}
+\medskip\noindent\textbf{Blocker induction.}
A \emph{blocker} is an earlier input parent whose entire refinement has
succeeded. It is queried at its original fixed radius. An atlas child,
@@ -2567,8 +2553,8 @@ become a blocker.
\begin{proposition}\label{refine:cover-preservation}
Suppose Stage B runs on a finite list of records with valid Root
-certificates, under the arithmetic assumptions and error bounds of
-Section~\ref{sec:rounding}. On a completed run, let $\mathcal A$ be the
+certificates, under the arithmetic assumptions and error bounds
+described above. On a completed run, let $\mathcal A$ be the
final atlas of children and $\mathcal B$ the list of input parents
whose refinement failed. Then
\begin{equation}\label{refine:cover-inclusion}
@@ -2620,7 +2606,7 @@ Later radius growth cannot invalidate an earlier certificate, because
centers and Root constants are immutable and the corresponding
solution sets only enlarge.
-\subsection{Batch files and finite failure conditions}
+\medskip\noindent\textbf{Batch files and finite failure conditions.}
Batching writes appended atlas Roots in their insertion order, in groups
of at most $256$. The radius written for each Root is the common cap
@@ -2663,26 +2649,25 @@ $8{,}000{,}000$. The grid product is checked before multiplication past
its limit. Within the admitted ranges $L\le 1262$; the mixed-radix
indices fit the stated integer types, and every split uses at most
$2^{10}$ children. The integer and floating-point bounds are recorded
-in Section~\ref{sec:rounding}.
+in the arithmetic bounds above.
% =====================================================================
-\section{Excluding two further mutually unbiased bases}
+\medskip\noindent\textbf{Excluding two further mutually unbiased bases.}
\label{sec:exclusion}
% =====================================================================
-The final stage (called ``C'' in the source) takes a certified Root
-$(P,T)$ with $0\le r\le .03$ and rules out two more mutually unbiased
-orthonormal bases in the phase ball of radius $r$. We divide the phase
-variables of the two extra bases into closed balls, retain a permissive
-graph of necessary edge relations, and then run a finite search for the
-required clique pattern. Every rejection is a strict violation of a
-necessary condition with a certified margin; no rejection depends on a
-center being exact.
-
-Throughout, $e(t)=\exp(2\pi i t)$. A real matrix in $\R^{36}$ is iden-
-tified with row-major indexing. The Root constants $\omega,n_0,\iota,
-\Gamma$ denote $\mathtt{ort},\mathtt{n0},\mathtt{id},\mathtt{C}$ as in
-Section~\ref{sec:phase-cover}. Its certified data give
+The final stage takes a certified Root $(P,T)$ with $0\le r\le .03$ and
+rules out two more mutually unbiased orthonormal bases in the phase ball
+of radius $r$. The phase variables of the two extra bases are divided
+into closed balls, a permissive graph of necessary edge relations is
+retained, and a finite search runs for the required clique pattern.
+Every rejection is a strict violation of a necessary condition with a
+certified margin; no rejection depends on a center being exact.
+
+Throughout, $e(t)=\exp(2\pi i t)$. A real matrix in $\R^{36}$ is
+identified with row-major indexing. The Root constants $\omega,n_0$,
+$\iota,\Gamma$ denote $\mathtt{ort},\mathtt{n0},\mathtt{id},\mathtt{C}$
+as in the arithmetic bounds above. Its certified data give
\begin{equation}\label{exclude:root-data}
\|T^*T-I\|\le\omega,\qquad
\|F(P)\|\le f_0<10^{-6},\qquad 0\le\omega<10^{-5},
@@ -2712,7 +2697,7 @@ $\|AA^*-6I\|_F=2\pi\sqrt2\,\|F(P)\|$ and~\eqref{exclude:root-data} give
where $A=e(P)$.
% ---------------------------------------------------------------
-\subsection{Closed phase bins}
+\medskip\noindent\textbf{Closed phase bins.}
% ---------------------------------------------------------------
At resolution $M$ the five variable phases are covered by closed
@@ -2849,7 +2834,7 @@ normalizes by that maximum, and uses the resulting stored coefficients
as the test direction. The stored direction itself is what matters.
% ---------------------------------------------------------------
-\subsection{From bins to closed vector balls}
+\medskip\noindent\textbf{From bins to closed vector balls.}
% ---------------------------------------------------------------
The initial resolution is $M=12$. Every bin is tested, and each retained
@@ -2896,15 +2881,15 @@ cutoff is simply not used; the bin is assigned to another center or to
a newly inserted midpoint. Thus no bin is dropped by the heuristic. For
each assigned center the radius is updated to the maximum of the
computed projected midpoint distance plus the bin-norm upper bound and
-$10^{-9}$; this is an outward upper bound as certified in
-Section~\ref{sec:rounding}. New midpoint centers use midpoint distance
+$10^{-9}$; this is an outward upper bound, as certified in the
+arithmetic bounds above. New midpoint centers use midpoint distance
zero, with the same allowance.
The earlier Lloyd iterations adapt the nearest-center/centroid heuristic
-of \cite[Sections IV--VI]{Lloyd1982}. They may move centers, but a
-subsequent complete assignment follows each such movement. In the last
-iteration the assigned centers are not moved. Deleting centers with no
-assigned bins cannot lose coverage. The returned centers and radii
+of Lloyd's 1982 least-squares quantization paper. They may move centers,
+but a subsequent complete assignment follows each such movement. In the
+last iteration the assigned centers are not moved. Deleting centers with
+no assigned bins cannot lose coverage. The returned centers and radii
therefore meet the covering assertion. An attempt to exceed $2048$
centers, or a failure of the final checks $|v_j|\le 2$ and $0\le s<.1$,
is unresolved rather than negative.
@@ -2941,7 +2926,7 @@ has one of these two relations, so no pair shares its ball.
% ---------------------------------------------------------------
-\subsection{Bin geometry and edge tests}
+\medskip\noindent\textbf{Bin geometry and edge tests.}
% ---------------------------------------------------------------
\begin{lemma}[Bin geometry]
@@ -2950,7 +2935,7 @@ Fix a bin with midpoint $u\in\R^6$ ($u_0=0$) and halfwidth
$a=1/(2M)$. Any phase vector in the bin is $u+d$ with $d_0=0$ and
$|d_j|\le a$ for $j\ge1$. The horizontal displacement
$x=d-\frac16(\sum_jd_j){\bf 1}$ satisfies $\sum_jx_j=0$ and, with the
-constants $X_M,L_M,I_M$ of Section~\ref{round:single},
+constants $X_M,L_M,I_M$ of ,
\begin{equation}\label{exclude:bin-norms}
\|x\|\le X_M,\quad \|x\|_1\le L_M,\quad \|x\|_\infty\le I_M.
\end{equation}
@@ -2961,7 +2946,7 @@ $\sum_jx_j=0$ is immediate from the definition.
Write $d=\bar d+(d-\bar d)$ with $\bar d=(1/6)\sum_jd_j$. Then
$\|x\|^2=\|d-\bar d{\bf 1}\|^2=\|d\|^2-6\bar d^2\le\|d\|^2\le5a^2$,
so $X_M\ge\sqrt5\,a$ suffices. Each $|d_j-\bar d|\le 2a$, so
-$L_M\ge10a$ and $I_M\ge2a$ also suffice. Section~\ref{round:single}
+$L_M\ge10a$ and $I_M\ge2a$ also suffice.
accounts for the $10^{-12}$ margin.
\end{proof}
@@ -3035,7 +3020,7 @@ $\|z\|\le r_e$ gives the support inequalities.
% ---------------------------------------------------------------
-\subsection{The joint test with one shared tangent variable}
+\medskip\noindent\textbf{The joint test with one shared tangent variable.}
% ---------------------------------------------------------------
For each ball $t=0,1$, form $c^t,J^t,B^t,S^t$ from
@@ -3120,13 +3105,13 @@ direction is not part of the certificate.
The inequalities just proved are necessary in exact real arithmetic. In
the implementation, each rejection is a strict violation of an
outward-enlarged bound; equalities and unresolved comparisons retain
-the candidate. Section~\ref{sec:rounding} certifies these comparisons,
-and Section~\ref{exclude:implementation} lists their margins. Thus every
+the candidate. certifies these comparisons,
+and lists their margins. Thus every
genuine pair retains its required relation when the tests are evaluated
numerically.
% ---------------------------------------------------------------
-\subsection{Exact graph exclusion}
+\medskip\noindent\textbf{Exact graph exclusion.}
% ---------------------------------------------------------------
Build one vertex for each retained ball. Join two distinct vertices by
@@ -3223,7 +3208,7 @@ conditional on a completed negative result for the individual Record;
no collection of unexecuted tests is itself such a result.
% ---------------------------------------------------------------
-\subsection{Implementation margins and invocation}
+\medskip\noindent\textbf{Implementation margins and invocation.}
\label{exclude:implementation}
% ---------------------------------------------------------------
@@ -3254,7 +3239,7 @@ Lemma~\ref{exclude:cluster-cover}.
The bounds $|P_{ij}|\le 4$ and $|v_j|\le 2$ keep all trigonometric
arguments used here within the guarded range of \texttt{expair}. The
-proof of Section~\ref{sec:rounding} includes the errors in these
+proof of includes the errors in these
arguments, in $q,S,c,J,B$, in the short weighted sums and norms, and in
the positive support expressions. Inexact solution of the proposal
systems supplies no separate assumption.
@@ -3270,7 +3255,7 @@ unexecuted tests is itself such a result.
% =====================================================================
-\section{Finite execution and the recorded certificate}
+\medskip\noindent\textbf{Finite execution and the recorded certificate.}
\label{sec:execution}
% =====================================================================
@@ -3278,26 +3263,20 @@ The computation used in the conclusion of this proof was completed on
4 October 2026 (UTC). This section specifies its finite inputs, the
tests for complete execution, and the implication from those tests to
nonexistence. The geometric and arithmetic justification of each
-rejection is in Sections~\ref{sec:seed}--\ref{sec:exclusion} and
-Appendix~\ref{sec:rounding}. A successful exit by itself is not the
+rejection lies in the seed cover, the completion and refinement stages,
+the exclusion tests, and the certified arithmetic. A successful exit by
+itself is not the
certificate: the inputs, record counts, saved failures, and coverage of
all shards must agree as described here.
% ---------------------------------------------------------------
-\subsection{Programs, records, and machine arithmetic}
+\medskip\noindent\textbf{Programs, records, and machine arithmetic.}
\label{execute:programs}
% ---------------------------------------------------------------
The recorded platform was x86-64, Intel Xeon Platinum 8573C, Ubuntu
-GCC 13.3.0, and glibc 2.39. The builds, prepared on the same UTC date
-before the run, were
-\begin{lstlisting}
-g++ -O3 -march=native -ffp-contract=off covout.cpp -o covrun
-g++ -std=gnu++17 -O3 -march=native -ffp-contract=off atlas.cpp -o arun
-g++ -std=gnu++17 -O3 -march=native -ffp-contract=off stageB.cpp -o brun
-g++ -std=gnu++17 -O3 -march=native -ffp-contract=off stageC.cpp -o crun
-\end{lstlisting}
-The first command uses this compiler's default GNU C++17 dialect. The
+GCC 13.3.0, and glibc 2.39. Each stage was compiled separately, all four on the same UTC date as
+the run, with contraction disabled and a fixed language dialect. The
arithmetic assumptions are binary64, round to nearest, separate
operations without contraction or fast-math reassociation, correctly
rounded binary64 square root, masked floating-point exceptions, and
@@ -3310,51 +3289,44 @@ Both probes recorded nearest rounding on entry and during the check,
and passed the square-root and gradual-underflow samples. These probes
and the program checks provide limited evidence for the stated platform
conditions, not a proof of all primitive-operation or compiler
-semantics. Those semantics remain assumptions; Appendix~\ref{sec:rounding}
+semantics. Those semantics remain assumptions; the certified arithmetic
supplies the numerical bounds under them.
-The five source files used by the four programs are
-\texttt{covout.cpp}, \texttt{patchx.cpp} (which contains
-\texttt{buildH::gen}, \texttt{buildH::patch}, and \texttt{makeD}), and
-the sources of \texttt{atlas.cpp}, \texttt{stageB.cpp},
-\texttt{stageC.cpp} together with the two shared headers that carry
-the Root, Atlas, and graph data structures. This is what
-Section~\ref{execute:control} refers to as the seven specified source
-files; the archived copies at the locations given in
-Section~\ref{execute:observed} are what make the certificate concrete.
-
-\subsection{How the pipeline is split}
-
-The driver \texttt{covrun} writes the seed-center file: one record per
-retained midpoint, with its rational midpoint phases (in cycles), the
-selected column position $s$, and the chosen radius $0.032$. It
-performs only the seed filters certified in Section~\ref{sec:seed}.
-
-Stage~A (\texttt{arun}) processes seeds in disjoint shards and writes
-the Phase ball Records of Section~\ref{sec:phase-cover}. Stage~B
-(\texttt{brun}) refines that cover
-(Section~\ref{sec:refinement}) and writes its batch files. Stage~C
-(\texttt{crun}) tests each ball for exclusion of two extra bases
-(Section~\ref{sec:exclusion}) and writes its per-batch bad records.
-
-Each program writes its own status file. The pipeline wrapper writes
-an outer \texttt{run.json} and per-stage \texttt{*.stage.json} files.
-The same wrapper runs the B fallback and the four final C shards when
-the initial C reports any bad record. Every intermediate file is
-checked against the outer status before the pipeline is considered
-complete.
+Four programs carry out the search: one builds the seed cover, one runs
+the completion stage, one refines the resulting phase balls, and one
+performs the exclusion tests. They share the Root, Atlas and graph data
+structures through common declarations, and the arithmetic bounds below
+fix every floating-point operation any of them performs. The archived
+sources, identified by their recorded digests, are what make the
+certificate concrete rather than notional.
+
+\medskip\noindent\textbf{How the pipeline is split.}
+
+The first program writes a seed-center table, one entry per retained
+midpoint, carrying its rational phases in cycles, the selected column
+position $s$, and the radius $0.032$. It performs only the seed filters
+whose margins are certified in the arithmetic bounds.
+
+The completion stage processes seeds in disjoint shards and fills the
+atlas of certified phase balls. The refinement stage then shrinks that
+cover and writes its batch files, and the exclusion stage tests every
+resulting ball for two extra bases, writing a per-batch record of the
+few that resist exclusion.
+
+Each program reports its own exit status and counts. A supervising
+driver records one outer summary and one summary per stage, reruns the
+fallback and the final exclusion shards whenever the initial exclusion
+pass leaves any record unexcluded, and compares every intermediate
+count against the outer summary before the run counts as complete.
% ---------------------------------------------------------------
-\subsection{Control flow and terminal conditions}
+\medskip\noindent\textbf{Control flow and terminal conditions.}
\label{execute:control}
% ---------------------------------------------------------------
-The pipeline has an explicit control flow with documented terminal
-conditions. Every stage writes its inputs, outputs, exit codes, and
-counts to a status file, and the wrapper compares these against the
-recorded expectations. A pipeline that fails any listed condition is
-not a certificate.
+The control flow is finite and every terminal condition is documented.
+A run that fails any listed condition is not a certificate.
The required terminal conditions are:
\begin{enumerate}
@@ -3381,106 +3353,94 @@ unresolved count was nevertheless zero.
The finite bounds governing this control flow --- the bin counts, the
range of stored differences, the grid~$64$ cell-test count, and the
-extra-node and deepest-grid caps --- are stated and checked at the end
-of Section~\ref{sec:completion}.
+extra-node and deepest-grid caps --- are stated and checked in the
+completion stage.
Reaching the C-stage bin cap of $2{,}000{,}000$ retained bins, exceeding
the cluster center count of $2048$, or exhausting the graph work cap
-each produce an unresolved outcome rather than a negative certificate
-(see Section~\ref{sec:exclusion}).
+each produce an unresolved outcome rather than a negative certificate.
% ---------------------------------------------------------------
-\subsection{The recorded execution}
+\medskip\noindent\textbf{The recorded execution.}
\label{execute:observed}
% ---------------------------------------------------------------
The complete run consists of 100 program invocations:
\begin{itemize}
-\item one cover (\texttt{covrun});
-\item four A shards (\texttt{arun});
-\item two B refinements (\texttt{brun}, mid and fine);
-\item 88 initial C batches (\texttt{crun});
-\item one B fallback;
-\item four final C batches.
+\item one pass over the seed cover;
+\item four shards of the completion stage;
+\item two refinement passes, a mid one and a fine one;
+\item 88 batches of the initial exclusion pass;
+\item one fallback refinement pass;
+\item four final exclusion batches.
\end{itemize}
-The initial C stage reports some nonzero bad files. These are the
-residual candidates that the initial C bin/graph tests could not reject;
-they are handed to B fallback, whose own batches are then handed to the
-four final C batches. Section~\ref{execute:programs} lists the platform;
-the status files referenced below record every count and hash for
-verification.
-
-For every initial C process, the normal status is $0$ exactly when its
-saved bad count is zero, and $1$ exactly when that count is positive.
-The four reported failure categories --- uncapped graph candidate,
+The initial exclusion pass leaves a nonzero count on some batches: the
+residual candidates that the bin and graph tests could not reject. They
+are handed to the fallback, whose own batches then feed the four final
+exclusion batches. Recorded counts and hashes accompany the whole run.
+
+For every initial exclusion process the recorded status is $0$ exactly
+when its unresolved count is zero, and $1$ exactly when that count is
+positive. The four failure categories --- uncapped graph candidate,
graph-step cap, bin overflow, and clustering failure --- sum to that
-bad count. None of them is an exclusion. Every nonempty-count bad file
-is passed to B fallback in C-locale filename order, including failures
-whose locations differ from those in another run. The final C uses all
-four modulo-$4$ parts of the fallback output. If initial C has no bad
-records, fallback and final C would be unnecessary; that shortcut was
-not used in the recorded run.
-
-The nonzero initial C failure files, in the order actually supplied to
-B fallback, were
-\begin{lstlisting}
-bad10.bin bad3.bin bad4.bin bad5.bin bad52.bin bad53.bin
-bad55.bin bad56.bin bad6.bin bad7.bin bad78.bin bad79.bin
-bad8.bin bad80.bin bad84.bin
-\end{lstlisting}
-They contain all $163$ unresolved records. There were no initial bin
+count, and none of them is an exclusion. Every nonempty batch reaches
+the fallback, sorted by locale, including batches whose locations differ
+from one run to the next. The final exclusion pass uses all four
+modulo-$4$ parts of the fallback output. Had the initial pass left no
+unresolved record, the fallback and the final pass would have been
+unnecessary; that shortcut was not taken.
+
+Fifteen initial exclusion batches left unresolved records, and together
+they carry all $163$ unresolved records. There were no initial bin
overflows, clustering failures, or uncapped graph candidates. There were
-no final failures of any category. So all 100 program invocations are
-accounted for: one cover, four A processes, two B refinements, 88
-initial C processes, one B fallback, and four final C processes. The
-fifteen initial C exits 1 are fully resolved by that fallback chain. No
-rejection threshold, graph cap, refinement width, or mathematical
-source file was altered, and no additional refinement level was
-inserted.
-
-For scale, the wrapper-measured stage wall times, including polling and
-validation, were $621.59$ seconds for the cover, $2020.32$ seconds for
-the four parallel A shards, $1071.49$ and $407.45$ seconds for B mid and
-B fine, and $300.23$, $8.12$, and $36.27$ seconds for initial C,
-fallback B, and final C. The outer supervisor measured $4470.33$
-seconds for the complete pipeline. These are observations on this
-platform, not native CPU times or running-time guarantees. No stage hit
-its wall deadline, and no retry or resource-limit increase was used.
-
-The execution archive identified by
-\texttt{verification/\allowbreak computation/README.md} preserves the
-numerical data and records of this complete run, with internal path and
-host fields redacted: all sources and binaries, center and record files,
-all 88 input batches and their C bad files, fallback data, all final
-bad files, stdout and stderr, commands, exits, platform information, and
-validation records. In the execution archive,
-\texttt{full-run-01/pipeline/status.json} is the whole-run record;
-\texttt{*.stage.json} files describe stages and individual
-\texttt{*.status.json} files describe child processes. The outer record
-is \texttt{full-run-01/run.json}. \texttt{verification/REPRODUCE.md}
-gives rebuild and execution instructions. Archived native binaries
-document this run; they are not a portability claim.
-
-The certificate used here depends only on this newly completed chain and
-the values recorded in the status files. No earlier execution,
-diagnostic sample, or intermediate timed measurement substitutes for
-any stage of this full run.
+no final failures of any category. All 100 program invocations are
+therefore accounted for: one cover pass, four completion shards, two
+refinement passes, 88 initial exclusion batches, one fallback pass, and
+four final exclusion batches. The fifteen nonzero exits are fully
+resolved by that fallback chain. No rejection threshold, graph cap,
+refinement width, or mathematical input was altered, and no additional
+refinement level was inserted.
+
+For scale, the measured wall times, including polling and validation,
+were $621.59$ seconds for the cover, $2020.32$ seconds for the four
+parallel completion shards, $1071.49$ and $407.45$ seconds for the two
+refinement passes, and $300.23$, $8.12$ and $36.27$ seconds for the
+initial exclusion, the fallback and the final exclusion. The outer
+supervisor measured $4470.33$ seconds for the complete pipeline. These
+are observations on this platform, not native CPU times or running-time
+guarantees. No stage hit its wall deadline, and no retry or resource
+limit was raised.
+
+The execution archive preserves the numerical data and records of this
+complete run, with internal path and host fields redacted: sources and
+binaries, center and record files, all 88 initial exclusion batches and
+their unresolved records, fallback data, every final unresolved record,
+stdout and stderr, commands, exits, platform information, and validation
+records. Inside it one record describes the whole run, one record per
+stage describes that stage, and one record per child describes that
+child. Rebuild and execution instructions accompany the archive.
+Archived native binaries document this run; they are not a portability
+claim.
+
+The certificate depends only on this newly completed chain and the
+counts recorded alongside it. No earlier execution, diagnostic sample,
+or intermediate timed measurement substitutes for any stage of this
+full run.
% ---------------------------------------------------------------
-\subsection{The finite-execution certificate}
+\medskip\noindent\textbf{The finite-execution certificate.}
\label{execute:theorem}
% ---------------------------------------------------------------
\begin{theorem}[Finite-execution certificate]
\label{execute:finite-theorem}
-Use the seven specified source files (Section~\ref{execute:programs})
-and the arithmetic conditions of Appendix~\ref{sec:rounding}. Suppose
-the invocations of Section~\ref{execute:control} meet every terminal
-condition listed there, with the record provenance and batch checks
-stated in Section~\ref{execute:observed}. Then four mutually unbiased
-orthonormal bases in $\C^6$ do not exist.
+Fix the four recorded programs and the arithmetic conditions of the
+certified arithmetic. Suppose the recorded invocations meet every
+terminal condition listed above, together with the record provenance
+and batch checks stated there. Then four mutually unbiased orthonormal
+bases in $\C^6$ do not exist.
\end{theorem}
\begin{proof}
@@ -3494,9 +3454,9 @@ balls. All A shards together process that seed.
\emph{Stages A and B.} Proposition~\ref{phase:A-cover} therefore places
an equivalent exact solution in a coarse Record. Each equivalence
preserves extendibility by two further bases
-(Lemma~\ref{seed:equivalences}). On that Record,
-Section~\ref{sec:refinement} replaces its ball by a finite atlas of
-children and any bad parents; Proposition~\ref{refine:cover-preservation}
+(Lemma~\ref{seed:equivalences}). On that Record the refinement stage
+replaces the ball by a finite atlas of children together with any
+unresolved parent; Proposition~\ref{refine:cover-preservation}
gives containment. Since the run has no remaining bad parent at the
end of the initial C stage and no bad record at the end of the final C
stage, the record is either covered by a completed child at its own
@@ -3504,11 +3464,11 @@ precomputed local certificate, or refined into a further record that is
similarly covered.
\emph{Stage C.} Proposition~\ref{exclude:local-certificate} then rules
-out two extra bases in every such local ball. The C run has no bad
-records at the end (terminal condition~5 of Section~\ref{execute:control}
-together with the terminal conditions of the fallback chain). Therefore
-every individual pointer to the Hadamard solution lies in a phase ball
-that C excludes.
+out two extra bases in every such local ball. The exclusion run leaves
+no unresolved record at the end, by terminal condition~5 together with
+the terminal conditions of the fallback chain. Therefore every
+individual pointer to the Hadamard solution lies in a phase ball that
+the exclusion stage rules out.
Contradiction: the assumed family would induce a Hadamard displacement
that lands inside some ball of the final cover, but each such ball has a
@@ -3516,9 +3476,9 @@ completed negative certificate. Hence four such bases do not exist.
\end{proof}
The certificate therefore has three independent components: the
-finite-arithmetic premises of Appendix~\ref{sec:rounding}, the finite
-invocations and terminal conditions of Section~\ref{execute:control},
-and the mathematical chain of Sections~\ref{sec:seed}--\ref{sec:exclusion}.
+finite-arithmetic premises of the certified arithmetic, the finite
+invocations and terminal conditions listed above, and the mathematical
+chain of the preceding stages.
A change to any one of them --- different build flags, different
terminal conditions, or a different proof of one of the local lemmas ---
would require a fresh execution of the affected stage, but the logical
@@ -3527,11 +3487,11 @@ structure of the certificate is unchanged.
The theorem and its proof complete the computer-assisted upper bound.
% =====================================================================
-\section{Conclusion of the proof}
+\medskip\noindent\textbf{Conclusion of the proof.}
\label{sec:conclusion}
% =====================================================================
-We have now completed the proof of Theorem~\ref{thm:main}. The
+The proof of Theorem~\ref{thm:main} is now complete. The
overall argument is the following chain of strictly finer covers, each
preserving every exact candidate solution.
@@ -3552,8 +3512,8 @@ preserving every exact candidate solution.
(Proposition~\ref{exclude:local-certificate}).
\end{enumerate}
-The recorded execution of the pipeline (Section~\ref{execute:observed})
-meets every terminal condition of Section~\ref{execute:control}, so the
+The recorded execution of the pipeline
+meets every terminal condition listed above, so the
finite-execution certificate Theorem~\ref{execute:finite-theorem}
applies and yields the negative upper bound. The lower bound is
Lemma~\ref{lem:three-mub-six}; the two together give $N(6)=3$.
@@ -3565,8 +3525,8 @@ cover, exclude two further mutually unbiased bases by the graph test;
and check the whole chain by an actual computer run with certified
arithmetic.
-The historical and mathematical antecedents cited in
-Section~\ref{sec:introduction} are complementary; the combination
+The historical and mathematical antecedents surveyed above are
+complementary; the combination
needed for the theorem above is new. In particular, the present proof
covers every second-basis Hadamard matrix directly, rather than running
a certified search inside a presumed family.
@@ -3575,27 +3535,27 @@ a certified search inside a presumed family.
\appendix
% =====================================================================
-\section{Certified arithmetic for the recorded execution}
+\medskip\noindent\textbf{Certified arithmetic for the recorded execution.}
\label{sec:rounding}
% =====================================================================
-This appendix records the outward error estimates that back each
-inequality quoted in Sections~\ref{sec:seed}--\ref{sec:exclusion} and
-Section~\ref{sec:execution}. Every certified rejection is a strict violation
+The outward error estimates behind each inequality used above are fixed
+below. Every certified rejection is a strict violation
of an outward bound computed under the primitive-operation model below.
Nothing here assumes that a floating-point center is an exact solution,
and no step relies on the observed size of an error over a specific
input.
% ---------------------------------------------------------------
-\subsection{Primitive-operation model and unit roundoff}
+\medskip\noindent\textbf{Primitive-operation model and unit roundoff.}
% ---------------------------------------------------------------
The primitive-operation model is the binary64 specification
-of IEEE~754~\cite[Sections 3.4, 3.6, 4.3, 5.4.1 and 7.5]{IEEE7542019}.
+of IEEE 754-2019, in its Sections 3.4, 3.6, 4.3, 5.4.1 and 7.5.
The accumulation estimates use the usual product-of-rounding-factors
-argument~\cite[Section 2.12 and Lemma 3.1]{Higham2002Accuracy}, with the
-explicit additive underflow allowance retained here.
+argument of Section 2.12 and Lemma 3.1 of Higham's 2002 book on the
+accuracy of numerical algorithms, with the explicit additive underflow
+allowance retained here.
The arithmetic premises are separate, correctly rounded binary64
addition, subtraction, multiplication, division, and square root in
@@ -3606,18 +3566,19 @@ flushed to zero, and denormal inputs are not treated as zero. Floating
exceptions are masked, so an unsuccessful heuristic calculation can
produce an infinity or NaN and be rejected by its subsequent checks.
The relevant integer types, numeric locale, and file representation are
-specified in Section~\ref{sec:execution}.
+specified with the execution above.
The function \texttt{environment} sets and checks nearest rounding and
-checks the binary64 properties of \texttt{double}. The A/B/C entry
+checks the binary64 properties of \texttt{double}. The three entry
points also inspect MXCSR, rejecting a non-nearest mode, DAZ, FTZ, or
unmasked exceptions. The same no-DAZ/no-FTZ environment is required for
-\texttt{covout}, although its entry point does not itself inspect those
-bits. The default-nearest premise also applies to constants and to the
-global basis constructed before \texttt{main}. These are explicit
-arithmetic premises, not a claim that a source-level static assertion
-formally verifies every compiler transformation. The recorded build
-checks and their limits are described in Section~\ref{sec:execution}.
+the cover-building program, although its entry point does not itself
+inspect those bits. The default-nearest premise also applies to
+constants and to the global basis constructed before \texttt{main}.
+These are explicit arithmetic premises, not a claim that a source-level
+static assertion formally verifies every compiler transformation. The
+recorded build checks and their limits are described with the execution
+above.
The functions \texttt{nearbyint} and \texttt{floor} choose integers at
finite bounded arguments. The particular integer chosen at a boundary is
@@ -3666,7 +3627,7 @@ Euclidean difference is added to this bound.
\begin{proof}
Iterating $|z_k|\le (1+u)|z_{k-1}|+u+b\tau$ for a length-$m$ dot product
with the standard addition/rounding analysis
-(Higham~\cite[Lemma 3.1]{Higham2002Accuracy}) gives an interpolation of
+(Lemma 3.1 of Higham's 2002 book) gives an interpolation of
the form $(1+u)^m\sum_{i=1}^m|a_ib_i|$ plus a $O(m\tau)$ term. The bound
$\gamma_m=2.1\cdot 10^{-16}(m+1)$ is a conservative choice: for
$m\le 2000$ one has $(1+u)^m-1\le mu\le 2m\cdot 10^{-16}$, which is
@@ -3678,7 +3639,7 @@ final $10^{-140}$ additive allowance.
\end{proof}
% ---------------------------------------------------------------
-\subsection{Pi and exponential evaluations}
+\medskip\noindent\textbf{Pi and exponential evaluations.}
\label{round:exponentials}
% ---------------------------------------------------------------
@@ -3720,7 +3681,7 @@ For $z=a+bi$ with $|a|,|b|\le20$, the pair
$(\operatorname{fl}(\cos b),\operatorname{fl}(\sin b))$ is multiplied by
$e^a$; the pair error and the multiplication error are each below
$2u$ in relative terms, and the total error is below $10^{-14}$
-in absolute value at the scales used here (bound: Section~\ref{round:root}).
+in absolute value at the scales used here (bound: ).
All relied-on arguments satisfy the range condition. Seed and dyadic
unitary phases are bounded near $[0,1]$; \texttt{gen} checks $|p_j|\le4$;
Candidate checks $|P_j|\le .51$ before its exponential; C validates
@@ -3729,7 +3690,7 @@ largest C difference has magnitude at most six.
% ---------------------------------------------------------------
-\subsection{Dephasing and projection}
+\medskip\noindent\textbf{Dephasing and projection.}
\label{round:dephasing}
% ---------------------------------------------------------------
@@ -3763,7 +3724,7 @@ Searching only some buckets or transforms may miss a merge; it cannot
certify a merge that fails these tests.
% ---------------------------------------------------------------
-\subsection{Seed filtering and seed-ball reuse}
+\medskip\noindent\textbf{Seed filtering and seed-ball reuse.}
\label{round:seed-filters}
% ---------------------------------------------------------------
@@ -3819,7 +3780,7 @@ error before the subtraction is below $10^{-12}$, so this is smaller
than the ideal $(.032\cdot112)^2$. This reasoning requires the
\texttt{pow(x,2)} calls in \texttt{covout} to be lowered to binary64
multiplication, as checked for the fresh build documented in
-Section~\ref{sec:execution}. It is not a claim about an arbitrary library
+. It is not a claim about an arbitrary library
implementation of \texttt{pow}. The other square-power value $T$,
bucket reach, and integer cuts only select reuse attempts; missing an
attempt does not discard the current bin pair. A newly inserted midpoint
@@ -3829,7 +3790,7 @@ $10^{-14}$, which is absorbed when the A seed radius is increased to
$.0320001$.
% ---------------------------------------------------------------
-\subsection{Frames, comparison blocks, and A exclusion tests}
+\medskip\noindent\textbf{Frames, comparison blocks, and A exclusion tests.}
\label{round:frames}
% ---------------------------------------------------------------
@@ -3896,7 +3857,7 @@ pre-equation coefficients & $6\cdot 10^{-14}$ & unit exponentials\\
\end{tabular}
\end{center}
-\paragraph{The horizontal-projector identity.}
+\medskip\noindent\textbf{The horizontal-projector identity..}
An entry of the exact double-centering projector is the product of two
centering-matrix entries. The computed \texttt{PI} differs by less than
$10^{-15}$ per entry. In the matrix $L_P$, each row has only 12 nonzero
@@ -3914,7 +3875,7 @@ $2\cdot 10^{-6}$ addition in \texttt{id} suffices.
% ---------------------------------------------------------------
-\subsection{Root certificates and normal constants}
+\medskip\noindent\textbf{Root certificates and normal constants.}
\label{round:root}
% ---------------------------------------------------------------
@@ -3945,7 +3906,7 @@ $\mathtt{id}<10^{-4}$ after the $2\cdot 10^{-6}$ addition, and
$\mathtt{mnorm}\cdot\mathtt{froot}\le\mathtt{n0}$.
% ---------------------------------------------------------------
-\subsection{Candidate conversion and ellipsoidal coverage}
+\medskip\noindent\textbf{Candidate conversion and ellipsoidal coverage.}
\label{round:candidate}
% ---------------------------------------------------------------
@@ -3967,7 +3928,7 @@ than $1.56\cdot 10^{-7}$. If a circular phase distance in cycles is
$v\in[0,1/2]$, its chord is $2\sin(\pi v)\ge 4v$. Across $16$ entries
the phase-center correction therefore has norm below
$1.56\cdot 10^{-7}$, which is below the $2\cdot 10^{-6}$ allowance used
-in Section~\ref{sec:phase-cover}. The nine seed entries use exact stored
+in . The nine seed entries use exact stored
seed centers and an exact integer subtraction.
For the D-position coefficients $X$, the normalized-direction error
@@ -3995,7 +3956,7 @@ quantities are upper bounds with
\qquad \mathtt{invmag}_j<6.8.
\end{equation}
-\paragraph{Tangent offsets and external errors.}
+\medskip\noindent\textbf{Tangent offsets and external errors..}
The computed \texttt{off} approximates $2\pi T^*\Delta$ within $10^{-9}$
in norm, by~\eqref{round:t-operator}, the projected-difference error,
and short-dot rounding. The error in the whole $X$ array is at most
@@ -4024,7 +3985,7 @@ $k\le 10$. Hence the exact stored $G$ is positive semidefinite and
dominates the required covariance.
% ---------------------------------------------------------------
-\subsection{The stored spectral upper bound}
+\medskip\noindent\textbf{The stored spectral upper bound.}
\label{round:ell}
% ---------------------------------------------------------------
@@ -4072,7 +4033,7 @@ whole-candidate error bound $10^{-12}$ dominate at the used scales.
% ---------------------------------------------------------------
-\subsection{The base grid and the outside test}
+\medskip\noindent\textbf{The base grid and the outside test.}
\label{round:base-grid}
% ---------------------------------------------------------------
@@ -4095,7 +4056,7 @@ to reduce the parent-distance test to a single comparison against $E_P$,
without loss elsewhere.
% ---------------------------------------------------------------
-\subsection{Single-vector filters and vector-ball construction}
+\medskip\noindent\textbf{Single-vector filters and vector-ball construction.}
\label{round:single}
% ---------------------------------------------------------------
@@ -4139,7 +4100,7 @@ The combined bound uses the same $2\cdot 10^{-7}$. The nested
squared-magnitude crossing band is $2\cdot 10^{-7}$; the squared
increment is $7\cdot 10^{-7}$.
-\paragraph{The directional single-vector support.}
+\medskip\noindent\textbf{The directional single-vector support..}
The heuristic solve is accepted only with finite coordinates and a
maximum magnitude between $10^{-100}$ and $10^{100}$. After division
by that maximum, regard the resulting stored $|y_i|\le 1$ as the test
@@ -4182,7 +4143,7 @@ ideal expression inside $\pi$, and the whole error against the ideal
support is below $10^{-10}$. The code adds $2\cdot 10^{-7}$.
% ---------------------------------------------------------------
-\subsection{The joint coefficient support}
+\medskip\noindent\textbf{The joint coefficient support.}
\label{round:joint}
% ---------------------------------------------------------------
@@ -4207,7 +4168,7 @@ upper bound at the recorded threshold.
% ---------------------------------------------------------------
-\subsection{Finite paths and NaN handling}
+\medskip\noindent\textbf{Finite paths and NaN handling.}
\label{round:summary}
% ---------------------------------------------------------------
@@ -4242,145 +4203,16 @@ preconditions.
after a successful atlas update, and the final count is the
terminal cover size. A failed temporary write records an
unresolved parent.
-\item The cluster output is checked as in Section~\ref{round:single}
+\item The cluster output is checked as in
at $|v_j|\le 2$ and $0\le s<.1$. The two edges share the
distance bound $r_e=s_u+s_v$. If the direct tests reject an
edge, its weight is zero with infinity cost. Otherwise the
stored $D_E$ and $q_E$ are finite. The joint coefficient
- guard from Section~\ref{round:joint} then rejects any failed
+ guard from then rejects any failed
proposal and keeps the corresponding previous bound. A failed
proposal cannot certify a pair excluded.
\end{enumerate}
-\begin{thebibliography}{99}
-
-\bibitem{BandyopadhyayEtAl2002}
-S.~Bandyopadhyay, P.~O.~Boykin, V.~Roychowdhury, and F.~Vatan,
-\emph{A new proof for the existence of mutually unbiased bases},
-Algorithmica \textbf{34} (2002), 512--528.
-
-\bibitem{BengtssonEtAl2007MUBHadamard}
-I.~Bengtsson, W.~Bruzda, A.~Ericsson, and K.~Zyczkowski,
-\emph{Mutually unbiased bases and Hadamard matrices of order six},
-J. Math. Phys. \textbf{48} (2007), 052106.
-
-\bibitem{BrierleyWeigert2008}
-S.~Brierley and S.~Weigert,
-\emph{Maximal sets of mutually unbiased quantum states in dimension six},
-Phys. Rev. A \textbf{78} (2008), 042312.
-
-\bibitem{BrierleyWeigert2009}
-S.~Brierley and S.~Weigert,
-\emph{Constructing mutually unbiased bases in dimension six},
-Phys. Rev. A \textbf{79} (2009), 052316.
-
-\bibitem{ButterleyHall2007Numerical}
-P.~Butterley and W.~Hall,
-\emph{Numerical evidence for the maximum number of mutually unbiased
-bases in dimension six}, Phys. Lett. A \textbf{369} (2007), 5--8.
-
-\bibitem{BoykinSitharamTiepWocjan2005}
-P.~O.~Boykin, M.~Sitharam, P.~H.~Tiep, and P.~Wocjan,
-\emph{Optimal combinatorics for mutually unbiased bases},
-Quantum Inf. Process. \textbf{4} (2005), 383--390.
-
-\bibitem{CardenesWuttigTindall2026Classification}
-J.~C\'ardenes, I.~Wuttig, and J.~Tindall,
-\emph{Classification of order-six Hadamard matrices and their MUB
-extendibility}, (2026).
-
-\bibitem{FanHoffman1955}
-K.~Fan and A.~J.~Hoffman,
-\emph{Lower bounds for the maximum number of mutually unbiased bases},
-Proc. Amer. Math. Soc. \textbf{6} (1955), 826--828.
-
-\bibitem{Grassl2004SICMUB6}
-M.~Grassl,
-\emph{On SIC-POVMs and MUBs in dimension 6},
-(2004), eprint \texttt{quant-ph/0406175}.
-
-\bibitem{Higham1986Polar}
-N.~J.~Higham,
-\emph{Computing the polar decomposition---with applications},
-SIAM J. Sci. Statist. Comput. \textbf{7} (1986), 1160--1174.
-
-\bibitem{Higham2002Accuracy}
-N.~J.~Higham,
-\emph{Accuracy and Stability of Numerical Algorithms},
-2nd ed., SIAM, 2002.
-
-\bibitem{IEEE7542019}
-IEEE,
-\emph{Standard for Floating-Point Arithmetic}, IEEE Std 754-2019,
-IEEE, 2019.
-
-\bibitem{Ivanovic1981StateDetermination}
-I.~D.~Ivanovi\'c,
-\emph{Geometrical description of quantal state determination},
-J. Phys. A \textbf{14} (1981), 3241--3245.
-
-\bibitem{JamingEtAl2009}
-P.~Jaming, M.~Matolcsi, P.~M\'ora, F.~Sz\"oll\H osi, and M.~Weiner,
-\emph{A generalized Pauli problem and an infinite family of MUB-triplets
-in dimension 6}, J. Phys. A \textbf{42} (2009), 245305.
-
-\bibitem{JamingMatolcsiMora2010}
-P.~Jaming, M.~Matolcsi, and P.~M\'ora,
-\emph{Mutually unbiased bases in dimension six: an overview and a
-numerical exploration}, (2010).
-
-\bibitem{KlappeneckerRotteler2004}
-A.~Klappenecker and M.~R\"otteler,
-\emph{Constructions of mutually unbiased bases},
-in {\em Finite Fields and Applications}, Lecture Notes in Computer
-Science \textbf{2948}, Springer, 2004, 137--144.
-
-\bibitem{Lloyd1982}
-S.~Lloyd,
-\emph{Least squares quantization in PCM},
-IEEE Trans. Inform. Theory \textbf{28} (1982), 129--137.
-
-\bibitem{MatolcsiEtAl2026}
-M.~Matolcsi, F.~Sz\"oll\H osi, and M.~Weiner,
-\emph{On triplets of mutually unbiased bases}, (2026).
-
-\bibitem{McNultyWeigert2026Review}
-D.~McNulty and S.~Weigert,
-\emph{Mutually unbiased bases: a composite-dimension review}, (2026).
-
-\bibitem{Rump2011VerifiedSingularValues}
-S.~M.~Rump,
-\emph{Verified bounds for singular values, in particular for the
-spectral norm of a matrix and its inverse},
-BIT Numer. Math. \textbf{51} (2011), 367--384.
-
-\bibitem{Schwinger1960Unitary}
-J.~Schwinger,
-\emph{Unitary operator bases},
-Proc. Nat. Acad. Sci. USA \textbf{46} (1960), 570--579.
-
-\bibitem{WoottersFields1989}
-W.~K.~Wootters and B.~D.~Fields,
-\emph{Optimal state-determination by mutually unbiased measurements},
-Ann. Physics \textbf{191} (1989), 363--381.
-
-\bibitem{Zauner1991Diploma}
-G.~Zauner,
-\emph{Orthogonale lateinische Quadrate und Anordnungen, verallgemeinerte
-Hadamard-Matrizen und Unabh\"angigkeit in der
-Quanten-Wahrscheinlichkeitstheorie},
-Diplomarbeit, Universit\"at Wien, 1991.
-
-\bibitem{Zauner1999}
-G.~Zauner,
-\emph{Quantendesigns: Grundz\"uge einer nichtkommutativen
-Designtheorie}, Dissertation, Universit\"at Wien, 1999.
-
-\bibitem{Zauner2011}
-G.~Zauner,
-\emph{Quantum designs: foundations of a noncommutative design theory},
-Int. J. Quantum Inf. \textbf{9} (2011), 445--507.
-
-\end{thebibliography}
+
\end{document}