Amsbook + Paracol pagebreak broken with mdframed

Question

I am trying to typeset some code and some commentary side-by-side using paracol and listings with the amsbook document class. It mostly works but I encounter a bug, when there is a pagebreak the paragraph immediately following the pagebreak is "flush bottom". For example:

Before the page break, the left column starts vertically aligned with the right column, but after the page break this is no longer true.

If I remove the mdframed background from the listings environment, things work as expected:

(It's a little harder to discern without the vertical lines separating the "chunks" in the right column, but it's true.)

This only is a problem with the amsbook document class, at least in my experiments with comparing the output to book, article, and amsart. I honestly do not understand what amsbook is doing differently which breaks things.

It does not seem to be related to syntax highlighting or color usage, or font encoding.

The minimal working example to reproduce this, although length (sorry):

\documentclass[leqno,oneside]{amsbook}
\usepackage[inner=6pc,outer=6pc,bottom=6pc,top=5pc,headheight=13.6pt]{geometry}
\usepackage{listings}
\usepackage{mdframed}

\mdfsetup{skipabove=\medskipamount,
  outermargin=0pt,
  innermargin=0pt,
  leftmargin=0pt,
  rightmargin=0pt,
  innerleftmargin=0.25em,
  innerrightmargin=0pt,
  rightline=false,
  leftline=false,
  frametitlerule=false,
  innertopmargin=0pt,
  innerbottommargin=0pt,
  splittopskip=\topsep
}
\lstset{%
  basicstyle=\ttfamily,
  language=Mizar,
}
\lstnewenvironment{mizar}%
                  {\lstset{language=Mizar,
                      basicstyle=\ttfamily\small,
                      upquote=true}\mdframed[usetwoside=false]}%
                  {\endmdframed}

\usepackage{paracol}

\begin{document}

\chapter{Foundations}
\section{Tarski Grothendieck Set Theory}

\begin{paracol}{2}
For simplicity we adopt the following convention: $x$, $y$,
$z$, $u$ will denote objects of any type; $N$, $M$, $X$, $Y$, $Z$
will denote objects of the type set.
  
Next we will state two axioms:
\begin{equation}
x \mbox{ is } \textrm{set},
\end{equation}
\begin{equation}
(\mbox{ for } x\mbox{ holds } x\in X\mbox{ iff } x\in Y)\mbox{ implies } X=Y.
\end{equation}

\switchcolumn

\begin{mizar}
 reserve x,y,z,u for object;
 reserve N,M,X,Y,Z for set;

:: Everything is a set
theorem :: TARSKI:1
  for x being object holds x is set;

:: Extensionality
theorem :: TARSKI:2 
  (for x being object
   holds x in X iff x in Y)
  implies X = Y;
\end{mizar}

\switchcolumn*

We now introduce two functors. Let us consider $y$. The functor
\[ \{\,y\,\} \]
with values of the type set, is defined by
\[ x\in\mbox{ it } \mbox{ iff } x=y.\]
Let us consider $z$. The functor
\[ \{\,y,z\,\} \]
with values of the type set, is defined by
\[ x\in\mbox{ it } \mbox{ iff } x=y \mbox{ or } x=z.\]
The following axioms hold:
\begin{equation}
X=\{y\} \mbox{ iff }\ \mbox{ for } x \mbox{ holds } x\in X \mbox{ iff } x=y,
\end{equation}
\begin{multline}
X=\{y,z\} \mbox{ iff }\ \mbox{ for } x\mbox{ holds } x\in X\mbox{ iff }\\
%\textbf{iff}~
x=y\mbox{ or } x=z.
\end{multline}

\switchcolumn

\begin{mizar}
definition
  let y be object;
  func { y } -> set means
:: TARSKI:def 1
    for x being object
    holds x in it iff x = y;

  let z be object;
  func { y, z } -> set means
:: TARSKI:def 2
    x in it iff x = y or x = z;
  commutativity;
end;
\end{mizar}

\switchcolumn*


Let us consider $X$, $Y$. The predicate
\[ X\subset Y\quad\mbox{is defined by}\quad x\in
X\mbox{ implies } x\in Y.\]
\switchcolumn
\begin{mizar}
definition 
  let X,Y;
  pred X c= Y
  means :: TARSKI:def 3
  for x being object 
  holds x in X implies x in Y;
  reflexivity;
end;
\end{mizar}

\switchcolumn*
Let us consider $X$. The functor
\[\bigcup X,\]
with values of the type set, is defined by
\[x\in\mbox{ it }\ \mbox{ iff }\ \mbox{ ex } Y\mbox{ st } x\in Y\mathrel{\&} Y\in X.\] 
Then we get
\begin{multline}
X=\bigcup Y\mbox{ iff }\ \mbox{ for } x\mbox{ holds } x\in
X\mbox{ iff }\\
\mbox{ ex } Z\mbox{ st } x\in Z\mathrel{\&} Z\in Y,
\end{multline}
\begin{equation}
X=\mbox{ bool } Y\mbox{ iff }\ \mbox{ for } Z\mbox{ holds } 
Z\in X \mbox{ iff } Z\subset Y.
\end{equation}

\switchcolumn

\begin{mizar}
definition 
  let X;
  func union X -> set means
:: TARSKI:def 4
    x in it iff ex Y st x in Y & Y in X;
end;
\end{mizar}

\switchcolumn*


The regularity axiom claims that
\begin{multline}
x\in X\mbox{ implies }\ \mbox{ ex } Y\mbox{ st } Y\in X\mathrel{\&}\\
\neg\ \mbox{ ex } x\mbox{ st } x\in X\mathrel{\&} x\in Y.
\end{multline}

\switchcolumn

\begin{mizar}
:: Regularity
theorem :: TARSKI:3
  x in X implies
   ex Y st Y in X &
     not ex x st x in X & x in Y;
\end{mizar}

\begin{mizar}
definition let x, X be set;
  redefine pred x in X;
  asymmetry;
end;
\end{mizar}

\switchcolumn*


The scheme \textit{Fraenkel} deals with a constant $\mathcal{A}$ that
has the type set and a binary predicate $\mathcal{P}$ and states that
the following holds:
\begin{multline*}
  \mbox{ ex } X\mbox{ st }\ \mbox{ for } x\mbox{ holds } \\
  x\in X\mbox{ iff }
\mbox{ ex } y\mbox{ st } y\in\mathcal{A}\mathrel{\&}\mathcal{P}[y,x]
\end{multline*}
provided the parameters satisfy the following extra condition:
\begin{itemize}
\item $\mbox{ for }$ $x$, $y$, $z$ $\mbox{ st }$ 
  $\mathcal{P}[x,y]\mathrel{\&}\mathcal{P}[x,z]$ $\mbox{ holds }$  $y=z$.
\end{itemize}

\switchcolumn

\begin{mizar}
scheme :: TARSKI:sch 1
 Replacement{ A() -> set,
              P[object,object] }:
 ex X
 st for x being object 
    holds x in X iff
          ex y being object 
          st y in A() & P[y,x]
provided
 for x,y,z being object 
 st P[x,y] & P[x,z]
 holds y = z;
\end{mizar}

\switchcolumn*


Let us consider $x$, $y$. The functor
\[\langle x,y\rangle,\]
is defined by
\[\mbox{ it } = \{\,\{x,y\,\},\{\,x\,\}\,\}.\]
According to the definition
\begin{equation}
\langle x,y\rangle = \{\,\{x,y\,\},\{\,x\,\}\,\}.
\end{equation}

\switchcolumn
\begin{mizar}
definition
  let x,y be object;
  func [x,y] -> object equals
:: TARSKI:def 5
    { { x,y }, { x } };
end;
\end{mizar}


\switchcolumn*

Let us consider $X$, $Y$. The predicate
\[X\approx Y\]
is defined by
\begin{multline*}
\mbox{ ex } Z\mbox{ st }\!\! (\mbox{ for } x\mbox{ st } x\in X\mbox{ ex } 
y\mbox{ st } y\in Y\mathrel{\&}\langle x,y\rangle\in Z)\mathrel{\&}\\
(\mbox{ for } x\mbox{ st } x\in X\mbox{ ex } 
y\mbox{ st } y\in Y\mathrel{\&}\langle x,y\rangle\in Z)\mathrel{\&}\\
\mbox{ for } x,y,z,u\mbox{ st } \langle x,y\rangle\in Z\mathrel{\&}\langle z,u\rangle\in Z\\
\mbox{ holds } x=z\mbox{ iff } y=u.
\end{multline*}

\switchcolumn

\begin{mizar}
definition let X,Y;
  pred X,Y are_equipotent means
:: TARSKI:def 6
  ex Z st
  (for x st x in X
   ex y st y in Y & [x,y] in Z) &
  (for y st y in Y
   ex x st x in X & [x,y] in Z) &
  for x,y,z,u st [x,y] in Z & [z,u] in Z
  holds x = z iff y = u;
end;
\end{mizar}

\switchcolumn*
The Tarski's axiom A claims that
\begin{multline}
\mbox{ ex }  M \mbox{ st } N\in M\mathrel{\&}\\
(\mbox{ for } X,Y \mbox{ holds }  X\in M\mathrel{\&}
Y\subset X \mbox{ implies } Y\in M)\mathrel{\&}\\
(\mbox{ for } X \mbox{ holds }  X\in M
 \mbox{ implies } \mbox{ bool } X\in M)\mathrel{\&}\\
(\mbox{ for } X \mbox{ holds }  X\subset M \mbox{ implies } 
X\approx M \mbox{ or } X\in M).
\end{multline}

\switchcolumn\nopagebreak

\begin{mizar}
theorem :: TARSKI_A:1
 ex M st N in M &
   (for X,Y holds X in M & Y c= X
    implies Y in M) &
   (for X st X in M
    ex Z st Z in M &
            for Y st Y c= X
            holds Y in Z) &
   (for X holds X c= M 
    implies X,M are_equipotent
            or X in M);
\end{mizar}

\end{paracol}
\end{document}

Using PDFlatex (version 3.141592653-2.6-1.40.22 from TeX live 2022) this produces a 3-page PDF which has the misaligned left column immediately after both page breaks.

If I add, e.g., \ensurevspace{5cm} to each \switchcolumn*, then the situation remains unchanged as far as this bizarre bug is concerned.

(And my actual TeX code looks much cleaner than this, with semantic macros, etc., but this is the smallest self-contained example I could create.)

Answer 1

Barbara Beeton had a profound insight, which made me examine the code more closely for amsbook. I discovered there is this macro which is invoked whenever a chapter starts, and it changes the topskip to be 7.5pc globally...which is, well, not the intended goal of that particular line of code. The fix is to add the following lines:

\makeatletter
\def\@makechapterhead#1{\vspace*{7.5pc}\relax%
  \begingroup
  \fontsize{\@xivpt}{18}\bfseries\centering
    \ifnum\c@secnumdepth>\m@ne
      \leavevmode \hskip-\leftskip
      \rlap{\vbox to\z@{\vss
          \centerline{\normalsize\mdseries
              \uppercase\@xp{\chaptername}\enspace\thechapter}
          \vskip 3pc}}\hskip\leftskip\fi
     #1\par \endgroup
  \skip@34\p@ \advance\skip@-\normalbaselineskip
  \vskip\skip@ }
\def\@makeschapterhead#1{\vspace*{7.5pc}\relax
  \begingroup
  \fontsize{\@xivpt}{18}\bfseries\centering
  #1\par \endgroup
  \skip@34\p@ \advance\skip@-\normalbaselineskip
  \vskip\skip@ }
\makeatother

This only changes the first line, changing \global\topskip7.5pc to \vspaces*{7.5pc}. Apparently that was the goal, according to the documentation, and no one really bothered to check if the code actually did that.