==== TABLE OF CONTENTS ====
The-Partition-Principle-does-not-imply-Choice//figures/moved-generic-transport.tex
The-Partition-Principle-does-not-imply-Choice//figures/probe-divisibility.tex
The-Partition-Principle-does-not-imply-Choice//figures/support-descent.tex
The-Partition-Principle-does-not-imply-Choice//main.tex
The-Partition-Principle-does-not-imply-Choice//sections/conclusion.tex
The-Partition-Principle-does-not-imply-Choice//sections/forcing.tex
The-Partition-Principle-does-not-imply-Choice//sections/introduction.tex
The-Partition-Principle-does-not-imply-Choice//sections/metatheory.tex
The-Partition-Principle-does-not-imply-Choice//sections/monoid.tex
The-Partition-Principle-does-not-imply-Choice//sections/quotients.tex
The-Partition-Principle-does-not-imply-Choice//references.bib
===========================

==== BEGIN The-Partition-Principle-does-not-imply-Choice//figures/moved-generic-transport.tex ====
\begin{figure}[htbp]
\centering
\begin{tikzpicture}[font=\small,>=Stealth]
  \node (a) at (0,1.65) {$L_C$};
  \node (b) at (6,1.65) {$B_C(\pi^{-1}F)$};
  \node (c) at (0,0) {$L_C$};
  \node (d) at (6,0) {$B_C(F)$};
  \draw[->] (a) -- node[above] {$f_C^0(\pi^{-1}F)$} (b);
  \draw[->] (a) -- node[left] {$\pi\restriction L_C$} (c);
  \draw[->] (b) -- node[right] {$T_\pi^{\pi^{-1}F}$} (d);
  \draw[->] (c) -- node[below] {$f_C^{\pi K_C}(F)$} (d);
\end{tikzpicture}
\caption{Transporting a preliminary bijection, for $\pi\in G_C$.
The square commutes: to assign the bottom label $j$, first compute
at $\pi^{-1}j$ in the generic $\pi^{-1}F$, then transport the result
to $F$. The top and bottom computations use $\pi^{-1}F$ and $F$,
respectively.}
\label{fig:moved-generic-transport}
\end{figure}
==== END The-Partition-Principle-does-not-imply-Choice//figures/moved-generic-transport.tex ====

==== BEGIN The-Partition-Principle-does-not-imply-Choice//figures/probe-divisibility.tex ====
\begin{figure}[htbp]
\centering
\begin{tikzpicture}[font=\small,>=Stealth]
  \node (pathpoint) at (0,0) {$n_i$};
  \node (oldpoint) at (3,1) {$a$};
  \node (probe) at (3,-1) {$m=p_0$};
  \node (commonmultiple) at (6,0) {$ae$};
  \draw[->] (pathpoint) -- node[above left] {$c_i$} (oldpoint);
  \draw[->] (pathpoint) -- node[below left] {$p_i$} (probe);
  \draw[->] (oldpoint) -- node[above right] {$e$} (commonmultiple);
  \draw[->] (probe) -- node[below right] {$b$} (commonmultiple);
\end{tikzpicture}
\caption{The relations defining the probe give two factorizations of
the prescribed common multiple $ae$.  Each arrow means right
multiplication by its label, not a covering relation.  This is not a
Hasse diagram: path points may coincide with $a$, and $a$ may divide
$m$.  The exact-profile assertion is that a divisor of $a$ omitted
from the path's downward closure has join $ae$ with $m$.}
\label{fig:probe-divisibility}
\end{figure}
==== END The-Partition-Principle-does-not-imply-Choice//figures/probe-divisibility.tex ====

==== BEGIN The-Partition-Principle-does-not-imply-Choice//figures/support-descent.tex ====
\begin{figure}[htbp]
\centering
\begin{tikzpicture}[font=\small,
    diagramrange/.style={draw,rounded corners=2pt,fill=white,
                  inner xsep=9pt,inner ysep=5pt},
    overlap/.style={fill=white,inner sep=3pt}]
  \node[diagramrange] (t) at (0,1.8) {$D_t$};
  \node[diagramrange] (v) at (-3,-.8) {$D_{v'}$};
  \node[diagramrange] (w) at (3,-.8) {$D_{v''}$};
  \draw (t) -- node[overlap,pos=.52] {$D_{\bar s}$} (v);
  \draw (t) -- node[overlap,pos=.52] {$D_{\bar s'}$} (w);
  \draw (v) -- node[overlap] {$D_u$} (w);
  \node[align=center,font=\footnotesize] at (0,-.15)
    {$D_p$\\triple intersection};
\end{tikzpicture}
\caption{The independent-copy case of support descent. Each edge is
labelled by the exact intersection of its endpoint ranges. The two
placed equality witnesses $v',v''$ use the same fresh copy $u$ of $s_1$;
$t$ carries the proposed inequality between the copies on
$\bar s$ and $\bar s'$, whose ranges meet exactly in $D_p$.
These exact intersections allow the three diagrams to be amalgamated
over their common root $p$.}
\label{fig:support-descent}
\end{figure}
==== END The-Partition-Principle-does-not-imply-Choice//figures/support-descent.tex ====

==== BEGIN The-Partition-Principle-does-not-imply-Choice//main.tex ====
\documentclass[11pt]{article}
\pdfinfoomitdate=1
\pdftrailerid{}
\pdfsuppressptexinfo=15
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage[expansion=false]{microtype}
\usepackage[margin=1.04in]{geometry}
\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage{enumitem,booktabs,array,needspace}
\usepackage{tikz}
\usetikzlibrary{arrows.meta,positioning,calc,fit}
\usepackage[hyphens]{url}
\usepackage[hidelinks,hypertexnames=false]{hyperref}
\usepackage[nameinlink,capitalize,noabbrev]{cleveref}
\hypersetup{pdftitle={The Partition Principle does not imply Choice},pdfauthor={OpenAI}}
\setlength{\emergencystretch}{2em}
\allowdisplaybreaks[1]
\numberwithin{equation}{section}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}
\newcommand{\ZF}{\mathsf{ZF}}
\newcommand{\ZFC}{\mathsf{ZFC}}
\newcommand{\AC}{\mathsf{AC}}
\newcommand{\PP}{\mathsf{PP}}
\newcommand{\ACwo}{\mathsf{AC}_{\mathrm{WO}}}
\newcommand{\Con}{\operatorname{Con}}
\newcommand{\Ord}{\mathrm{Ord}}
\newcommand{\HS}{\mathrm{HS}}
\newcommand{\forces}{\Vdash}
\DeclareMathOperator{\Fix}{Fix}
\DeclareMathOperator{\Sym}{Sym}
\DeclareMathOperator{\dom}{dom}
\DeclareMathOperator{\ran}{ran}
\DeclareMathOperator{\supp}{supp}
\DeclareMathOperator{\id}{id}
\title{The Partition Principle does not imply Choice}
\author{OpenAI}
\date{September 24, 2026}
\begin{document}
\maketitle
\begin{abstract}
We prove that the Partition Principle does not imply the Axiom of Choice:
if ZF is consistent, then so is ZF with the Partition Principle, Choice for
ordinal-indexed families, and the negation of the Axiom of Choice.
Separately, over every countable transitive model of ZFC, we construct a
transitive symmetric model of this theory with the same ordinals and no new
countable sequences of ground elements.
\end{abstract}
\tableofcontents
\clearpage
\input{sections/introduction}
\input{sections/monoid}
\input{sections/forcing}
\input{sections/quotients}
\input{sections/conclusion}
\input{sections/metatheory}
{\small\raggedright
\bibliographystyle{plain}
\bibliography{references}}
\end{document}
==== END The-Partition-Principle-does-not-imply-Choice//main.tex ====

==== BEGIN The-Partition-Principle-does-not-imply-Choice//sections/conclusion.tex ====
\section{From quotient classification to the Partition Principle}
\label{sec:conclusion}

We now pass from the classification of quotients of the label set to
arbitrary surjections.  The reduction uses only three statements inside
the symmetric model: every nonempty set is an image of the label set
times an ordinal, choice holds for ordinal-indexed families, and every
nonwellorderable image of the label set is bijective to it.  We first
prove this reduction in $\ZF$, independently of the construction.

The ordinal slicing and assembly of injections follow the local-to-global
method in Ryan-Smith's analysis of $\PP$
\cite[Propositions~3.17 and~3.20]{RyanSmith2025}. We use the stronger
classification of nonwellorderable images stated below and give the
complete reduction under these hypotheses.

\begin{lemma}[The all-set reduction]\label{lemma:pp-reduction}
Work in $\ZF$.  Suppose that a nonempty set $A$ has the following
properties.
\begin{enumerate}
\item For every nonempty set $X$, there are an ordinal $\eta$ and
a surjection $A\times\eta\longrightarrow X$.
\item Every ordinal-indexed family of nonempty sets has a choice
function.
\item Every nonwellorderable surjective image of $A$ is in bijection
with $A$.
\end{enumerate}
Then $\PP$ holds: for all sets $X,Y$, every surjection
$f:X\longrightarrow Y$ has an injection $j:Y\longrightarrow X$.
\end{lemma}

\begin{proof}
We will use two elementary observations about images of $A$.
If $h:A\longrightarrow B$ is onto and $\varnothing\ne S\subseteq B$,
then $S$ is also an image of $A$.  Indeed, fix one $s_0\in S$ and
define
\[
 h_S(a)=
 \begin{cases}
 h(a),&h(a)\in S,\\
 s_0,&h(a)\notin S.
 \end{cases}
\]
This proves an existence assertion for one given nonempty subset;
it does not choose a default element simultaneously for a family.
Also, the image of a wellorderable set under any function is
wellorderable: order its image by the least preimages in a fixed
wellordering of its domain.  Both observations are theorems of $\ZF$.

Fix a surjection $f:X\longrightarrow Y$.  If $Y=\varnothing$, the
empty function is the desired injection.  Otherwise $X$ is nonempty.
Choose a surjection $s:A\times\eta\longrightarrow X$ from the first
assumption.  Define, for $i<\eta$,
\begin{align}
 B_i&=s[A\times\{i\}],\notag\\
 Y_i&=f[B_i]\setminus\bigcup_{k
 \sup\{\epsilon_d:d\sqsubseteq y,\ d\not\sqsubseteq x\}
 \qquad(x\sqsubset y).
 \end{gathered}
\end{equation}
An empty supremum of costs is understood to be zero.

\begin{lemma}\label{lem:mono-countable-ideal}
If a monoid has conditional joins and satisfies
Equation~\eqref{eq:mono-margin}, every ideal in $\downarrow a$ has a
nondecreasing cofinal sequence of length $\omega$, with repetitions
allowed.  The same conclusion holds in any $\ZFC$ extension in which
the monoid, order, heights and costs retain their meanings, for ideals
belonging to that extension.
\end{lemma}
\begin{proof}
For an ideal $U$, choose elements whose heights approach
$\sup\rho[U]$, and replace their successive initial segments by their
finite joins.  This gives a nondecreasing sequence $(n_i)$ in $U$
with heights approaching the same supremum.  If $d\in U$ divides
none of the $n_i$, then
\[
 \rho(n_i\vee d)-\rho(n_i)>\epsilon_d
\]
for every $i$, contradicting convergence to the supremum.  Prepending
$1$ makes $n_0=1$.  The proof applies in the stated extension as well;
its choices are made in that $\ZFC$ universe.
\end{proof}

Here is the finite overlap condition used below.  Take finitely many
copies $\{i\}\times M$.  For each pair of distinct copies prescribe
either no overlap or elements $a_{ij},a_{ji}\in M$ and the
identifications
\[
 (i,a_{ij}x)\sim(j,a_{ji}x)\qquad(x\in M).
\]
We call the prescription \emph{valid} if these pair identifications,
together with equality, already form an equivalence relation and do
not identify distinct elements of any one copy.  In particular,
transitive closure is not allowed to create extra overlaps.

\begin{theorem}\label{thm:monoid}
There is a monoid $T$ of cardinality $\mu$, with a distinguished
$e\ne1$, having the following properties.
\begin{enumerate}
\item $T$ is left cancellative and conical, has conditional joins,
and has heights and costs satisfying Equation~\eqref{eq:mono-margin}.
\item Every valid finite overlap prescription on copies of $T$ is
realized by left translations $x\mapsto l_i x$ in $T$, with exactly
the prescribed identifications.
\item For $a,b\in T$ with $b\ne1$, and every ideal
$U\subseteq\downarrow a$, there are $\mu$ distinct elements $m$ with
\begin{equation}\label{eq:mono-probes}
 \begin{gathered}
 mb=ae,\qquad m\not\sqsubseteq a,\qquad
 \downarrow m\cap\downarrow a=U,\\
 n\vee m=ae\quad(n\sqsubseteq a,\ n\notin U).
 \end{gathered}
\end{equation}
The cones of distinct elements in this family intersect exactly in
$aeT$.  Moreover $|T\setminus eT|=\mu$.
\item For every countable subset of $T$ there is a countable
submonoid $T_0$ containing it and a continuous conservative tower
starting at $T_0$ and ending at $T$.  Each successor step has one of
the following properties:
\begin{enumerate}
\item no new element divides an old element;
\item every new element $w$ with an old right multiple has a least
old right multiple $g(w)$, and
\begin{equation}\label{eq:mono-gate-old}
 d\text{ old},\quad g(w)\sqsubseteq wd
       \quad\Longrightarrow\quad wd\text{ old}.
\end{equation}
\end{enumerate}
Here ``old'' means belonging to the base of that particular successor
step, and the comparisons may be tested in the final monoid.
\end{enumerate}
\end{theorem}

For diagrams indexed by $T$, the finite-merger clause supplies a common
larger diagram for finitely many copies with compatible overlaps.  The
probe clause supplies $\mu$ copies with one prescribed intersection
pattern: for $n\sqsubseteq a$, the cone $nT$ contains $mT$ exactly when
$n\in U$, and otherwise meets it in $aeT$.  The margin makes every such
ideal countably cofinal.  The countable-base clause serves a different
purpose: it will allow suitably extendible positions below a countable
path to be moved into a countable submonoid.  We formulate that descent
precisely at the end of the section and use it to bound the residual
symmetries of diagrams.

We prove the theorem through two extension lemmas.  They preserve more
than the order: keeping right factors and nonjoins fixed is what permits
the operations to be rearranged over a countable submonoid.

\subsection{The extension that inserts a probe}

Suppose $M$ has all the algebraic and margin properties above.
Fix $a,b,e\in M$, with $b,e\ne1$, and a nondecreasing path
\begin{equation}\label{eq:mono-path}
 1=n_0\sqsubseteq n_1\sqsubseteq\cdots\sqsubseteq a,
 \qquad n_id_i=n_{i+1},\qquad n_ic_i=a.
\end{equation}
Left cancellation gives $d_ic_{i+1}=c_i$.
Form the monoid presentation over $M$ with new generators $p_i$ and
relations
\begin{equation}\label{eq:mono-probe-relations}
 p_i=d_ip_{i+1},\qquad p_ib=c_ie\qquad(i<\omega).
\end{equation}
Put $m=p_0$.  Since $n_0=1$ and $n_id_i=n_{i+1}$, the first
relations give $n_ip_i=m$ for every $i$.  Thus every point of the path
divides the new probe.  The second relations make both factorizations
in Figure~\ref{fig:probe-divisibility} end at $ae$:
\[
 n_ip_ib=n_ic_ie=ae,\qquad mb=ae.
\]
These identities explain the presentation, but do not yet establish
its exact divisor profile.  We must prove that no old divisor of $a$
outside the path's downward closure is inserted below $m$, that $m$
does not divide $a$, and that every omitted divisor meets $m$ first
at $ae$.  The next lemma proves these
claims even for new divisors of $a$ introduced by the same extension.

\input{figures/probe-divisibility}

\begin{lemma}\label{lem:mono-probe-algebra}
The presented extension $M'$ is left cancellative and conical, has
conditional joins, and conservatively contains $M$.  Every new element
with an old right multiple has a least old right multiple, and
Equation~\eqref{eq:mono-gate-old} holds at this extension.
For $m=p_0$,
\begin{equation}\label{eq:mono-probe-profile}
 \begin{gathered}
 mb=ae,\qquad m\not\sqsubseteq a,\qquad
 \downarrow m\cap\downarrow a=\bigcup_i\downarrow n_i,\\
 x\vee m=ae\qquad
 (x\sqsubseteq a,\ x\not\sqsubseteq m),
 \end{gathered}
\end{equation}
where the downsets and joins in this display are computed in $M'$.
\end{lemma}

\begin{proof}
\smallskip\noindent\textit{Normal forms.}
Let $S$ be the direct limit of the sets $M$ under the maps
$x\mapsto xd_i$.  Write $[x,i]$ for the image of $x$ at stage $i$.
Equality in this direct limit means equality at a finite common stage.
The transition maps need not be injective: no right cancellation has
been assumed.  Nevertheless the left $M$-action on $S$ is injective
for each multiplier.  Indeed, equality after multiplying two letters
by an old $u$ becomes $uX=uY$ at a common stage, where left
cancellation gives $X=Y$.

There are well-defined equivariant maps
\[
 k([x,i])=xc_i,\qquad h(s)=k(s)e.
\]
The identity $d_ic_{i+1}=c_i$ proves well-definedness.  Before imposing
the second relation in Equation~\eqref{eq:mono-probe-relations}, the
normal forms are strings
\[
 s_1\cdots s_j y\qquad(s_i\in S,\ y\in M),
\]
including $j=0$.  The letter $[x,i]$ represents $xp_i$.
Old factors between new generators are absorbed into the following
letter, and the transition relations are precisely equality in $S$.
Multiplication concatenates strings, using the left action to absorb
the terminal old factor of the first string.

The remaining reductions are
\begin{equation}\label{eq:mono-reduction}
 s(bt)\longmapsto h(s)t,
\end{equation}
where $t$ is a letter of $S$ or a terminal old element.  The quotient
$t$ is unique because the left $b$-action is injective.  Each reduction
removes one new letter.  The only overlapping reductions occur in
$s\,(bt)\,(bu)$, with the final factor possibly terminal.  Reducing
in either order gives the same result by
\[
 h(bt)=b h(t),\qquad h(h(s)t)=h(s)h(t).
\]
Disjoint reductions commute by associativity of the action.  By Newman's
lemma \cite{Newman1942} (see \cite[Lemma~5.13]{DershowitzPlaisted2001}), these
local diamonds and termination give unique irreducibles: besides the
old elements, they are strings whose first letter is arbitrary and
whose later letters and terminal factor are not left-divisible by $b$.

Old left multipliers act injectively on these forms.  Left multiplication
by a letter $s$ either prepends $s$, when the input is not a $b$-multiple,
or sends $bZ$ to $h(s)Z$.  Both cases are injective.  Their ranges are
disjoint, because
\begin{equation}\label{eq:mono-head-separation}
 s\notin h(s)S.
\end{equation}
To see this, $s\in xS$ implies $x\sqsubseteq k(s)$, whereas
$k(s)e\not\sqsubseteq k(s)$ by conicality and left cancellation.
Thus every left multiplication is injective.  A new word can become
old only by consuming its first letter, at which point it is a multiple
of $h(s)\ne1$.  It cannot equal $1$, proving conicality.

\smallskip\noindent\textit{Old cones and the first-letter blocks.}
For $s\in S$, let $B_s$ consist of all irreducibles beginning with $s$.
For old $x$ the normal forms give
\begin{equation}\label{eq:mono-old-cone}
 xM'=xM\ \cup\!\bigcup_{s\in xS}B_s.
\end{equation}
At a common stage in the direct limit,
$xS\cap yS$ is $(x\vee y)S$ if the old join exists, and is empty
if the old cones are disjoint.  Thus old comparisons, their right
factors, joins and nonjoins are unchanged.  Notice that this conclusion
has not used a join theorem for arbitrary new words.

\smallskip\noindent\textit{Exits and gates.}
Fix an irreducible $w=sY$.  Right multiplication either leaves its
first letter intact or eventually consumes that letter.  We prove the
following precise alternative: the set $wM'\setminus B_s$ is empty,
or it is one cone $g(w)M'$ whose root $g(w)$ is old.  Thus the gate
will describe every exit from the fixed-head block, not only the old
multiples of $w$.

The first letter is consumed exactly when the suffix becomes a
$b$-multiple, so first calculate $YM'\cap bM'$.  If $Y$ is old,
Equation~\eqref{eq:mono-old-cone} gives the old join $Y\vee b$,
or an empty intersection.  If $Y$ is new with head $t$,
irreducibility gives $t\notin bS$.  No member of $B_t$ is then a
$b$-multiple.  By induction on the number of letters in the suffix,
all possible exits of $Y$ form the old-rooted cone $g(Y)M'$, if
there are any.  Its intersection with $bM'$ is calculated by the
old join $g(Y)\vee b$.

In either case the suffix intersection is empty or is $zM'$ for
an old $z=bu$ with old $u$.  The factor $u$ is old by conservation
of old comparisons.  In the nonempty case, multiplication by $s$
and the reduction $sbu=h(s)u$ give
\begin{equation}\label{eq:mono-gate-formula}
 wM'\setminus B_s=g(w)M',\qquad g(w)=h(s)u.
\end{equation}
This cone cannot return to $B_s$: every new head in it belongs to
$h(s)S$, whereas $s\notin h(s)S$ by
Equation~\eqref{eq:mono-head-separation}.  This proves the exit
alternative.  Every old multiple of $w$ lies outside $B_s$, so
$g(w)$ is in particular its least old multiple.

We record also the right factor $c(w)$ with $wc(w)=g(w)$.
If $Y$ is old, it is the old quotient of $z$ by $Y$.
If $Y$ is new and $Yc(Y)=g(Y)$, it is
\begin{equation}\label{eq:mono-gate-quotient}
 c(w)=c(Y)v,
 \qquad g(Y)v=z.
\end{equation}
All quotients in this recursion are old except the already constructed
$c(Y)$.  This explicit calculation will ensure conservation of right
factors when the same presentation is simulated over a larger base.

Append an old $d$ to $w$.  If the product leaves $B_s$, its first
letter has been consumed; that reduction can occur only after all
intervening letters have been consumed.  The result is then entirely
old.  Since the gate cone is disjoint from $B_s$, the hypothesis
$g(w)\sqsubseteq wd$ implies just such an exit.  This proves
Equation~\eqref{eq:mono-gate-old}.

\smallskip\noindent\textit{All conditional joins.}
For two forms with the same head, cancel that head and intersect their
suffix cones, using induction on the total number of new letters.
For old $x$ and new $w\in B_s$, either $s\in xS$, in which case
$x\sqsubseteq w$, or every common multiple must leave $B_s$.
The latter intersection is computed through $g(w)$ and an old join.
For $w\in B_s$ and $v\in B_t$ with $s\ne t$, an intersection
inside $B_s$ requires $g(v)$ to divide a member of $B_s$.  By
Equation~\eqref{eq:mono-old-cone} it then divides all of $B_s$, so
$v\sqsubseteq w$.  The symmetric case is the same.  Otherwise a
common multiple must leave both blocks, and the intersection is
computed by the old join of their gates.  Missing gates or missing
old joins give an empty intersection.  This proves conditional joins
in every case.

\smallskip\noindent\textit{The prescribed divisor profile.}
For any letter $s$, the old divisors of every element of $B_s$ form
\begin{equation}\label{eq:mono-letter-ideal}
 P_s=\{x\in M:s\in xS\}\subseteq\downarrow k(s).
\end{equation}
This is an ideal: common-stage representatives and old joins prove
join closure.  For the head $[1,0]$ of $m=p_0$, it is precisely
$\bigcup_i\downarrow_M n_i$, and the gate is $ae$.  The defining
relation gives $mb=ae$.  Since $ae\not\sqsubseteq a$, no member
of $B_{[1,0]}$ divides $a$; in particular $m\not\sqsubseteq a$.

Now let $x$ be a new divisor of $a$.  It is outside that block and
has an old gate $g(x)\sqsubseteq a$.  If $x\sqsubseteq m$, the
comparison leaves its block, so $g(x)\sqsubseteq m$, and the old
profile puts $g(x)$ below some $n_i$.  Conversely $x\sqsubseteq n_i$
implies $x\sqsubseteq m$.  If $x\not\sqsubseteq m$, its gate also
fails to divide $m$.  The possibility $m\sqsubseteq x$ is excluded
by $x\sqsubseteq a$.  The gate calculation consequently gives
$x\vee m=g(x)\vee m=ae$.  The corresponding assertions for old
$x$ follow directly from its block membership.  This proves
Equation~\eqref{eq:mono-probe-profile}, including new divisors of $a$.
\end{proof}

\subsection{Extending the real heights}

The gate description also controls the costs of all newly introduced
divisors.  This is the reason for keeping a cost as well as a height:
pointwise strict inequalities alone would not control suprema at a
limit stage.

\begin{lemma}\label{lem:mono-probe-heights}
The height and cost functions on $M$ extend to the probe extension
$M'$ so that Equation~\eqref{eq:mono-margin} holds.  For any old
comparison, its missed-cost supremum is unchanged.
\end{lemma}
\begin{proof}
Use $P_s$ from Equation~\eqref{eq:mono-letter-ideal}, and put
$A_s=\sup\rho[P_s]$.  We place the whole block $B_s$ in a short
height interval above its old divisors and below $\rho(h(s))$.
Here $h(s)$ is the gate of the bare letter $s$; the gate of a longer
word in $B_s$, when present, is a multiple of $h(s)$ and need not
equal it.  The interval must leave enough room for the costs of both
the old divisors and the new words.  More precisely, there are
positive $u_s,\delta_s$ with
\begin{equation}\label{eq:mono-height-interval}
 \begin{split}
 u_s-A_s&>\delta_s,\\
 \rho(h(s))-u_s-\delta_s
  &>\sup\{\epsilon_d:d\sqsubseteq h(s),\ d\in M\setminus P_s\}.
 \end{split}
\end{equation}
Indeed, put $p=\rho(k(s))-A_s\geq0$ and
$q=\rho(h(s))-\rho(k(s))>0$.  For $d\sqsubseteq k(s)$ missing
$P_s$, every $x\in P_s$ misses $d$, and the old margin yields
$\epsilon_d<\rho(k(s))-\rho(x)$.  The supremum of these costs is
at most $p$.  The supremum for $d\sqsubseteq h(s)$ not dividing
$k(s)$ is strictly below $q$.  Thus the full supremum on the right
of Equation~\eqref{eq:mono-height-interval} is strictly less than
$p+q=\rho(h(s))-A_s$, also when $p=0$.  This leaves the required
positive room for $u_s$ and $\delta_s$.

Define recursively on irreducibles
\begin{equation}\label{eq:mono-probe-height-definition}
 \begin{gathered}
 \rho(sY)=u_s+\delta_s\rho(Y),\qquad
 0<\epsilon_{sY}\leq\delta_s\epsilon_Y,\\
 \epsilon_{sY}\leq\epsilon_{g(sY)}
       \quad\text{whenever the gate exists}.
 \end{gathered}
\end{equation}
These choices give heights in $(0,1)$ and costs in $(0,1]$.
We verify all comparisons, including the suprema.

For two elements in one block $B_s$, a divisor of the upper element
from outside that block also divides the lower one.  An old divisor
belongs to $P_s$; a new divisor with a different head must enter by
its old gate, which then divides every member of $B_s$.
Inside the block, cancellation removes $s$, and the margin follows
by induction from the factor $\delta_s$ in both height differences
and cost bounds.

Suppose an old $x$ lies strictly below $sY$.  Then $x\in P_s$.
A missed divisor outside $B_s$ is old in $P_s$, or has an old gate
there of at least its cost.  For such an old divisor $d$ missing
$x$, the join $x\vee d$ lies in $P_s$, and hence
\[
 \epsilon_d<\rho(x\vee d)-\rho(x)\leq A_s-\rho(x).
\]
Their supremum is at most $A_s-\rho(x)$.  Divisors inside $B_s$
have cost at most $\delta_s$.  Equation~\eqref{eq:mono-height-interval}
makes $\rho(sY)-\rho(x)$ strictly larger than both bounds.

Suppose $sY$ lies strictly below an old $y$.  Then
$h(s)\sqsubseteq y$.  Every divisor of $y$ missing $sY$ is old
outside $P_s$, or has a gate there with at least its cost: a gate
in $P_s$ would put the divisor below all of $B_s$.
Among these old costs, those for divisors of $h(s)$ are bounded by
Equation~\eqref{eq:mono-height-interval}.  If $y\ne h(s)$, the
remaining costs have supremum strictly below
$\rho(y)-\rho(h(s))$ by the old margin.  The total gap
$\rho(y)-\rho(sY)$ is the sum of two positive gaps and exceeds both
cost suprema.  This proves this comparison case.

Distinct comparable new blocks have an intervening old gate, so the
preceding cases apply transitively.  To justify this use, if
$x0$.
A common multiple requires $x=y$ and equality of the letters before
position $\min(p,q)$.  If $p=q$, their intersection is obtained by
joining $z_p$ and $t_p$ in $D$, or is empty if that join is absent.
If $p0$ with $\theta+\phi<1$, and recursively set
\begin{equation}\label{eq:mono-merger-heights}
 \begin{split}
 \rho(wz)&=\rho(w)+(1-\rho(w))(\theta+\phi\rho_D(z)),\\
 0<\epsilon_{wz}&\leq
 (1-\rho(w))\min(\theta/2,\phi\epsilon^D_z).
 \end{split}
\end{equation}
For comparable new words of equal length only their last letters
vary; missed divisors of that length are handled by the scaled
$D$-margin, and all shorter divisors divide both words.  For a word
$w$ compared with $wz$, every missed divisor has the new length and
prefix $w$, so its cost is at most $(1-\rho(w))\theta/2$, strictly
less than the height increase.  An arbitrary comparison factors
through these comparisons, and, when the lower word is old, an old
comparison of leading coefficients.  Transitivity of the margin,
proved in Lemma~\ref{lem:mono-probe-heights}, finishes the check.
Old cost suprema are unchanged because there are no new old divisors.
\end{proof}

\subsection{Conservation under simulation}

We next establish the compatibility needed to reorder the construction.
This step also explains why overlap prescriptions remain valid when
operations are scheduled before they are executed.

\begin{lemma}\label{lem:mono-simulation}
Suppose $B\subseteq M$ is conservative and both monoids have the
algebraic properties above.  Either extension operation with parameters
in $B$ is valid over $M$, and the extension of $B$ conservatively
embeds into the corresponding extension of $M$ by the same generators.
A finite overlap prescription with parameters in $B$ is valid in $B$
if and only if it is valid in $M$.
\end{lemma}
\begin{proof}
For the last assertion, the only nontrivial transitivity check passes
through three copies.  In the middle copy, intersect the two prescribed
overlap starts.  If their old cones are disjoint, conservativity keeps
them disjoint.  Otherwise their old join and its right quotients are
unchanged.  Every later common multiple is a multiple of that join.
The two endpoint identifications at the join already agree in a valid
prescription over $B$, so right multiplication gives agreement at all
later common multiples.  This proves validity over $M$.  Conversely,
restrict a valid prescription to $B$.  Comparisons between its old
parameters have their quotients in $B$, so no identification or
transitivity witness between elements of $B$ requires leaving $B$.
The restriction has exactly the indicated pair relations and is valid.

For probes, equality of two letters in the smaller direct limit is
preserved and reflected because it is an equality at a common finite
stage.  If an old $b\in B$ divides a smaller letter $[x,i]$ in the
larger direct limit, there is a common stage at which
\[
 by=x d_i\cdots d_{j-1}.
\]
Both endpoints of this comparison belong to $B$, so its right factor
$y$ belongs to $B$.  Thus divisibility of a smaller letter by an old
smaller multiplier, including its quotient, is unchanged.  The same
irreducible words therefore embed.  The gate recursion uses only the
previous gates and old joins and quotients, so it has the same outcome,
including the absence of a gate.  The join calculations in
Lemma~\ref{lem:mono-probe-algebra} now preserve and reflect joins and
nonjoins.

For clarity, preservation of right quotients between new forms follows
by a separate division argument.  If both forms are old, use the base
hypothesis.  If the divisor is old and the dividend new, divide its
first direct-limit letter by the preceding common-stage calculation,
and retain its suffix.  If both forms have the same new head, cancel
that head and recurse on their suffixes.  In the remaining cases the
new divisor must leave its first-letter block.  Factor through its
gate, using the quotient in Equation~\eqref{eq:mono-gate-quotient},
and divide that old gate into the dividend by the first two cases.
Every factor obtained lies in the smaller extension.  Left
cancellation makes their product the unique required quotient.

For mergers, representation in an overlap and intersections of cones
in $D$ were calculated solely using old joins and their right
quotients.  These calculations are consequently unchanged.  The
normal forms in Equation~\eqref{eq:mono-merger-forms} then preserve
comparisons, their right factors, joins and nonjoins.  This proves
conservative simulation for both operations.
\end{proof}

\begin{lemma}\label{lem:mono-profile-persistence}
Suppose a probe satisfies Equation~\eqref{eq:mono-probe-profile} in
one stage of a tower of the two operations.  It continues to satisfy
that equation at every later stage and at the union, with the full
later downward closure of its original path.  Previously constructed
joins between probes are also preserved.
\end{lemma}
\begin{proof}
A merger introduces no new divisor of the old $a$.  At a probe
extension, a new $x\sqsubseteq a$ has an old gate
$g(x)\sqsubseteq a$.  If $x$ also divides the old probe, its gate
lies below that probe and hence below some original path element;
then $x$ does too.  If $x$ does not divide the old probe, its gate
does not either.  The old probe cannot divide $x$, because it does
not divide $a$.  The join calculation through the gate therefore
gives $ae$ in this case.  This proves both alternatives at a successor
step.  At a limit every tested element has already appeared, and all
comparisons and joins have been preserved.  Conservativity directly
preserves joins between existing probes.
\end{proof}

\subsection{The schedule and the countable-base rearrangement}

We now assemble the operations.  The height bound ensures that the
apparently arbitrary ideal requirements can be scheduled using only
countable paths.  The rearrangement proved afterward concerns the
same resulting monoid, not a separately constructed substitute.

\begin{proof}[Proof of Theorem~\ref{thm:monoid}]
\smallskip\noindent\textit{Saturating the geometric requirements.}
Start with the free monoid on $e$.  For $n<\omega$, for example, put
\[
 \rho(e^n)=1-2^{-n-1},\qquad \epsilon_{e^n}=2^{-n-3}.
\]
These satisfy Equation~\eqref{eq:mono-margin}.  Perform $\omega_1$
rounds.  At the start of a round schedule every available probe datum
$(a,b,(n_i))$ with the fixed $e$, and every available finite valid
merger.  For each probe datum schedule $\mu$ successive insertions.
Execute the resulting wellordered list with the two lemmas, and take
unions at limits.  Lemma~\ref{lem:mono-simulation} keeps every
scheduled merger valid until it is executed.

A monoid of size at most $\mu$ has at most $\mu^{\aleph_0}=\mu$
countable paths and at most $\mu$ finite prescriptions.  A probe
extension uses a quotient of $M\times\omega$ and finite strings;
a merger uses finitely many copies and finite strings.  Thus every
operation preserves size at most $\mu$, and each round has at most
$\mu$ steps.  The union of $\omega_1$ such rounds still has size
at most $\mu$.  The margin lemmas ensure that old values are never
changed and that old missed-cost suprema never increase, so the final
union $T$ has Equation~\eqref{eq:mono-margin} as well as all the
algebraic properties.

Given an ideal in $\downarrow_T a$, use
Lemma~\ref{lem:mono-countable-ideal} to obtain a cofinal path starting
at $1$.  Its elements, $a,b$, and all its transition and terminal
quotients occur before one round: the set is countable and the rounds
have cofinality $\omega_1$.  Alternatively, quotient conservativity
already puts every quotient into any stage containing its endpoints.
The corresponding requirement is scheduled.  Its final lower closure
is the given ideal, and Lemma~\ref{lem:mono-profile-persistence}
therefore gives Equation~\eqref{eq:mono-probes} for the $\mu$
insertions.  For any earlier and later insertion with the same datum, the
earlier probe is old but is not a divisor of $a$, so it is not an old
divisor of the new probe.  Joining through the new probe's gate gives
$ae$.  This join persists in the final union, proving independence.

Every final finite overlap prescription has its parameters in one
stage.  Its validity reflects to that stage by
Lemma~\ref{lem:mono-simulation}, and the schedule realizes it later.
The realization remains exact by conservation of comparisons and
quotients: equality $l_i x=l_j y$ in a later stage must still factor
through the preserved join of the two roots, with its prescribed
quotients.  Thus later right factors add exactly the stipulated
identifications and no others.  Finally use $a=1,b=e$ and $U=\{1\}$.
Its probes have no old divisor $e$, so there are $\mu$ elements of
$T\setminus eT$.  This proves both cardinality assertions.

\smallskip\noindent\textit{Extracting a countable initial base.}
It remains to prove the local construction property for this same $T$.
We first select countably many operations containing any prescribed
countable set of elements, and then perform all omitted operations over
their union.  The resulting tower must retain the gate rule: this is what
will let a later descent replace a position by one born at an earlier
stage.  Regard the
entire schedule as a continuous tower $(M_\alpha)_{\alpha\leq\lambda}$
of individual operations.  Record each parameter by a finite word in
previous generators.  Every element of the presented monoid has such
a word, and each equality has a finite derivation from the relations.
This does not assert that a whole countable path has finite support.

Choose a sufficiently large regular $\Theta$ and a countable elementary
submodel $N$ of $H_\Theta$ containing the tower, its presentations and
an enumeration of the prescribed countable subset of $T$.
Countable objects in $N$, in particular the parameter paths of
operations indexed in $N$, have all their entries in $N$.
First perform just the operations whose indices belong to $N$, in
their original order.  Let $S_\alpha$ denote this subconstruction
using selected indices below the cut $\alpha$.

At cuts $\alpha\in N$ we have
\begin{equation}\label{eq:mono-elementary-cut}
 S_\alpha=M_\alpha\cap N,
\end{equation}
with a conservative inclusion in $M_\alpha$.  Here is the induction
justifying the assertion.  Old comparisons, their quotients and joins
in an elementary intersection are reflected by elementarity; a
nonjoin remains a nonjoin in the larger monoid.  Before a selected
operation, every parameter is already present: its finite term code
belongs to $N$, and all entries of a countable path in $N$ belong to
$N$.  Conservative simulation makes that operation legal in the
subconstruction and embeds its result.  Conversely, every element of
$M_\alpha\cap N$ has by elementarity a finite term code in $N$;
all of its finitely many generator indices belong to $N$ and precede
$\alpha$.  It is therefore produced by the selected subconstruction.
This proves Equation~\eqref{eq:mono-elementary-cut} and the successor
step of the induction.  At a cut $\alpha\notin N$, fix the finitely
many words in a comparison or join test.  If they use selected operation
indices, let $\gamma$ be the greatest such index and put
$\beta=\gamma+1$; if there are no such indices, put $\beta=0$.
Then $\beta\in N$, $\beta<\alpha$, and all the words belong to
$S_\beta=M_\beta\cap N$.  The original inclusion
$M_\beta\subseteq M_\alpha$ is conservative.  Any right quotient or
conditional join required by the test therefore already lies in
$M_\beta$ and, by elementarity, in $N$, hence in $S_\beta$.
This also preserves nonjoins and proves conservation at $\alpha$.
Unions introduce no additional finite relation.  This completes the
induction.

The resulting selected submonoid $T_0$ is countable: the initial
monoid is countable, there are countably many selected steps, and each
operation over a countable base adds only countably many elements.
It contains the prescribed sequence by its finite term codes.
The set of selected indices need not be an initial segment; the
argument has used Equation~\eqref{eq:mono-elementary-cut} only at
cuts belonging to $N$.

\smallskip\noindent\textit{Reinserting the omitted operations.}
Append now the omitted steps in their original order.  Before an
omitted step $\alpha$, the current presentation is the union of the
original relations below $\alpha$ and all selected relations.  It has
an alternative realization: start with $M_\alpha$, and then perform
the selected steps at indices at least $\alpha$ in their order.
Indeed $S_\alpha\subseteq M_\alpha$ is conservative, and repeatedly
simulating the selected subconstruction makes all these operations
legal.  Each extends its whole base conservatively, so this alternative
realization conservatively contains $M_\alpha$.  It has precisely
the same generators and relations as the current reordered
presentation.  Consequently the original operation at $\alpha$ is
legal over the current base, by conservative simulation again.
Induction validates every appended step.  At limits the presentations
are their unions; at the end their union is exactly the original
presentation of $T$.

Each step of this reordered tower is one of the two operations.
The merger has no new old divisors, and the probe extension has its
least-old-multiple rule, including
Equation~\eqref{eq:mono-gate-old}.  Conservation allows those
comparisons to be tested in $T$.  This proves the last assertion and
completes the theorem.
\end{proof}

We isolate the consequence of the local construction property that will
be used for symmetries.  It makes explicit why a position below a
countable path can be moved to the countable base after finitely many
steps; it does not claim that every such position was in that base
already.

\begin{lemma}\label{lem:mono-descent}
Let $(n_i)$ be a nondecreasing sequence in $T$, and choose a
countable-base tower from Theorem~\ref{thm:monoid} whose initial
submonoid contains all $n_i$ and all right quotients between them.
Let $\mathcal A\subseteq\omega\times T$ be a set of pairs such that
each $(l,m)\in\mathcal A$ has $m\sqsubseteq n_N$ for some $N$.
Assume that for each $(l,m)\in\mathcal A$ and each $N$ there is
$(l',md)\in\mathcal A$ with $l'\geq l$, $n_ld=n_{l'}$, and
$n_N\sqsubseteq md$.  Then, starting from any pair in $\mathcal A$,
a finite succession of these replacements reaches a pair whose second
coordinate belongs to the initial countable submonoid.
\end{lemma}
\begin{proof}
If $m$ is not in that submonoid, take its first birth step in the
reordered tower.  It has the old multiple $n_N$, so this is a probe
step and its gate satisfies $g(m)\sqsubseteq n_N$.  Choose an
admissible replacement with $n_N\sqsubseteq md$.  The quotient
$d$ belongs to the initial submonoid and is therefore old at this
step.  Conservation and Equation~\eqref{eq:mono-gate-old} imply
that $md$ belongs to the strictly earlier base.  Repeat if necessary.
Each repetition strictly lowers the birth ordinal, so the process
terminates after finitely many repetitions.  The resulting position
lies in the countable initial submonoid.
\end{proof}
==== END The-Partition-Principle-does-not-imply-Choice//sections/monoid.tex ====

==== BEGIN The-Partition-Principle-does-not-imply-Choice//sections/quotients.tex ====
\section{Exact fibers of a symbolic quotient}\label{sec:quotient-fibers}\label{sec:quotients}

Our next objective is a bijection between $A$ and each of its
nonwellorderable quotients. A local count of names is insufficient:
assignments made in two diagrams must agree whenever those diagrams
occur in one generic filter. We first classify local elements by the
subdiagrams on which they are available. We then construct bijections
which respect every restriction and every change of coordinates.

Throughout the quotient construction, the cardinal parameters are those
of Section~\ref{sec:forcing}, with the monoid $T$ supplied there by
Theorem~\ref{thm:monoid}. The forcing $\mathbb P$ remains the
ground set of diagrams, including when it is used after forcing with
$\mathbb R$. We use countable closure of $\mathbb R$, regularity of
$\kappa=\omega_1$, preservation of the ground cardinals $\mu,\mu^+$,
and the ground equality $\mu^{\aleph_0}=\mu$. Preservation of smaller
cardinals is unnecessary. In particular, $\mu$ always denotes the
chosen ground ordinal, not a cardinal recomputed from a new continuum.
All ground selections below are choices over specified sets in $V$.

Fix a hereditarily symmetric name $\dot E$ and a product condition
$(d_0,p)$ symmetrically forcing that $\dot E$ is an equivalence relation
on $A$ whose quotient is not wellorderable. Enlarge the diagram so that
$D_p$ supports $\dot E$ and contains $\supp_I(d_0)$. Choose $q$ with
$q_e=p$. Our bijection will have support $D_q$ and will be forced below
$(d_0,q)$. Write $G_q=\Fix(D_q)$. This group fixes $q,p,d_0$ and
$\dot E$ literally.

We write $F$ for an $\mathbb R$-generic filter containing $d_0$, and
work temporarily in $V[F]$. A product name $\tau$ determines an ordinary
$\mathbb P$-name $\tau[F]$ there. Thus an assertion such as
$r\forces\tau=\sigma$ in this section means ordinary $\mathbb P$-forcing
in $V[F]$, using these sections of the product names. The generic
notation abbreviates forcing arguments uniform below $d_0$; no claim
that a ground permutation acts on one fixed evaluated universe is used.

\subsection{Local names and their cardinal bound}

Recall the local name collection from
Equation~\eqref{eq:normalized-local-names}. A normalized subset name
means a subset of the ground set
\[
 \{(\dot A_j,(d,s)):j\in I,
                 \ (d,s)\in\mathbb R\times\mathbb P\}.
\]
For a diagram $r$, $\mathcal X(r)$ is the ground set of all such
names fixed literally by $\Fix(D_r)$. Each is hereditarily symmetric,
since its member names are the individual label names. Normalization by
the forcing relation retains any given support. When $r\le q$, define
in $V[F]$
\[
 \mathcal D_F(r)=
 \{\tau\in\mathcal X(r):
       r\forces\tau\text{ is an }\dot E\text{-class}\}/\mathord\sim_r,
 \qquad
 \tau\sim_r\sigma\ \Longleftrightarrow\ r\forces\tau=\sigma.
\]
These are quotients of ground sets, so they are sets. We sometimes omit
$F$ from the notation. Their elements are symbolic classes of names,
not yet the evaluated members of $A/E$ in a product extension.
Lemma~\ref{lem:local-decision} applies to the
class and equality tests. Consequently, for $r\le s\le q$, retaining
the same name defines an injection
\begin{equation}\label{eq:symbolic-inclusion}
 \iota_{s,r}:\mathcal D_F(s)\longrightarrow\mathcal D_F(r).
\end{equation}
Indeed, if a stronger diagram forced two local names equal, the decision
at $s$ would already be equality. These maps compose literally on
representatives. Every $j\in D_r$ has a normalized name, supported by
$D_r$, for its $E$-class: use the forcing relation to name the labels
$E$-related to $\dot A_j$. Below the present hypothesis it is an
eligible member of $\mathcal D_F(r)$.

\begin{lemma}[Local quotient bound]\label{lem:local-quotient-bound}
For every $F$ as above and every ground $r\le q$,
$|\mathcal D_F(r)|\le\mu$ in $V[F]$.
\end{lemma}
\begin{proof}
For an element choose a representative $\tau$ and a diagram $t\le r$
forcing $\tau=[\dot A_j]_E$ for some $j\in D_t$. The ordinary forcing
theorem permits deciding a representative label; extending the diagram
includes its index. Write $r=t_b$. By Cohen restriction in
Lemma~\ref{lem:local-decision}, there is $d\in F$, supported in $D_t$,
witnessing this $\mathbb P$-forcing assertion. Record the triple
\[
 (b,x,t^{-1}d),\qquad t(x)=j,
\]
where $t^{-1}d$ is the partial binary function on $T\times\kappa$
obtained by replacing each coordinate $t(y)$ with $y$. Its domain has
size less than $\kappa$. The ground set of possible records has size
at most $\mu$, since $|T|=\mu$, $\kappa\le\mu$, and
$\mu^{<\kappa}=\mu$. Its ground enumeration remains an enumeration in
$V[F]$.

Suppose two chosen representatives $\tau_1,\tau_2$ have the same
record, witnessed by $t_1,t_2,d_1,d_2,j_1,j_2$. The ground bijection
$t_1(y)\mapsto t_2(y)$ agrees with the identity on $D_r$: in both
diagrams $r=(t_i)_b$. It maps points outside $D_r$ to points outside
$D_r$. Extend it to a ground permutation $\pi$ of $I$ fixing $D_r$.
This is possible since the two ranges have size $\mu<|I|$ and their
complements have the same cardinality $|I|$. Then
\[
 \pi t_1=t_2,\qquad \pi d_1=d_2,\qquad \pi j_1=j_2,
 \qquad \pi\tau_1=\tau_1.
\]
Product symmetry makes $d_2$ witness at $t_2$ equality of both
$\tau_1$ and $\tau_2$ with $[\dot A_{j_2}]_E$. Since $d_2\in F$,
$t_2$ forces $\tau_1=\tau_2$ in $V[F]$. Decision at $r$ gives the
same equality there. Thus distinct elements have distinct records.
Choosing representatives and records uses Choice in the ordinary
extension $V[F]$, not in the symmetric model.
\end{proof}

\subsection{Availability and exact multiplicities}

For $r\le q$, write $q=r_a$. For $h\in\mathcal D_F(r)$ and
$j\in D_r$, respectively, define
\begin{align}
 U_h&=\{n\sqsubseteq a:
             h\in\ran(\iota_{r_n,r})\},\label{eq:class-availability}\\
 U_j&=\{n\sqsubseteq a:j\in D_{r_n}\}.
             \label{eq:label-availability}
\end{align}
An ideal here is nonempty, downward closed, and closed under finite
joins. All joins needed within $\downarrow a$ exist.

\begin{lemma}[Availability ideals]\label{lem:availability-ideals}
Each set in Equations~\eqref{eq:class-availability} and
\eqref{eq:label-availability} is an ideal of $\downarrow a$.
Every ideal of $\downarrow a$ in $V[F]$ belongs to $V$.
\end{lemma}
\begin{proof}
Both sets contain $1$ and are downward closed by inclusion of
subdiagrams. Suppose $n,n'\in U_h$ and put $k=n\vee n'$. The ranges
of $r_n,r_{n'}$ intersect exactly in $D_{r_k}$. Choose supported names
for their representations of $h$. They are forced equal by $r$.
Lemma~\ref{lem:support-descent}, with root $r_k$, supplies a
$D_{r_k}$-supported name equal to them. Normalize it without changing
support. Decision at $r_k$ shows it is an $E$-class there: its
negation would persist to the extension $r$. Thus $k\in U_h$.
For labels the identical argument is the literal equality of cone
intersections, without any name descent.

For the final assertion, apply Lemma~\ref{lem:mono-countable-ideal}
in $V[F]$. The ground monoid, order, heights and costs retain their
meanings there, so every nonempty ideal has a countable cofinal sequence.
It consists of ground elements of $T$, so countable closure of
$\mathbb R$ puts it in $V$. Its downward closure, computed with the
unchanged ground order, is the original ideal. The argument applies
to every ideal in $V[F]$, not only to ground ideals.
\end{proof}

For a nonempty ideal $U\subseteq\downarrow a$, put
\[
 B_{r,U}(F)=\{h\in\mathcal D_F(r):U_h=U\},\qquad
 L_{r,U}=\{j\in D_r:U_j=U\}.
\]
The second set is ground data; the first can depend on $F$.
These exact fibers, rather than the whole local sets $\mathcal D_F(r)$,
are the pieces on which a bijection can respect restriction: a label
and its assigned class must remain available at precisely the same
subdiagrams.

\begin{lemma}[Exact fibers]\label{lem:exact-fibers}
For every $r\le q$ and every nonempty ideal
$U\subseteq\downarrow a$, where $q=r_a$, both $B_{r,U}(F)$ and
$L_{r,U}$ have cardinality $\mu$ in $V[F]$. The label fiber already
has that cardinality in $V$.
\end{lemma}
\begin{proof}
The common root $p$ will separate the copies used in this proof.
We first find a class with no representation supported by $D_p$.
Copying it into diagrams whose unwanted intersections are exactly
$D_p$ will then rule out both coincidences between copies and
availability at forbidden subdiagrams, by support descent.

\smallskip\noindent\textit{A class unavailable at the root.}
Enumerate
$\mathcal X(p)$ in $V$ as $(\tau_\xi:\xi<\lambda)$. The canonical
name for the sequence of its evaluations is hereditarily symmetric
with support $D_p$. Explicitly, its entries are the canonical pairs
$(\check\xi,\tau_\xi)$, each placed under every product condition.
Every member of $\Fix(D_p)$ fixes each entry literally. The range
of this sequence is wellorderable inside $W$: map each value to its
least index of occurrence. If it contained every $E$-class, the same
map restricted to $A/E$ would wellorder that quotient. The hypothesis
therefore implies, ordinarily below $(d_0,p)$, that some $E$-class
lies outside the evaluations of all names in $\mathcal X(p)$.

Fix $F$ containing $d_0$. By the ordinary forcing theorem choose
$t\le p$ and $j\in D_t$ such that $t$ forces the class of $A_j$
outside that entire evaluation list. Choose a witnessing Cohen
condition $d\in F$ supported in $D_t$, using
Lemma~\ref{lem:local-decision}. Write $p=t_b$. Necessarily $b\ne1$,
since a class represented by a label in $D_p$ has a name in
$\mathcal X(p)$.

\smallskip\noindent\textit{Independent copies with active Cohen conditions.}
As $p=r_{ae}$, the probe property of Theorem~\ref{thm:monoid}
supplies $\mu$ elements $m$ with $mb=ae$ and the prescribed ideal
$U$. The diagrams $r_m$ are copies of $t$ over $p$, with pairwise
intersection exactly $D_p$. Choose the ground permutations taking
$t$ to these diagrams and fixing $D_p$, and transport $d$ and the
class name along them. Their nonroot coordinate sets are disjoint.
This is the role of the earlier extension $q_e=p$: the availability
pattern is prescribed among divisors of $a$, while the common root
lies at $ae$, strictly beyond $a$.

There are $\mu$ copies whose transported Cohen conditions belong to
$F$. To see this without any $\mu$-closure assertion, partition the
ground family into $\mu$ ground subfamilies of size $\mu$. In each
subfamily the conditions extending at least one transported copy of
$d$ form a dense set below $d\restriction D_p$. Indeed, a Cohen
condition uses countably many coordinate indices; among the pairwise
disjoint nonroot ranges there is one it misses, and on the root the
two conditions agree. Their union is a Cohen condition. Genericity
meets each of these ground dense sets. A hit in each disjoint
subfamily yields $\mu$ different hits.

\smallskip\noindent\textit{Distinct classes with the prescribed exact ideal.}
Each hit gives a $D_{r_m}$-supported class name forced at $r_m$
to lie outside the evaluations of $\mathcal X(p)$. The diagram
$r_m$ extends $p$ but need not extend $q$; we use its class name,
not a set $\mathcal D_F(r_m)$. As $r$ extends $r_m$, this name
represents a symbolic class in the defined set $\mathcal D_F(r)$.
Two such
classes cannot be equal there: support descent over their common
root $p$ would supply a name in $\mathcal X(p)$ for their common
value, contrary to the outside assertion. If $n\in U$, then
$n\sqsubseteq m$, so $r_n$ extends $r_m$ and the class is available
at $r_n$. If $n\sqsubseteq a$ and $n\notin U$, the exact probe
intersection gives
\[
 nT\cap mT=aeT,
 \qquad D_{r_n}\cap D_{r_m}=D_p.
\]
Availability at $r_n$ would again descend to a name in
$\mathcal X(p)$, a contradiction. Its exact availability ideal is
therefore $U$. This gives $\mu$ distinct elements of $B_{r,U}(F)$;
Lemma~\ref{lem:local-quotient-bound} bounds that fiber from above.

\smallskip\noindent\textit{The label fiber.}
For labels use the probe centers $r(m)$. Their availability ideals
are exactly $\downarrow m\cap\downarrow a=U$, and distinct probes
have distinct centers. This supplies a ground $\mu$-subset of
$L_{r,U}$; the upper bound follows from $|D_r|=\mu$.
\end{proof}

\section{Components of subdiagrams and their stabilizers}
\label{sec:quotient-components}

The exact fibers have equal cardinality, but choosing their bijections
independently would not preserve assignments when a diagram is replaced
by a subdiagram. We first show that restriction identifies entire
exact fibers, not merely subsets of them. Following these canonical
identifications groups the fibers into components. Only after forming
the components will we choose bijections; their stabilizers determine
which symmetries those choices must respect.

\subsection{Contractions and canonical identifications}

A vertex is a pair $v=(r,U)$, where $r\le q$, $q=r_a$, and $U$ is a
nonempty ideal of $\downarrow a$. Vertices form a ground set by
Lemma~\ref{lem:availability-ideals}. For $n\in U$ define a
\emph{contraction}
\begin{equation}\label{eq:quotient-contraction}
 (r,U)\longrightarrow(r_n,U_n),\qquad
 U_n=\{x\sqsubseteq c:nx\in U\},\quad nc=a.
\end{equation}
Left multiplication preserves conditional joins. In fact cancellation
and the common-cone description of a join give
$n(x\vee y)=nx\vee ny$ whenever these elements have a common right
multiple. It follows that $U_n$ is an ideal. Contractions compose;
there is at most one contraction between fixed endpoints, since the
center of $r_n$ is $r(n)$ and $r$ is injective. Write $B_v(F)$ and
$L_v$ for the two fibers at a vertex.

\begin{lemma}[Contraction identifications]\label{lem:contraction-fibers}
For every contraction $v\to w$, the label fibers satisfy $L_v=L_w$,
and inclusion of symbolic elements gives a bijection
$B_w(F)\longrightarrow B_v(F)$. These identifications commute with
composition.
\end{lemma}
\begin{proof}
Let $v=(r,U)$, $w=(r_n,U_n)$, and first take a symbolic class
available at $r_n$. Its full availability ideal $J$ at $r$ contains
$n$. For $z\sqsubseteq a$, ideal closure gives
\[
 z\in J\quad\Longleftrightarrow\quad z\vee n\in J.
\]
Write $z\vee n=nx$. Availability at $r_{z\vee n}$ is exactly the
corresponding availability at the subdiagram $(r_n)_x$ of $r_n$.
Thus the restricted ideal at $r_n$ determines the full ideal at $r$.
If that restricted ideal is $U_n$, the last test is equivalent to
$z\vee n\in U$, and hence to $z\in U$. Conversely, an element of
$B_v(F)$ is available at $r_n$ because $n\in U$, and its restricted
ideal is $U_n$. This proves surjectivity; injectivity follows from
Equation~\eqref{eq:symbolic-inclusion}. For labels use the same
argument with literal membership in ranges. Commutation follows
because all the symbolic maps retain the same representative names.
\end{proof}

Let a component be a connected component of the vertex system when
the direction of contractions is ignored. The successors of each
vertex are directed: contract at the join of two contraction indices.
Any two vertices in one component have a common successor. Indeed,
this holds along a single edge; along a finite path combine a common
successor of its initial part with the final edge, using directedness
of successors at the shared vertex. The same induction gives a common
successor for any finite set of vertices in a component.

Consequently all finite chains of the identifications in
Lemma~\ref{lem:contraction-fibers} are consistent. One can compare a
finite chain at a common successor, where both composites are the
same map. In a component $C$, glue the disjoint union of its $B_v(F)$
by these identifications and call the resulting set $B_C(F)$. Each
fiber maps bijectively onto $B_C(F)$. In particular, the gluing creates
no new identifications within one fiber. All label fibers in $C$
are the same ground subset of $I$; denote it by $L_C$. Both sets have
cardinality $\mu$ in $V[F]$.

Choose in $V$ a vertex $(r,U)$ of $C$ and a nondecreasing cofinal
sequence $(n_i:i<\omega)$ in $U$, with $n_0=1$. Let $v_i$ be its
contraction at $n_i$. This chain is cofinal in the entire component.
To check this, compare any vertex with $v_0$ at a common successor,
which is a contraction of $v_0$ at some $n\in U$. Choose $i$ with
$n\sqsubseteq n_i$. Then $v_i$ is a successor of that common
successor and hence of the given vertex.

\subsection{Only countably many residual symmetries}

The group $G_q$ acts on the ground vertex system. On symbolic fibers
it acts by transport between generics:
\begin{equation}\label{eq:symbolic-transport}
 T_\pi^F:\mathcal D_F(r)\longrightarrow
                   \mathcal D_{\pi F}(\pi r),
 \qquad [\tau]_r\longmapsto[\pi\tau]_{\pi r}.
\end{equation}
The forcing symmetry lemma makes this well defined, and it commutes
with all contraction identifications. We use the same notation for
transport on the glued fibers, and suppress the superscript when its
source generic is specified by the argument.

Let $G_C$ be the setwise stabilizer of $C$ in $G_q$. Define
\[
 K_C=\bigcup_{i<\omega}\Fix(D_{r_{n_i}}).
\]
Each displayed fixer is a subgroup of $G_q$, because $D_q$ is contained
in every chain range. It fixes a vertex and therefore lies in $G_C$.
The ranges decrease, so the subgroups increase and their union is a
subgroup. For $\sigma\in G_C$, the moved chain is also cofinal.
For every $i$ there is $j$ with
$D_{r_{n_j}}\subseteq D_{\sigma r_{n_i}}$. Hence
\[
 \sigma\Fix(D_{r_{n_i}})\sigma^{-1}
 =\Fix(D_{\sigma r_{n_i}})\subseteq\Fix(D_{r_{n_j}}).
\]
Applying the same reasoning to $\sigma^{-1}$ proves that $K_C$ is
normal in $G_C$.

\begin{lemma}[Countable stabilizer quotient]\label{lem:countable-germs}
In the ground model, $|G_C/K_C|\le\aleph_0$.
\end{lemma}
\begin{proof}
Choose the countable-base tower of Theorem~\ref{thm:monoid} so that
its initial submonoid $T_0$ contains all $n_i$ and all right
quotients between them. For $\pi\in G_C$, consider its alignments
with contractions of the chosen vertex:
\[
 \mathcal A_\pi=
 \{(l,m)\in\omega\times U:\pi r_{n_l}=r_m\}.
\]
This set is nonempty: the moved chain is cofinal in $C$, so one of
its terms is a successor of $v_0$. Every second coordinate $m$ of
an alignment divides some $n_N$, by cofinality of $(n_i)$ in $U$.

To apply Lemma~\ref{lem:mono-descent}, fix $(l,m)\in\mathcal A_\pi$
and any $N$. Choose $l'\ge l$ so that $\pi v_{l'}$ is a successor
of $v_N$. Its diagram is $r_k$ for some $k\in U$ with
$n_N\sqsubseteq k$. Let $d\in T_0$ be the right quotient
$n_ld=n_{l'}$. Then
\[
 r_k=\pi r_{n_{l'}}=(\pi r_{n_l})_d=r_{md}.
\]
Injectivity of $r$ gives $k=md$. Consequently $md\in U$,
$n_N\sqsubseteq md$, and $(l',md)\in\mathcal A_\pi$.
These are exactly the replacement hypotheses of
Lemma~\ref{lem:mono-descent}. Its conclusion supplies an alignment
$(l,m)$ with $m\in T_0$.

There are countably many resulting alignment pairs
$(l,m)\in\omega\times T_0$. Two permutations giving the same pair
agree pointwise on $D_{r_{n_l}}$; if they are $\pi$ and $\rho$,
then $\pi^{-1}\rho\in\Fix(D_{r_{n_l}})\subseteq K_C$.
Enumerate the pairs, and assign to each coset the first
pair realized by any of its members. Distinct cosets receive distinct
pairs. This proves the bound.
\end{proof}

\section{Equivariant assignments and the quotient bijection}
\label{sec:quotient-equivariance}

For each component $C$ we seek a bijection
$f_C(F):L_C\to B_C(F)$ satisfying
\begin{equation}\label{eq:component-covariance}
 f_C(\sigma F)(\sigma j)=T_\sigma^F(f_C(F)(j))
              \qquad(\sigma\in G_C).
\end{equation}
This is an identity between computations at different generics, not
an action on one fixed extension. We first construct a bijection
covariant under $K_C$: its elements fix a sufficiently late subdiagram,
so they fix the tails of suitable name codes. We then handle the
remaining countable quotient $G_C/K_C$. Bounded Cohen-row patterns
distinguish its cosets and select a transported bijection with the
full covariance in Equation~\eqref{eq:component-covariance}.

\subsection{An assignment invariant under a tail fixer}

For the chosen chain of $C$, let $\mathcal Q_C$ be the ground set of
sequences
\[
 c=(\tau_i:i<\omega),\qquad \tau_i\in\mathcal X(r_{n_i}).
\]
Say that $c$ represents $b\in B_C(F)$ if, from some index onward,
$\tau_i$ represents an element of the exact fiber $B_{v_i}(F)$ and
its image in $B_C(F)$ is $b$. Finite initial segments are ignored.
Every $b$ has such a code: choose representatives at all chain
vertices in $V[F]$, using their bijections with $B_C(F)$. This is a
countable sequence of ground name codes, and hence belongs to $V$
by countable closure of $\mathbb R$.

Fix a ground wellordering of $\mathcal Q_C$, of order type $\lambda_C$.
Assign to $b$ its least representing code. Distinct $b$ have different
codes, so this defines a wellorder $<_F$ of $B_C(F)$.

\begin{lemma}[Covariance of the least-code order]
\label{lem:least-code-covariance}
For every $k\in K_C$, transport $T_k^F$ is an order isomorphism
from $(B_C(F),<_F)$ to $(B_C(kF),<_{kF})$. The group $K_C$ fixes
$L_C$ pointwise.
\end{lemma}
\begin{proof}
Choose $N$ such that $k$ fixes $D_{r_{n_N}}$ pointwise. For $i\ge N$
it fixes $r_{n_i}$ and every name in $\mathcal X(r_{n_i})$ literally.
Consequently each particular ground code $c$ represents $b$ at $F$
if and only if the \emph{same code} represents $T_k^F(b)$ at $kF$.
The forcing symmetry lemma proves this on the tail; the definition
ignores the remaining finite prefix. Thus the sets of functioning
codes are identical, and their minima under the fixed ground
wellorder are identical. This proves the order assertion. Also
$L_C\subseteq D_{r_{n_i}}$ for every $i$, so $k$ fixes its every
member.
\end{proof}

Let $\theta_C(F)$ be the order type of this order. It is at most
$\lambda_C$, since it is the order induced on a subset of the ordered
code set. It has cardinality $\mu$ in $V[F]$. Preservation of $\mu$
and $\mu^+$ implies
\[
 \mu\le\theta_C(F)<\mu^+,
 \qquad |\theta_C(F)|^V=\mu.
\]
Here the order type is an ordinal, hence a ground ordinal. The two
preserved cardinal endpoints justify the last equality even if smaller
cardinals have collapsed. In $V$, choose bijections
$e_\theta:\mu\longrightarrow\theta$ for the set of ordinals
$\theta\le\lambda_C$ with ground cardinality $\mu$. Also fix a ground
bijection $l_C:\mu\longrightarrow L_C$. If
$b_F:\theta_C(F)\longrightarrow B_C(F)$ is the unique order
isomorphism, define
\[
 f_C^0(F)=b_F\circ e_{\theta_C(F)}\circ l_C^{-1}.
\]
This is a bijection $L_C\to B_C(F)$. All choices have been restricted
to sets; no simultaneous choice over a proper class of ordinals occurs.
Lemma~\ref{lem:least-code-covariance} gives
\begin{equation}\label{eq:preliminary-covariance}
 f_C^0(kF)(j)=T_k^F\bigl(f_C^0(F)(j)\bigr)
       \qquad(k\in K_C,\ j\in L_C).
\end{equation}
The ground wellorder of all codes need not be invariant under $k$.
The proof uses eventual fixation of each code's entries instead.

\subsection{Detecting and choosing a coset}

Put $\Gamma_C=G_C/K_C$, writing cosets as $\pi K_C$. It is a
countable ground
group by Lemma~\ref{lem:countable-germs}. For each nonidentity coset
$\delta$, choose a ground representative $\gamma_\delta$ and points
\[
 s_{\delta,i}\in D_{r_{n_i}},\qquad
 \gamma_\delta(s_{\delta,i})\ne s_{\delta,i}
       \quad(i<\omega).
\]
Such a point exists for every $i$, since otherwise
$\gamma_\delta\in K_C$. Fix an enumeration of the set of nonidentity
cosets. For $\alpha<\kappa$ and $\pi\in G_C$, define the pattern
\begin{equation}\label{eq:detector-pattern}
 P_F^\alpha(\pi K_C)=
 \left(
  \left[\left(A_{\pi(s_{\delta,i})}^F
                       \restriction\alpha:i<\omega\right)\right]_{\rm ev}
              :\delta\in\Gamma_C\setminus\{1\}\right),
\end{equation}
where $[\cdot]_{\rm ev}$ denotes equivalence modulo eventual equality
of sequences. We regard each row as its binary characteristic
function. The equivalence classes in this formula are taken in the
ground set of sequences of subsets of $\alpha$.

This ground interpretation is legitimate. Every $\alpha<\omega_1$
is countable. The bounded row restrictions and all their countably
many coordinates, for all detectors, form a countable sequence of
ground bits and indices. Since $\mathbb R$ adds no such sequences,
these data belong to $V$. Eventual equality between ground sequences
has the same meaning in the extension. For all $\alpha<\kappa$
together the possible patterns form a ground set, on which choose a
ground wellorder, separately for each $\alpha$ if desired.

\begin{lemma}[A covariant coset selector]\label{lem:coset-selector}
Formula~\eqref{eq:detector-pattern} is independent of the
representative of $\pi K_C$. For each $F$ there is an
$\alpha<\kappa$ at which all distinct cosets have distinct patterns.
There is a definable selection $c_C(F)\in\Gamma_C$ satisfying
\begin{equation}\label{eq:coset-selector-covariance}
 c_C(\sigma F)=\sigma c_C(F)\qquad(\sigma\in G_C).
\end{equation}
\end{lemma}
\begin{proof}
If $k\in K_C$, it fixes all $s_{\delta,i}$ once $i$ is sufficiently
large. Replacing $\pi$ with $\pi k$ therefore changes each detector
sequence in only finitely many places, proving representative
independence.

Suppose $\pi K_C\ne\pi'K_C$. Use the detector for
$\delta=(\pi^{-1}\pi')K_C$ and write
$\pi^{-1}\pi'=\gamma_\delta k$ with $k\in K_C$. Eventually
$k(s_{\delta,i})=s_{\delta,i}$, and hence
\[
 \pi(s_{\delta,i})\ne\pi'(s_{\delta,i}).
\]
Distinct label indices give distinct Cohen rows. For each of these
tail positions choose a bit where the two rows differ. The countably
many bit ordinals are bounded below regular $\kappa$. Above that
bound the two restricted sequences disagree at every position on a
tail, so are unequal modulo eventual equality. There are countably
many pairs of cosets; a further countable supremum supplies one bound
that distinguishes all pairs. These choices take place in $V[F]$.
They use regularity of $\kappa$, not closure of $\mathbb P$.

At the least distinguishing $\alpha$, choose the coset whose pattern
is least in the fixed ground wellorder. If $\Gamma_C$ is trivial,
choose its sole element and use $\alpha=0$. For $\sigma\in G_C$,
label transport gives, for every $s\in I$,
$A_{\sigma s}^{\sigma F}=A_s^F$. Thus
\begin{equation}\label{eq:pattern-covariance}
 P_{\sigma F}^\alpha((\sigma\pi)K_C)
                    =P_F^\alpha(\pi K_C).
\end{equation}
The actual ground pattern objects on the two sides are equal. Left
multiplication permutes the coset set, so the least distinguishing
bound is unchanged and the same pattern object is minimal. This
proves Equation~\eqref{eq:coset-selector-covariance}.
\end{proof}

For a coset $\gamma=\pi K_C$, define a transported preliminary
bijection by
\begin{equation}\label{eq:coset-assignment}
 f_C^\gamma(F)(j)=
 T_\pi^{\pi^{-1}F}
       \left(f_C^0(\pi^{-1}F)(\pi^{-1}j)\right),\qquad j\in L_C.
\end{equation}
Equivalently, the square in Figure~\ref{fig:moved-generic-transport}
commutes.

\input{figures/moved-generic-transport}

This is independent of $\pi$. Replacing $\pi$ with $\pi k$ inserts
$k^{-1}$ in the source generic, and
Equation~\eqref{eq:preliminary-covariance} cancels its transport;
$k$ fixes every label of $L_C$. Define
$f_C(F)=f_C^{c_C(F)}(F)$. Equations~\eqref{eq:coset-selector-covariance}
and~\eqref{eq:coset-assignment} now give the required
Equation~\eqref{eq:component-covariance}.
This calculation explains why the preliminary computation in
Equation~\eqref{eq:coset-assignment} is made at $\pi^{-1}F$.
An arbitrary transport of the computation at $F$ would not give the
required identity.

\subsection{Transport over all components}

Choose in $V$ one representative from each $G_q$-orbit of components
and perform the preceding set-sized choices for these representatives.
For $C'=\sigma C$, transport $f_C(\sigma^{-1}F)$ by $\sigma$ to
obtain $f_{C'}(F)$. Two possible choices of $\sigma$ differ by an
element of $G_C$, so Equation~\eqref{eq:component-covariance} proves
that this definition is independent of the choice. It yields
bijections for every component, covariant under all $G_q$. Pulling
back along the canonical maps $B_v(F)\to B_C(F)$ gives bijections
\begin{equation}\label{eq:coherent-fiber-bijections}
 f_{r,U}(F):L_{r,U}\longrightarrow B_{r,U}(F).
\end{equation}
They commute with every contraction, and their transports under every
$\pi\in G_q$ are the corresponding bijections at $\pi F$.

We record the definability needed to convert these computations into
one symmetric name. The ground sets of vertices, components, name
codes, code wellorders, patterns and auxiliary bijections are all
sets. The sections of the product names can be constructed in an
$\mathbb R$-extension from its generic filter; the ordinary forcing
relation for the ground set poset $\mathbb P$ is definable there.
Symbolic quotients and their gluing use equivalence relations on sets.
All remaining steps use set operations, least elements of prescribed
wellorders, and unique order isomorphisms. They therefore define,
by an ordinary set-theoretic formula in an $\mathbb R$-extension, the
predicate
\begin{equation}\label{eq:assignment-predicate}
 \Phi(F,r,j,\tau):
 \quad \tau\in\mathcal X(r)\text{ represents }
 f_{r,U_j}(F)(j)\text{ in }\mathcal D_F(r).
\end{equation}
Here $U_j$ is ground data from Equation~\eqref{eq:label-availability}.
One formal implementation uses a ground set of all normalized name
codes and its ordinary name-evaluation relation to construct their
$\mathbb P$-sections. The variable for a ground code and the actual
forcing name that it codes are kept distinct. In particular, we never
use the false assertion that an automorphism moves a check-name for a
ground code to the check-name for its transported code.

The proved semantic covariance is the identity
\[
 \Phi(F,r,j,\tau)\quad\Longleftrightarrow\quad
 \Phi(\pi F,\pi r,\pi j,\pi\tau)
       \qquad(\pi\in G_q).
\]
These computations are ordinary forcing arguments for this fixed
formula. More explicitly, let
\[
 \dot F^{\pi}=
 \{(\check{\pi d},d):d\in\mathbb R\},
\]
whose value at $F$ is $\pi F$. The preceding covariance proof gives
the equivalence, forced by $d_0$ in $\mathbb R$, between
$\Phi(\dot F,r,j,\tau)$ and
$\Phi(\dot F^{\pi},\pi r,\pi j,\pi\tau)$, with all auxiliary
ground choices fixed. Under the name action,
$\pi\dot F^{\pi}=\dot F$ literally, while check names for the
displayed ground arguments remain fixed. Applying ordinary forcing
symmetry therefore gives
\begin{equation}\label{eq:assignment-forcing-covariance}
 d\forces_{\mathbb R}\Phi(\dot F,r,j,\tau)
 \quad\Longleftrightarrow\quad
 \pi d\forces_{\mathbb R}
                  \Phi(\dot F,\pi r,\pi j,\pi\tau)
 \qquad(d\le d_0).
\end{equation}
All auxiliary ground choices are already fixed in the defining
formula; covariance was proved for this one construction. The
$\mathbb R$-forcing values in this display are ground sets of
conditions. Equivalently, if $F'$ contains $\pi d$, put
$F=\pi^{-1}F'$ and apply covariance to the computation at $F$;
the converse uses $\pi^{-1}$. This generic description abbreviates
the fixed-formula argument above and requires no transitive-ground
assumption in the consistency deduction.

\subsection{One hereditarily symmetric graph}

\begin{theorem}[Quotient classification]\label{thm:quotient-classification}
In $W$, every nonwellorderable surjective image of $A$ is in bijection
with $A$.
\end{theorem}
\begin{proof}
We first finish the construction for the equivalence relation fixed
at the start of Section~\ref{sec:quotient-fibers}. Use canonical
equivariant ordered-pair names and form the product name
\begin{equation}\label{eq:quotient-bijection-name}
 \dot J=
 \left\{
 \left(\langle\dot A_j,\tau\rangle^{\bullet},(d,r)\right):
 \begin{array}{l}
 r\le q,\ j\in D_r,\ \tau\in\mathcal X(r),\ d\le d_0,\\
 d\forces_{\mathbb R}\Phi(\dot F,r,j,\tau)
 \end{array}\right\}.
\end{equation}
The superscript denotes the name for the ordered pair. This is a set
name: every index ranges over a ground set and the defining forcing
relation is a ground relation. Equation~\eqref{eq:assignment-forcing-covariance}
sends each entry under $\pi\in G_q$ to another entry. Applying
$\pi^{-1}$ gives equality of the sets of entries, so $G_q$ fixes
$\dot J$ literally. Each member name is a pair of HS names; thus
$\dot J$ is HS with support $D_q$. The individual member names may
have different supports. Hereditary symmetry does not require all of
them to use $D_q$.

Take a product generic $(F,H)$ containing $(d_0,q)$. For every
$r\in H$ below $q$, the graph contains exactly the local assignments
of Equation~\eqref{eq:coherent-fiber-bijections}. In detail, whenever
$\Phi(F,r,j,\tau)$ holds, the $\mathbb R$ truth lemma gives a
condition of $F$ forcing it; strengthening with $d_0$ retains a
condition of $F$, and Equation~\eqref{eq:quotient-bijection-name}
includes its entry. Conversely, every active entry forces its
asserted assignment. All classes are represented by names in their
symbolic equivalence classes, so the local assignments are complete.

We check the comparison when the diagram is strengthened. Suppose
$t\le r\le q$, $r=t_b$, and $j\in D_r$. The availability ideal
of $j$ at $t$ contains $b$. Hence
\[
 (t,U_j\text{ computed at }t)
        \longrightarrow(r,U_j\text{ computed at }r)
\]
is a contraction. Equation~\eqref{eq:coherent-fiber-bijections}
therefore gives the same assigned symbolic element under inclusion.
In particular, its product-name evaluations are equal in every
$\mathbb P$-generic containing $t$.

Any two active entries of $\dot J$ occur together below a common
stronger diagram in $H$. At that diagram the union of the
exact-fiber bijections is a bijection
$D_t\to\mathcal D_F(t)$: availability ideals partition both sets.
The preceding comparison proves single-valuedness and injectivity of
$\dot J^{F,H}$. Distinct symbolic elements are forced unequal there
by local decision, and distinct indices have distinct Cohen labels.
Thus these are also single-valuedness and injectivity for the actual
sets of the graph.

Every label index belongs to a diagram in $H$ below $q$, by the
density of extending diagrams to contain prescribed supports.
Therefore the graph has domain $A$. To reach an arbitrary $E$-class,
take any label belonging to that class and include its index in such
a diagram $r$. Its canonical supported class name represents an
element of $\mathcal D_F(r)$. The local fiber bijection is onto the
fiber containing that element, so the graph reaches the class.
This is a pointwise existence argument; no simultaneous selection
of representatives of all classes has been made. The range is
exactly $A/E$. The graph belongs to $W$ because its name is HS.

The construction was made on an extension of an arbitrary symmetric
condition asserting the nonwellorderable-quotient hypothesis. Applying
the symmetric forcing theorem and truth lemma therefore proves in
$W$ that every such quotient $A/E$ is in bijection with $A$.
Finally, for a surjection $h:A\to Y$ in $W$, form its kernel
relation $E$ in $W$. The map $[a]_E\mapsto h(a)$ is a bijection
$A/E\to Y$, defined by its unique values without choosing class
representatives. If $Y$ is nonwellorderable, so is $A/E$, and composing
this bijection with the one just constructed proves the theorem.
\end{proof}
==== END The-Partition-Principle-does-not-imply-Choice//sections/quotients.tex ====

==== BEGIN The-Partition-Principle-does-not-imply-Choice//references.bib ====
@article{BanaschewskiMoore1990,
  author = {Banaschewski, Bernhard and Moore, Gregory H.},
  title = {The dual {Cantor--Bernstein} theorem and the partition principle},
  journal = {Notre Dame Journal of Formal Logic},
  volume = {31},
  number = {3},
  year = {1990},
  pages = {375--381},
  doi = {10.1305/ndjfl/1093635502},
  url = {https://doi.org/10.1305/ndjfl/1093635502}
}

@article{daSilva2021,
  author = {da Silva, Samuel G.},
  title = {The Axiom of Choice and the Partition Principle from {Dialectica} Categories},
  journal = {Logic Journal of the IGPL},
  volume = {29},
  number = {5},
  year = {2021},
  pages = {783--797},
  doi = {10.1093/jigpal/jzaa023},
  url = {https://doi.org/10.1093/jigpal/jzaa023}
}

@article{Karagila2026,
  author = {Karagila, Asaf},
  title = {Approaching a {Bristol} model},
  journal = {The Bulletin of Symbolic Logic},
  volume = {32},
  number = {1},
  year = {2026},
  pages = {1--46},
  doi = {10.1017/bsl.2025.10126},
  url = {https://doi.org/10.1017/bsl.2025.10126}
}

@article{RyanSmith2025,
  author = {Ryan-Smith, Calliope},
  title = {Local reflections of choice},
  journal = {Acta Mathematica Hungarica},
  volume = {176},
  number = {1},
  year = {2025},
  pages = {244--257},
  doi = {10.1007/s10474-025-01533-3},
  url = {https://doi.org/10.1007/s10474-025-01533-3}
}

@misc{HolySchilhan2025,
  author = {Holy, Peter and Schilhan, Jonathan},
  title = {The Ordering Principle and Higher Dependent Choice},
  year = {2025},
  eprint = {2510.14821v2},
  howpublished = {\href{https://arxiv.org/abs/2510.14821v2}{arXiv:2510.14821v2}},
  archivePrefix = {arXiv},
  primaryClass = {math.LO},
  note = {Version 2, 17 October 2025},
  url = {https://arxiv.org/abs/2510.14821v2}
}

@misc{BlassKulshreshtha2026,
  author = {Blass, Andreas and Kulshreshtha, Dhruv},
  title = {Cardinal Well-foundedness and Choice},
  year = {2026},
  eprint = {2310.09643v3},
  howpublished = {\href{https://arxiv.org/abs/2310.09643v3}{arXiv:2310.09643v3}},
  archivePrefix = {arXiv},
  primaryClass = {math.LO},
  note = {Version 3, 21 August 2026},
  url = {https://arxiv.org/html/2310.09643v3}
}

@misc{Welch2020,
  author = {Welch, P. D.},
  title = {Axiomatic Set Theory},
  year = {2020},
  howpublished = {\url{https://people.maths.bris.ac.uk/~mapdw/current-axiomatic-set-theory.pdf}},
  note = {Lecture notes, 16 August 2020, line-numbered version},
  url = {https://people.maths.bris.ac.uk/~mapdw/current-axiomatic-set-theory.pdf}
}

@misc{Williams2019,
  author = {Williams, Kameryn J.},
  title = {{Math655} Lecture Notes: Part 2.1, An Introduction to Forcing},
  year = {2019},
  howpublished = {\url{https://juliakw.net/teaching/2019/math655/part2.1.pdf}},
  note = {Lecture notes, 7 March 2019},
  url = {https://juliakw.net/teaching/2019/math655/part2.1.pdf}
}

@misc{KaragilaNotes2026,
  author = {Karagila, Asaf},
  title = {Lecture Notes: Forcing \& Symmetric Extensions},
  year = {2026},
  howpublished = {\url{https://karagila.org/files/Forcing-2023.pdf}},
  note = {Updated 24 August 2026},
  url = {https://karagila.org/files/Forcing-2023.pdf}
}

@book{Jech2003,
  author = {Jech, Thomas},
  title = {Set Theory},
  edition = {Third millennium, revised and expanded},
  series = {Springer Monographs in Mathematics},
  publisher = {Springer-Verlag},
  address = {Berlin},
  year = {2003}
}

@article{Blass1979,
  author = {Blass, Andreas},
  title = {Injectivity, projectivity, and the axiom of choice},
  journal = {Transactions of the American Mathematical Society},
  volume = {255},
  year = {1979},
  pages = {31--59},
  doi = {10.1090/S0002-9947-1979-0542870-6},
  url = {https://doi.org/10.1090/S0002-9947-1979-0542870-6}
}

@misc{Usuba2021,
  author = {Usuba, Toshimichi},
  title = {Geology of symmetric grounds},
  year = {2021},
  eprint = {1912.10246v3},
  howpublished = {\href{https://arxiv.org/abs/1912.10246v3}{arXiv:1912.10246v3}},
  archivePrefix = {arXiv},
  primaryClass = {math.LO},
  note = {Version 3, 15 February 2021},
  url = {https://arxiv.org/abs/1912.10246v3}
}

@misc{GilsonIterationCorrection2026,
  author = {Gilson, Frank},
  title = {A countable-support symmetric iteration separating {PP} from {AC}},
  year = {2026},
  eprint = {2601.01855v8},
  howpublished = {\href{https://arxiv.org/abs/2601.01855v8}{arXiv:2601.01855v8}},
  archivePrefix = {arXiv},
  primaryClass = {math.LO},
  note = {Version 8, 10 September 2026; construction withdrawn in the correction},
  url = {https://arxiv.org/abs/2601.01855v8}
}

@misc{GilsonExternalCorrection2026,
  author = {Gilson, Frank},
  title = {From Internal to External: Classical Models of {ZF + PP + $\neg$AC}},
  year = {2026},
  eprint = {2511.09764v5},
  howpublished = {\href{https://arxiv.org/abs/2511.09764v5}{arXiv:2511.09764v5}},
  archivePrefix = {arXiv},
  primaryClass = {math.LO},
  note = {Version 5, 10 September 2026; model constructions withdrawn},
  url = {https://arxiv.org/abs/2511.09764v5}
}

@misc{GilsonSheafCorrection2026,
  author = {Gilson, Frank},
  title = {Partition Principle without Choice via Symmetric Iterations and Sheaf-Toposes},
  year = {2026},
  eprint = {2511.07675v6},
  howpublished = {\href{https://arxiv.org/abs/2511.07675v6}{arXiv:2511.07675v6}},
  archivePrefix = {arXiv},
  primaryClass = {math.LO},
  note = {Version 6, 10 September 2026; model and preservation claims withdrawn},
  url = {https://arxiv.org/abs/2511.07675v6}
}

@article{Pincus1977,
  author = {Pincus, David},
  title = {Adding dependent choice},
  journal = {Annals of Mathematical Logic},
  volume = {11},
  number = {1},
  year = {1977},
  pages = {105--145},
  doi = {10.1016/0003-4843(77)90011-0},
  url = {https://doi.org/10.1016/0003-4843(77)90011-0}
}

@article{Newman1942,
  author = {Newman, M. H. A.},
  title = {On Theories with a Combinatorial Definition of ``Equivalence''},
  journal = {Annals of Mathematics},
  volume = {43},
  number = {2},
  pages = {223--243},
  year = {1942},
  doi = {10.2307/1968867},
  url = {https://doi.org/10.2307/1968867}
}

@incollection{DershowitzPlaisted2001,
  author = {Dershowitz, Nachum and Plaisted, David A.},
  title = {Rewriting},
  booktitle = {Handbook of Automated Reasoning},
  year = {2001},
  publisher = {Elsevier},
  url = {https://www.cs.tau.ac.il/~nachum/papers/hand-final.pdf},
  note = {\url{https://www.cs.tau.ac.il/~nachum/papers/hand-final.pdf}}
}
==== END The-Partition-Principle-does-not-imply-Choice//references.bib ====