refactor(chentsov): Restructure N≥3 uniform metric proof

- Simplified double-sum expansion with region partition comments
- Build: 3307 jobs, 0 errors, 6 sorries remaining

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