Remove OpenGALib/MinMax/ — paper-bound, out of lib scope

The MinMax subtree (Sweepout/{Defs, ONVP, NonExcessive, MinMaxLimit,
MassCancellation, HomotopicMinimization, Interpolation, PullTight}) was
CLS22 / Almgren-Pitts / DLT13 paper terminology, conflicting with the
"MinMax must not reference paper-specific concepts" rule. Min-max /
sweepout content belongs in a paper-companion repo, not the lib.

- 9 files deleted (~1100 LOC, 12 sorry'd statements removed).
- OpenGALib.lean: drop import + remove MinMax from layering diagram and
  sub-namespace list.
- OpenGALib/Riemannian.lean: drop MinMax from layering ASCII; AltRegularity
  consumer line removed.
- OpenGALib/Riemannian/BumpFunction.lean: drop "GMT / MinMax" downstream
  mention.
- OpenGALib/GeometricMeasureTheory/{FlatDistance, Varifold}.lean: drop
  "Used by Sweepout" docstring entries.
- docs/SORRY_CATALOG.md: drop MinMax row, totals 32 → 20.
- .github/workflows/ci.yml: EXPECTED 32 → 20.
- .claude/CLAUDE.md: rewrite Architecture section (4 sub-namespaces:
  Algebraic, Riemannian, GMT, Regularity).

Author: Xinze-Li-Moqian

.claude/CLAUDE.md

@@ -4,7 +4,7 @@
 
 This framework is a Lean 4 mathematical software project, not a one-shot paper formalization.
 
-**Reusable Lean 4 mathematical software libraries**: Riemannian, GeometricMeasureTheory, MinMax theory, Regularity theory — Mathlib upstream candidates.
+**Reusable Lean 4 mathematical software libraries**: Riemannian, GeometricMeasureTheory, Regularity theory — Mathlib upstream candidates.
 
 Architectural decisions favor long-term software value. Paper-specific
 formalization sub-projects live in separate repos and consume this lib stack
@@ -14,27 +14,28 @@ Phase 1 (Layer A + Layer B real grounding) is complete: 20 GMT analysis primitiv
 
 ## Architecture
 
-Single OpenGALib Lean library, layered:
+Single OpenGALib Lean library, layered under `OpenGALib/`:
 
 ```
 OpenGALib (single lean_lib, 4 sub-namespaces)
+├── Algebraic                  ← lib (BilinearForm, Riesz, concrete instances)
+│         ↑
 ├── Riemannian                 ← lib (Connection, Curvature, SecondFundamentalForm, Gradient)
 │         ↑
 ├── GeometricMeasureTheory     ← lib (Variation/, HasNormal, Stable, Varifold, ...)
 │         ↑
-├── MinMax                     ← lib (min-max theory, Sweepout subnamespace)
 └── Regularity                 ← lib (regularity theory; Wickramasekera, Allard, Schoen-Simon, etc.)
 ```
 
-OpenGALib is a single Lake package containing 4 sub-namespaces (Riemannian, GeometricMeasureTheory,
-MinMax, Regularity). Namespace separation reflects layering — sub-namespaces are independently
-meaningful and any subset is a future Mathlib-upstream candidate.
+OpenGALib is a single Lake package containing 4 sub-namespaces (Algebraic, Riemannian,
+GeometricMeasureTheory, Regularity). Namespace separation reflects layering — sub-namespaces
+are independently meaningful and any subset is a future Mathlib-upstream candidate.
 Riemannian is independent of paper-domain concerns and is a future spin-out
 candidate as a standalone Lean library (Mathlib upstream / community use).
 GeometricMeasureTheory must not reference paper-specific or domain-specific concepts.
-MinMax and Regularity must not reference paper-specific concepts.
-Paper-specific sub-projects live outside this repo and consume the OpenGALib lib
-stack via `require OpenGALib from ".."`.
+Regularity must not reference paper-specific concepts.
+Paper-specific sub-projects (including min-max / sweepout machinery) live outside this
+repo and consume the OpenGALib lib stack via `require OpenGALib from ".."`.
 
 ## Self-build is the default action
 

.github/workflows/ci.yml

@@ -22,7 +22,7 @@ jobs:
             --include="*.lean" \
             OpenGALib \
             2>/dev/null | wc -l | tr -d ' ')
-          EXPECTED=32
+          EXPECTED=20
           if [ "$ACTUAL" -ne "$EXPECTED" ]; then
             echo "::error::Sorry count drift: expected $EXPECTED, found $ACTUAL"
             echo "If the change is intentional, update docs/SORRY_CATALOG.md (and the EXPECTED constant in this workflow)."

OpenGALib.lean

@@ -1,22 +1,21 @@
 import OpenGALib.Algebraic
 import OpenGALib.Riemannian
 import OpenGALib.GeometricMeasureTheory
-import OpenGALib.MinMax
 import OpenGALib.Regularity
 
 /-!
 # OpenGALib — Open Geometric Analysis Library
 
 A Lean 4 library of algebraic-geometry, Riemannian-geometry,
-geometric-measure-theory, min-max, and regularity primitives. Layered:
+geometric-measure-theory, and regularity primitives. Layered:
 
 ```
-Algebraic ← Riemannian ← GeometricMeasureTheory ← {MinMax, Regularity}
+Algebraic ← Riemannian ← GeometricMeasureTheory ← Regularity
 ```
 
 Each sub-namespace is built on Mathlib and intended as a future
-Mathlib-upstream candidate. Application papers (e.g., AltRegularity)
-consume this lib as a separate sub-project.
+Mathlib-upstream candidate. Application papers consume this lib as a
+separate sub-project.
 
 ## Sub-namespaces
 
@@ -26,6 +25,5 @@ consume this lib as a separate sub-project.
                               second fundamental form, manifold gradient
 * `GeometricMeasureTheory`  — finite-perimeter, varifolds, stationary,
                               tangent cones, rectifiability, isoperimetric
-* `MinMax`                  — sweepout-based min-max
 * `Regularity`              — Wickramasekera 𝒮_α + smooth regularity
 -/

OpenGALib/GeometricMeasureTheory/FlatDistance.lean

@@ -31,9 +31,7 @@ Specialization of the flat norm on integral $n$-currents to indicator
 functions of Caccioppoli sets, where boundary-minimization in the
 general flat norm collapses to the symmetric-difference volume.
 
-**Ground truth**: Simon 1983 §31; specialization Maggi 2012 §15.
-
-**Used by**: `Sweepout.FContinuous` def (`Sweepout/Defs.lean`). -/
+**Ground truth**: Simon 1983 §31; specialization Maggi 2012 §15. -/
 noncomputable def flatDist (Ω₁ Ω₂ : FinitePerimeter M) : ℝ :=
   (MeasureTheory.volume (symmDiff Ω₁.carrier Ω₂.carrier)).toReal
 

OpenGALib/GeometricMeasureTheory/Varifold.lean

@@ -128,9 +128,7 @@ applications (which only use mass measure / support information).
 
 **Ground truth**: Simon 1983 §38 (varifold convergence as weak-*
 convergence of Radon measures on the Grassmann bundle, paired against
-compactly supported continuous test functions); Allard 1972 §3.
-
-**Used by**: `Sweepout.MinMaxLimit` def (`Sweepout/MinMaxLimit.lean`). -/
+compactly supported continuous test functions); Allard 1972 §3. -/
 def VarifoldConverge (Vᵢ : ℕ → Varifold M) (V : Varifold M) : Prop :=
   ∀ φ : M → ℝ, Continuous φ → HasCompactSupport φ →
     Filter.Tendsto
@@ -245,8 +243,7 @@ exact value of `(ofBoundary Ω).dim`.
 structure theorem (Maggi 2012, Ch. 15) for the reduced boundary as a
 rectifiable set.
 
-**Used by**: `Sweepout.MinMaxLimit` def (`OpenGALib/MinMax/Sweepout/MinMaxLimit.lean`),
-`dlt_criterion` (`AltRegularity/Integrality/PerimeterConvergence.lean`). -/
+-/
 noncomputable def ofBoundary (Ω : FinitePerimeter M) : Varifold M where
   dim := 0
   massMeasure := Ω.perimMeasure