Docs: spell out author abbreviations in prose; cite forms unchanged

The integration section in both README and paper §4 was using the
bare abbreviation "DLT" in running prose ("DLT Lemma 3.1", "DLT's
open interval", "DLT §3.2 Step 1"). Citation forms like
\cite{DLT13} are unaffected (they render as the citation key
"[DLT13]" by design).

In prose, "DLT" is replaced as follows:
- "DLT Lemma 3.1" / "DLT 3.1" -> "the local replacement lemma"
  (with the inline citation \cite[Lemma 3.1]{DLT13} added on first
  occurrence in each subsection).
- "DLT §3.2 Step 1/2" -> "\cite{DLT13} §3.2 Step 1/2".
- "DLT-style 1D cover refinement" -> "De Lellis-Tasnady-style 1D
  cover refinement".
- The §4.2 subsection title "The instantiation: LocalWitness <- DLT
  3.1" -> "The instantiation: LocalWitness from the local
  replacement lemma".

The single remaining "DLT" reference is inside the displayed
lstlisting comment "-- Lean image of DLT Lemma 3.1: per-parameter
local witness." (in the skeleton client code). That is a code
comment, not paper prose, so it stays.

Paper rebuilt at 11 pages, no errors.

Author: Xinze-Li-Moqian

README.md

@@ -24,9 +24,10 @@ per-piece replacement energies `E_l` and uniform savings
   - **(II)** every `t` lies in at most two pieces (two-fold overlap),
   - **(III)** `{t : f t ≥ m₀ − 1/N} ⊆ ⋃ pieces`.
 
-This is the non-trivial content extracted from the DLT-style
-1D cover refinement (Lebesgue-number cover, bounded
-smallest-index refinement induction, skip-2 parity rescue).
+This is the non-trivial content extracted from the
+De Lellis–Tasnady-style 1D cover refinement (Lebesgue-number
+cover, bounded smallest-index refinement induction, skip-2
+parity rescue).
 
 ### Sup-reduction bookkeeping corollary — `CombArg.exists_sup_reduction_of_cover`
 
@@ -188,10 +189,11 @@ four public declarations make no GMT references and stand for
 the four pieces the literature recombines at every instantiation.
 `LocalWitness K f t ε` carries the abstract per-parameter
 local-reducer data. `exists_refinement` is the formal counterpart
-of DLT §3.2 Step 1, the interval refinement that turns a family
-of local witnesses on the near-critical set into a finite cover
-with two-fold overlap. `exists_sup_reduction_of_cover` is the
-formal counterpart of DLT §3.2 Step 2, the scalar bookkeeping
+of De Lellis–Tasnady §3.2 Step 1, the interval refinement that
+turns a family of local witnesses on the near-critical set into
+a finite cover with two-fold overlap. `exists_sup_reduction_of_cover`
+is the formal counterpart of De Lellis–Tasnady §3.2 Step 2, the
+scalar bookkeeping
 that turns such a cover into a sup-reducing competitor. The
 chained one-parameter step `exists_sup_reduction` composes these
 two into a single call.
@@ -212,28 +214,30 @@ instantiated forms — they are exactly the same definitions
 either way; what changes is that this min-max-side data flows in
 as the inputs.
 
-### The instantiation: `LocalWitness` ← DLT Lemma 3.1
+### The instantiation: `LocalWitness` from the local replacement lemma
 
 The `LocalWitness` structure was designed to be the data shape
-DLT Lemma 3.1 produces, with each field naming a specific piece
-of the GMT-side replacement data. DLT's open interval
-`(a_i, b_i) ⊆ [0,1]` on which the local replacement saves energy
-becomes the `neighborhood` field; the boundary energy of the
-replaced sweepout, `s ↦ ℋⁿ(∂Ω̃_s)`, becomes `replacementEnergy`;
-its continuity in `s` (which DLT treats implicitly through the
-continuity of the replaced family in the inserted parameter)
-becomes the `replacementEnergy_continuous` obligation that the
-GMT side must discharge explicitly; and DLT's quantitative
-inequality `f(s) − ℋⁿ(∂Ω̃_s) ≥ 1/(4N)` on `(a_i, b_i)` becomes
+that the De Lellis–Tasnady local replacement lemma
+([DLT13] Lemma 3.1) produces, with each field naming a specific
+piece of the GMT-side replacement data. The open interval
+`(a_i, b_i) ⊆ [0,1]` on which the local replacement saves
+energy becomes the `neighborhood` field; the boundary energy of
+the replaced sweepout, `s ↦ ℋⁿ(∂Ω̃_s)`, becomes
+`replacementEnergy`; its continuity in `s` (which the local
+replacement lemma treats implicitly through the continuity of
+the replaced family in the inserted parameter) becomes the
+`replacementEnergy_continuous` obligation that the GMT side
+must discharge explicitly; and the quantitative inequality
+`f(s) − ℋⁿ(∂Ω̃_s) ≥ 1/(4N)` on `(a_i, b_i)` becomes
 `saving_bound`. The full mapping:
 
 | Library field | The corresponding piece of the original proof |
 |---|---|
-| `neighborhood : Set unitInterval` | DLT's open interval `(a_i, b_i) ⊆ [0,1]` around `t`. |
+| `neighborhood : Set unitInterval` | The open interval `(a_i, b_i) ⊆ [0,1]` around `t`. |
 | `isOpen_neighborhood` + `t_mem` | Openness of the interval; the parameter `t` lies in it. |
 | `replacementEnergy : unitInterval → ℝ` | `s ↦ ℋⁿ(∂Ω̃_s)`, the boundary energy of the replaced sweepout. |
 | `replacementEnergy_continuous` | Continuity of `s ↦ ℋⁿ(∂Ω̃_s)` in `s`. |
-| `saving_bound` | The quantitative DLT 3.1 inequality `f(s) − ℋⁿ(∂Ω̃_s) ≥ 1/(4N)` for `s ∈ (a_i, b_i)`. |
+| `saving_bound` | The quantitative inequality `f(s) − ℋⁿ(∂Ω̃_s) ≥ 1/(4N)` for `s ∈ (a_i, b_i)`. |
 
 ### The proof chain: from sup reduction to contradiction
 
@@ -305,8 +309,9 @@ theorem minmax_contradiction
 The three `YourGMT.*` identifiers mark the GMT-side
 responsibility: `YourGMT.choose_N` picks `N` so that `1/(4N)`
 beats the admissible class's contradiction window;
-`YourGMT.localWitness_of_DLT` is the GMT formalization of DLT
-Lemma 3.1, returning a per-`t` `LocalWitness`; and
+`YourGMT.localWitness_of_DLT` is the GMT formalization of the
+local replacement lemma ([DLT13] Lemma 3.1), returning a
+per-`t` `LocalWitness`; and
 `YourGMT.lift_sweepout` converts the scalar `f'` (with its
 modification set `S`) back to a sweepout in `𝒜`.
 
@@ -321,8 +326,8 @@ modification set `S`, and must lift back to a sweepout in `𝒜` on
 the GMT side; the `f' = f` off `S` guarantee is designed to make
 this lift mechanical. Continuity of `replacementEnergy` in the
 inserted parameter falls on the consumer to discharge explicitly,
-since DLT 3.1 supplies it only implicitly through the continuity
-of the replaced family. The library is pinned to
+since the local replacement lemma supplies it only implicitly
+through the continuity of the replaced family. The library is pinned to
 `leanprover/lean4:v4.30.0-rc2` plus the Mathlib revision in
 `lake-manifest.json`, so bumps on either side may require
 coordination. The library itself uses only the three standard

paper/paper.pdf

@@ -988,11 +988,12 @@ \section{Use as a software dependency}
 (Definition~\ref{def:witness}) carries the abstract
 per-parameter local-reducer data;
 \lean{exists\_refinement}{Refinement/Assembly.lean} is the
-formal counterpart of DLT~\S3.2 Step~1, the interval refinement
-that turns a family of local witnesses on the near-critical set
-into a finite cover with two-fold overlap;
+formal counterpart of \cite{DLT13}~\S3.2 Step~1, the interval
+refinement that turns a family of local witnesses on the
+near-critical set into a finite cover with two-fold overlap;
 \lean{exists\_sup\_reduction\_of\_cover}{Core.lean} is the
-formal counterpart of DLT~\S3.2 Step~2, the scalar bookkeeping
+formal counterpart of \cite{DLT13}~\S3.2 Step~2, the scalar
+bookkeeping
 that turns such a cover into a sup-reducing competitor; and
 \lean{exists\_sup\_reduction}{SupReduction.lean} composes these
 two into a single one-parameter call.
@@ -1015,24 +1016,24 @@ \section{Use as a software dependency}
 in as the inputs.
 
 \subsection{The instantiation:
-\texorpdfstring{\texttt{LocalWitness} $\leftarrow$ DLT~3.1}{LocalWitness from DLT 3.1}}
+\texorpdfstring{\texttt{LocalWitness} from the local replacement lemma}{LocalWitness from the local replacement lemma}}
 \label{sec:integration-dictionary}
 
 The \texttt{LocalWitness} structure was designed to be the data
-shape DLT~Lemma~3.1 produces, with each field naming a specific
-piece of the GMT-side replacement data. DLT's open interval
-$(a_i, b_i) \subseteq [0,1]$ on which the local replacement
-saves energy becomes the \texttt{neighborhood} field; the
-boundary energy of the replaced sweepout,
+shape that the De~Lellis--Tasnady local replacement lemma
+\cite[Lemma~3.1]{DLT13} produces, with each field naming a
+specific piece of the GMT-side replacement data. The open
+interval $(a_i, b_i) \subseteq [0,1]$ on which the local
+replacement saves energy becomes the \texttt{neighborhood}
+field; the boundary energy of the replaced sweepout,
 $s \mapsto \mathcal{H}^n(\partial \widetilde{\Omega}_s)$ with
 $\widetilde{\Omega}_s$ the original sweepout with the local
 replacement inserted at parameter $s$, becomes
-\texttt{replacementEnergy}; its continuity in $s$ (which DLT
-treats implicitly through the continuity of the replaced family
-in the inserted parameter) becomes the
+\texttt{replacementEnergy}; its continuity in $s$ (which
+\cite{DLT13} treats implicitly through the continuity of the
+replaced family in the inserted parameter) becomes the
 \texttt{replacementEnergy\_continuous} obligation that the GMT
-side must discharge explicitly; and DLT's quantitative
-inequality
+side must discharge explicitly; and the quantitative inequality
 $f(s) - \mathcal{H}^n(\partial \widetilde{\Omega}_s) \ge 1/(4N)$
 on $(a_i, b_i)$ becomes \texttt{saving\_bound}.
 
@@ -1113,7 +1114,8 @@ \subsection{Skeleton client code}
 responsibility: \texttt{YourGMT.choose\_N} picks $N$ so that
 $1/(4N)$ beats the admissible class's contradiction window;
 \texttt{YourGMT.localWitness\_of\_DLT} is the GMT formalization
-of DLT~Lemma~3.1, returning a per-$t$ \texttt{LocalWitness};
+of the local replacement lemma~\cite[Lemma~3.1]{DLT13},
+returning a per-$t$ \texttt{LocalWitness};
 and \texttt{YourGMT.lift\_sweepout} converts the scalar $f'$
 (together with its modification set $S$) back into a sweepout
 in $\mathcal{A}$.
@@ -1130,9 +1132,9 @@ \subsection{Known friction}
 in $\mathcal{A}$ on the GMT side, with the (b)~off-$S$
 agreement designed to make this lift mechanical. Continuity of
 \texttt{replacementEnergy} in the inserted parameter falls on
-the consumer to discharge explicitly, since DLT~3.1 supplies
-it only implicitly through the continuity of the replaced
-family. The library is pinned to
+the consumer to discharge explicitly, since the local
+replacement lemma supplies it only implicitly through the
+continuity of the replaced family. The library is pinned to
 \texttt{leanprover/lean4:v4.30.0-rc2} together with the
 Mathlib revision in \texttt{lake-manifest.json}, so bumps on
 either side may require coordination. The library itself uses