\documentclass[11pt]{article}
\usepackage[T1]{fontenc}
\usepackage[margin=1in]{geometry}
\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage{booktabs,array,longtable}
\usepackage{microtype}
\usepackage{xcolor}
\usepackage{listings}
\usepackage[colorlinks=true,linkcolor=blue!55!black,citecolor=blue!55!black,urlcolor=blue!55!black]{hyperref}
\hypersetup{pdftitle={A Formally Verified Certificate Proof of the Maximum Number of Stable Matchings for Six Men and Six Women},pdfauthor={Yuran Xiu},pdfkeywords={stable marriage, stable matchings, maximum number, six by six, f(6)=48, rotation poset, order ideals, permanent bound, Lean}}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{remark}[theorem]{Remark}
\newcommand{\N}{\mathbb N}
\newcommand{\Sn}{\mathfrak S_n}
\newcommand{\Stab}{\mathcal S}
\newcommand{\Ideals}{\mathcal J}
\newcommand{\supp}{\operatorname{supp}}
\newcommand{\per}{\operatorname{per}}
\newcommand{\Safe}{\operatorname{Safe}}
\newcommand{\ind}{\mathbf 1}
\newcommand{\code}[1]{\texttt{\small\detokenize{#1}}}
\lstset{basicstyle=\ttfamily\small,columns=fullflexible,keepspaces=true,breaklines=true,frame=single,framerule=0.3pt,aboveskip=1em,belowskip=1em}
\title{A Formally Verified Certificate Proof of the\\Maximum Number of Stable Matchings\\for Six Men and Six Women}
\author{Yuran Xiu\\IIIS, Tsinghua University\\\texttt{xiuyr23@mails.tsinghua.edu.cn}}
\date{16 October 2026}

\begin{document}
\maketitle
\begin{abstract}
We give a complete Lean~4 verification of the theorem that the maximum
number of stable matchings for six men and six women with strict complete
preferences is $f(6)=48$. Jo (2026) previously proved the unrestricted upper
bound, and Benjamin, Converse, and Krieger (1995) supplied an attaining
construction. Our contribution is an alternative, fully formalized proof using a finite
certificate; the value 48 and the unrestricted theorem are already known. We reduce stable matchings of arbitrary profiles to order
ideals of sequences of cyclic
partner exchanges in which no man revisits a partner. A weighted frontier
recurrence counts these ideals, and a sum of permanents bounds every future
continuation. These bounds yield a finite certificate with 135,828 states.
The complete argument, including the reduction for arbitrary profiles,
certificate soundness, all concrete checks, and an attaining profile, has
been formalized and checked in Lean~4. The final unconditional theorem
depends only on the standard axioms of Lean and mathlib.
\end{abstract}

\section{Introduction}

In the stable marriage problem, each of $n$ men and $n$ women strictly ranks
all members of the other side. A perfect matching is stable if no unmatched
pair strictly prefer each other to their assigned partners. Gale and
Shapley~\cite{GS62} proved that every such instance has a stable matching.
How many stable matchings can one instance have? Write
\[
 f(n)=\max_P |\Stab(P)|,
\]
where $P$ ranges over all strict complete preference profiles and $\Stab(P)$
is its set of stable matchings. We give a fully formalized proof of the
known value $f(6)=48$, established by Jo~\cite[Theorem~5.1]{Jo26}.

\begin{theorem}\label{thm:main}
Every strict complete preference profile on six men and six women has at
most $48$ stable matchings. Some such profile has exactly $48$ stable
matchings. Consequently, $f(6)=48$.
\end{theorem}

The contribution of this paper is the complete Lean verification of
Theorem~\ref{thm:main} by the cycle-schedule and certificate method developed
below. The verification starts from arbitrary strict complete preference
profiles and includes the structural reduction, certificate soundness,
every concrete check, and an attaining profile. The numerical value and
the unrestricted upper bound were already proved by Jo~\cite{Jo26}; we
make no priority claim for that theorem. The lower-bound construction
belongs to the dihedral/Latin family analyzed by Benjamin, Converse, and
Krieger~\cite{BCK95}. Our rank tables are taken from Eilers's presentation
of the construction attributed to Converse~\cite{EilersLatin}.

\paragraph{Previous work.}
Benjamin, Converse, and Krieger~\cite{BCK95} studied Latin marriage
constructions and gave the order-six lower bound 48. Thurber~\cite{Thurber02}
developed further constructions and lower bounds for the extremal function.
Eilers's sequences record exact values and lower bounds
\cite{EilersExact,EilersLower}. Latin profiles form a restricted class in
which the two ranks assigned to each pair have constant sum;
Borodin et al.~\cite[Section~3.7]{Borodin24} distinguish these restricted
counts from the unrestricted extremal problem.

Jo's preprint~\cite{Jo26}, first deposited on 20 September 2026, proves the
unrestricted upper bound by a different route. It derives local constraints
on rotation posets and proves that a poset with at most fifteen elements,
width at most three, and a specified common-incomparability property has at
most 48 antichains. The rotation correspondence then gives $f(6)=48$.
Our proof instead uses a weighted frontier recurrence and a permanent bound
to certify all legal cycle schedules. As described in Jo's verification
note~\cite[Section~6]{Jo26}, his Lean development checks the finite-poset
core and supporting components, while the passage from stable marriage to
that core remains in the manuscript. Our formal development includes its
own reduction from preference profiles and proves the unconditional
stable-marriage statement in Lean. This difference concerns formal proof
coverage: Jo gives a complete mathematical proof of the theorem. We do not
claim that the unformalized connections in that development constitute a
mathematical gap, or that our method improves the bound.

For general $n$, Karlin, Oveis Gharan, and Weber~\cite{KOGW18} proved a
simply exponential upper bound on $f(n)$. Palmer and
P\'alv\"olgyi~\cite{PP21} subsequently proved the bound
$3.55^n+O(1)$. Our formalization concerns one exact finite value; it does not
improve the asymptotic exponential base. Lattice and rotation methods
underlie the structural part of the proof. In particular, Cai and
Thomas~\cite{CT19} give a representation of all stable matchings using a
maximal chain. We give the cover and coordinate-clamping arguments needed
for our reduction explicitly, and claim no novelty for the classical
lattice structure.

\paragraph{Proof strategy.}
A maximal chain of stable matchings changes one cyclic group of partners
at each step. Each man's partners strictly worsen whenever he changes, so
he never revisits a partner. We associate to such a sequence the partial
order generated by chronological precedence between events sharing a man.
Every stable matching injects into an order ideal of this partial order.
This order can omit constraints from the full rotation representation;
the injection is enough for an upper bound.

We count these ideals by a vector indexed by subsets of the men. Together
with a normalized matrix of already visited pairs, this vector contains
all information needed to update the count along further cyclic exchanges.
A permanent bound allows an entire continuation to be certified without
listing its events. The resulting certificate checks every legal cycle
at every stored state, either by the bound or by a reference to an earlier
state. The universal reduction and the entire finite certificate are
checked in Lean, culminating in the quantified statement of
Theorem~\ref{thm:main}. Sections~\ref{sec:schedules}--\ref{sec:certificate}
describe the mathematics; Section~\ref{sec:formal} describes the formal
artifact and its verification boundary.

\section{Preference profiles and cycle schedules}\label{sec:schedules}

We label each side by $[n]=\{0,\ldots,n-1\}$. A profile consists of rank
functions $r_m:[n]\to[n]$ for each man $m$ and $s_w:[n]\to[n]$ for each
woman $w$, all bijections; smaller ranks are preferred. A matching is a
bijection $p:[n]\to[n]$. Its stability condition is
\begin{equation}\label{eq:stable}
 \text{there are no }m,w\text{ such that }
 r_m(w)<r_m(p(m))\quad\text{and}\quad
 s_w(m)<s_w(p^{-1}(w)).
\end{equation}
The labels on the two sides designate different people.

\begin{definition}\label{def:schedule}
A \emph{cycle schedule} is a sequence of matchings
$p_0,p_1,\ldots,p_t$ and permutations $q_1,\ldots,q_t\in\Sn$ such that
each $q_i$ is a single cycle of length at least two, fixing every label
outside its support $C_i$, and
\[
 p_i(m)=p_{i-1}(q_i(m)).
\]
Each man must receive a previously unvisited woman whenever he participates:
if $m\in C_i$, then $p_i(m)\ne p_j(m)$ for every $0\leq j<i$.
The event order is generated by $i\prec j$ whenever $i<j$ and
$C_i\cap C_j\ne\varnothing$. Let $\Ideals(S)$ be the order ideals of
this order for a schedule $S$.
\end{definition}

An order ideal contains every predecessor of each of its events. Equivalently,
on each man's chronological list of events, its selected events form a prefix.
Every event consumes at least two previously unvisited pairs. Thus
$t\leq n(n-1)/2$. The certificate argument below bounds arbitrary finite
legal continuations directly and does not assume this length bound.

\begin{lemma}\label{lem:ideal-injection}
Executing the events of an ideal in chronological order produces a matching.
The resulting map $\Ideals(S)\to\Sn$ is injective.
\end{lemma}
\begin{proof}
Before a selected event, every participant has executed all his earlier
events in the full schedule. He therefore holds exactly the woman prescribed
just before that event. The selected event performs the specified cyclic
exchange and preserves the matching property. This proves the first claim
by induction through the selected events.

For a fixed man, the selected events on his list form a prefix. His partners
after successive changes are all distinct, including his initial partner,
so his final partner determines the length of this prefix. The final
matching therefore determines every participant's decision at every event.
Every event has a participant, which determines the ideal.
\end{proof}

\subsection{From stable matchings to a schedule}

Order stable matchings by $x\leq y$ if
$r_m(x(m))\leq r_m(y(m))$ for all $m$. Thus moving upward weakly worsens
the men's partners.

\begin{lemma}[Lattice closure]\label{lem:lattice}
The stable matchings are closed under coordinatewise minimum and maximum
of the men's partner ranks. If nonempty, they form a finite lattice under
the order above.
\end{lemma}
\begin{proof}
The union of two matchings $x,y$ decomposes into common edges and alternating
cycles. On a nontrivial cycle, suppose $m$ prefers $x(m)=w$ to $y(m)$,
and put $m'=y^{-1}(w)$. Stability of $y$ forces $w$ to prefer $m'$ to $m$.
Stability of $x$ then forces $m'$ to prefer $x(m')$ to $y(m')=w$.
Repeating around the cycle shows that all its men prefer their $x$ partners,
and all its women prefer their $y$ partners. The reverse case is symmetric.

Consequently, choosing the better partner for each man takes whole cycles
from $x$ or $y$ and yields a bijection $a$; choosing the worse yields a
bijection $b$. Each woman receives her less preferred old partner in $a$
and her more preferred old partner in $b$.

If $(m,w)$ blocked $a$, then $m$ would prefer $w$ to both his old partners.
Stability of each old matching would make $w$ prefer each of her old
partners to $m$, contradicting a block. If $(m,w)$ blocked $b$, choose an
old matching assigning $m$ the partner $b(m)$. Its stability makes $w$
prefer its partner to $m$; her partner in $b$ is at least as good.
Thus both $a$ and $b$ are stable. Finite closure provides a least and a
greatest matching and proves the assertion.
\end{proof}

\begin{lemma}[Covers are cyclic exchanges]\label{lem:cover}
If $x<y$ are stable matchings and no stable matching lies strictly between
them, then $y$ is obtained from $x$ by one nontrivial cyclic exchange.
\end{lemma}
\begin{proof}
Let $D=\{m:x(m)\ne y(m)\}$. For each $m\in D$, choose his most preferred
woman $a(m)$ satisfying
\begin{equation}\label{eq:acceptable}
 r_m(x(m))<r_m(a(m))\leq r_m(y(m)),\qquad
 s_{a(m)}(m)<s_{a(m)}(x^{-1}(a(m))).
\end{equation}
Such a woman exists: $y(m)$ qualifies by the opposite preference property
on alternating cycles. Put $h(m)=x^{-1}(a(m))$. Then $h(m)\ne m$.
Also $h(m)\in D$. Otherwise $y(h(m))=x(h(m))=a(m)$; bijectivity of $y$
and $h(m)\ne m$ imply $a(m)\ne y(m)$. The weak rank inequality in
\eqref{eq:acceptable} is then strict and $(m,a(m))$ blocks $y$.

The finite self-map $h:D\to D$ has a directed cycle $C$ of length at least
two. Change $x(m)$ to $a(m)=x(h(m))$ for $m\in C$, leaving other partners
unchanged, and call the resulting matching $z$. We have $x<z\leq y$,
and every woman affected by the cycle strictly improves relative to $x$.

An unchanged man cannot newly block. For a changed man $m$, a woman strictly
better than $x(m)$ cannot block, by stability of $x$ and the women's weak
improvement. His old partner $x(m)$ has strictly improved, so cannot block
either. Any remaining prospective blocking woman would lie strictly between
$x(m)$ and $a(m)$ on his list and prefer $m$ to her partner in $z$, hence
also to her partner in $x$. This contradicts the choice of $a(m)$.
Thus $z$ is stable. The cover hypothesis gives $z=y$.
\end{proof}

\begin{proposition}[Universal schedule reduction]\label{prop:reduction}
For every strict complete profile $P$ on $n$ men and $n$ women, there is a
cycle schedule $S$ such that
\begin{equation}\label{eq:reduction}
 |\Stab(P)|\leq |\Ideals(S)|.
\end{equation}
\end{proposition}
\begin{proof}
If the stable set is empty, the inequality holds for the empty schedule.
Otherwise choose a saturated chain from the least to the greatest stable
matching,
\[
 c_0<c_1<\cdots<c_t.
\]
By Lemma~\ref{lem:cover}, its steps are cyclic exchanges. A man's rank
strictly increases whenever he changes, so the sequence is a cycle schedule.

For a stable matching $x$ and $1\leq i\leq t$, form the lattice clamp
\[
 F_i(x)=(x\vee c_{i-1})\wedge c_i.
\]
It lies between the endpoints of a cover and hence equals one of them.
For each participant $m\in C_i$, the alternatives imply, respectively,
\begin{align}
 F_i(x)=c_{i-1}&\ \Longrightarrow\ r_m(x(m))\leq r_m(c_{i-1}(m)),\label{eq:clamp-low}\\
 F_i(x)=c_i&\ \Longrightarrow\ r_m(x(m))\geq r_m(c_i(m)).\label{eq:clamp-high}
\end{align}
Indeed, the clamped rank is
$\min\{\max\{r_m(x(m)),r_m(c_{i-1}(m))\},r_m(c_i(m))\}$,
and the two endpoint ranks are distinct.

Let $I(x)=\{i:F_i(x)=c_i\}$. If $i<j$ share a man and $j\in I(x)$,
then that man's rank in $x$ is at least his rank at $c_j$, and hence at
$c_i$. Alternative~\eqref{eq:clamp-low} at $i$ is impossible. Thus
$i\in I(x)$, and $I(x)$ is an ideal.

Fix a man. The partners he encounters at changes along the chain have
strictly increasing ranks, starting with his best stable partner and ending
with his worst. The clamp alternatives exclude any stable partner rank
strictly between two consecutive entries. Hence $x(m)$ is one of these
partners. Its position is precisely the prefix length of this man's events
selected by $I(x)$. Executing the ideal therefore recovers $x(m)$ for
every $m$. This proves that $x\mapsto I(x)$ is injective. A singleton
stable set yields an empty chain and is included.
\end{proof}

This reduction allows any initial matching $c_0$. Relabeling women by their
partners in $c_0$ makes it the identity without restricting the profile.
No hypothesis about columns of the preference tables, rotation lengths,
or the shape of the stable lattice is imposed.

\section{An exact recurrence for schedule ideals}\label{sec:frontier}

Consider a prefix of a schedule. For an ideal $I$ of the prefix, define its
\emph{frontier}
\[
 A(I)=\{m:\text{$m$ has no event in the prefix, or his latest event belongs to $I$}\}.
\]
Let $a(A)$ be the number of prefix ideals with frontier $A\subseteq[n]$.
The total ideal count is $T(a)=\sum_A a(A)$. Initially,
$a([n])=1$ and all other entries are zero.

\begin{lemma}[Frontier update]\label{lem:frontier}
When an event with support $C$ is appended, the new weights are obtained
by the additions
\begin{equation}\label{eq:frontier}
 a'(A\setminus C)\mathrel{+}=a(A)\quad\text{for every }A,
 \qquad
 a'(A)\mathrel{+}=a(A)\quad\text{if }C\subseteq A,
\end{equation}
starting from the zero vector.
\end{lemma}
\begin{proof}
Every old ideal extends by excluding the new event, giving frontier
$A\setminus C$. It extends by including the event precisely when all its
participants' earlier events have been selected, which is equivalent to
$C\subseteq A$. Inclusion then leaves frontier $A$. The restriction of an
extended ideal to the old prefix, together with its decision on the new
event, is unique. The two contributions therefore count all extensions
without omission or duplication.
\end{proof}

To record chronological legality, name each currently held woman by her
current holder. Let $R_{ij}=1$ if man $i$ has already visited the woman
currently held by man $j$. The diagonal entries equal one. A cyclic exchange
$q$ with support $C$ is legal exactly when
\begin{equation}\label{eq:legal}
 R_{i,q(i)}=0\qquad(i\in C).
\end{equation}
After the exchange, rename women by their new holders. The matrix update is
\begin{equation}\label{eq:matrix}
 R'_{ij}=R_{i,q(j)}\lor\ind_{i=j}.
\end{equation}
The column permutation records the new holder of every woman; the added
diagonal records the newly acquired partners. For a legal exchange, the
number of entries equal to one increases by $|C|$.

We call $s=(R,a)$ a state and write $s\cdot q=(R',a')$ for
\eqref{eq:frontier}--\eqref{eq:matrix}. The initial state is
\begin{equation}\label{eq:initial}
 R_{ij}=\ind_{i=j},\qquad a(A)=\ind_{A=[n]}.
\end{equation}
For every schedule, iterating these updates from the initial state gives
exactly its ideal count. The normalized matrix decides which future
chronological exchanges are legal; the weights give the exact effect of
each exchange on the ideal count.

\paragraph{Relabeling.}
If new man $i$ denotes old man $\pi(i)$, with normalized women relabeled
the same way, define
\begin{equation}\label{eq:relabel}
 R^\pi_{ij}=R_{\pi(i),\pi(j)},\qquad a^\pi(A)=a(\pi(A)).
\end{equation}
The corresponding event is $\pi^{-1}\circ q\circ\pi$. Substitution into
the transition formulas shows that relabeling commutes with transitions,
preserves legality, and preserves $T$. Thus it preserves all continuation
bounds. The certificate checks these equalities for each supplied
permutation; its correctness does not require a canonical labeling algorithm.

\section{A permanent bound for all continuations}\label{sec:permanent}

For a state $s=(R,a)$, define a zero--one matrix
\[
 B_R(i,j)=\ind_{\{i=j\text{ or }R_{ij}=0\}}
\]
and set
\begin{equation}\label{eq:perbound}
 U(R,a)=\sum_{A\subseteq[n]}a(A)\per(B_R[A,A]),
 \qquad \per(B_R[\varnothing,\varnothing])=1.
\end{equation}

\begin{proposition}[Continuation bound]\label{prop:perbound}
For a state reached by a schedule prefix, every finite legal continuation
has at most $U(R,a)$ ideals in total.
\end{proposition}
\begin{proof}
Fix a prefix ideal $I$ with frontier $A$. If $m\notin A$, his last prefix
event is excluded. Every future event involving him has that excluded event
as a predecessor, so no such event can be selected by an ideal extending $I$.
If $m\in A$, all his prefix events are selected, and his partner after
executing $I$ is the woman currently labeled $m$. Hence the men in $A$
hold exactly the women labeled by $A$.

Selected future events are confined to $A$, leaving the outside matching
fixed. Their final matching on $A$ uses either a current diagonal pair or
a pair unvisited by that man in the full chronological prefix. It is thus
a bijection counted by $\per(B_R[A,A])$. Distinct extensions of $I$ give
distinct final matchings by Lemma~\ref{lem:ideal-injection}. There are
$a(A)$ choices of $I$ with this frontier. Summing the bound over all old
ideals proves the claim.
\end{proof}

The checker also needs the bound for stored states without assuming that
each state is reachable. We next establish the stronger algebraic invariant
used in its soundness proof.

\subsection{Support expansion and monotonicity}

Let $\mathcal P(R)$ consist of permutations $\rho\in\Sn$ such that
$\rho(i)=i$ or $R_{i,\rho(i)}=0$ for every $i$. Put
$D(\rho)=\supp(\rho)$ and
\[
 Z_a(D)=\sum_{A\supseteq D}a(A).
\]
Extending a bijection of $A$ by the identity outside $A$ gives
\begin{equation}\label{eq:fullperm}
 U(R,a)=\sum_{\rho\in\mathcal P(R)}Z_a(D(\rho)).
\end{equation}
Different permutations with the same support remain different terms.

\begin{lemma}[Support formula]\label{lem:support}
Suppose $R$ has diagonal one, $a$ has nonnegative integer entries, and $q$
is a legal cyclic exchange with support $C$. Then
\begin{equation}\label{eq:support}
 U((R,a)\cdot q)=
 \sum_{\substack{\rho\in\mathcal P(R)\\
       D(\rho)\cap C=\varnothing\ \text{or}\ C\subseteq D(\rho)}}
 Z_a(D(\rho)).
\end{equation}
In particular, the value of this next-state bound depends on the support
of a legal exchange and not on its cyclic orientation.
\end{lemma}
\begin{proof}
Fix an old frontier $A$. The exclusion term in~\eqref{eq:frontier}
has permanent $\per(B_{R'}[A\setminus C,A\setminus C])$. The permutation
$q$ fixes columns outside $C$, so this equals
$\per(B_R[A\setminus C,A\setminus C])$. In old full-permutation notation,
it counts precisely $\rho\in\mathcal P(R)$ with
$D(\rho)\subseteq A$ and $D(\rho)\cap C=\varnothing$.

The inclusion term exists when $C\subseteq A$. If $\pi$ is an allowed
completion on $A$ in the new labels, its old-label form is
$\rho=q\circ\pi$. For a moved row of $\pi$, the condition
$R'_{i,\pi(i)}=0$ implies $R_{i,\rho(i)}=0$.
For a fixed row of $\pi$ that is moved by $q$, the same old entry is zero
by legality of $q$. Thus $\rho\in\mathcal P(R)$ and it fixes the
complement of $A$. Moreover, every $i\in C$ is moved by $\rho$: if
$\pi(i)=i$ this follows from $q(i)\ne i$; otherwise $\rho(i)=i$ would
contradict $R_{ii}=1$.

Conversely, suppose $\rho\in\mathcal P(R)$, $D(\rho)\subseteq A$,
and $C\subseteq D(\rho)$. Set $\pi=q^{-1}\circ\rho$. It fixes the
complement of $A$. If $\pi(i)\ne i$, then $\rho(i)\ne i$: otherwise
$i\notin C$ and $q^{-1}(i)=i$, a contradiction. Hence
$R_{i,\rho(i)}=0$; together with $i\ne\pi(i)$, formula~\eqref{eq:matrix}
gives $R'_{i,\pi(i)}=0$. This proves the desired bijection for inclusion.

For each $A$, the two contributions therefore count old allowed permutations
whose supports are contained in $A$ and either avoid or contain $C$.
These cases are disjoint because $C$ is nonempty. Summing with weight
$a(A)$ and interchanging the finite sums gives~\eqref{eq:support}.
\end{proof}

\begin{corollary}\label{cor:monotone}
For every state with diagonal one and nonnegative weights,
\[
 T(a)\leq U(R,a),\qquad U((R,a)\cdot q)\leq U(R,a)
\]
for every legal cyclic exchange $q$. If $U(R,a)\leq b$, then every finite
legal continuation has total weight at most $b$.
\end{corollary}
\begin{proof}
The identity permutation belongs to $\mathcal P(R)$ and contributes
$Z_a(\varnothing)=T(a)$ to~\eqref{eq:fullperm}. Formula~\eqref{eq:support}
retains a subset of its nonnegative summands, proving monotonicity.
Transitions preserve the diagonal and nonnegativity. Induction on the
continuation length proves the final assertion.
\end{proof}

The initial bound is $n!$; if all pairs have been visited it is just the
current total. A small bound therefore certifies the entire remaining
continuation, rather than only the count at the current prefix.

\section{The finite certificate for six participants per side}\label{sec:certificate}

Fix a threshold $b$. Write $\Safe_b(s)$ if every finite legal continuation
from $s$, including the empty continuation, has total weight at most $b$.
The following rules suffice:
\begin{enumerate}
\item If $U(s)\leq b$, then $\Safe_b(s)$ by Corollary~\ref{cor:monotone}.
\item If $T(s)\leq b$ and $\Safe_b(s\cdot q)$ for every legal cycle $q$,
then $\Safe_b(s)$, by separating the empty and nonempty continuations.
\item Relabeling a state as in~\eqref{eq:relabel} preserves $\Safe_b$.
\end{enumerate}
The stored states have diagonal one and nonnegative integer weights.

\begin{definition}[Local certificate]
A certificate consists of states $s_0,\ldots,s_{N-1}$, an initial-state
reference, and the following local data. Each state satisfies $T(s_i)\leq b$.
For every cycle $q$ legal at $s_i$, either the checker proves
$U(s_i\cdot q)\leq b$, or there is an index $j<i$ and a permutation
$\pi$ for which $(s_i\cdot q)^\pi=s_j$. The initial-state reference
identifies a relabeling of~\eqref{eq:initial} with a stored state.
\end{definition}

\begin{lemma}[Certificate soundness]\label{lem:certificate}
Every state in a valid local certificate satisfies $\Safe_b$. In particular,
every cycle schedule from the initial state has at most $b$ ideals.
\end{lemma}
\begin{proof}
Induct on the stored index. A legal successor is safe either by its permanent
bound or by a relabeling of an earlier safe state. The current total is at
most $b$, so rule 2 proves safety of the present state. The checked root
reference transfers safety to the initial state. The exact recurrence of
Section~\ref{sec:frontier} then bounds the ideal count of every schedule.
\end{proof}

For $n=6$ there are
\begin{equation}\label{eq:cycles}
 \sum_{k=2}^6 {6\choose k}(k-1)!=409
\end{equation}
nontrivial single cycles. A cycle is represented by listing its least
participant first and then ordering the remaining participants. Both
orientations are retained whenever they differ. The formal development
checks coverage of every single-cycle permutation on six labels.

\begin{proposition}[Checked certificate]\label{prop:checked}
There is a valid local certificate at threshold $48$ for the initial state
on six labels, with $135{,}828$ stored states and $177{,}338$ reference edges.
Its root is stored node $135{,}827$ in zero-based indexing.
\end{proposition}
\begin{proof}[Computational proof]
The certificate is the file \code{certificate-n6.json} in the accompanying
artifact. Each stored state is represented by six row masks and 64 natural
number weights. Each explicit edge contains a cycle index, a referenced
state, and a relabeling permutation. The checker verifies the state format,
diagonal, current total, and every one of the 409 possible cycle moves.
For a legal move, it checks either an explicit reference or the
support-form upper bound from Lemma~\ref{lem:support}. The reference check
compares the entire transformed matrix and weight vector with the target.
The bound check retains multiplicities of permutations sharing a support.
All sums and comparisons are over natural numbers.

The exported data are converted to explicit Lean definitions and local
Boolean-check theorems, proved by kernel reduction. A proved checker
soundness theorem combines each local check with the already proved safety
of its referenced states. The generated proof graph is acyclic; every
reference is discharged by an earlier safety theorem. The checked root
equality identifies the last state with the initial state, using the
identity relabeling for this certificate.

All local checks and all safety theorems compiled successfully.
This includes the root theorem
\code{StableSix.ProductionChunks.initial_safe}.
The final full-source run accepted all 2,181 modules and then checked the
unconditional public theorem and its transitive axioms.
Section~\ref{sec:formal} specifies the source identities and audit.
\end{proof}

For clarity, the mathematical content of the local checking procedure can
be written as follows. The actual implementation uses sparse weights and
reuses support sums, but proves their connection to these conditions.
\begin{lstlisting}
check_state(i):
    require valid_state(s[i]) and total(s[i]) <= 48
    for each of the 409 single cycles q:
        if not legal(s[i], q): continue
        if a checked reference (j, pi) satisfies
             j < i and relabel(next(s[i], q), pi) == s[j]:
            continue
        require support_bound(s[i], support(q)) <= 48
    accept
\end{lstlisting}

\paragraph{Generation and coverage.}
An external search generates candidate data using the normalized recurrence,
permanent pruning, and memoization up to simultaneous relabeling. The
recorded certificate replay has $4{,}228{,}638$ legal transitions:
$4{,}051{,}300$ are discharged by the bound and $177{,}338$ by references.
These replay counts describe the artifact; the formal proof uses the
verified local checks and cycle coverage. It does not assume correctness
of the search, its hash table, canonicalization, or replay program.
Neither a timeout nor an observed maximum in a partial search is used as
an upper bound. There is no restriction to swaps, to Latin profiles, or
to a selected first event.

\begin{corollary}\label{cor:upper}
Every strict complete six-by-six preference profile has at most 48 stable
matchings.
\end{corollary}
\begin{proof}
Proposition~\ref{prop:checked} and Lemma~\ref{lem:certificate} bound the
number of ideals of every cycle schedule on six labels by 48.
Apply Proposition~\ref{prop:reduction} to the arbitrary profile.
\end{proof}

\section{A known profile attaining 48}\label{sec:lower}

Benjamin, Converse, and Krieger~\cite[Theorem~3 and Section~5]{BCK95}
analyzed the dihedral/Latin construction $DS_n$. Their counting formula
gives $(3+1)\binom{6}{3}-2^5=48$ stable matchings for $DS_3$, an instance
with six participants on each side. The following rank tables use the
presentation attributed to Converse and reproduced by
Eilers~\cite{EilersLatin}. In the left table,
row $m$, column $w$ is $r_m(w)$. In the right table, row $w$, column $m$
is $s_w(m)$. Entries are ranks starting at zero, not lists of partner labels.
\begin{equation}\label{eq:witness}
 (r_m(w))_{m,w}=
 \begin{pmatrix}
 0&1&2&3&4&5\\
 1&0&3&2&5&4\\
 2&5&4&1&0&3\\
 3&4&5&0&1&2\\
 4&3&0&5&2&1\\
 5&2&1&4&3&0
 \end{pmatrix},\qquad
 (s_w(m))_{w,m}=
 \begin{pmatrix}
 5&4&3&2&1&0\\
 4&5&0&1&2&3\\
 3&2&1&0&5&4\\
 2&3&4&5&0&1\\
 1&0&5&4&3&2\\
 0&1&2&3&4&5
 \end{pmatrix}.
\end{equation}
Each row is a permutation, so these are strict complete preferences.
For every pair $(m,w)$ the two ranks sum to five.

\begin{lemma}\label{lem:lower}
The profile in~\eqref{eq:witness} has at least 48 stable matchings.
\end{lemma}
\begin{proof}
Table~\ref{tab:matchings} lists 48 distinct permutations
$p=(p(0),\ldots,p(5))$. For each listed permutation and every pair $(m,w)$,
direct substitution in~\eqref{eq:witness} verifies
\[
 r_m(w)\geq r_m(p(m))\quad\text{or}\quad
 s_w(m)\geq s_w(p^{-1}(w)).
\]
Thus each is stable. The formal proof checks the row inverses for the rank
tables, inverse tables for all listed matchings, stability, and distinctness
by kernel reduction, giving an injection from a 48-element type into the
stable matchings of this profile.
\end{proof}

\begin{proof}[Proof of Theorem~\ref{thm:main}]
Corollary~\ref{cor:upper} gives the universal upper bound, and
Lemma~\ref{lem:lower} gives an attaining profile. The profile consequently
has exactly 48 stable matchings.
\end{proof}

\section{Formal verification and reproducibility}\label{sec:formal}

\subsection{Statement and proof coverage}

The formal model assigns each person an independent permutation of ranks.
A matching is a permutation, and stability is exactly~\eqref{eq:stable}.
The public proposition is
\begin{lstlisting}
def MaximumStableSixIs48 : Prop :=
  (forall P : Profile 6, Nat.card (StableMatching P) <= 48) /\
    (exists P : Profile 6, Nat.card (StableMatching P) = 48)
\end{lstlisting}
The notation above uses ASCII equivalents of the logical symbols in the
source. The checked endpoint is
\begin{lstlisting}
StableSix.maximumStableSixIs48 : StableSix.MaximumStableSixIs48
\end{lstlisting}
It has no profile restriction and no remaining safety or certificate-validity
premise. In particular, the intermediate theorem taking initial-state safety
as a hypothesis is closed by the proved concrete root theorem.

The model includes all strict complete six-by-six profiles. Each row is
independent of every other row. The stable-matching subtype is finite, so
its \code{Nat.card} is the usual cardinality. The statement does not concern
ties, incomplete lists, unequal sides, or stable roommates.

Table~\ref{tab:formal} identifies the main formal components. The proof
includes the universal reduction, rather than treating it as an assumption
attached to a finite census. In particular, the initial state corresponds
to any initial matching after normalization, and the safety property covers
all finite legal paths, including the empty one.

\begin{table}[htbp]
\centering\small
\begin{tabular}{@{}p{0.37\linewidth}p{0.58\linewidth}@{}}
\toprule
Mathematical component & Lean source or endpoint within \code{StableSix}\\
\midrule
Preference model and lattice & \code{Profile.lean}\\
Cover cycles and clamp injection & \code{Reduction.lean}, \code{Profile.exists_schedule}\\
Exact frontier recurrence & \code{Frontier.lean}\\
Permanent bound and support identity & \code{Permanent.lean}, \code{SupportBound.lean}\\
Safety and relabeling & \code{Certificate.lean}, \code{Symmetry.lean}\\
Executable bound and state correspondence & \code{RawSupportEnumeration.lean}, \code{RawBridge.lean}\\
Concrete checker soundness & \code{ReferenceFirstSoundness.lean}\\
Complete cycle coverage and certificate & \code{ProductionChunks/Moves.lean}, \code{Check/}, \code{Safe/}, \code{Root.lean}\\
Known lower witness & \code{LowerBound.lean}\\
Full endpoint & \code{Statement.lean}, \code{Main.lean}; top-level \code{Verification.lean}\\
\bottomrule
\end{tabular}
\caption{Correspondence between the paper and the checked development.}
\label{tab:formal}
\end{table}

\subsection{Concrete computation and the trust boundary}

There are 135,828 certificate states; these are compressed matrix-and-weight
states, not preference profiles or independent mathematical conjectures.
The generated files separate local checks from their safety composition,
allowing independent checks to run concurrently while their dependencies
are composed in order. The complete local source graph contains 2,181
modules. All were accepted, including the final module
\code{Verification}, which prints the expanded proposition, preference and
stability definitions, and the endpoint axiom dependencies.

The three public endpoints---the exact-maximum theorem, universal upper
bound, and existential attainment---have the transitive axiom list
\begin{lstlisting}
[propext, Classical.choice, Quot.sound]
\end{lstlisting}
No \code{sorryAx}, new mathematical axiom, \code{native_decide}, or
external-certificate oracle occurs in these dependencies. Concrete local
checks use \code{decide +kernel}; externally generated data acquire
mathematical force only through the kernel-checked Boolean results and
the proved soundness theorems. Natural-number arithmetic avoids machine
integer overflow in the formal checks. The support enumeration has a
proved weighted coverage inequality, so possible duplicate entries could
only increase its nonnegative bound; equal supports are not silently
deduplicated.

The successful verification uses Lean~4.27.0 and mathlib commit
\begin{center}\small\ttfamily
a3a10db0e9d66acbebf76c5e6a135066525ac900.
\end{center}
It reuses 769 audited modules checked on macOS arm64 and checks the remaining
1,412 modules on Linux x86\_64. The migrated proof objects and recorded
external proof artifacts were checked for byte identity. Thus the recorded
run is a complete reproduction with an audited migrated prefix, not a
fresh build of every module on Linux. The final module finished on
14 October 2026 at 20:50 UTC.

The post-run audit matched the source inventory and dependency pins,
every accepted compilation receipt and compiler log, the final theorem,
and the actual compiled proof objects. It also checked the recorded
source/object import resolution and coupled those checks to the final
2,181-module checkpoint. These are execution-integrity checks; their hashes
are not mathematical axioms. The trust boundary includes Lean's kernel
and the pinned imported dependency caches.

\subsection{Artifact contents}

The accompanying archive \code{stable-six-artifact.tar.gz} contains the
complete Lean source, the certificate, the lower witness, the pinned
toolchain and dependency manifest, and reproduction instructions. The
verification evidence records the actual commands, accepted source hashes,
compiler output, migration provenance, resource policies, and final audits.
The certificate SHA-256 is
\begin{center}\small\ttfamily
4f12664594d20f916e8e0534428dab83a58e6\\
bdd1c06f08767173090420fa5a7.
\end{center}
For the recorded run, the checked source-inventory SHA-256 is
\begin{center}\small\ttfamily
57bb8bf3d6147a175a88d51ecce218dc1b\\
1812be85a00b20a7d0a8195e1ad0e1.
\end{center}
The line breaks in these displayed digests are typographical only.

The archive preserves the original verification snapshot, including the
manuscript and README prepared on 15 October 2026. The present revision
supersedes their contribution statements by correcting the prior-work
attribution. The Lean sources and verification evidence are unchanged.

A fresh reproduction should use a separate working directory, preserve
the pinned versions, and follow the supplied dependency order and resource
instructions. The final accepted command used a 32\,GiB Lean memory limit
and a 128\,MiB stack. Several earlier checks required larger limits or
longer timeouts than the initial settings; completed proof objects were
retained and the mathematical source was unchanged. The recorded result
is established by the completed run and final audits, not by a promise
that a default-resource build will finish within a particular time.

\appendix
\section{The 48 matching witnesses}\label{app:witnesses}

The tuple $p(0)p(1)\cdots p(5)$ denotes the women assigned, in order, to
men $0,1,\ldots,5$. All entries refer to the rank tables
in~\eqref{eq:witness}. The list is the one used in
\code{StableSix.LowerBound.matchingTable}.

\begin{table}[htbp]
\centering
\begin{tabular}{@{}rr@{\qquad}rr@{\qquad}rr@{}}
\toprule
Index & Matching & Index & Matching & Index & Matching\\
\midrule
1 & \texttt{013425} & 17 & \texttt{203541} & 33 & \texttt{352041}\\
2 & \texttt{013452} & 18 & \texttt{204351} & 34 & \texttt{352104}\\
3 & \texttt{013542} & 19 & \texttt{230451} & 35 & \texttt{420513}\\
4 & \texttt{014325} & 20 & \texttt{230514} & 36 & \texttt{425013}\\
5 & \texttt{014352} & 21 & \texttt{230541} & 37 & \texttt{425103}\\
6 & \texttt{103425} & 22 & \texttt{235014} & 38 & \texttt{425130}\\
7 & \texttt{103452} & 23 & \texttt{235041} & 39 & \texttt{451203}\\
8 & \texttt{103542} & 24 & \texttt{235104} & 40 & \texttt{451230}\\
9 & \texttt{104325} & 25 & \texttt{320451} & 41 & \texttt{452013}\\
10 & \texttt{104352} & 26 & \texttt{320514} & 42 & \texttt{452103}\\
11 & \texttt{130425} & 27 & \texttt{320541} & 43 & \texttt{452130}\\
12 & \texttt{130452} & 28 & \texttt{325014} & 44 & \texttt{541203}\\
13 & \texttt{130542} & 29 & \texttt{325041} & 45 & \texttt{541230}\\
14 & \texttt{135042} & 30 & \texttt{325104} & 46 & \texttt{542013}\\
15 & \texttt{203451} & 31 & \texttt{351204} & 47 & \texttt{542103}\\
16 & \texttt{203514} & 32 & \texttt{352014} & 48 & \texttt{542130}\\
\bottomrule
\end{tabular}
\caption{Forty-eight distinct stable matchings of the known dihedral profile.}
\label{tab:matchings}
\end{table}

\begin{thebibliography}{10}

\bibitem{GS62}
D.~Gale and L.~S.~Shapley.
College admissions and the stability of marriage.
\emph{The American Mathematical Monthly} 69(1) (1962), 9--15.
\href{https://doi.org/10.1080/00029890.1962.11989827}{doi:10.1080/00029890.1962.11989827}.

\bibitem{BCK95}
A.~T.~Benjamin, C.~Converse, and H.~A.~Krieger.
How do I marry thee? Let me count the ways.
\emph{Discrete Applied Mathematics} 59(3) (1995), 285--292.
\href{https://doi.org/10.1016/0166-218X(95)80006-P}{doi:10.1016/0166-218X(95)80006-P}.

\bibitem{Jo26}
M.~Jo.
Small rotation blocks and the order-six stable marriage problem.
Zenodo preprint, first deposited 20 September 2026,
\href{https://doi.org/10.5281/zenodo.22860585}{doi:10.5281/zenodo.22860585}.
Version v09, 23 September 2026,
\href{https://doi.org/10.5281/zenodo.22909380}{doi:10.5281/zenodo.22909380}.
Theorem and section references are to v09.

\bibitem{Thurber02}
E.~G.~Thurber.
Concerning the maximum number of stable matchings in the stable marriage problem.
\emph{Discrete Mathematics} 248 (2002), 195--219.
\href{https://doi.org/10.1016/S0012-365X(01)00194-7}{doi:10.1016/S0012-365X(01)00194-7}.

\bibitem{KOGW18}
A.~R.~Karlin, S.~Oveis Gharan, and R.~Weber.
A simply exponential upper bound on the maximum number of stable matchings.
In \emph{Proceedings of STOC 2018}, 920--925.
\href{https://arxiv.org/abs/1711.01032}{arXiv:1711.01032}.

\bibitem{PP21}
C.~Palmer and D.~P\'alv\"olgyi.
At most $3.55^n$ stable matchings.
\href{https://arxiv.org/abs/2011.00915v2}{arXiv:2011.00915v2}, 2021.

\bibitem{CT19}
L.~Cai and C.~Thomas.
Representing all stable matchings by walking a maximal chain.
\href{https://arxiv.org/abs/1910.04401}{arXiv:1910.04401}, 2019.

\bibitem{Borodin24}
M.~Borodin, A.~Duncan, B.~Litchev, J.~Liu, V.~Moroz, M.~Qian,
R.~Raghavan, G.~Rastogi, M.~Voigt, and T.~Khovanova.
Sequences of the stable matching problem.
\emph{Journal of Integer Sequences} 27 (2024), Article 24.2.2.
\url{https://cs.uwaterloo.ca/journals/JIS/VOL27/Khovanova/khova32.html}.

\bibitem{EilersExact}
D.~Eilers.
Sequence A357269: maximum number of stable matchings in the stable marriage problem.
\emph{The On-Line Encyclopedia of Integer Sequences}.
\url{https://oeis.org/A357269}. Accessed 15 October 2026.

\bibitem{EilersLower}
D.~Eilers.
Sequence A357271: lower bounds for the maximum number of stable matchings
in the stable marriage problem based on composing smaller instances.
\emph{The On-Line Encyclopedia of Integer Sequences}.
\url{https://oeis.org/A357271}. Accessed 15 October 2026.

\bibitem{EilersLatin}
D.~Eilers.
Sequence A351413: maximum number of stable matchings in the Latin marriage problem.
\emph{The On-Line Encyclopedia of Integer Sequences}.
Includes the dihedral construction attributed to C.~Converse's 1992 thesis.
\url{https://oeis.org/A351413}. Accessed 15 October 2026.

\end{thebibliography}
\end{document}