\documentclass[11pt]{article}

% The release build loads these maps explicitly so that it does not depend on
% a machine-generated updmap configuration.
\pdfmapfile{=lm.map}
\pdfmapfile{+symbols.map}
\pdfmapfile{+euler.map}

\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage{microtype}
\usepackage[margin=1.08in]{geometry}
\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage{booktabs}
\usepackage{enumitem}
\usepackage{xcolor}
\usepackage[hidelinks]{hyperref}
\hypersetup{
  pdftitle={An Intrinsic Formula for the Ray--West Correction Term},
  pdfauthor={Donald D. Poindexter, Jr.},
  pdfsubject={Permutation patterns; intrinsic formula for the Ray--West correction term; DOI 10.5281/zenodo.21857882},
  pdfkeywords={permutation patterns, permutation statistics, enumerative combinatorics, pattern containment, Ray--West correction term, near-diagonal containment, Wilf equivalence, deletion classes, strong intervals, layered permutations}
}
\pdfinfo{/DOI (10.5281/zenodo.21857882)}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{remark}[theorem]{Remark}

\newcommand{\Ssym}{\mathfrak S}
\newcommand{\std}{\operatorname{std}}
\newcommand{\Av}{\operatorname{Av}}
\newcommand{\supp}{\operatorname{supp}}
\newcommand{\del}{\partial}
\newcommand{\one}{\mathbf 1}

\title{\textbf{An Intrinsic Formula for the Ray--West Correction Term}\\
\large Preliminary technical report, version 0.1}
\author{Donald D. Poindexter, Jr.\\
\normalsize Stanford University}
\date{August 9, 2026\\[4pt]
\normalsize\href{https://doi.org/10.5281/zenodo.21857882}{doi:10.5281/zenodo.21857882}}

\begin{document}
\maketitle

\begin{abstract}
For a nonempty permutation $\beta\in\Ssym_m$, let $g_2(\beta)$ denote the number of
distinct permutations of length $m+2$ containing $\beta$.  Ray and West
showed that
\[
 g_2(\beta)=\frac{m^4+2m^3+m^2+4m+4-2j(\beta)}2,
 \qquad 0\le j(\beta)\le m-1 \quad (m\ge1),
\]
but their correction term was not expressed as a statistic of $\beta$.
This was posed explicitly as Problem~3.7 by Vatter.  We give a polynomial-time,
$\beta$-internal formula.  The statistic is the number of licensed gaps of
$\beta$, plus the number of anchor-free two-deletion classes containing a
collision whose canonical alignment support is a permutation interval.  We
also derive the Ray--West bound internally and show that equality holds
exactly for layered or reverse-layered permutations.  The proof is
combinatorial.  Exact computation is used only for independent corroboration;
the accompanying replay package checks the formula on bounded ranges and
contains the full proof supplement.
\end{abstract}

\noindent\textbf{Keywords.} permutation patterns; Ray--West statistic;
near-diagonal containment; Wilf equivalence; deletion classes; strong
intervals.

\section{Introduction}

Write $\sigma\le\pi$ when $\pi$ contains a subsequence order-isomorphic to
$\sigma$.  For a fixed $\beta\in\Ssym_m$, let
\[
 g_k(\beta)=\bigl|\{\pi\in\Ssym_{m+k}:\beta\le\pi\}\bigr|.
\]
The word \emph{distinct} is important: $g_k$ counts upper objects, not
embeddings.  Ray and West~\cite{raywest2003} proved the displayed formula in
the abstract and, for $m\ge1$, established $0\le j(\beta)\le m-1$.  Vatter asked for an
expression for $j$ in terms of statistics of $\beta$~\cite[Problem~3.7]{vatter2026};
the question was raised at Permutation Patterns 2007 and recorded in its
published problem session~\cite{vatter2010}.

Our answer uses only intervals and collisions in the two-deletion shadow of
$\beta$.  In particular, its definition neither constructs a permutation
longer than $\beta$ nor counts insertion histories.  Upper-shadow fibres enter
only in the proof.

\begin{theorem}[Main theorem]\label{thm:main}
For every $\beta\in\Ssym_m$ with $m\ge1$,
\[
 2g_2(\beta)+2\bigl(L(\beta)+R(\beta)\bigr)
   =m^4+2m^3+m^2+4m+4,
\]
where the intrinsic statistics $L$ and $R$ are defined in
Section~\ref{sec:statistic}.  Consequently
\[
 j(\beta)=L(\beta)+R(\beta).
\]
Moreover, for $m\ge1$,
\[
 0\le L(\beta)+R(\beta)\le m-1.
\]
For $m\ge2$, equality holds if and only if $\beta$ is layered or
reverse-layered.
\end{theorem}

For the empty permutation we separately set $L(\varnothing)=R(\varnothing)=0$;
the main identity then remains valid with $g_2(\varnothing)=2$, without
invoking Ray--West's range statement at $m=0$.

The proof has three components.  First, a fibre-forest identity rewrites
Ray--West's correction as a count of boundaries between overlap components.
Second, one classwise theorem identifies the defect of a two-deletion class:
licensed gaps account for its rectangular boundaries, while an active
anchor-free class accounts for one nonrectangular boundary.  Third, a
strong-interval-tree charging theorem bounds the resulting intrinsic objects
and determines equality.  Proposition~\ref{prop:cleanup} shows that the
side conditions used to orient the boundary geometry are automatic, leaving
the formula \(J=L+R\).

\paragraph{Scope.}
This preliminary technical report is intended to establish a citable,
auditable proof claim.  Several local lemmas are lengthy; their complete
versions are supplied in the accompanying proof supplement and are summarized
in the appendices.  The PDF is a theorem-driven roadmap; the PDF and integral
companion supplement together constitute the claimed proof.  No
machine-checked formalization is included or claimed, and the result is not
described as fully machine-checked.

\paragraph{Integral proof supplement and reproducibility archive.}
The complete companion proof supplement, which is part of the claimed proof,
and the independent exact-computation replay are permanently available in
the original Zenodo release at
\url{https://doi.org/10.5281/zenodo.21857882}.  Download the proof-and-replay
archive from that record and consult its \texttt{proof\_supplement/} directory.

\section{The intrinsic statistic}\label{sec:statistic}

Write $[m]=\{0,\ldots,m-1\}$; positions are zero based.  For
$D\in\binom{[m]}2$, let
\[
 \del_D\beta=\std(\beta\setminus D).
\]
Partition the deletion pairs into classes
\[
 \mathcal C_\tau=\{D:\del_D\beta=\tau\}.
\]

\subsection{Licensed gaps}

A consecutive set of positions is a \emph{permutation interval} if its set of
values is consecutive.  Let $\delta_r$ and $\iota_r$ denote the decreasing and
increasing permutations of length $r$.

\begin{definition}
The gap $i$ between positions $i$ and $i+1$ is \emph{licensed} if some
permutation interval $[r,s]$ crossing the gap induces either
\[
 \delta_p\oplus\delta_q
 \quad\text{or}\quad
 \iota_p\ominus\iota_q,
 \qquad p=i-r+1,\quad q=s-i.
\]
Singleton blocks are allowed.  Let $L(\beta)$ be the number of licensed gaps.
For a deletion class $\mathcal C$, let $a_\beta(\mathcal C)$ be the number of
licensed gaps whose adjacent deletion pair $\{i,i+1\}$ lies in $\mathcal C$.
Call $\mathcal C$ \emph{anchored} if $a_\beta(\mathcal C)>0$ and
\emph{anchor-free} otherwise.
\end{definition}

Every licensed gap belongs to one deletion class, so
\begin{equation}\label{eq:Lsum}
 L(\beta)=\sum_{\mathcal C}a_\beta(\mathcal C).
\end{equation}

\subsection{Bi-interval collisions}

Let $D,E$ be distinct pairs in the same deletion class.  List the surviving
positions
\[
 [m]\setminus D=\{x_1<\cdots<x_{m-2}\},\qquad
 [m]\setminus E=\{y_1<\cdots<y_{m-2}\}.
\]
The \emph{canonical survivor alignment} maps $x_k$ to $y_k$.  Its support is
\begin{equation}\label{eq:support}
 S(D,E)=D\cup E\cup\{x_k,y_k:x_k\ne y_k\}.
\end{equation}

\begin{definition}
The pair $\{D,E\}$ is a \emph{bi-interval collision} if $S(D,E)$ is a
consecutive set of positions and $\{\beta_i:i\in S(D,E)\}$ is a consecutive
set of values.  Let $R(\beta)$ be the number of anchor-free deletion classes
that contain a bi-interval collision.
\end{definition}

Thus the answer to Vatter's problem is the particularly short statistic
\begin{equation}\label{eq:Jclean}
 J(\beta)=L(\beta)+R(\beta).
\end{equation}
The two interval requirements are both necessary.  Exhaustive replay from
length zero upward finds the first failures at length four.  Dropping position
intervality changes $1423,2314,3241,4132$, while dropping value intervality
changes $1342,2431,3124,4213$; in every case the true value $J=2$ becomes
$3$ under the mutant definition.

\paragraph{Example.}
For $\beta=2413$, there are no licensed gaps.  The deletion class with core
$12$ contains the bi-interval collision $\{\{0,1\},\{2,3\}\}$, and the class
with core $21$ contains $\{\{0,2\},\{1,3\}\}$.  Hence $J(2413)=2$.

\subsection{Automatic side conditions}

For reference, an \emph{oriented interval shift} is a bi-interval collision
whose deletion pairs are disjoint, whose increasing position pairs are
componentwise comparable, and whose increasing deleted-value pairs are
componentwise comparable.  These conditions are convenient in the boundary
proof but are unnecessary in the statement.

\begin{lemma}[Equal one-deletions]\label{lem:one-delete}
If two distinct positions of a permutation give the same standardized
one-deletion, then every position between them gives that same deletion, and
the intervening entries form a monotone run of consecutive values.
\end{lemma}

\begin{proof}
Let the deleted entries have values $u$ and $v$.  For any surviving value $z$,
its rank after deleting $u$ is
\[
 z-\one_{z>u},
\]
and analogously for $v$.  If the deleted positions are $a<b$, then at output
coordinate $k$, for $a\le k<b$, equality of the two standardized words gives
\[
 \beta_{k+1}-\one_{\beta_{k+1}>u}
 =\beta_k-\one_{\beta_k>v}.
\]
The indicator difference is in $\{-1,0,1\}$ and adjacent entries are
distinct, so $\beta_{k+1}-\beta_k=\pm1$.  If $u<v$, a $-1$ step would require
simultaneously $\beta_{k+1}\le u$ and $\beta_k>v$, which is impossible;
hence every step is $+1$.  The case $u>v$ is symmetric and every step is
$-1$.  Thus the intervening entries form a monotone run of consecutive
values.  Conversely, deleting any entry of such a run merely shifts and
shortens it, preserving all comparisons and giving the same standardized
word.
\end{proof}

\begin{proposition}[Comparability cleanup]\label{prop:cleanup}
Let $\mathcal C$ be anchor-free.  Every bi-interval collision $\{D,E\}$ in
$\mathcal C$ is an oriented interval shift: $D$ and $E$ are disjoint and the
two position pairs and two deleted-value pairs are componentwise comparable.
\end{proposition}

\begin{proof}
Suppose first that $D$ and $E$ share a position $z$.  Delete $z$.  The two
remaining holes give equal one-deletions, so Lemma~\ref{lem:one-delete}
produces a monotone consecutive run.  Let $t$ be the number of old run entries
before $z$, and let $u$ be the one-based rank of $z$ among the support values.
If $u=t+1$, $z$ and a
neighboring run entry are consecutive in both position and value, so their
singleton blocks license the gap.  If $u>t+1$, the singleton $z$ and the run
segment of ranks $t+1,\ldots,u-1$ form an increasing skew cut immediately
after $z$; if $u<t+1$, the symmetric segment forms such a cut immediately
before $z$.  For a decreasing run, value complementation turns these into
decreasing direct cuts.  In every case the adjacent pair at the cut remains
in $\mathcal C$, giving an anchor, a contradiction.

Now assume the pairs are disjoint but not componentwise comparable in
position.  After exchanging their names, their four holes have order
\[
 d_1<e_1<e_2<d_2.
\]
Restrict to the bi-interval support and standardize.  Full support of the
canonical alignment forces $d_1$ and $d_2$ to be the two extreme positions
and $e_2=e_1+1$.  The alignment has two directed paths running outward from
this central gap.  Conjugating the position alignment by the permutation gives
the analogous value alignment.  Between its two sources, the two path colors
occur as $P^rQ^s$ (this follows directly by listing the six relative orders of
the two domain and two range holes).  Consequently the entries abutting the
central gap form either two decreasing consecutive blocks in direct-sum order
or two increasing consecutive blocks in skew-sum order.  Thus the central
pair is a licensed anchor in $\mathcal C$, again a contradiction.

The position pairs are therefore comparable.  Apply the same argument to
$\beta^{-1}$.  Position comparability there is deleted-value comparability
here.  The licensed-anchor transport uses the opposite-corner lemma: in a
licensing interval, the adjacent pair at the position cut and the adjacent
pair at the value cut have the same two-deletion core.  After transposition,
the value-cut corner is therefore an adjacent licensed pair in the original
class.  This again contradicts anchor-freeness, so the deleted-value pairs are
comparable as well.
\end{proof}

In an anchored class, any additional shift bit is absorbed by
$a_\beta(\mathcal C)\ge1$; in an anchor-free class,
Proposition~\ref{prop:cleanup} identifies bi-interval collisions with oriented
interval shifts.  This proves that the reader-facing formula
\eqref{eq:Jclean} is exactly the expanded statistic used in the boundary
proof.

\section{The fibre-defect identity}\label{sec:fibres}

Put $N=m+2$.  For $\rho\in\Ssym_N$, define the producing fibre
\[
 F_\rho=\{X\in\tbinom{[N]}2:\std(\rho\setminus X)=\beta\}.
\]
Join two members of $F_\rho$ when their two-sets intersect.  When the fibre is
nonempty, write $e_\rho=|F_\rho|$ and let $c_\rho$ be its number of overlap
components.

\begin{proposition}[Fibre forest identity]\label{prop:phaseI}
For every $\beta\in\Ssym_m$,
\begin{equation}\label{eq:forest}
 \sum_{\rho:F_\rho\ne\varnothing}(e_\rho-c_\rho)
   =2m(m+1)(m+2).
\end{equation}
\end{proposition}

The proof is an exact split-and-insert count.  Its delicate point is not the
enumeration but the forest assertion inside each one-deletion run.  The full
argument is given in Appendix~\ref{app:phaseI} and in the proof supplement.

There are
\[
 H_m=2\binom{m+2}{2}^{\!2}
\]
two-point insertion histories: choose two positions, two values, and one of
the two bijections.  Histories are precisely pairs $(\rho,X)$ with
$X\in F_\rho$.  Therefore
\begin{equation}\label{eq:histories}
 H_m-g_2(\beta)=\sum_{\rho:F_\rho\ne\varnothing}(e_\rho-1).
\end{equation}
Write
\[
 T(\beta)=\sum_{\rho:F_\rho\ne\varnothing}(c_\rho-1).
\]
Since $e_\rho-1=(e_\rho-c_\rho)+(c_\rho-1)$, substitution of
Proposition~\ref{prop:phaseI} into \eqref{eq:histories} yields
\begin{align}
 g_2(\beta)
 &=H_m-2m(m+1)(m+2)-T(\beta)\\
 &=\frac{m^4+2m^3+m^2+4m+4}{2}-T(\beta).
\end{align}
Thus Ray--West's correction satisfies
\begin{equation}\label{eq:jT}
 j(\beta)=T(\beta).
\end{equation}

\section{Boundary classification}\label{sec:boundary}

Regard the pairs in $F_\rho$ as edges of a ground graph on the physical points
of $\rho$.  Fibre overlap components are precisely the nontrivial connected
components of this graph.  Distinct such components have disjoint position
hulls and disjoint value hulls; the two hull orders either agree or reverse.
Order the components by position hull as $K_1<\cdots<K_{c_\rho}$.  The adjacent pairs
$(K_i,K_{i+1})$ are the \emph{boundary units}; there are $c_\rho-1$.

For a boundary $A<B$, choose $X\in A$ and $Y\in B$.  The pairs are disjoint.
Delete $X$, identify $\rho-X$ with $\beta$, and transport $Y$ into $\beta$.
A shielding argument shows that the resulting two-deletion class is
independent of $X$ and $Y$.  Denote it by $\mathcal C(A,B)$.  If
$b(\mathcal C)$ counts boundaries with label $\mathcal C$, then
\begin{equation}\label{eq:boundarysum}
 T(\beta)=\sum_{\mathcal C}b(\mathcal C).
\end{equation}

The two moving tracks in the canonical identification can be encoded, in
position and value order, by two monotone lattice paths.  Hull separation
rules out an $A,B,A$ component pattern and any third component between
adjacent $A,B$.  Hence there is a unique transition excursion.  It is
\emph{rectangular} when its two words are $A^pB^q$ and $B^qA^p$; otherwise it
is \emph{nonrectangular}.  If either track has size one, the excursion is
necessarily rectangular.  Appendix~\ref{app:words} gives the elementary
two-letter prolongation proof explicitly.

\begin{proposition}[Classwise boundary theorem]\label{prop:classwise}
For every two-deletion class $\mathcal C$:
\begin{enumerate}[label=(\roman*)]
\item rectangular boundaries labelled $\mathcal C$ are in bijection with
      licensed gaps whose adjacent pair lies in $\mathcal C$;
\item if $\mathcal C$ is anchored, it labels no nonrectangular boundary;
\item if $\mathcal C$ is anchor-free, it labels exactly one nonrectangular
      boundary when it contains a bi-interval collision, and none otherwise.
\end{enumerate}
Consequently
\[
 b(\mathcal C)=
 \begin{cases}
 a_\beta(\mathcal C),&a_\beta(\mathcal C)>0,\\
 1,&a_\beta(\mathcal C)=0\text{ and $\mathcal C$ has a bi-interval collision},\\
 0,&\text{otherwise}.
 \end{cases}
\]
\end{proposition}

\begin{proof}[Proof sketch; complete proof in the companion supplement]
A rectangular excursion exposes a position/value cut whose two sides are a
direct sum of decreasing blocks or a skew sum of increasing blocks; this is a
licensed gap.  Conversely, prolonging a licensed gap produces two corner
occurrences.  The central position/value cut forbids every mixed producing
deletion, so those corners lie in distinct adjacent full-fibre components.
The cut and prolongation recover one another, proving (i).

A nonrectangular excursion has a strong simple-root support.  If its class had
a licensed pair, transport through the strong-interval tree would carry an
anchor into that simple support, contradicting simplicity; the terminal
two-point-child case is checked separately.  This gives (ii).

For (iii), start with an anchor-free collision.  By
Proposition~\ref{prop:cleanup} it has the oriented geometry used by the
two-track proof.  Among all supports in the class there is a common minimum
simple support.  On a fixed support the track partition and witness are
unique.  Contracting through same-class linear strips reaches the unique
terminal witness, while restoring the strips adds the same constant fringe
to both coordinate words.  At a maximal support the two endpoint pairs lie
in distinct full-fibre components.  A third component would force either a
nested same-class witness on the terminal support or a strictly larger
same-class support, both contradictions.  Thus the canonical fibre has
exactly the two endpoint components and produces one adjacent boundary.
Finally, the literal inverse reads the local position and value words from any
nonrectangular boundary and reconstructs the same support, ambient
permutation, and ordered component pair.  This proves existence and
uniqueness.  Appendix~\ref{app:inverse} records the precise lemma chain and
the proof supplement contains the complete local arguments.
\end{proof}

Combining \eqref{eq:boundarysum}, Proposition~\ref{prop:classwise}, and
\eqref{eq:Lsum} gives
\[
 T(\beta)=L(\beta)+R(\beta).
\]
Together with \eqref{eq:jT}, this proves the identity in
Theorem~\ref{thm:main}.

\section{Range and extremizers}\label{sec:range}

Permutation intervals that are strong form a laminar rooted tree.  If an
internal node $N$ has $k_N$ maximal proper strong children, its quotient is
increasing, decreasing, or simple; a simple quotient has $k_N\ge4$.  Every
position gap has a unique owner, namely the lowest strong node whose two
consecutive children contain its endpoints.  Hence
\begin{equation}\label{eq:budget}
 \sum_{N\text{ internal}}(k_N-1)=m-1.
\end{equation}

\begin{proposition}[Strong-tree charging]\label{prop:charging}
Licensed gaps are owned by linear nodes.  Every anchor-free class containing
a bi-interval collision has a minimum support equal to a simple strong node,
and at most two such classes are assigned to any one simple node.
\end{proposition}

\begin{proof}[Proof sketch]
The complete four-case analysis is in the companion supplement.
A licensing interval crossing two children of a simple node would induce a
nontrivial sum or skew cut in its simple quotient.  Thus licensed gaps are
owned by linear nodes.

Take a minimum collision support in an anchor-free class.  At a direct or skew
cut, the four possible distributions of its endpoint deletions either expose
a licensed pair or produce a strictly smaller same-class collision.  The
common-hole boundary case reduces to Lemma~\ref{lem:one-delete}.  Therefore a
minimum support cannot straddle a linear node and its least strong container
is simple; minimality makes the support that whole node.

Orient a full-support collision from left to right.  Full support gives exactly
two corner possibilities:
\[
\begin{array}{c|cc}
 &D&E\\ \hline
+&\{\text{first position},\min\}&\{\text{last position},\max\}\\
-&\{\text{first position},\max\}&\{\text{last position},\min\}.
\end{array}
\]
At a simple quotient these four extreme points occupy four distinct quotient
children: identifying a position extreme with a value extreme would leave a
proper prefix or suffix quotient interval.  Each displayed orientation
therefore determines at most one deletion core, so a simple node receives at
most two residual classes.
\end{proof}

A linear node uses at most its $k_N-1$ owned-gap slots.  A simple node uses at
most two slots, and $2\le k_N-1$ because $k_N\ge4$.  Summing against
\eqref{eq:budget} proves $J(\beta)\le m-1$.

If equality holds, no simple node can occur: at a simple node the residual
load is at most $2<k_N-1$, whereas every linear-node gap must be licensed.  At an
increasing node, licensing every child boundary forces every child to be
decreasing; otherwise a proper licensing suffix would split a maximal
sum-indecomposable child.  Dually, every child of a decreasing node is
increasing.  Thus $\beta$ is a direct sum of decreasing blocks (layered) or a
skew sum of increasing blocks (reverse-layered).  Conversely, every gap of a
layered permutation is licensed, and value complementation gives the
reverse-layered case.  This proves the equality characterization.

The usual avoidance descriptions are
\[
 \text{layered}=\Av(231,312),\qquad
 \text{reverse-layered}=\Av(213,132).
\]

\section{Consequences and computation}

The proof yields several immediate corollaries.

\begin{corollary}
For a simple permutation $\beta$, $j(\beta)\le2$.  The bound is attained by
$2413$ and $3142$.
\end{corollary}

\begin{proof}
For $m<4$ the assertion is checked directly.  For a simple permutation of
length $m\ge4$, the root of the strong-interval tree is simple.  It owns no
licensed gap and, by Proposition~\ref{prop:charging}, receives at most the two
residual corner orientations.  The two length-four examples have value two by
the explicit calculation in Section~\ref{sec:statistic} and its symmetry
image.
\end{proof}

\begin{corollary}
The statistic $j$ is invariant under reversal, complementation, and inversion.
For $m\ge2$, exactly $2^m-2$ permutations in $\Ssym_m$ have $j=m-1$.
\end{corollary}

\begin{proof}
Plot symmetries carry equal-deletion classes and bi-interval supports to their
images.  Reversal and complementation visibly carry licensing intervals to
licensing intervals.  For inversion, the opposite-corner lemma used in
Proposition~\ref{prop:cleanup} supplies the correctly adjacent image anchor;
the detailed transport is in the companion supplement.  Thus $J$ is
dihedrally invariant.  Layered permutations are indexed by the $2^{m-1}$
compositions of $m$, as are reverse-layered permutations.  Their intersection
consists of the increasing and decreasing permutations, so their union has
$2^{m-1}+2^{m-1}-2=2^m-2$ elements.
\end{proof}

The accompanying clean evaluator uses $O(m^2)$ internal deletions and tests
pairs only within equal-core classes.  Its straightforward worst-case running
time is $O(m^5)$ and it never allocates a permutation longer than $m$.

Exact computations are corroboration rather than proof.  The public replay
compares the intrinsic route with a semantically independent direct $g_2$
route on a frozen exhaustive range; compares the clean and expanded
statistics through length eight; checks range, symmetry, and extremizers; and
mutation-tests both interval requirements.  It also independently enumerates
the binary prolongation theorem through target length thirteen, checking the
coordinate sets, path-type uniqueness, and constant-fringe commutation.  A
separate exact normal-path audit checks all 31,200 pairs with individual track
counts at most fifteen: 4,691 pairs have only rectangular excursions, 2,744
have multiple raw excursions, and none has more than one nonrectangular
excursion.
A separate slow hostile replay exhausts all permutations of length nine.  It
checks 7,979,820 within-class deletion-pair comparisons, including 6,577,712
anchor-free comparisons, with no cleanup, clean/expanded-formula, range, or
extremizer failure; its maximizer set is exactly the 510 layered or
reverse-layered permutations.

\section{Discussion and formalization status}

Formula \eqref{eq:Jclean} identifies the codimension-two containment term as a
combination of local interval cuts and lower-shadow collisions.  The
strong-interval-tree proof explains the
otherwise opaque upper bound $m-1$: it is the total budget
$\sum_N(k_N-1)$.

No machine-checked formalization accompanies this release, and none is used
as evidence.  If a formalization is undertaken, the natural order is the
equal-one-deletion lemma and cleanup proposition, the strong-tree charging
theorem and equality case, and finally the larger fibre and boundary layers.

\section*{Acknowledgments and disclosure}

This work was carried out as part of the conjecture-prover and
autoformalization project led by the author for Stanford's Lean Club.  OpenAI's
GPT-5.6 Sol Ultra was used extensively for conjecture generation, exact computation,
proof development, adversarial repair, and preparation of the initial proof
artifacts.  Codex assisted with independent reconstruction, simplification,
and preparation of this preliminary technical report.  The author directed the project,
selected the claims for release, and takes responsibility for the manuscript.
Automated audits and exact replay are not substitutes for external
peer review.  Stanford University and Stanford Lean Club do not endorse the
mathematical claims by virtue of the affiliation or project context.
This report is released under the Creative Commons Attribution 4.0
International license.

\appendix

\section{The fibre forest theorem}\label{app:phaseI}

We record the points needed to make Proposition~\ref{prop:phaseI} uniform in
$m$.  Fix an elementary split of a producing occurrence.  The producing
positions for a fixed one-deletion form the entire interval between any two of
them, by Lemma~\ref{lem:one-delete}.  In the associated grid of possible
second insertions, accept the non-strict-frontier cells and contract each
one-deletion run.  First-exit induction---including the case where the first
point is already the first element of its run---shows that every accepted
edge joins the contracted path without closing a cycle.  Conversely every
non-strict-frontier cell is reached, so the accepted graph is a spanning
forest of each overlap component.  Strict-frontier cells are rejected.

Index a rejected cell by its first strict exit and the elementary edge crossed
there.  The first-exit index is in range, and two rejected cells cannot have
the same index: reversing the split at the first differing grid coordinate
recovers the cell.  Thus the rejected cells are counted without collision.
The elementary-edge enumeration gives $2m(m+2)^2$ total edges.  For each of
the two split orientations and each split position $i=1,\ldots,m$, exactly
$3+2(m-i)$ cells are rejected.  Hence the number of rejected edges is
\[
 2\sum_{i=1}^{m}\bigl(3+2(m-i)\bigr)=2m(m+2),
\]
and the accepted forest has
\[
 2m(m+2)^2-2m(m+2)=2m(m+1)(m+2)
\]
edges.  Accepted edges contribute exactly $e_\rho-c_\rho$ in each fibre,
proving \eqref{eq:forest}.  The proof supplement gives the literal grid
notation, frontier inequalities, and inverse indexing map.

\section{Binary-word prolongations}\label{app:words}

We give the word theorem used in the two-track argument, including the
indexing that is easy to obscure in a path picture.  If a word $U$ contains
$a+1$ copies of $A$ and $b+1$ copies of $B$, number the occurrences of each
letter from zero.  Let $T_f(U)$ delete $A_0,B_0$, let $T_\ell(U)$ delete
$A_a,B_b$, and put
\[
 {\cal D}_U(P)=
 \{(i,j):U-\{A_i,B_j\}=P\}.
\]
If $P=p_1\cdots p_{a+b}$, its prefix-count path has vertices
\[
 v_k=\bigl(|p_1\cdots p_k|_A,\ |p_1\cdots p_k|_B\bigr),
 \qquad 0\le k\le a+b.
\]
Thus the path runs from $(0,0)$ to $(a,b)$, exactly the zero-based deletion
index range.

\begin{lemma}[Binary prolongation]\label{lem:prolongation}
Suppose $a,b\ge1$ and
\[
 T_f(U)=T_\ell(U)=P.
\]
Then \({\cal D}_U(P)\) is either the whole rectangle
$\{0,\ldots,a\}\times\{0,\ldots,b\}$ or precisely
$\{v_0,\ldots,v_{a+b}\}$.  The rectangle occurs only for the two block
words.  For every admissible target $P$, its nonblock, path-type
prolongation is unique.
\end{lemma}

\begin{proof}
Assume first that $a\ge b$ and put $d=a-b$.  We claim that the complete
list of $U$ is
\begin{equation}\label{eq:prolong-table}
\begin{aligned}
 F_t&=A^{a+1-t}(BA)^tB^{b+1-t},&&0\le t\le b,\\
 G_t&=B^{b+1-t}(AB)^tA^{a+1-t},&&0\le t\le b,\\
 H_r&=A^r(BA)^{b+1}A^{d-r},&&1\le r\le d.
\end{aligned}
\end{equation}
The last family is empty when $d=0$; if $a<b$, exchange the roles of
$A$ and $B$, and hence also their counts.

Here is a direct necessity proof.  If $U$ starts in $A$, ends in $B$, and
is not a block word, write
\[
 U=A^u B M A B^v,\qquad u,v\ge1,
\]
using the first $B$ and last $A$.  Equality of the two trims, after
cancelling the common outside runs, is
\[
 MAB=ABM.
\]
Since $AB$ is primitive, a word commuting with it is $(AB)^k$.  Directly,
the empty word is the $k=0$ case, a one-letter word cannot commute with
$AB$, and every longer solution begins with $AB$; cancelling it proves the
claim by induction.  Hence
$U=A^u(BA)^{k+1}B^v=F_{k+1}$.  Exchanging the letters gives $G_t$.

If $U$ starts and ends in $A$, write
\[
 U=A^u B M B A^v.
\]
Trim equality becomes $MBA=ABM$.  If $M$ were empty this would say
$BA=AB$, so $M$ is nonempty.  Thus $M=AM'$ and
$M'BA=BAM'$, so $M'=(BA)^k$.  Counting $B$'s gives $k=b-1$, while
counting $A$'s gives $u+v=d+1$.  This is exactly $H_u$.  The start/end
$B$ case is its letter-exchanged version and can occur only when $b>a$.
This proves that \eqref{eq:prolong-table} is exhaustive; direct trimming
proves sufficiency.

For $t\ge1$, the three target families are
\[
\begin{aligned}
 T_f(F_t)&=A^{a+1-t}(BA)^{t-1}B^{b+1-t},\\
 T_f(G_t)&=B^{b+1-t}(AB)^{t-1}A^{a+1-t},\\
 T_f(H_r)&=A^r(BA)^bA^{d-r}.
\end{aligned}
\]
Their first and last letters separate the families, and their initial
constant-run lengths determine $t$ or $r$.  Thus each target has exactly
one nonblock prolongation, including the two-block targets, whose path
prolongations are $F_1$ and $G_1$.

It remains to identify the working coordinates.  For
$F_t=A^R(BA)^tB^S$, where $R=a+1-t$ and $S=b+1-t$, direct deletion gives
\[
\begin{aligned}
{\cal D}_{F_t}(P)
={}&\{(i,0):0\le i\le R\}\\
&{}\cup\{(R+q-1,q),(R+q,q):1\le q\le t-1\}\\
&{}\cup\{(a,j):t\le j\le b\}.
\end{aligned}
\]
These are exactly the prefix-count vertices of
$P=A^R(BA)^{t-1}B^S$.  Scanning a putative deletion equality from left to
right proves the converse: before the first $B$, at each successive $BA$,
and after the last alternating pair, any coordinate off the displayed
list makes the next surviving letter disagree with $P$.  Letter exchange
handles $G_t$.  For $H_r$ the identical scan gives
\[
\begin{aligned}
{\cal D}_{H_r}(P)
={}&\{(i,0):0\le i\le r\}\\
&{}\cup\{(r+q-1,q),(r+q,q):1\le q\le b\}\\
&{}\cup\{(i,b):r+b\le i\le a\},
\end{aligned}
\]
again exactly the prefix-count vertices.  At $t=0$, deleting any $A_i,B_j$
from a block word gives the same block target, yielding the full rectangle.
\end{proof}

The count-one excursion is a separate elementary corollary.  If its
increments are $(r,1)$, every path word has the form
\[
 W_i=A^iBA^{r-i}.
\]
For $i<j$, the two sides of the sole excursion are $BA^{j-i}$ and
$A^{j-i}B$, the opposite sides of a rectangle.  Exchanging $A$ and $B$
handles increments $(1,s)$.  Thus an excursion with either track count one
is rectangular.  The companion supplement proves the remaining
component-labelled bridge statements.

The supplement also proves the exact normal-path statement needed later.
For two distinct normal words with the same letter counts, either every
excursion is rectangular or exactly one excursion is nonrectangular.  The
proof orders the normal words by the displayed $F,H,G$ families and compares
their prefix-height functions.  Consecutive rows replace a factor $(AB)^r$
by $(BA)^r$ and can therefore have several unit-square excursions; any two
nonconsecutive rows have one excursion.  When both track counts are at least
two, that excursion is nonrectangular except for the two block extremes.
This is the corrected statement: the proof never infers that an arbitrary
pair of normal words has only one raw excursion.

Finally, if normal targets satisfy $P=P_0X^q$ or $P=X^qP_0$, their unique
path prolongations satisfy the same identity.  The proof supplement checks
the four word-level endpoint families explicitly, including transitions in
which adding the fringe changes the named $F,H,G$ family.  Thus constant
fringe restoration preserves both the ambient amalgam and its unique
nonrectangular excursion in the anchor-free inverse chain.

\section{The anchor-free inverse chain}\label{app:inverse}

For auditability we list the exact logical order of the residual argument.
The proof supplement proves each item without assuming the classwise count.
\begin{enumerate}
\item An active anchor-free equal-two-deletion class has a common minimum
      simple support contained in every oriented witness support.
\item On a fixed support there is at most one witness, and track partitions
      restrict literally along nested supports.
\item Same-class linear strips contract to the unique terminal witness.
\item Reversing a strip appends the same constant fringe to both coordinate
      words and therefore preserves the ambient boundary.
\item At maximal support the two canonical endpoint pairs lie in different
      full-fibre components.
\item A third component would make the three pairwise four-deletion cores
      equal.  Transporting the middle component then gives either a nested
      same-class terminal witness or a larger same-class support, each
      impossible.  Hence there are exactly two components.
\item From any nonrectangular boundary, track occurrence counts fix every
      outside label.  The local prolongation table then reconstructs the exact
      position word, value word, ambient permutation, and ordered endpoint
      components.  This is inverse to the canonical construction.
\end{enumerate}
Only this seven-step inverse chain is used; no local-confluence claim is
required.  The exact source file for every step is listed in the companion
supplement's \texttt{DEPENDENCY\_MAP.md}.

% Bibliography embedded for a self-contained TeX submission.
\begin{thebibliography}{1}

\bibitem{raywest2003}
Nigel Ray and Julian West.
\newblock Posets of matrices, and permutations with forbidden subsequences.
\newblock {\em Annals of Combinatorics}, 7(1):55--88, 2003.

\bibitem{vatter2010}
Vincent Vatter.
\newblock Problems and conjectures.
\newblock In {\em Permutation Patterns}, volume 376 of {\em London Mathematical
  Society Lecture Note Series}, pages 339--345. Cambridge University Press,
  2010.

\bibitem{vatter2026}
Vincent Vatter.
\newblock An assortment of problems in permutation patterns: Unimodality,
  equivalence, derangements, and sorting, 2026.
\newblock arXiv:2602.16355.

\end{thebibliography}

\end{document}