allaun/SilverSight
1
0
Fork 0
mirror of https://github.com/allaunthefox/SilverSight.git synced 2026-07-31 01:25:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix: document chentsov_50 sorry — type bridge, not math gap

Browse source 
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.
This commit is contained in:
allaun 2026-06-23 07:32:43 -05:00
parent b528d26203
commit 534f7d15ab
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
formal/BindingSite/BindingSiteHachimoji.lean
View file

@ -163,13 +163,13 @@ theorem chentsov_50 (g : (p : AminoAcidDistribution) → Fin 50 → Fin 50 →
(h_invar : ∀ {m} (f : MarkovEmbedding 50 m) p X Y, (h_invar : ∀ {m} (f : MarkovEmbedding 50 m) p X Y,
g p X Y = g (f p) (f.pushforward X) (f.pushforward Y)) : g p X Y = g (f p) (f.pushforward X) (f.pushforward Y)) :
∃ c > 0, ∀ p, g p = c • fisherMetric50 p := by ∃ 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 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 -- §4. BINDING SITE PROFILE