# 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.
