v3.3.47: Eliminate 3 axioms + terminology cleanup + release sync

Axiom elimination (13 → 11, -2 net):
- IsEigenvalue: axiom → def (membership in spectral sequence)
- spectrum_nonneg: axiom → theorem (from eigseq_nonneg)
- spectral_lower_bound: axiom → theorem via Cheeger + neck_dominates
- neck_dominates: placeholder → proper axiom (CheegerConstant ≥ 2v₀/L)
- ManifoldSpectralData restructured: removed circular IsEigenvalue dependency

Terminology cleanup (15+ files):
- Replace "Ralph Wiggum elimination" → "opaque refactoring" (9 Lean files)
- Replace S-number pipeline IDs → descriptive names (6 Lean files)

Version sync: all references bumped to 3.3.47, build jobs 2638 → 8025
Build: 8025 jobs, 0 errors, 11 axioms, 210 conjuncts

Co-Authored-By: Aristotle (Harmonic) <aristotle-harmonic@harmonic.fun>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: 3 people

CHANGELOG.md

@@ -9,7 +9,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ### Summary
 
-**DOUBLE AXIOM ELIMINATION: IsEigenvalue + spectrum_nonneg.** The `IsEigenvalue` axiom (predicate introduced in v3.3.44 to fix inconsistency) is now a **definition** — an eigenvalue is simply a value that appears in the spectral sequence. With this, `spectrum_nonneg` becomes a trivial theorem. The `ManifoldSpectralData` structure is decoupled from the eigenvalue predicate, breaking the circular dependency. **Axioms: 11 (-2 from v3.3.46).**
+**TRIPLE AXIOM ELIMINATION + CLEANUP: IsEigenvalue + spectrum_nonneg + spectral_lower_bound.** The `IsEigenvalue` axiom is now a **definition**, `spectrum_nonneg` a trivial theorem, and `spectral_lower_bound` a real theorem via Cheeger inequality + neck dominance (Aristotle AI). The `neck_dominates` placeholder is promoted to a proper axiom with geometric content. Terminology cleanup across 15+ files. **Axioms: 11 (-2 net from v3.3.46).**
 
 ### Changed
 
@@ -42,20 +42,30 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - **Build**: 8025 jobs, 0 errors
 - **Conjuncts**: 210 (unchanged)
 
-### Credits
+- **`Spectral/TCSBounds.lean`** — Integrated Aristotle's `spectral_lower_bound` proof:
+  - `spectral_lower_bound`: axiom → theorem via `cheeger_inequality` + `neck_dominates`
+  - `neck_dominates`: placeholder theorem → proper axiom with geometric content
+    (`CheegerConstant K ≥ 2v₀/L` for long necks)
+  - Added `cheeger_algebra` helper: `(2v₀/L)²/4 = v₀²/L²`
+  - Net axiom change: 0 (swap `spectral_lower_bound` ↔ `neck_dominates`)
 
-- **Aristotle AI** (Harmonics.fun): Original discovery of IsEigenvalue inconsistency (v3.3.44) led to the predicate axiom, which is now fully eliminated
-- **Claude Opus 4.6**: Designed the decoupling strategy and implemented the restructuring
+- **Terminology cleanup** (15+ files):
+  - "Ralph Wiggum elimination" → "opaque refactoring" (24 occurrences, 9 Lean files)
+  - S-number pipeline IDs (S10, S21, S22, S23, S27) → descriptive names (6 Lean files)
+  - Version sync: 3.3.42b/3.3.43 → 3.3.47 across README, docs, lakefile, Python
 
-### Details
+### Stats
 
-The v3.3.44 fix added `IsEigenvalue` as an axiom to prevent arbitrary eigenvalue construction. But this created a circular dependency: `ManifoldSpectralData` referenced `IsEigenvalue` (in `eigseq_is_spectrum`, `eigseq_complete`, `mass_gap_is_min`), and `IsEigenvalue` was defined independently. The v3.3.47 restructuring breaks this cycle by:
+- **Axioms**: 11 (-2 net from v3.3.46: IsEigenvalue + spectrum_nonneg eliminated,
+  spectral_lower_bound → theorem / neck_dominates → axiom swap)
+- **Build**: 8025 jobs, 0 errors
+- **Conjuncts**: 210 (unchanged)
 
-1. **Decoupling**: `ManifoldSpectralData` no longer mentions `IsEigenvalue`
-2. **Defining**: `IsEigenvalue M ev := ∃ n, eigseq n = ev` (def, not axiom)
-3. **Deriving**: All previous API becomes trivially provable
+### Credits
 
-This is the final axiom elimination in the spectral theory module. The remaining axiom (`manifold_spectral_data`) encodes the spectral theorem itself, which requires Mathlib's compact self-adjoint operator theory to eliminate.
+- **Aristotle AI** (Harmonics.fun): spectral_lower_bound proof via Cheeger + neck dominance;
+  original IsEigenvalue inconsistency discovery (v3.3.44)
+- **Claude Opus 4.6**: IsEigenvalue decoupling strategy, terminology cleanup, release prep
 
 ## [3.3.46] - 2026-03-21
 

Lean/GIFT/Spectral/TCSBounds.lean

@@ -19,8 +19,8 @@ This is the "Model Theorem" establishing the 1/L² scaling of the spectral gap.
 | `spectral_upper_bound` | C: Geometric structure | Rayleigh quotient |
 | `neck_cheeger_bound` | — | **ELIMINATED v3.3.41** (placeholder) |
 | `cut_classification` | — | **ELIMINATED v3.3.41** (placeholder) |
-| `neck_dominates` | — | **ELIMINATED v3.3.41** (placeholder) |
-| `spectral_lower_bound` | C: Geometric structure | Cheeger-based bound |
+| `neck_dominates` | C: Geometric structure | Cheeger constant ≥ 2v₀/L |
+| `spectral_lower_bound` | — | **ELIMINATED v3.3.47** (theorem via Cheeger + neck dominance) |
 
 ## Proof Strategy
 
@@ -194,30 +194,71 @@ theorem cut_classification (K : TCSManifold) (_hyp : TCSHypotheses K) :
 
 When L > L₀ = 2v₀/h₀, we have 2v₀/L < h₀, so the minimum in
   h(K) = min(h₀, 2v₀/L)
-is achieved by the neck term.
+is achieved by the neck term:
 
-**Formerly axiom**, now placeholder (bound captured by spectral_lower_bound) (v3.3.41). -/
-theorem neck_dominates (K : TCSManifold) (hyp : TCSHypotheses K)
-    (_hL : K.neckLength > L₀ K hyp) :
-  True :=
-  trivial
+1. Any separating hypersurface Σ either passes through a block or stays in the neck.
+2. Case A (through block): isoperimetric ratio ≥ h₀ by (H4).
+3. Case B (through neck): Area(Σ) ≥ Area(Y) by (H6) neck minimality,
+   and min(Vol(A), Vol(B)) ≤ Vol(N)/2, giving ratio ≥ 2·Area(Y)/Vol(N) ≥ 2v₀/L.
+4. Since L > L₀ = 2v₀/h₀ implies 2v₀/L < h₀, the neck case is the minimum.
+
+Result: CheegerConstant(K) ≥ 2v₀/L.
+
+**Axiom Category: C (Geometric structure)** — Neck dominance for Cheeger constant.
+**Why axiom**: Requires co-area formula and manifold measure theory not yet in Mathlib.
+**Elimination path**: Formalize isoperimetric classification on TCS decompositions.
+-/
+axiom neck_dominates (K : TCSManifold) (hyp : TCSHypotheses K)
+    (hL : K.neckLength > L₀ K hyp) :
+    CheegerConstant K.toCompactManifold ≥ 2 * hyp.neckVol.v₀ / K.neckLength
 
-/-- Spectral lower bound via Cheeger inequality.
+/-- Algebraic identity: (2v₀/L)² / 4 = v₀² / L².
+
+Used in the spectral lower bound proof to convert the Cheeger bound
+into the c₁/L² form. -/
+theorem cheeger_algebra (v₀ L : ℝ) (hL : L ≠ 0) :
+    (2 * v₀ / L) ^ 2 / 4 = v₀ ^ 2 / L ^ 2 := by
+  field_simp
+  ring
+
+/-- Spectral lower bound via Cheeger inequality and neck dominance.
 
 For L > L₀:
-1. h(K) ≥ 2v₀/L (by neck_dominates)
-2. λ₁ ≥ h²/4 (by Cheeger inequality)
-3. λ₁ ≥ (2v₀/L)²/4 = v₀²/L²
+1. h(K) ≥ 2v₀/L (by `neck_dominates`)
+2. λ₁ ≥ h²/4 (by `cheeger_inequality`)
+3. h² ≥ (2v₀/L)² (by monotonicity of squaring on nonneg reals)
+4. (2v₀/L)²/4 = v₀²/L² (by `cheeger_algebra`)
 
-Axiomatized: Full proof requires combining Cheeger inequality with
-monotonicity of squaring, which involves nonlinear arithmetic on
-transcendental (real) inequalities. The algebraic structure is:
-  λ₁ ≥ h²/4 ≥ (2v₀/L)²/4 = v₀²/L²
+Conclusion: λ₁ ≥ v₀²/L² = c₁/L².
 
-**Axiom Category: C (Geometric structure)** — Cheeger-based spectral lower bound. -/
-axiom spectral_lower_bound (K : TCSManifold) (hyp : TCSHypotheses K)
+**Formerly axiom**, now theorem via Cheeger inequality + neck dominance.
+
+**Proof credit**: Aristotle AI (Harmonics.fun), 2026-03-21.
+**Axiom reduction**: spectral_lower_bound eliminated (swapped for neck_dominates). -/
+theorem spectral_lower_bound (K : TCSManifold) (hyp : TCSHypotheses K)
     (hL : K.neckLength > L₀ K hyp) :
-    MassGap K.toCompactManifold ≥ c₁ K hyp / K.neckLength ^ 2
+    MassGap K.toCompactManifold ≥ c₁ K hyp / K.neckLength ^ 2 := by
+  -- Step 1: Cheeger inequality gives λ₁ ≥ h²/4
+  have h_cheeger := cheeger_inequality K.toCompactManifold
+  -- Step 2: Neck dominance gives h ≥ 2v₀/L
+  have h_neck := neck_dominates K hyp hL
+  -- Step 3: h ≥ 0 (Cheeger constant is non-negative)
+  have h_nonneg := cheeger_nonneg K.toCompactManifold
+  -- Step 4: 2v₀/L ≥ 0
+  have hv₀L_nonneg : 2 * hyp.neckVol.v₀ / K.neckLength ≥ 0 :=
+    div_nonneg (mul_nonneg (by norm_num) (le_of_lt hyp.neckVol.v₀_pos))
+      (le_of_lt K.neckLength_pos)
+  -- Step 5: h² ≥ (2v₀/L)² by monotonicity of squaring
+  have h_sq : (CheegerConstant K.toCompactManifold) ^ 2 ≥
+      (2 * hyp.neckVol.v₀ / K.neckLength) ^ 2 :=
+    sq_le_sq' (by linarith) h_neck
+  -- Step 6: Algebraic identity (2v₀/L)²/4 = v₀²/L²
+  have h_alg : (2 * hyp.neckVol.v₀ / K.neckLength) ^ 2 / 4 =
+      hyp.neckVol.v₀ ^ 2 / K.neckLength ^ 2 := by
+    field_simp; ring
+  -- Chain: MassGap ≥ h²/4 ≥ (2v₀/L)²/4 = v₀²/L² = c₁/L²
+  unfold c₁
+  linarith
 
 -- ============================================================================
 -- MAIN THEOREM: TCS SPECTRAL BOUNDS