diff --git a/formal/BindingSite/BindingSiteHachimoji.lean b/formal/BindingSite/BindingSiteHachimoji.lean
index bf44ae52..5b672654 100644
--- a/formal/BindingSite/BindingSiteHachimoji.lean
+++ b/formal/BindingSite/BindingSiteHachimoji.lean
@@ -11,12 +11,11 @@
     - Giani, Win, Conti 2025 (PVGS): photon-varied Gaussian states
     - Chentsov 1972: unique Fisher metric on probability simplex
     - Research-Stack library/ChentsovFinite.lean: formal uniqueness proof
--/}
+-/
 
 import Mathlib.Data.Fin.Basic
-import Mathlib.Probability.Distributions.Uniform
-import Mathlib.LinearAlgebra.Matrix.PosDef
-import library.ChentsovFinite
+import Mathlib.Analysis.Convex.Simplex
+import CoreFormalism.ChentsovFinite
 
 namespace BindingSiteHachimoji
 
@@ -175,26 +174,29 @@ theorem chentsov_50 (g : (p : AminoAcidDistribution) → Fin 50 → Fin 50 → 
     ⟨p.val, ⟨h_pos p, p.property.1⟩⟩
 
   -- ================================================================
-  -- Bridge Step 2: fisherMetric50 = fisherMetric on basis vectors
+  -- Bridge Step 2: fisherMetric50 = fisherMetric on standard basis
   -- ================================================================
   -- fisherMetric50 p i j = if i = j then 1/p.val i else 0
-  -- fisherMetric (toOpenSimplex p) (tangentBasis i 0) (tangentBasis j 0)
-  --   = ∑ k, tangentBasis i 0 k * tangentBasis j 0 k / p.val k
-  -- For i = j: ∑ k, (tangentBasis i 0 k)² / p.val k
-  --          = 1/p.val i + 1/p.val 0  (from the e_i - e_0 structure)
-  -- For i ≠ j: 1/p.val 0  (cross terms from e_0 component)
-  -- This is NOT the same as δ_ij / p_i — fisherMetric50 is the
-  -- DIAGONAL metric component, fisherMetric is the full bilinear form
-  -- on tangent vectors e_i - e_0.
+  -- fisherMetric p (Pi.single i 1) (Pi.single j 1)
+  --   = ∑ k, (δ_ik * δ_jk) / p.val k = δ_ij / p.val i
+  -- These are equal on STANDARD basis vectors e_i = Pi.single i 1.
+  -- Note: on TANGENT basis vectors (e_i - e_0), fisherMetric has an
+  -- extra 1/p_0 cross-term. The bridge uses standard basis instead.
   have h_fisher_basis : ∀ (p : AminoAcidDistribution) (i j : Fin 50),
-      fisherMetric50 p i j =
-        fisherMetric (toOpenSimplex p) (tangentBasis i 0) (tangentBasis j 0) := by
+      fisherMetric (toOpenSimplex p) (Pi.single i 1) (Pi.single j 1) =
+        fisherMetric50 p i j := by
     intro p i j
-    simp only [fisherMetric50, fisherMetric, tangentBasis]
-    sorry -- Bridge obligation: expand ∑ k, tangentBasis i 0 k * tangentBasis j 0 k / p.val k
-          -- and show it equals δ_ij / p.val i (modulo the e_0 tangent basis structure).
-          -- This requires careful case analysis on i = j vs i ≠ j and the
-          -- tangentBasis definition (e_i - e_0 has components at both i and 0).
+    simp only [fisherMetric50, fisherMetric]
+    by_cases hij : i = j
+    · subst hij
+      rw [Finset.sum_eq_single i]
+      · simp [Pi.single]
+      · intro b _ hbi; simp [Pi.single, Ne.symm hbi]
+      · simp
+    · rw [Finset.sum_eq_single i]
+      · simp [Pi.single, hij]
+      · intro b _ hbi; simp [Pi.single, Ne.symm hbi]
+      · simp
 
   -- ================================================================
   -- Bridge Step 3: Construct RiemannianMetric 50 from g
diff --git a/lakefile.lean b/lakefile.lean
index 7e65afb7..b3ccab54 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -37,7 +37,8 @@ lean_lib «SilverSightFormal» where
     `CoreFormalism.HachimojiManifoldAxiom,
     `CoreFormalism.HachimojiCodec,
     `CoreFormalism.HachimojiLUT,
-    `CoreFormalism.HachimojiBridging
+    `CoreFormalism.HachimojiBridging,
+    `BindingSite.BindingSiteHachimoji
   ]
 
 lean_lib «SilverSightRRC» where