\documentclass[11pt]{amsart}
\usepackage{amssymb,amsmath,amsthm}
\usepackage[margin=1.2in]{geometry}
\usepackage{hyperref}
\usepackage{xcolor}
\usepackage{framed}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{fact}[theorem]{Fact}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{question}[theorem]{Question}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}

\newcommand{\w}{\omega}
\newcommand{\ww}{\omega^\omega}
\newcommand{\bb}{\mathfrak b}
\newcommand{\dd}{\mathfrak d}
\newcommand{\cc}{\mathfrak c}
\newcommand{\covM}{\operatorname{cov}(\mathcal M)}
\newcommand{\cf}{\operatorname{cf}}
\newcommand{\forces}{\Vdash}
\newcommand{\les}{\le^*}
\newcommand{\PP}{\mathbb P}
\newcommand{\res}{{\restriction}}
\newcommand{\conc}{{}^\frown}
\newcommand{\K}{\mathbb K}
\newcommand{\suc}{\operatorname{succ}}
\newcommand{\st}{\operatorname{stem}}

\title{A Michael space in the Laver model}
\date{Draft of 10 November 2026}

\subjclass[2020]{Primary 54D20, 03E35; Secondary 54B10, 03E17}
\keywords{Michael space, Lindel\"of space, Laver forcing, Michael sequence, dominating real}

\begin{document}

\begin{abstract}
A Michael space is a regular Lindel\"of space whose product with the
irrationals fails to be Lindel\"of. Whether such a space exists in
\textsf{ZFC} is a sixty-year-old problem of E.~Michael. We show that one
exists in the Laver model, where every previously known construction breaks
down: there $\covM=\aleph_1<\bb=\dd=\aleph_2$ and there are no selective
ultrafilters. Two ingredients go into the proof. The first is a dichotomy
for countable support iterations of Laver forcing of any length: each real
in the extension is either bounded by a real of the ground model, or
dominates every real of the ground model along one infinite set. The second
is a \textsf{ZFC} theorem saying that, when $\bb=\dd$, a scale which
satisfies this dichotomy at its points of uncountable cofinality gives rise
to a Michael sequence in the sense of J.~T.~Moore.
\end{abstract}

\maketitle


\section{Introduction}

In 1963 E.~Michael \cite{Mic} used the Continuum Hypothesis to build a
Lindel\"of space whose product with the space $\ww$ of irrationals is not
normal, and in particular not Lindel\"of. The example showed how badly the
Lindel\"of property can behave under products, even when one factor is as
tame as the irrationals. A regular Lindel\"of space $X$ for which
$X\times\ww$ is not Lindel\"of has since been called a \emph{Michael space},
and \emph{Michael's problem} asks whether one can be constructed without any
hypothesis beyond \textsf{ZFC}. The problem is still open.

What is known is that a Michael space exists whenever the cardinal
characteristics of the continuum are arranged favourably. This is the case
if $\bb=\aleph_1$ (Lawrence \cite{Law}), under Martin's Axiom (Alster
\cite{Als}), if $\dd=\covM$ (Moore \cite{Moo}), and if there is a selective
ultrafilter and $\max\{\bb,\mathfrak g\}=\dd$ (Mart\'inez-Celis \cite{MC}).
Moore's paper also changed the shape of the problem. He showed that building
a Michael space comes down to building a certain increasing sequence of sets
of irrationals, a \emph{Michael sequence} (Definition~\ref{def:ms}), so that
the question is really one about the combinatorics of $\ww$.

A model of \textsf{ZFC} without a Michael space, if there is one, must
defeat all of these constructions at once. The most natural place to look is
the Laver model, obtained by iterating Laver forcing $\w_2$ times with
countable support over a model of \textsf{CH} \cite{Lav}. In that model
$\covM=\aleph_1$ while $\bb=\dd=\aleph_2$, and by a theorem of Miller
\cite{Mil} there are no Q-points, hence no selective ultrafilters. So none of
the results above applies, and to our knowledge it was not known whether the
Laver model contains a Michael space; compare the discussion and questions
in \cite{MC}. Our main result is that it does.

\begin{theorem}\label{thm:main}
There is a Michael space in the Laver model.
\end{theorem}

The proof separates cleanly into a forcing part and a combinatorial part,
and each may be of interest on its own. Throughout, for $u,h\in\ww$ and
$A\subseteq\w$ we write $h\les u\res A$ to mean that $h(k)\le u(k)$ for all
but finitely many $k\in A$.

The forcing part describes how a new real can sit relative to the old ones
after a Laver iteration. One might expect many intermediate behaviours: a
new real could be unbounded over the ground model and yet exceed each ground
model function only on a set that depends on the function. The theorem says
that this does not happen.

\begin{theorem}[Dichotomy]\label{thm:dich}
Let $W$ be a model of \textsf{ZFC}, let $\alpha\ge 1$ be an ordinal, and let
$G$ be generic over $W$ for the countable support iteration $\PP_\alpha$ of
Laver forcing of length $\alpha$. For every $u\in\ww\cap W[G]$, exactly one of
the following holds.
\begin{enumerate}
\item $u\les h^*$ for some $h^*\in\ww\cap W$.
\item There is an infinite $A\subseteq\w$ in $W[G]$ such that $h\les u\res A$
for every $h\in\ww\cap W$.
\end{enumerate}
\end{theorem}

The combinatorial part is a theorem of \textsf{ZFC}. It says that the
simplest conceivable candidate for a Michael sequence, the one read off
directly from a scale, works as soon as the scale obeys the same dichotomy.

\begin{theorem}[\textsf{ZFC}]\label{thm:scale}
Assume $\bb=\dd=\kappa$ and let $\langle g_\gamma:\gamma<\kappa\rangle$ be a
scale. Suppose that for every $\alpha<\kappa$ of uncountable cofinality and
every $u\in\ww$, either $u\les g_\gamma$ for some $\gamma<\alpha$, or there is
an infinite $A\subseteq\w$ with $g_\gamma\les u\res A$ for all
$\gamma<\alpha$. Then there is a $\kappa$-Michael sequence, and therefore a
Michael space.
\end{theorem}

When $\kappa=\aleph_1$ there are no ordinals $\alpha<\kappa$ of uncountable
cofinality, the hypothesis is empty, and Theorem~\ref{thm:scale} becomes the
familiar fact that $\bb=\dd=\aleph_1$ yields a Michael space. The content of
the theorem lies in the case $\kappa>\aleph_1$.

Theorem~\ref{thm:main} follows by combining the two: in the Laver model the
Laver reals form a scale, and Theorem~\ref{thm:dich}, applied over the
intermediate models, shows that this scale satisfies the hypothesis of
Theorem~\ref{thm:scale}.

A word on the proof of Theorem~\ref{thm:dich}. The obvious strategy is an
induction on the length of the iteration, and it runs into trouble at limit
stages of countable cofinality, where a condition can make demands at
infinitely many coordinates simultaneously. We avoid the induction
altogether. Laver showed \cite[Lemma~14]{Lav} that a name for a real can be
approximated, at each node of the first coordinate's tree, by finitely many
candidate reals from the ground model. We apply this lemma once, after
allowing the candidates to take the value $\infty$. A candidate with an
entry $\infty$ at position $k$ records that $u(k)$ is being pushed to
infinity as the first Laver real grows, and the dichotomy is decided by
whether such candidates keep appearing along the generic branch. Only the
first coordinate is examined, so the length of the iteration plays no role.

The paper is organised as follows. Section~\ref{sec:prelim} fixes notation and
recalls Michael sequences. Section~\ref{sec:scale} proves
Theorem~\ref{thm:scale}. Section~\ref{sec:laver} recalls what we need about
Laver forcing, and Section~\ref{sec:dich} proves Theorem~\ref{thm:dich}.
Section~\ref{sec:main} derives Theorem~\ref{thm:main}, and
Section~\ref{sec:questions} collects remarks and questions.

\section{Preliminaries}\label{sec:prelim}

For $f,g\in\ww$, $f\les g$ means $f(n)\le g(n)$ for all but finitely many $n$,
and $f<^* g$ means $f(n)<g(n)$ for all but finitely many $n$. The cardinals
$\bb$ and $\dd$ are the least sizes of an unbounded and of a dominating
subfamily of $(\ww,\les)$. A \emph{scale} is a $\les$-dominating sequence
$\langle g_\gamma:\gamma<\kappa\rangle$ with $g_\gamma<^* g_\delta$ for
$\gamma<\delta$; a scale of length $\kappa$ exists if and only if
$\bb=\dd=\kappa$. For $s\in\w^{<\w}$ let $[s]=\{x\in\ww:s\subseteq x\}$. For
closed $K\subseteq\ww$, the tree of $K$ is $\{x\res n:x\in K,\ n<\w\}$. For
$g\in\ww$ and $m<\w$ put
\[
B_m(g)=\{x\in\ww:\ x(n)\le g(n)\text{ for all }n\ge m\}.
\]
Each $B_m(g)$ is closed, and the set of reals eventually below $g$ is the
increasing union $\bigcup_m B_m(g)$. A compact subset of $\ww$ is always
contained in some $B_0(g)$.

\begin{definition}[Moore \cite{Moo}; in this form \cite{MC}]\label{def:ms}
Let $\theta$ be an ordinal of uncountable cofinality. A
\emph{$\theta$-Michael sequence} is a strictly increasing sequence
$\langle Y_\alpha:\alpha\le\theta\rangle$ of subsets of $\ww$ with
$Y_\theta=\ww$ such that for every compact $K\subseteq\ww$ and every
$\alpha\le\theta$ of uncountable cofinality, if $K\subseteq Y_\alpha$ then
$K\subseteq Y_\gamma$ for some $\gamma<\alpha$.
\end{definition}

In words: the sets $Y_\alpha$ exhaust the irrationals, and a compact set can
never be captured for the first time at a stage of uncountable cofinality.
Moore's original formulation uses the complements of the sets $Y_\alpha$
inside a compactification of $\ww$ with countable remainder; the two
formulations are equivalent.

\begin{theorem}[Moore {\cite[Corollary~1.4]{Moo}}]\label{thm:moore}
If there is a $\theta$-Michael sequence for some $\theta$ of uncountable
cofinality, then there is a Michael space.
\end{theorem}

The next proposition is not needed for the main theorem, but it explains
where the difficulty lies. A Michael sequence of regular length must have
length between $\bb$ and $\dd$. So once $\bb>\aleph_1$, the sequence has
length at least $\w_2$ and the defining condition has to be verified at
ordinals of cofinality $\w_1$ strictly inside it. Those are exactly the
ordinals addressed by the hypothesis of Theorem~\ref{thm:scale}.

\begin{proposition}\label{prop:length}
If $\theta$ is regular uncountable and there is a $\theta$-Michael sequence,
then $\bb\le\theta\le\dd$.
\end{proposition}

\begin{proof}
Let $\langle Y_\alpha:\alpha\le\theta\rangle$ be a $\theta$-Michael sequence.
By the condition at $\alpha=\theta$, every compact set is contained in some
$Y_\gamma$ with $\gamma<\theta$, and since $\cf(\theta)>\w$ the same holds for
every $\sigma$-compact set.

Suppose $\theta<\bb$. For each $\xi<\theta$ choose $f_\xi\notin Y_\xi$ and let
$h\in\ww$ with $f_\xi\les h$ for all $\xi$. The set $\{f:f\les h\}$ is
$\sigma$-compact, so it is contained in some $Y_\gamma$, $\gamma<\theta$. But
then $f_\gamma\in Y_\gamma$, a contradiction.

Suppose $\theta>\dd$ and let $\{h_i:i<\dd\}$ be dominating. Each
$\{f:f\les h_i\}$ is contained in some $Y_{\gamma_i}$, and
$\gamma=\sup_i\gamma_i<\theta$. Then $Y_\gamma=\ww$, contradicting strict
monotonicity.
\end{proof}

\section{Michael sequences from scales}\label{sec:scale}

Given a scale $\langle g_\gamma:\gamma<\kappa\rangle$, the obvious candidate
for a Michael sequence is
\[
Y_\alpha=\{x\in\ww:\ x\les g_\gamma\text{ for some }\gamma<\alpha\},
\qquad\alpha\le\kappa,
\]
the reals bounded by an initial segment of the scale. What could go wrong is
the following. Take $\alpha$ of uncountable cofinality and a compact set $K$
every point of which is bounded by some $g_\gamma$ with $\gamma<\alpha$. We
need a single $\gamma<\alpha$ that works for all of $K$, and there is no
reason for one to exist: the bounds may climb cofinally in $\alpha$ as the
point moves through $K$. The proof shows that if they do climb, then inside
$K$ there is a point that escapes every $g_\gamma$, $\gamma<\alpha$. The
escaping point is built by walking up the tree of $K$ and, at each step,
taking a value as large as $K$ allows at a well-chosen coordinate. The
hypothesis of the theorem is what tells us which coordinates to choose.

\begin{proof}[Proof of Theorem~\ref{thm:scale}]
Define $Y_\alpha$ as above. The sequence is strictly increasing, since
$g_\gamma\in Y_{\gamma+1}\setminus Y_\gamma$, and $Y_\kappa=\ww$ because the
$g_\gamma$ are dominating. A compact set lies in some $B_0(h)$, and
$h\les g_\gamma$ for some $\gamma$, so the condition of
Definition~\ref{def:ms} holds at $\alpha=\kappa$.

Now fix $\alpha<\kappa$ with $\cf(\alpha)>\w$ and a compact
$K\subseteq Y_\alpha$. The set $K$ is covered by the closed sets
$B_m(g_\gamma)$ with $\gamma<\alpha$ and $m<\w$. We first discard the part
of $K$ where countably many of them suffice. Let $O$ be the union of all
relatively open subsets of $K$ which are covered by countably many sets
$B_m(g_\gamma)$, $\gamma<\alpha$. Since $K$ is second countable, $O$ is
itself covered by countably many such sets. Let $K'=K\setminus O$.

If $K'=\emptyset$, then $K$ is covered by sets $B_{m_j}(g_{\gamma_j})$,
$j<\w$, with $\gamma_j<\alpha$. As $\cf(\alpha)>\w$ there is $\gamma<\alpha$
above all $\gamma_j$, and $K\subseteq Y_\gamma$, which is what we want.

So suppose, towards a contradiction, that $K'\ne\emptyset$. Let $T$ be the
tree of $K'$. For $t\in T$ let $u_t\in\ww$ record the largest values that
points of $K'$ passing through $t$ can take:
\[
u_t(n)=\max\{x(n):\ x\in K',\ t\subseteq x\}.
\]

\smallskip\noindent\emph{Claim.} For no $t\in T$ and $\gamma<\alpha$ is
$u_t\les g_\gamma$.

\smallskip
Indeed, if $u_t\les g_\gamma$ then $K'\cap[t]\subseteq B_m(g_\gamma)$ for some
$m$. Then $K\cap[t]\subseteq O\cup B_m(g_\gamma)$ would be a relatively open
subset of $K$ covered by countably many of our closed sets, so
$K\cap[t]\subseteq O$ and $K'\cap[t]=\emptyset$, contradicting $t\in T$.

\smallskip
So every $u_t$ falls under the second alternative of the hypothesis: for each
$t\in T$ there is an infinite $A_t\subseteq\w$ along which $u_t$ dominates
the whole initial segment of the scale, that is,
$g_\gamma\les u_t\res A_t$ for all $\gamma<\alpha$. How far out one must go
before $u_t$ exceeds $g_\gamma$ on $A_t$ depends on $\gamma$; let
$F_\gamma(t)$ be the least $N$ such that $g_\gamma(n)\le u_t(n)$ for all
$n\in A_t$ with $n\ge N$. There are fewer than $\bb$ functions $F_\gamma$,
all defined on the countable set $T$, so a single $e:T\to\w$ dominates them:
for every $\gamma<\alpha$, $F_\gamma(t)\le e(t)$ for all but finitely many
$t\in T$.

We now walk up the tree. Let $t_0=\emptyset$. Given $t_k\in T$, pick a
coordinate in $A_{t_k}$ beyond both the length of $t_k$ and the threshold
$e(t_k)$,
\[
n_k=\min\bigl(A_{t_k}\setminus\max(|t_k|,e(t_k))\bigr),
\]
choose a point $x_k\in K'\cap[t_k]$ which attains the maximum there,
$x_k(n_k)=u_{t_k}(n_k)$, and let $t_{k+1}=x_k\res(n_k+1)$. The nodes $t_k$
are strictly increasing, so they are pairwise distinct and
$x=\bigcup_k t_k$ is a point of $K'$ with $x(n_k)=u_{t_k}(n_k)$ for all $k$.

This $x$ escapes the initial segment. Let $\gamma<\alpha$; then also
$\gamma+1<\alpha$. For all but finitely many $k$ we have
$F_{\gamma+1}(t_k)\le e(t_k)\le n_k$ and $n_k\in A_{t_k}$, hence
\[
x(n_k)=u_{t_k}(n_k)\ge g_{\gamma+1}(n_k)>g_\gamma(n_k),
\]
where the strict inequality holds for all large $k$ because
$g_\gamma<^*g_{\gamma+1}$ and $n_k\to\infty$. So $x\not\les g_\gamma$. Since
$\gamma<\alpha$ was arbitrary, $x\notin Y_\alpha$, contradicting
$x\in K'\subseteq K\subseteq Y_\alpha$.

Hence $\langle Y_\alpha:\alpha\le\kappa\rangle$ is a $\kappa$-Michael
sequence, and Theorem~\ref{thm:moore} gives a Michael space.
\end{proof}

\begin{remark}
The hypothesis of Theorem~\ref{thm:scale} can be read as a statement about
towers. For $u$ not below any $g_\gamma$, $\gamma<\alpha$, the sets
$\{k:u(k)\ge g_\gamma(k)\}$ form a $\subseteq^*$-decreasing sequence of
infinite sets, and the set $A$ we ask for is an infinite
pseudo-intersection. If $\mathfrak t=\dd$ the sequence is shorter than
$\mathfrak t$ and a pseudo-intersection exists for free, so every scale
satisfies the hypothesis. Since $\mathfrak t\le\covM$, that case is already
covered by Moore's theorem for $\dd=\covM$. In the Laver model
$\mathfrak t=\aleph_1<\dd$, towers of length $\w_1$ exist, and the hypothesis
has to be verified by other means. That is the purpose of
Theorem~\ref{thm:dich}.
\end{remark}

\section{Laver forcing}\label{sec:laver}

We use the notation of \cite{Lav}. A \emph{Laver tree} is a tree
$p\subseteq\w^{<\w}$ with a node $\st(p)$ such that every $s\in p$ is
comparable with $\st(p)$ and every $s\in p$ with $s\supseteq\st(p)$ has
infinitely many immediate successors in $p$. Laver forcing consists of all
Laver trees ordered by inclusion. For $t\in p$ let
$p_t=\{s\in p:s\subseteq t\text{ or }t\subseteq s\}$. We write $q\le^0 p$ if
$q\le p$ and $\st(q)=\st(p)$. For $s\in p$, $s\supseteq\st(p)$, let
$\suc_p(s)=\{i:s\conc i\in p\}$.

Let $\PP_\alpha$ denote the countable support iteration of Laver forcing of
length $\alpha$, and $\ell_\beta$ the generic real added at coordinate
$\beta$. For $p\in\PP_\alpha$ and $t\in p(0)$ with $t\supseteq\st(p(0))$ let
\[
p|t=p(0)_t\conc p\res[1,\alpha),
\]
the condition obtained from $p$ by restricting its first coordinate to the
part of the tree through $t$ and leaving everything else alone. A generic
filter $G$ contains $p|t$ if and only if $p\in G$ and $t\subseteq\ell_0$.

The tool we need is a lemma of Laver. It says that although a name for a
real may depend on the whole iteration, at each node of the first tree its
value is determined, up to any prescribed precision and up to finitely many
possibilities, by all but finitely many choices of the next value of
$\ell_0$. Laver states the lemma for $\PP_{\w_2}$ over a model of
\textsf{CH} and for names of real numbers; the proof works for any length,
over any ground model, and for names of elements of a compact metrizable
space. The formulation for $2^\w$ is \cite[Lemma~3.3]{MT}; see also
\cite{RZ}.

\begin{lemma}[Laver {\cite[Lemma~14]{Lav}}]\label{lem:laver14}
Let $\dot a$ be a $\PP_\alpha$-name for an element of $2^\w$ and
$p\in\PP_\alpha$. There are $p'\le p$ with $p'(0)\le^0 p(0)$ and finite sets
$U'_s\subseteq 2^\w$ for all $s\in p'(0)$ with $s\supseteq\st(p'(0))$, such
that for every such $s$ and every $n<\w$, for all but finitely many
$i\in\suc_{p'(0)}(s)$,
\[
p'|s\conc i\ \forces\ \exists y\in U'_s\ (\dot a\res n=y\res n).
\]
\end{lemma}

The lemma requires a compact space, and $\ww$ is not compact. The remedy is
to work in the compactification $\K=(\w+1)^\w$, where $\w+1$ carries the
order topology; $\K$ is compact, metrizable and zero-dimensional, and
contains $\ww$. We write $\infty$ for the top point of $\w+1$. The price is
that candidates may now have infinite entries, and this turns out to be
exactly the information we want. For $x\in\K$ and $n<\w$ let
\[
N_n(x)=\bigl\{y\in\K:\ \forall k<n\ \bigl[(x(k)<n\Rightarrow y(k)=x(k))
\wedge(x(k)\ge n\Rightarrow y(k)\ge n)\bigr]\bigr\}.
\]
The sets $N_n(x)$, $n<\w$, form a decreasing neighbourhood base of $x$ in
$\K$. For $u\in\ww$ we write $u\approx_n x$ if $u\in N_n(x)$, and say that
$x$ approximates $u$ to precision $n$. Explicitly: on the first $n$
coordinates, $u$ agrees with $x$ wherever $x$ is small (below $n$), and $u$
is large (at least $n$) wherever $x$ is large or infinite.

\begin{lemma}\label{lem:compact}
Let $W$ be the ground model, $\dot u$ a $\PP_\alpha$-name for an element of
$\ww$, and $p\in\PP_\alpha$. There are $p'\le p$ with $p'(0)\le^0p(0)$ and
finite sets $U_s\subseteq\K$ in $W$, for $s\in p'(0)$ with
$s\supseteq\st(p'(0))$, such that for every such $s$ and every $n<\w$, for
all but finitely many $i\in\suc_{p'(0)}(s)$,
\[
p'|s\conc i\ \forces\ \exists x\in U_s\ (\dot u\approx_n x).
\]
\end{lemma}

\begin{proof}
We transfer Lemma~\ref{lem:laver14} along an embedding. Fix in $W$ a
homeomorphism $e$ of $\K$ onto a closed set $C\subseteq2^\w$; its definition
is absolute, and in the extension $e(\dot u)\in C$. Apply
Lemma~\ref{lem:laver14} to a name $\dot a$ for $e(\dot u)$ to obtain $p'$ and
finite sets $U'_s$, and let $U_s=e^{-1}[U'_s\cap C]$. Candidates outside $C$
are simply dropped; we check that nothing is lost.

Fix $s$ and $n$. For each $y\in U'_s\setminus C$ choose $m_y$ such that no
element of $C$ extends $y\res m_y$; this is possible because $C$ is closed.
For each $x\in U_s$, by continuity of $e^{-1}$ at $e(x)$, choose $m_x$ such
that every $z\in C$ with $z\res m_x=e(x)\res m_x$ satisfies
$e^{-1}(z)\in N_n(x)$. Let $m$ be the maximum of these finitely many numbers.
For all but finitely many $i\in\suc_{p'(0)}(s)$, the condition $p'|s\conc i$
forces that $\dot a\res m=y\res m$ for some $y\in U'_s$. Since $\dot a\in C$
is forced, such a $y$ cannot lie outside $C$. So $y=e(x)$ for some
$x\in U_s$, and then $\dot u=e^{-1}(\dot a)\in N_n(x)$.
\end{proof}

The second fact we need is the familiar strong form of the statement that a
Laver real is dominating: it eventually exceeds any ground model function of
its own past.

\begin{fact}\label{fact:dom}
Let $p'\in\PP_\alpha$ and let $H\in W$ be a function from
$\{s\in p'(0):s\supseteq\st(p'(0))\}$ to $\w$. Then $p'$ forces that
$\ell_0(m)\ge H(\ell_0\res m)$ for all but finitely many $m$.
\end{fact}

\begin{proof}
Let $r\le p'$. Let $r'(0)$ consist of all $t\in r(0)$ such that
$t(m)\ge H(t\res m)$ whenever $|\st(r(0))|\le m<|t|$, and let
$r'(\beta)=r(\beta)$ for $\beta\ge1$. Each node above the stem loses only
finitely many successors, so $r'(0)$ is a Laver tree with the same stem as
$r(0)$. Thus $r'\le r$, and $r'$ forces $\ell_0(m)\ge H(\ell_0\res m)$ for
all $m\ge|\st(r(0))|$.
\end{proof}

\section{The dichotomy}\label{sec:dich}

Here is the idea. Fix a real $u$ of the extension and a condition $p'$ in
the generic filter as in Lemma~\ref{lem:compact}. As the first Laver real
$\ell_0$ is revealed one value at a time, each new value $\ell_0(m)$ tells
us more about $u$: it pins $u$ down, to a precision $n_m$ which tends to
infinity, to one of the finitely many candidates attached to the node
$\ell_0\res m$. A candidate is a point of $(\w+1)^\w$, and an entry $\infty$
at a position $k$ means that $u(k)$ has not been decided yet and is known
only to be large, at least $n_m$.

Either candidates with infinite entries keep being used for ever, or from
some stage on they do not. In the first case each use hands us a position
$k$ with $u(k)\ge n_m$. Since $\ell_0$ outgrows every ground model function
of its past, $n_m$ can be made to exceed $h(k)$ for any ground model $h$,
and the positions collected in this way form the set $A$. In the second
case every value $u(k)$ is eventually read off from a candidate with finite
entries, and there are only finitely many candidates at each node; taking
the maximum over the ones that matter produces a ground model bound.

The point which makes this work for iterations, and not only for a single
Laver real, is that we never need to know \emph{which} candidate is the
right one. That choice is made by the later coordinates, about which we
assume nothing.

\begin{proof}[Proof of Theorem~\ref{thm:dich}]
The two alternatives exclude each other, since (2) applied to $h=h^*+1$
contradicts (1). We show that one of them holds.

Let $\dot u$ be a name for $u$. By Lemma~\ref{lem:compact} and genericity
there is $p'\in G$ with finite sets $U_s\subseteq\K$, $s\in p'(0)$,
$s\supseteq\st(p'(0))$, as in that lemma. All objects defined below from
$p'$, $\langle U_s\rangle$ and the forcing relation belong to $W$. By a
\emph{node} we mean an $s\in p'(0)$ extending the stem.

For a node $s$ and $i\in\suc_{p'(0)}(s)$, let $n_s(i)$ be the precision that
the successor $i$ guarantees:
\[
n_s(i)=\max\{n\le i:\ p'|s\conc i\forces\exists x\in U_s\ (\dot
u\approx_n x)\}.
\]
Since the relations $\approx_n$ get stronger as $n$ grows,
Lemma~\ref{lem:compact} gives $n_s(i)\to\infty$ as $i\to\infty$ in
$\suc_{p'(0)}(s)$.

Work in $W[G]$. Let $m_0=|\st(p'(0))|$, and for $m\ge m_0$ let
$s_m=\ell_0\res m$ and $n_m=n_{s_m}(\ell_0(m))$. Applying
Fact~\ref{fact:dom} to the functions $s\mapsto\min\{i_0:\forall i\ge i_0\
n_s(i)\ge N\}$, $N<\w$, we get $n_m\to\infty$. Since $p'|s_{m+1}\in G$, for
every $m\ge m_0$ there is $x\in U_{s_m}$ with $u\approx_{n_m}x$; call such an
$x$ a \emph{witness at $m$}. Let
\[
\Gamma=\{m\ge m_0:\ \text{some witness at $m$ has an entry equal to }\infty\}.
\]

\medskip\noindent\textbf{Case 1: $\Gamma$ is infinite.}
We collect the first infinite entries of the witnesses. For
$x\in\K\setminus\ww$ let $k_x=\min\{k:x(k)=\infty\}$, and let
\[
A=\{k_x:\ m\in\Gamma,\ x\text{ a witness at }m,\ x\notin\ww,\ k_x<n_m\}.
\]
If $k=k_x$ arises from $m$ in this way, then $k<n_m$ and $x(k)\ge n_m$, so
$u\approx_{n_m}x$ gives
\begin{equation}\label{eq:big}
u(k)\ge n_m.
\end{equation}
We must show that $u$ beats every ground model function on $A$. Let
$h\in\ww\cap W$. The precision $n_m$ is controlled by $\ell_0(m)$, so it is
enough to ask $\ell_0(m)$ to be large. In $W$ define, for a node $s$,
$H_h(s)$ to be the least $i_0$ such that for all $i\ge i_0$ in
$\suc_{p'(0)}(s)$ and all $x\in U_s\setminus\ww$,
\[
n_s(i)>\max\bigl(k_x,h(k_x)\bigr).
\]
This is well defined because $U_s$ is finite and $n_s(i)\to\infty$. By
Fact~\ref{fact:dom} there is $m_h$ such that $\ell_0(m)\ge H_h(s_m)$ for all
$m\ge m_h$. Hence for $m\in\Gamma$, $m\ge m_h$, and every witness
$x\notin\ww$ at $m$ we have $k_x<n_m$, so $k_x\in A$, and by \eqref{eq:big}
\[
u(k_x)\ge n_m>h(k_x).
\]
The finitely many $m<m_h$ contribute only finitely many elements to $A$,
because each $U_{s_m}$ is finite. Therefore $h(k)\le u(k)$ for all but
finitely many $k\in A$.

It remains to see that $A$ is infinite. By the above with $h=0$, every
sufficiently large $m\in\Gamma$ contributes at least one element to $A$. By
\eqref{eq:big} a given $k$ can arise only from those $m$ with
$n_m\le u(k)$, and there are finitely many such $m$ because $n_m\to\infty$.
Since $\Gamma$ is infinite, so is $A$. Thus (2) holds.

\medskip\noindent\textbf{Case 2: $\Gamma$ is finite.}
Fix $m_1\ge m_0$ such that for $m\ge m_1$ every witness at $m$ lies in $\ww$,
and for each $m\ge m_1$ fix a witness $x^m\in U_{s_m}\cap\ww$. We look for
$h^*\in\ww\cap W$ with $u\les h^*$.

Say that a position $k$ is \emph{resolved at $m$} if $k<n_m$ and
$x^m(k)<n_m$. When this happens, $u\approx_{n_m}x^m$ gives $u(k)=x^m(k)$: the
value of $u(k)$ has been read off. Every $k$ is resolved at all sufficiently
large $m$, for once $n_m>\max(k,u(k))$ the alternative $x^m(k)\ge n_m$ would
give $u(k)\ge n_m$. The plan is to bound $u(k)$ by looking at the stage at
which $k$ is first resolved. At the stage just before, $k$ was still
unresolved, and for a fixed node only finitely many successors leave a given
$k$ unresolved. That finiteness is what gives a bound in the ground model.

To carry this out, work in $W$. For a node $s'$ and
$i'\in\suc_{p'(0)}(s')$ let $Q_{s',i'}$ be the set of positions that the
successor $i'$ can leave unresolved:
\[
Q_{s',i'}=\bigl\{k<\w:\ k\ge n_{s'}(i')\ \text{ or }\ x'(k)\ge n_{s'}(i')
\text{ for some }x'\in U_{s'}\cap\ww\bigr\}.
\]
Since $U_{s'}$ is finite and $n_{s'}(i')\to\infty$, each $k$ belongs to
$Q_{s',i'}$ for only finitely many $i'$. Hence
\[
H_{s'}(k)=\max\bigl\{x(k):\ i'\in\suc_{p'(0)}(s'),\ k\in Q_{s',i'},\ x\in
U_{s'\conc i'}\cap\ww\bigr\}
\]
(with $\max\emptyset=0$) defines a function $H_{s'}\in\ww\cap W$: it bounds
the value that $k$ can receive at the next node if $k$ was unresolved at
$s'$. There are countably many nodes, so in $W$ we can choose $h^*\in\ww$
and numbers $N(s')$ such that $H_{s'}(k)\le h^*(k)$ for all $k\ge N(s')$.
The positions below $N(s')$ are not covered by this, and we deal with them by
making sure they are resolved early. Let $H(s')$ be the least $i_0$ such that
for all $i'\ge i_0$ in $\suc_{p'(0)}(s')$,
\[
n_{s'}(i')>N(s')\quad\text{and}\quad n_{s'}(i')>x'(k)\ \text{ for all
}k<N(s'),\ x'\in U_{s'}\cap\ww.
\]
By Fact~\ref{fact:dom} fix $m_2\ge m_1$ such that $\ell_0(m)\ge H(s_m)$ for
all $m\ge m_2$.

Back in $W[G]$, let $m(k)$ be the least $m\ge m_2$ at which $k$ is resolved.
If $m(k)=m_2$ then $k<n_{m_2}$, so this happens for only finitely many $k$.

Let $k$ be such that $m=m(k)>m_2$, and put $s'=s_{m-1}$ and
$i'=\ell_0(m-1)$, so that $s_m=s'\conc i'$ and $n_{m-1}=n_{s'}(i')$. By
minimality, $k$ is not resolved at $m-1$, that is, $k\ge n_{s'}(i')$ or
$x^{m-1}(k)\ge n_{s'}(i')$. As $x^{m-1}\in U_{s'}\cap\ww$, this means
$k\in Q_{s',i'}$. As $x^m\in U_{s'\conc i'}\cap\ww$, we get
\[
u(k)=x^m(k)\le H_{s'}(k).
\]
Moreover $k\ge N(s')$. Otherwise, since $m-1\ge m_2$ gives $i'\ge H(s')$, we
would have $k<N(s')<n_{s'}(i')$ and $x^{m-1}(k)<n_{s'}(i')$, so $k$ would
already be resolved at $m-1$. Hence $u(k)\le H_{s'}(k)\le h^*(k)$.

Thus $u(k)\le h^*(k)$ for all but finitely many $k$, and (1) holds.
\end{proof}

\begin{remark}
It is worth isolating why the later coordinates of the iteration cause no
trouble. In Case~1 we use only that \emph{some} witness has an infinite
entry, and in Case~2 the bound $H_{s'}$ is a maximum over \emph{all}
candidates. A condition below $p'$ can restrict coordinate $0$ only above
its stem, which affects finitely many stages along the generic branch, and
whatever it does at coordinates $\beta\ge1$ cannot affect statements forced
by the conditions $p'|t$. This is the feature that an induction on the
length of the iteration lacks at limit stages of countable cofinality.
\end{remark}

In the language of towers, the theorem says the following.

\begin{corollary}\label{cor:tower}
Let $W$, $\alpha$ and $G$ be as in Theorem~\ref{thm:dich} and let
$\mathcal H\subseteq\ww\cap W$ be $\les$-cofinal in $\ww\cap W$. For every
$u\in\ww\cap W[G]$ which is not $\les$-below any member of $\mathcal H$, the
family $\{\{k:u(k)\ge h(k)\}:h\in\mathcal H\}$ has an infinite
pseudo-intersection in $W[G]$.
\end{corollary}

\section{Proof of the main theorem}\label{sec:main}

Let $V$ be a model of \textsf{CH}, let $\PP=\PP_{\w_2}$ and let $G$ be
$\PP$-generic over $V$. For $\alpha\le\w_2$ let $V_\alpha=V[G\cap\PP_\alpha]$.
We use the following standard facts; see \cite{Lav}, \cite{BJ} and
\cite{Gol}.

\begin{enumerate}
\item[(F1)] $\PP$ is proper and has the $\aleph_2$-chain condition; every
real of $V_{\w_2}$ belongs to $V_\beta$ for some $\beta<\w_2$, and
$\cc=\aleph_2$ in $V_{\w_2}$.
\item[(F2)] If $\alpha\le\w_2$ has uncountable cofinality, then
$\ww\cap V_\alpha=\bigcup_{\gamma<\alpha}\ww\cap V_\gamma$.
\item[(F3)] For $\alpha<\beta\le\w_2$, the model $V_\beta$ is a generic
extension of $V_\alpha$ by the countable support iteration of Laver forcing
of length $\beta-\alpha$ defined in $V_\alpha$, whose generic reals are
$\ell_{\alpha+\xi}$, $\xi<\beta-\alpha$.
\item[(F4)] For every $\gamma<\w_2$, $f\les\ell_\gamma$ for all
$f\in\ww\cap V_\gamma$.
\end{enumerate}

With these in hand the main theorem is a matter of putting the pieces
together. The Laver reals form a scale. The reals bounded by the first
$\alpha$ of them are, for $\alpha$ of cofinality $\w_1$, exactly the reals
bounded by the intermediate model $V_\alpha$. And the rest of the iteration
is again a Laver iteration over $V_\alpha$, so Theorem~\ref{thm:dich}
applies with $V_\alpha$ as the ground model.

\begin{proof}[Proof of Theorem~\ref{thm:main}]
Work in $V_{\w_2}$. By (F4), $\ell_\gamma<^*\ell_\delta$ for
$\gamma<\delta<\w_2$, since $\ell_\gamma+1\in V_\delta$. By (F1) and (F4),
$\langle\ell_\gamma:\gamma<\w_2\rangle$ is dominating, and every subset of
$\ww$ of size $\aleph_1$ is contained in some $V_\gamma$ and hence bounded.
So $\langle\ell_\gamma:\gamma<\w_2\rangle$ is a scale and
$\bb=\dd=\aleph_2$.

We verify the hypothesis of Theorem~\ref{thm:scale} for this scale. Let
$\alpha<\w_2$ with $\cf(\alpha)=\w_1$ and let $u\in\ww$. By (F2) and (F4),
$\{\ell_\gamma:\gamma<\alpha\}$ is a $\les$-cofinal subset of
$\ww\cap V_\alpha$. By (F1), $u\in V_\beta$ for some $\beta<\w_2$, and we may
assume $\beta>\alpha$. By (F3) and Theorem~\ref{thm:dich}, applied with
$W=V_\alpha$, one of two things happens. Either $u\les h^*$ for some
$h^*\in\ww\cap V_\alpha$, in which case $u\les\ell_\gamma$ for some
$\gamma<\alpha$. Or there is an infinite $A$ with $h\les u\res A$ for all
$h\in\ww\cap V_\alpha$, and in particular $\ell_\gamma\les u\res A$ for all
$\gamma<\alpha$.

By Theorem~\ref{thm:scale} there is an $\w_2$-Michael sequence and a Michael
space.
\end{proof}

\begin{remark}
For the record, here is why none of the previously known sufficient
conditions holds in the Laver model. There $\bb=\aleph_2$. Countable support
iterations of Laver forcing have the Laver property and therefore add no
Cohen reals, so the ground model meagre sets cover the reals and
$\covM=\aleph_1<\dd$; in particular Martin's Axiom fails. By Miller's theorem
\cite{Mil} there are no Q-points, hence no selective ultrafilters.
\end{remark}

\section{Remarks and questions}\label{sec:questions}

Theorem~\ref{thm:main} does not settle Michael's problem, but it narrows the
search for a counterexample. By Proposition~\ref{prop:length} and Moore's
results \cite{Moo}, when $\cc<\aleph_\w$ a Michael space exists if and only
if there is a $\kappa$-Michael sequence for some regular $\kappa$ with
$\bb\le\kappa\le\dd$. If $\cc=\aleph_2$, a model with no Michael space must
therefore satisfy $\covM=\aleph_1<\bb=\dd=\aleph_2$ and have no selective
ultrafilters. Among the standard models of $\cc=\aleph_2$, the Laver and
Mathias models are the ones satisfying these requirements that we are aware
of. Theorem~\ref{thm:main} disposes of the first.

\begin{question}
Is there a Michael space in the Mathias model?
\end{question}

There is some reason for optimism. For a selective ultrafilter
$\mathcal U$, Mathias forcing relative to $\mathcal U$ is forcing equivalent
to Laver forcing relative to $\mathcal U$, which suggests that an analogue
of Theorem~\ref{thm:dich} may hold for the Mathias iteration.

The second question is whether the forcing can be dispensed with.

\begin{question}
Does $\bb=\dd$ imply that there is a Michael space? More specifically, if
$\bb=\dd$, is there a scale satisfying the hypothesis of
Theorem~\ref{thm:scale}?
\end{question}

Not every scale does. If $\covM=\aleph_1$, one can construct a
$\les$-increasing sequence $\langle g_i:i<\w_1\rangle$ and a perfect compact
set $K\subseteq\bigcup_i\{f:f\les g_i\}$ such that each $\{f\in K:f\les
g_i\}$ is meagre in $K$; when $\bb=\dd>\aleph_1$, any scale extending such a
sequence fails the conclusion of Theorem~\ref{thm:scale} at
$\alpha=\w_1$. So a positive answer would require choosing the scale with
care, as the Laver reals are chosen for us in the Laver model.

\begin{question}
Is the dichotomy of Theorem~\ref{thm:dich} preserved by countable support
iterations of proper forcings in some generality? Precisely: for which
classes of forcings does every new real either lie below a ground model real
or dominate the ground model reals on an infinite set?
\end{question}

A positive answer for a class containing forcings that do not add
dominating reals cannot be expected in this form, but a suitable variant
might produce Michael sequences from other scales, or from unbounded
families when $\bb<\dd$.

\subsection*{Acknowledgments}
The statements and proofs in this paper were developed in a working session
with Claude, an AI system made by Anthropic, which proposed the reduction to
the Laver model, found the proofs of Theorems~\ref{thm:dich}
and~\ref{thm:scale}, and drafted the text.

\begin{thebibliography}{99}

\bibitem{Als} K.~Alster, \emph{The product of a Lindel\"of space with the
space of irrationals under Martin's axiom}, Proc. Amer. Math. Soc.
\textbf{110} (1990), 543--547.

\bibitem{BJ} T.~Bartoszy\'nski and H.~Judah, \emph{Set theory: on the
structure of the real line}, A K Peters, Wellesley, MA, 1995.

\bibitem{Gol} M.~Goldstern, \emph{Tools for your forcing construction}, in:
Set theory of the reals (Ramat Gan, 1991), Israel Math. Conf. Proc.
\textbf{6}, Bar-Ilan Univ., 1993, 305--360.

\bibitem{Lav} R.~Laver, \emph{On the consistency of Borel's conjecture},
Acta Math. \textbf{137} (1976), 151--169.

\bibitem{Law} L.~B.~Lawrence, \emph{The influence of a small cardinal on the
product of a Lindel\"of space and the irrationals}, Proc. Amer. Math. Soc.
\textbf{110} (1990), 535--542.

\bibitem{MC} A.~Mart\'inez-Celis, \emph{Michael spaces and ultrafilters},
preprint, arXiv:2310.02749.

\bibitem{Mic} E.~Michael, \emph{The product of a normal space and a metric
space need not be normal}, Bull. Amer. Math. Soc. \textbf{69} (1963),
375--376.

\bibitem{Mil} A.~W.~Miller, \emph{There are no Q-points in Laver's model for
the Borel conjecture}, Proc. Amer. Math. Soc. \textbf{78} (1980), 103--106.

\bibitem{MT} A.~W.~Miller and B.~Tsaban, \emph{Point-cofinite covers in the
Laver model}, Proc. Amer. Math. Soc. \textbf{138} (2010), 3313--3321.

\bibitem{Moo} J.~T.~Moore, \emph{Some of the combinatorics related to
Michael's problem}, Proc. Amer. Math. Soc. \textbf{127} (1999), 2459--2467.

\bibitem{RZ} D.~Repov\v{s} and L.~Zdomskyy, \emph{Products of Hurewicz
spaces in the Laver model}, Bull. Symb. Log. \textbf{23} (2017), 324--333.

\end{thebibliography}

\end{document}