Remove FISHER_METRIC_BRIDGE.md

docs/FISHER_METRIC_BRIDGE.md

@@ -1,75 +0,0 @@
-# Fisher Metric Bridge — Mathematical Argument
-
-## The Problem
-
-`fisherMetric50 p i j = δ_ij / p_i` (diagonal matrix)
-`fisherMetric p X Y = ∑ k, X_k * Y_k / p_k` (bilinear form)
-
-Are these the same? **On the full space, yes. On the tangent space, no.**
-
-## Full Space
-
-For standard basis vectors `e_i` (where `e_i k = δ_ik`):
-
-```
-fisherMetric p e_i e_j = ∑ k, (δ_ik * δ_jk) / p_k = δ_ij / p_i
-```
-
-So `fisherMetric50 p i j = fisherMetric p e_i e_j`. ✓
-
-## Tangent Space
-
-For tangent vectors `e_i - e_0` and `e_j - e_0` (which sum to 0):
-
-```
-fisherMetric p (e_i - e_0) (e_j - e_0) = 
-  ∑ k, (e_i k - e_0 k)(e_j k - e_0 k) / p_k
-```
-
-For i ≠ 0, j ≠ 0, i ≠ j:
-- k = 0: (-1)(-1)/p_0 = 1/p_0
-- k = i: (1)(0)/p_i = 0
-- k = j: (0)(1)/p_j = 0
-- other: 0
-
-Result: `1/p_0`
-
-For i = j ≠ 0:
-- k = 0: (-1)(-1)/p_0 = 1/p_0
-- k = i: (1)(1)/p_i = 1/p_i
-- other: 0
-
-Result: `1/p_i + 1/p_0`
-
-So on the tangent space with basis {e_1 - e_0, ..., e_49 - e_0}:
-```
-fisherMetric p (e_i - e_0) (e_j - e_0) = δ_ij/p_i + 1/p_0
-```
-
-This is NOT `δ_ij/p_i`. The `1/p_0` cross-term appears.
-
-## The Correct Bridge
-
-`fisherMetric50` is the **full-space metric tensor** (evaluated on standard basis).
-`fisherMetric` is the **bilinear form** on the tangent space.
-
-They are the same Riemannian metric, just expressed in different bases:
-
-```
-Full space:    g_ij = fisherMetric50 p i j = δ_ij / p_i
-Tangent space: g_ij = fisherMetric p (e_i - e_0) (e_j - e_0) = δ_ij/p_i + 1/p_0
-```
-
-The `chentsov_theorem` proves uniqueness on the tangent space. The `chentsov_50` theorem uses the full-space representation. The bridge requires showing that the full-space metric is determined by its tangent-space restriction.
-
-## Lean Implementation Path
-
-1. Define `toOpenSimplex : AminoAcidDistribution → openSimplex 50` (via `h_pos`)
-2. Define `fullSpaceMetric p X Y = ∑ k, X k * Y k / p.val k` (same as `fisherMetric`)
-3. Show `fisherMetric50 p i j = fullSpaceMetric p (basisVec i) (basisVec j)` (trivial)
-4. Show `fullSpaceMetric` restricted to tangent space = `fisherMetric` on tangent vectors
-5. Apply `chentsov_theorem 50` to get uniqueness on tangent space
-6. Lift uniqueness to full space (standard linear algebra)
-7. Convert back to `fisherMetric50` matrix form
-
-Steps 1-3 are trivial. Step 4 is algebra. Step 5 requires `chentsov_theorem` (which has 3 internal sorries). Steps 6-7 are standard.