Paper: split into per-section files, add references.bib, promote generality to §5

Structural refactor of the paper directory. Until now paper.tex was
a single 1228-line file with an inline \begin{thebibliography}; this
change splits sections into individual files and switches the
bibliography to BibTeX.

New layout:

  paper/
    paper.tex            (preamble + \input + \bibliography)
    references.bib       (11 entries, BibTeX)
    sections/
      intro.tex          §1 Introduction
      spec.tex           §2 Specification (incl. architecture figure)
      proof.tex          §3 Proof structure
      integration.tex    §4 Lifting to a min-max proof
                         (input / chain / scope subsections)
      generality.tex     §5 Generality across one-parameter min-max
                         settings (promoted from §4 subsection)
      appendix.tex       Appendix A: end-to-end Lean script

Bibliography:
- Citations migrated from inline \bibitem entries to BibTeX entries
  in references.bib. Style: \bibliographystyle{alpha} (gives
  Author+Year labels like [Pit81], [DLT13], [LZ21]).
- Four new entries cited in §5 (Generality):
  * Chambers-Liokumovich, Invent. Math. 2020 (complete manifolds
    of finite volume)
  * Zhou-Zhu, Invent. Math. 2019 (CMC hypersurfaces)
  * M. Li-X. Zhou, J. Diff. Geom. 2021 (free boundary)
  * De Philippis-De Rosa-Y. Li, arXiv:2409.15232 (anisotropic)

The generality discussion (now §5) explains that the LocalWitness
interface is agnostic to which one-parameter min-max variant
supplies the local replacement lemma: closed minimal hypersurfaces
(DLT 2013), free boundary (Li-Zhou 2021), CMC (Zhou-Zhu 2019),
complete finite-volume (Chambers-Liokumovich 2020), and anisotropic
(De Philippis-De Rosa-Li 2024) all use the same combinatorial step
formalized here, with only the geometric stubs in the end-to-end
Lean script (Appendix A) replaced by the relevant variant's
formalization.

Paper rebuilt at 11 pages, no errors after BibTeX + two LaTeX passes.

Author: Xinze-Li-Moqian

paper/paper.pdf

@@ -0,0 +1,102 @@
+@book{Pit81,
+  author    = {Pitts, J. T.},
+  title     = {Existence and regularity of minimal surfaces on Riemannian manifolds},
+  series    = {Mathematical Notes},
+  volume    = {27},
+  publisher = {Princeton University Press},
+  year      = {1981}
+}
+
+@article{SS81,
+  author  = {Schoen, R. and Simon, L.},
+  title   = {Regularity of stable minimal hypersurfaces},
+  journal = {Comm. Pure Appl. Math.},
+  volume  = {34},
+  number  = {6},
+  pages   = {741--797},
+  year    = {1981}
+}
+
+@article{CDL03,
+  author  = {Colding, T. H. and De Lellis, C.},
+  title   = {The min-max construction of minimal surfaces},
+  journal = {Surv. Differ. Geom.},
+  volume  = {VIII},
+  pages   = {75--107},
+  year    = {2003}
+}
+
+@article{DLT13,
+  author  = {De Lellis, C. and Tasnady, D.},
+  title   = {The existence of embedded minimal hypersurfaces},
+  journal = {J. Differential Geom.},
+  volume  = {95},
+  number  = {3},
+  pages   = {355--388},
+  year    = {2013}
+}
+
+@article{DLR17,
+  author  = {De Lellis, C. and Ramic, J.},
+  title   = {Min-max theory for minimal hypersurfaces with boundary},
+  journal = {Ann. Inst. Fourier},
+  volume  = {68},
+  number  = {5},
+  pages   = {1909--1986},
+  year    = {2018}
+}
+
+@misc{DL12,
+  author = {De Lellis, C.},
+  title  = {Exposition of the combinatorial step in the min-max construction},
+  note   = {Annales de l'Institut Fourier, 2016. Precise article reference to be confirmed against the author's library.},
+  year   = {2016}
+}
+
+@article{MN14,
+  author  = {Marques, F. C. and Neves, A.},
+  title   = {Min-max theory and the Willmore conjecture},
+  journal = {Ann. of Math. (2)},
+  volume  = {179},
+  number  = {2},
+  pages   = {683--782},
+  year    = {2014}
+}
+
+@article{ChL19,
+  author  = {Chambers, G. R. and Liokumovich, Y.},
+  title   = {Existence of minimal hypersurfaces in complete manifolds of finite volume},
+  journal = {Invent. Math.},
+  volume  = {219},
+  number  = {1},
+  pages   = {179--217},
+  year    = {2020},
+  note    = {arXiv:1609.04058}
+}
+
+@article{ZZ19,
+  author  = {Zhou, X. and Zhu, J. J.},
+  title   = {Min-max theory for constant mean curvature hypersurfaces},
+  journal = {Invent. Math.},
+  volume  = {218},
+  number  = {2},
+  pages   = {441--490},
+  year    = {2019}
+}
+
+@article{LZ21,
+  author  = {Li, M. M.-c. and Zhou, X.},
+  title   = {Min-max theory for free boundary minimal hypersurfaces, {I}: regularity theory},
+  journal = {J. Differential Geom.},
+  volume  = {118},
+  number  = {3},
+  pages   = {487--553},
+  year    = {2021}
+}
+
+@misc{DDL24,
+  author       = {De Philippis, G. and De Rosa, A. and Li, Y.},
+  title        = {Existence and regularity of min-max anisotropic minimal hypersurfaces},
+  howpublished = {Preprint, arXiv:2409.15232},
+  year         = {2024}
+}

paper/paper.tex

@@ -0,0 +1,49 @@
+\section{End-to-end Lean script}
+\label{app:lean-script}
+
+The Lean script in Listing~\ref{lst:end-to-end} below realizes
+the chain of \S\ref{sec:integration-chain}. The identifiers
+\texttt{YourGMT.SweepoutType}, \texttt{YourGMT.admissibleClass},
+\texttt{YourGMT.choose\_N}, \texttt{YourGMT.localWitness\_of\_DLT},
+and \texttt{YourGMT.lift\_sweepout} stand for the surrounding
+formalization's geometric machinery; the four
+\texttt{CombArg.*} declarations are those provided by the
+formalization presented in this paper.
+
+The script reads from top to bottom as the three steps of
+\S\ref{sec:integration-chain}: the per-parameter local witness
+is constructed by \texttt{YourGMT.local\-Witness\_of\_DLT}; the
+sup-reducing competitor $(f', S)$ is obtained from
+\texttt{CombArg.exists\_sup\_reduction}; and the geometric
+lift to $\Omega' \in \mathcal{A}$ followed by the inf-sup
+contradiction occupies the closing block.
+
+\begin{lstlisting}[caption={End-to-end script for a min-max
+contradiction.}, label=lst:end-to-end]
+import CombArg
+import YourGMT
+
+theorem minmax_contradiction
+    (O : YourGMT.SweepoutType) (hO : O in YourGMT.admissibleClass)
+    (h_minmax : O.boundaryEnergy.sup = YourGMT.infMinmax) :
+    False := by
+  set f := O.boundaryEnergy
+  set m0 := sSup (Set.range f)
+  obtain <N, hN_pos, hN_window> := YourGMT.choose_N O
+  -- Per-parameter local witness from the local replacement lemma.
+  have witness : forall t : unitInterval, f t >= m0 - 1 / (N : R) ->
+                   LocalWitness unitInterval f t (1 / (4 * (N : R))) :=
+    fun t ht => YourGMT.localWitness_of_DLT O t ht hN_pos
+  -- Combinatorial step (this paper) -> scalar sup reduction.
+  obtain <f', S, _, h_le, h_eq, h_sup> :=
+    CombArg.exists_sup_reduction
+      O.boundaryEnergyContinuous rfl hN_pos witness
+  -- Geometric lift back to a sweepout in admissibleClass.
+  obtain <O', hO', hO'_energy> :=
+    YourGMT.lift_sweepout f' h_le h_eq O hO
+  -- Contradiction with the inf-sup characterization of m0.
+  have h_lt : O'.boundaryEnergy.sup < m0 := by
+    rw [hO'_energy]; linarith [h_sup, hN_window]
+  exact absurd h_lt (YourGMT.le_of_admissible hO' h_minmax)
+\end{lstlisting}
+

paper/references.bib

@@ -0,0 +1,58 @@
+\section{Generality across one-parameter min-max settings}
+\label{sec:integration-generality}
+
+The combinatorial step formalized here is not specific to the
+closed-minimal-hypersurface setting of~\cite{DLT13}. The
+$1$-parameter Almgren--Pitts pattern --- a continuous family of
+sweepouts indexed by $t \in [0,1]$, a scalar energy $f(t)$
+attached to each sweepout, the inf-sup level
+$m_0 = \inf_{\mathcal{A}} \sup f$ over an admissible class
+$\mathcal{A}$, a local replacement lemma producing a
+quantitative saving on a neighborhood of each near-critical
+$t$, and a combinatorial step combining these local
+replacements into a competitor strictly below $m_0$ --- recurs
+in several geometric variants beyond the original. We mention
+four:
+
+\begin{itemize}
+\item \emph{Free boundary minimal hypersurfaces}~\cite{LZ21}:
+  the sweepout is by free-boundary regions in a manifold with
+  boundary, and the local replacement lemma uses level sets of
+  the distance function to the hypersurface in place of the
+  exponential-map construction of~\cite{DLT13}. The energy is
+  again the boundary $\mathcal{H}^n$-area.
+\item \emph{Constant mean curvature
+  hypersurfaces}~\cite{ZZ19}: the energy is the
+  prescribed-mean-curvature functional
+  $f_\Omega = \mathcal{H}^n(\partial \Omega) - c \cdot
+  \mathrm{vol}(\Omega)$, and the local replacement lemma is
+  adapted to produce a quantitative saving in this functional.
+\item \emph{Complete manifolds of finite
+  volume}~\cite{ChL19}: the sweepout is by hypersurfaces of
+  bounded volume in a complete non-compact manifold; the
+  substantive geometric input is the disjointing lemma stating
+  that any such sweepout can be made by mutually disjoint
+  hypersurfaces of nearly the same volume.
+\item \emph{Anisotropic min-max}~\cite{DDL24}: the area
+  $\mathcal{H}^n(\partial \Omega)$ is replaced by an elliptic
+  integrand $F(\partial \Omega)$; the local replacement lemma
+  carries the anisotropic structure but produces an analogous
+  quantitative saving.
+\end{itemize}
+
+In each case the local replacement lemma differs substantively
+from~\cite{DLT13}'s, but the subsequent combinatorial step ---
+the interval refinement, the two-fold overlap invariant, and
+the scalar bookkeeping that turns the resulting cover into a
+sup-reducing competitor --- is the same. The
+\texttt{LocalWitness} structure of \S\ref{sec:integration-input}
+is agnostic to the geometric origin of its four data fields,
+specifying only an open neighborhood, a continuous scalar
+energy, and the quantitative saving inequality. Any of the
+local replacement lemmas above can therefore feed the present
+formalization to produce a sup-reducing competitor for the
+corresponding inf-sup level, with the script of
+Appendix~\ref{app:lean-script} carrying over verbatim and only
+the geometric stubs (\texttt{YourGMT.*}) replaced by the
+relevant variant's geometric formalization.
+

paper/sections/appendix.tex

@@ -0,0 +1,120 @@
+\section{Lifting to a min-max proof}
+\label{sec:integration}
+
+We indicate how the formalization developed in
+\S\S\ref{sec:spec}--\ref{sec:proof} fits into a complete
+formalization of an Almgren--Pitts min-max construction.
+Suppose the surrounding geometric and admissibility infrastructure
+has been set up in Lean: an admissible class $\mathcal{A}$ of
+sweepouts, the inf-sup characterization
+$m_0 = \inf_{\Omega \in \mathcal{A}} \sup f_\Omega$, the local
+replacement construction~\cite[Lemma~3.1]{DLT13}, and the
+Hausdorff measure of boundary surfaces. The four objects
+introduced in \S\ref{sec:spec} ---
+\texttt{LocalWitness} (Definition~\ref{def:witness}),
+\lean{exists\_refinement}{Refinement/Assembly.lean},
+\lean{exists\_sup\_reduction\_of\_cover}{Core.lean}, and the
+chained \lean{exists\_sup\_reduction}{SupReduction.lean} ---
+carry no geometric content; they stand for, respectively, the
+abstract local-reducer data, \cite{DLT13}~\S3.2 Step~1
+(the interval refinement to a finite cover with two-fold
+overlap), \cite{DLT13}~\S3.2 Step~2 (the scalar bookkeeping
+over the cover), and the chained $1$-parameter conclusion. The
+same four declarations apply in the abstract and the
+instantiated forms; what changes between them is only the
+data passed in.
+
+\subsection{The geometric input:
+\texorpdfstring{\texttt{LocalWitness} from the local replacement lemma}{LocalWitness from the local replacement lemma}}
+\label{sec:integration-input}
+
+The \texttt{LocalWitness} structure was chosen so that its
+fields match the data the local replacement
+lemma~\cite[Lemma~3.1]{DLT13} produces. Fix a sweepout
+$\Omega \in \mathcal{A}$ realizing $m_0 = \sup f_\Omega$ and an
+integer $N \ge 1$. At every parameter $t \in [0,1]$ with
+$f_\Omega(t) \ge m_0 - 1/N$, the replacement lemma supplies an
+open interval $(a_t, b_t) \subseteq [0,1]$ around $t$ on which
+a local replacement saves boundary energy. Recording the
+interval as the \texttt{neighborhood} field, the boundary
+energy of the replaced sweepout
+\[
+  s \;\longmapsto\; \mathcal{H}^n(\partial \widetilde{\Omega}_s),
+  \qquad
+  \widetilde{\Omega}_s := \text{$\Omega$ with the local
+  replacement inserted at parameter $s$},
+\]
+as the \texttt{replacementEnergy} field, its continuity in $s$
+as \texttt{replacementEnergy\_continuous}, and the quantitative
+estimate
+\[
+  f_\Omega(s) - \mathcal{H}^n(\partial \widetilde{\Omega}_s)
+  \;\ge\; \frac{1}{4N}
+  \qquad \text{for } s \in (a_t, b_t)
+\]
+as \texttt{saving\_bound}, one obtains an instance of
+\texttt{LocalWitness}\,$([0,1], f_\Omega, t, 1/(4N))$. Of these
+four data items, only the continuity is treated implicitly in
+the literature (through the continuity of the replaced family
+in the inserted parameter); in the Lean formalization it must
+be supplied explicitly.
+
+\subsection{The chain: from sup reduction to inf-sup contradiction}
+\label{sec:integration-chain}
+
+With the per-parameter local witnesses in place, the chained
+theorem \lean{exists\_sup\_reduction}{SupReduction.lean}
+produces a competitor $f' : [0,1] \to \mathbb{R}$ together
+with a modification set $S \subseteq [0,1]$ satisfying
+\[
+  \{t : f_\Omega(t) \ge m_0 - 1/N\} \subseteq S, \qquad
+  f' \le f_\Omega \text{ on } [0,1], \qquad
+  f' = f_\Omega \text{ on } [0,1] \setminus S,
+\]
+together with the supremum bound
+$\sup f' \le m_0 - 1/(4N)$. This is the formalization of the
+sup-reduction step in the literature argument: $f'$ is the
+boundary energy of $\Omega$ after the local replacements have
+been combined, and the off-$S$ agreement ensures that $f'$ is
+a genuine combinatorial reduction of $f_\Omega$ rather than a
+trivial constant.
+
+The proof of the min-max theorem now closes the standard way.
+The off-$S$ agreement makes the geometric lift routine: there
+exists $\Omega' \in \mathcal{A}$ that agrees with $\Omega$
+outside $S$ and uses the local replacement on each component
+of $S$, and one checks $f' = f_{\Omega'}$. The three
+inequalities
+\[
+  \sup f_{\Omega'} \;=\; \sup f' \;\le\; m_0 - \tfrac{1}{4N}
+  \;<\; m_0 \;=\; \inf_{\mathcal{A}} \sup
+\]
+together with $\Omega' \in \mathcal{A}$ contradict the
+inf-sup characterization of $m_0$. The first
+inequality is the present formalization; the geometric lift
+producing $\Omega'$ is supplied by the surrounding Lean
+formalization. The full Lean script for this chain appears as
+Listing~\ref{lst:end-to-end} in Appendix~\ref{app:lean-script}.
+
+
+\subsection{Scope of the present formalization}
+\label{sec:integration-scope}
+
+We close with three caveats. First, the parameter space is
+fixed at $[0,1]$; multi-parameter sweepouts ($[0,1]^m$, in
+particular Almgren cycles) require a multi-parameter cover
+construction not carried out here. Second, the output is the
+scalar pair $(f', S)$, not a geometric replacement: the
+construction of the sweepout $\Omega' \in \mathcal{A}$
+realizing $f' = f_{\Omega'}$ falls outside the present
+formalization, though the off-$S$ agreement was chosen so as
+to make this lift mechanical. Third, the continuity of the
+replaced family in the inserted parameter is treated
+implicitly in~\cite{DLT13}; in the Lean formalization this
+becomes the \texttt{replacementEnergy\_continuous} field of
+\texttt{LocalWitness} and must be supplied explicitly. The
+formalization itself depends only on the three standard
+foundational axioms \texttt{propext}, \texttt{Classical.choice},
+and \texttt{Quot.sound}; standard measure-theory work in
+Mathlib stays within the same three.
+