Paper: §6 Future work + redraw fig:arch as v0.4 two-tier architecture

Add `paper/sections/future.tex` (§6) with two follow-up directions
prepared for by the v0.4 architecture: (§6.1) the geometric lift
`DLTCover → {∂Ω'_t}` realizing DLT's modified sweepout via the
purely set-algebraic blending formula, available once an ambient
Lean GMT framework supplies a `FinitePerimeter` / `Sweepout` /
flat-continuity API; and (§6.2) multi-parameter sweepouts
($K = [0,1]^m$, Marques--Neves) via a sister namespace
`CombArg.MultiDim` reusing the $K$-generic bookkeeping corollary
with an $m$-dimensional spacing / parity-rescue construction.

Replace `fig:arch` with a v0.4-faithful two-tier diagram. The
v0.2-era pillars-plus-theorems figure is superseded by a layout
that shows the two parallel proof paths (Tier 1 `OneDim` with three
stages culminating in `DLTCover`; Tier 2 `Scalar` direct via
`exists_refinement_partition`), the shared abstract output
`FiniteCoverWithWitnesses`, the bookkeeping corollary producing the
sup-reducing competitor, and the dashed off-shoot to the future
geometric lift consuming the structured `DLTCover`. The diagram
makes the dependency-graph fact behind Remark 1.5 visible: only
Tier 1 carries the spacing / refinement / parity data, and only
that data is consumed by the geometric lift.

Paper-only follow-up to v0.4.0 release; no Lean code changes.

Author: Xinze-Li-Moqian

paper/paper.pdf

@@ -131,6 +131,7 @@
 \input{sections/proof}
 \input{sections/integration}
 \input{sections/generality}
+\input{sections/future}
 
 \appendix
 \input{sections/appendix}

paper/paper.tex

@@ -0,0 +1,87 @@
+\section{Future work}
+\label{sec:future}
+
+Two natural extensions sit immediately downstream of the present
+formalization, both prepared for by the v0.4 two-tier architecture
+of \S\ref{sec:proof}.
+
+\subsection{Geometric lift to a modified sweepout}
+\label{sec:future-lift}
+
+The structured output of \S\ref{sec:proof}
+(\lean{exists\_DLTCover}{OneDim/Assembly.lean}) packages the Stage A
+initial cover with spacing condition~(a), the Stage B partial
+refinement, $\sigma$-injectivity, and the termination invariant
+$\forall i,\ I_i \subseteq \bigcup_k J_k$ as a single Lean structure
+\texttt{DLTCover}. The companion lift
+\[
+  \texttt{DLTCover}\;\longrightarrow\;
+  \{\partial \Omega'_t\}_{t \in [0,1]}\ \text{flat-continuous}
+\]
+realizes the De~Lellis--Tasnady modified sweepout
+$\Omega'_t$ defined by cut-paste blending on the positive-measure
+overlaps $J_i \cap J_{i+1}$. The blending formula
+\[
+  \Omega'_t \;=\; [\Omega_t \setminus (U_i' \cup U_{i+1}')]
+   \;\cup\; [\Omega_{i,t} \cap U_i']
+   \;\cup\; [\Omega_{i+1,t} \cap U_{i+1}']
+\]
+is purely set-algebraic, and its $t$-continuity in the flat metric
+follows from $t$-continuity of the input families
+$\{\Omega_t\}, \{\Omega_{i,t}\}$ together with $t$-independence of
+the cut sets $U_i', U_{i+1}'$; no smooth structure or partition of
+unity is required. The lift therefore becomes formally available
+once an ambient Lean library supplies a finite-perimeter / sweepout
+API with a flat-continuity notion --- a strictly geometric
+prerequisite, separate from the combinatorial argument formalized
+here.
+
+The placeholder directory \texttt{CombArg/Geometric/} marks the
+import position the future lift module will occupy.
+Remark~\ref{rem:why-construction} is the design contract:
+\texttt{DLTCover}'s preserved spacing/overlap structure, not the
+abstract scalar bound of Corollary~\ref{thm:main}, is what the
+geometric lift consumes; the cheap partition route
+(\texttt{CombArg.Scalar.exists\_refinement\_partition}) shipped as
+its companion verifies by dependency-graph fact that the DLT
+structure is essential exactly at this lift step and at no earlier
+one.
+
+\subsection{Multi-parameter sweepouts}
+\label{sec:future-multiparam}
+
+The cover construction in \S\ref{sec:proof} is specialized to the
+$1$-parameter case $K = [0,1]$. Multi-parameter min-max
+constructions ($K = [0,1]^m$ for $m \ge 2$, in particular Almgren
+cycles in Marques--Neves~\cite{MN14}) replace the skip-$2$ spacing
+of \S\ref{sec:proof} (an inequality on $1$-dimensional indices)
+with a corresponding spacing structure on an $m$-dimensional grid;
+the parity rescue (\S\ref{sec:proof}, Proposition~\ref{prop:twofold})
+that delivers the two-fold overlap invariant from skip-$2$ spacing
+needs an $m$-dimensional analogue. The bookkeeping corollary
+\lean{exists\_sup\_reduction\_of\_cover}{Cover.lean} is already
+$K$-generic in compact $K$, so only the cover construction itself
+must be redone for the multi-parameter setting.
+
+The natural development is a sister namespace
+\texttt{CombArg.MultiDim} parallel to the present
+\texttt{CombArg.OneDim}, producing a \texttt{DLTCover}-analogous
+structured output for each $m \ge 1$ that the same bookkeeping
+corollary then turns into a sup-reducing competitor on $K =
+[0,1]^m$. The two-tier architecture inherited from the
+$1$-dimensional case --- a structured DLT-style cover preserving
+geometric data and a cheaper alternative scalar proof for the same
+abstract conclusion --- is expected to carry over: in each
+dimension, the abstract scalar reduction admits a partition-style
+shortcut, while the geometric lift to a multi-parameter modified
+sweepout consumes the structured form.
+
+\medskip
+
+Together, the two directions complete the formalization arc
+sketched at the start of \S\ref{sec:integration}: this paper
+formalizes the combinatorial slice; \S\ref{sec:future-lift} crosses
+into geometric measure theory once an ambient library is in place;
+and \S\ref{sec:future-multiparam} extends the combinatorial slice
+itself across parameter dimensions. Each is independently scoped and
+does not block the other.

paper/sections/future.tex

@@ -286,75 +286,116 @@ \subsection{Internal lemmas}
 \lean{exists\_refinement}{OneDim/Assembly.lean} chains the
 sub-lemmas above.
 
-Figure~\ref{fig:arch} shows the layered architecture.
+Figure~\ref{fig:arch} shows the two-tier architecture.
 
 \begin{figure}[tb]
 \centering
 \begin{tikzpicture}[
   font=\small,
   every node/.style={align=center},
-  pillar/.style={draw=black, thin, rectangle, rounded corners=3pt,
-                 inner sep=5pt, text width=38mm},
+  input/.style={draw=black, thin, rectangle, rounded corners=3pt,
+                inner sep=5pt, text width=46mm},
+  stage/.style={draw=black!55, thin, rectangle, rounded corners=2pt,
+                inner sep=3pt, text width=42mm, font=\scriptsize},
+  stagemain/.style={draw=black, thick, rectangle, rounded corners=2pt,
+                    inner sep=3pt, text width=42mm, font=\scriptsize,
+                    fill=black!5},
+  tierbox/.style={draw=black!40, thin, rectangle, rounded corners=4pt,
+                  dashed, inner sep=8pt},
   thm/.style={draw=black, thin, rectangle, rounded corners=3pt,
-              inner sep=5pt, text width=46mm},
+              inner sep=5pt, text width=58mm},
+  future/.style={draw=black!50, dashed, rectangle, rounded corners=3pt,
+                 inner sep=4pt, text width=44mm, text=black!60,
+                 font=\scriptsize},
   arr/.style={-Latex, thin, black!70},
+  futarr/.style={-Latex, thin, black!50, dashed},
   arrlab/.style={font=\scriptsize\itshape, midway, fill=white,
-                 inner sep=2pt, text=black!60}
+                 inner sep=2pt, text=black!60},
+  tierlab/.style={font=\scriptsize\bfseries\itshape, text=black!70}
 ]
 
-% Top row: three combinatorial pillars
-\node[pillar] (P1) at (-5.0, 4) {%
-  cover construction \\
-  {\scriptsize\itshape Lebesgue number on $\NC$}
+% Input
+\node[input] (input) at (0, 6.4) {%
+  \texttt{LocalWitness} hypothesis \\
+  {\scriptsize on the $1/N$-near-critical set of $f$}
 };
-\node[pillar] (P2) at ( 0.0, 4) {%
-  refinement induction \\
-  {\scriptsize\itshape smallest-index dispatch}
+
+% Tier 1 (left): DLT path with three stages
+\node[stage] (sA) at (-4.6, 4.6) {%
+  Stage A: \texttt{exists\_initialCover} \\
+  Lebesgue number $\to$ skip-$2$ spacing (a)
+};
+\node[stage] (sB) at (-4.6, 3.3) {%
+  Stage B: \texttt{exists\_terminal\_refinement} \\
+  smallest-index induction $\to$ $\sigma$ injective
 };
-\node[pillar] (P3) at ( 5.0, 4) {%
-  bookkeeping arithmetic \\
-  {\scriptsize\itshape pointwise case split}
+\node[stagemain] (sC) at (-4.6, 1.9) {%
+  Stage C: \texttt{exists\_DLTCover} \\
+  \textbf{structured output} (Stage A + B + invariants)
 };
 
-% Middle row: the two main theorems
-\node[thm] (core) at (-3.0, 1) {%
-  \texttt{exists\_refinement} \\
-  {\scriptsize combinatorial core, $K = [0,1]$}
+% Tier 1 grouping label
+\node[tierlab] at (-4.6, 5.6)
+  {Tier 1 \,---\, \texttt{CombArg.OneDim} \,---\, DLT-faithful path};
+
+% Tier 2 (right): single direct theorem
+\node[thm, text width=46mm] (sP) at (4.2, 3.3) {%
+  \texttt{exists\_refinement\_partition} \\
+  {\scriptsize partition by sorted endpoints}
 };
-\node[thm, text width=54mm] (genc) at ( 3.0, 1) {%
-  \texttt{exists\_sup\_reduction\_of\_cover} \\
-  {\scriptsize bookkeeping corollary, generic $K$}
+
+% Tier 2 grouping label
+\node[tierlab] at (4.2, 5.6)
+  {Tier 2 \,---\, \texttt{CombArg.Scalar} \,---\, cheap path};
+
+% Common abstract output
+\node[thm] (fcw) at (0, 0.0) {%
+  \texttt{FiniteCoverWithWitnesses} \\
+  {\scriptsize abstract scalar output (multiplicity $\le 2$, saving $\ge 1/(4N)$)}
 };
 
-% Bottom row: the chained 1D corollary (the user-facing entry point)
-\node[thm] (app) at (0, -2) {%
+% Bookkeeping corollary
+\node[thm] (sup) at (0, -2.0) {%
   \texttt{exists\_sup\_reduction} \\
-  {\scriptsize 1D chained corollary on $K = [0,1]$}
+  {\scriptsize sup-reducing competitor $f'$ with
+   $\sup f' \le m_0 - 1/(4N)$}
 };
 
-% Pillars feed the two main theorems
-\draw[arr] (P1.south) -- (core.north west);
-\draw[arr] (P2.south) -- (core.north);
-\draw[arr] (P3.south) -- (genc.north);
+% Future: geometric lift (dashed)
+\node[future] (geom) at (-4.6, 0.0) {%
+  \emph{(future)} \texttt{Geometric/} \\
+  modified sweepout $\{\partial \Omega'_t\}$ via blending
+};
 
-% The two main theorems compose into the 1D chained corollary
-\draw[arr] (core.south) -- node[arrlab, left=2pt] {via core}
-  (app.north west);
-\draw[arr] (genc.south) -- node[arrlab, right=2pt] {via bookkeeping}
-  (app.north east);
+% Arrows
+\draw[arr] (input.south) -| (sA.north);
+\draw[arr] (input.south) -| (sP.north);
+\draw[arr] (sA.south) -- (sB.north);
+\draw[arr] (sB.south) -- (sC.north);
+\draw[arr] (sC.south) -- node[arrlab, sloped, above]
+  {\texttt{toFinite}} (fcw.north west);
+\draw[arr] (sP.south) -- (fcw.north east);
+\draw[arr] (fcw.south) --
+  node[arrlab, right=1pt] {bookkeeping (\texttt{Cover.lean})}
+  (sup.north);
+\draw[futarr] (sC.east) to[bend right=15] (geom.north);
 
 \end{tikzpicture}
-\caption{\label{fig:arch}\CombArg{} v0.2 conceptual
-architecture. Three combinatorial pillars (cover construction
-via Lebesgue number, refinement induction via smallest-index
-dispatch, bookkeeping arithmetic via pointwise case split) feed
-two main theorems: the combinatorial core
-\texttt{exists\_refinement}, which produces a finite cover
-with two-fold overlap on $K = [0,1]$, and the bookkeeping
-corollary \texttt{exists\_sup\_reduction\_of\_cover}, which
-turns any such cover into a sup-reducing competitor on a
-generic compact $K$. The chained 1D corollary
-\texttt{exists\_sup\_reduction} composes the two on
-$K = [0,1]$ and is the user-facing entry point.}
+\caption{\label{fig:arch}\CombArg{} v0.4 two-tier architecture.
+The witness hypothesis feeds two independent proof paths producing
+the same abstract output: Tier~1 (\texttt{CombArg.OneDim}) follows
+the DLT \S3.2 Step~1 algorithm in three stages culminating in the
+structured \texttt{DLTCover}; Tier~2 (\texttt{CombArg.Scalar})
+proves the same conclusion directly by partition by endpoints and
+imports none of Tier~1's spacing / refinement / parity machinery
+(the dependency-graph fact behind
+Remark~\ref{rem:why-construction}). Both deliver a
+\texttt{FiniteCoverWithWitnesses} that the $K$-generic bookkeeping
+corollary in \texttt{Cover.lean} turns into a sup-reducing
+competitor $f'$. The future geometric lift consumes the
+\texttt{DLTCover} structure, not the abstract output --- the
+positive-measure overlap on $J_i \cap J_{i+1}$ that DLT's
+modified sweepout requires is preserved by Tier~1 and discarded
+by Tier~2.}
 \end{figure}