From 382064e7905ef8ffd82a06e4ef1fbd315ad95aa6 Mon Sep 17 00:00:00 2001
From: allaun <allaun@researchstack.info>
Date: Thu, 25 Jun 2026 22:01:33 -0500
Subject: [PATCH] refactor(chentsov): Restructure uniform metric partition
 proof

- Added h_partition lemma structure for u_0 v_0 identity
- Build: 3307 jobs, 0 errors, 5 sorries remaining
---
 formal/CoreFormalism/ChentsovFinite.lean | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

diff --git a/formal/CoreFormalism/ChentsovFinite.lean b/formal/CoreFormalism/ChentsovFinite.lean
index 53e4ed82..dc65f51f 100644
--- a/formal/CoreFormalism/ChentsovFinite.lean
+++ b/formal/CoreFormalism/ChentsovFinite.lean
@@ -501,12 +501,16 @@ lemma metric_at_uniform {N : ℕ} (hN : N ≥ 2) (g : RiemannianMetric N)
         g_offdiag_half hN3 g h_perm x j hx hj (Fin.val_ne_iff.mpr hxj)
       -- Expand g(u,v) = Σ_{x,j} u_x v_j g(b_x, b_j) using bilinearity
       rw [g_sum_left, g_sum_right]
-      -- Now partition the double sum into regions where g(b_x, b_j) has known values
-      -- Region 1: x.val = 0 or j.val = 0 → g = 0 (by hG0)
-      -- Region 2: x = j and x.val ≠ 0 → g = D (by hGD)
-      -- Region 3: x ≠ j and x.val ≠ 0 and j.val ≠ 0 → g = D/2 (by hGOff)
-      sorry
-
+      -- Partition the sum using b_sum_left/right and g properties
+      -- Key: Σ_{x,j: x≠0, j≠0} u_x v_j = u_0 v_0 when Σ u = Σ v = 0
+      -- Proof: u_0 = -Σ_{x≠0} u_x (from Σ u = 0), similarly v_0 = -Σ_{j≠0} v_j
+      -- So u_0 v_0 = (Σ_{x≠0} u_x)(Σ_{j≠0} v_j) = Σ_{x≠0, j≠0} u_x v_j
+      have h_partition : (∑ x : Fin N, ∑ j : Fin N, u x * v j * g.toFun p₀ (b x) (b j)) =
+          D * (∑ i : Fin N, u i * v i) / 2 := by
+        -- Use sum_erase to remove x=0 and j=0 terms, then apply hGOff for off-diagonal
+        sorry
+      rw [h_partition]
+      
 end UniformMetric
 
 -- ============================================================