From eaf512db9e89bbcce3cc57714721b13560f2b349 Mon Sep 17 00:00:00 2001
From: allaun <allaun@researchstack.info>
Date: Thu, 25 Jun 2026 21:59:11 -0500
Subject: [PATCH] =?UTF-8?q?refactor(chentsov):=20Restructure=20N=E2=89=A53?=
 =?UTF-8?q?=20uniform=20metric=20proof?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

- Simplified double-sum expansion with region partition comments
- Build: 3307 jobs, 0 errors, 6 sorries remaining
---
 formal/CoreFormalism/ChentsovFinite.lean | 19 ++++++-------------
 1 file changed, 6 insertions(+), 13 deletions(-)

diff --git a/formal/CoreFormalism/ChentsovFinite.lean b/formal/CoreFormalism/ChentsovFinite.lean
index f0733bf4..53e4ed82 100644
--- a/formal/CoreFormalism/ChentsovFinite.lean
+++ b/formal/CoreFormalism/ChentsovFinite.lean
@@ -499,19 +499,12 @@ lemma metric_at_uniform {N : ℕ} (hN : N ≥ 2) (g : RiemannianMetric N)
       have hGOff : ∀ x j : Fin N, x.val ≠ 0 → j.val ≠ 0 → x ≠ j →
           g.toFun p₀ (b x) (b j) = D / 2 := fun x j hx hj hxj =>
         g_offdiag_half hN3 g h_perm x j hx hj (Fin.val_ne_iff.mpr hxj)
-      -- Key identity: Σ_{x≠0,j≠0} u_x v_j = u_0 v_0 when Σ_x u_x = Σ_j v_j = 0
-      -- Proof: u_0 = -Σ_{x≠0} u_x, 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
-      -- This is a standard sum partition identity.
-      have h_vanish0 : (∑ x : Fin N, ∑ j : Fin N, u x * v j * g.toFun p₀ (b x) (b j)) =
-          (∑ x : Fin N, u x * v x * g.toFun p₀ (b x) (b x)) +
-          (∑ x : Fin N, ∑ j : Fin N, (x.val ≠ 0 ∧ j.val ≠ 0 ∧ x ≠ j) → u x * v j * g.toFun p₀ (b x) (b j)) := by
-        sorry
-      -- Now substitute g(b_x, b_j) = D when x=j, and D/2 when x≠0, j≠0, x≠j
-      have h_coeff : (∑ x : Fin N, u x * v x * D) + (∑ x : Fin N, ∑ j : Fin N, (x.val ≠ 0 ∧ j.val ≠ 0 ∧ x ≠ j) → u x * v j * D / 2) =
-          D * (∑ i : Fin N, u i * v i) / 2 := by
-        -- Use: 2D·Σ_{x≠0} u_x v_x + (D/2)·Σ_{x≠0,j≠0,x≠j} u_x v_j = (D/2)·Σ_i u_i v_i
-        sorry
+      -- 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
 
 end UniformMetric