From 534f7d15ab7c00cdcb678e26bceaf2c1897b2c32 Mon Sep 17 00:00:00 2001 From: allaun Date: Tue, 23 Jun 2026 07:32:43 -0500 Subject: [PATCH] =?UTF-8?q?fix:=20document=20chentsov=5F50=20sorry=20?= =?UTF-8?q?=E2=80=94=20type=20bridge,=20not=20math=20gap?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The sorry is a type bridge between AminoAcidDistribution and RiemannianMetric 50. The mathematical content (Chentsov uniqueness for n=50) is correct — ChentsovFinite.lean has chentsov_theorem for arbitrary n ≥ 3. Remaining work: convert AminoAcidDistribution ↔ openSimplex 50, fisherMetric50 ↔ fisherMetric, MarkovEmbedding ↔ MarkovMorphism. Q16_16 unification (5 duplicates in PVGS_DQ_Bridge) deferred: files have Mathlib compatibility issues, not in lakefile. --- formal/BindingSite/BindingSiteHachimoji.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) 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