diff --git a/formal/BindingSite/BindingSiteHachimoji.lean b/formal/BindingSite/BindingSiteHachimoji.lean
index 29757e9b..e1351a70 100644
--- a/formal/BindingSite/BindingSiteHachimoji.lean
+++ b/formal/BindingSite/BindingSiteHachimoji.lean
@@ -163,13 +163,13 @@ theorem chentsov_50 (g : (p : AminoAcidDistribution) → Fin 50 → Fin 50 → 
     (h_invar : ∀ {m} (f : MarkovEmbedding 50 m) p X Y,
       g p X Y = g (f p) (f.pushforward X) (f.pushforward Y)) :
     ∃ c > 0, ∀ p, g p = c • fisherMetric50 p := by
+  -- BLOCKED: Type bridge between AminoAcidDistribution and RiemannianMetric 50.
+  -- Mathematical content is correct (dimension-instantiation of Chentsov's theorem).
+  -- ChentsovFinite.lean has chentsov_theorem for arbitrary n ≥ 3.
+  -- Engineering: convert AminoAcidDistribution ↔ openSimplex 50,
+  -- fisherMetric50 ↔ fisherMetric, MarkovEmbedding ↔ MarkovMorphism.
+  -- Status: routine type conversion, not yet done.
   sorry
-  -- BLOCKED: Dimension-instantiation of ChentsovFinite.lean theorem.
-  -- The proof in ChentsovFinite.lean covers Fin 8; extending to Fin 50
-  -- requires the same functional equation h(t) = c/t argument, which
-  -- is dimension-independent. The blocker is not mathematical but
-  -- engineering: the proof structure must be generalized from n=8
-  -- to arbitrary n. Status: routine generalization, not yet done.
 
 -- =================================================================
 -- §4. BINDING SITE PROFILE