diff --git a/archive/2026-07-02/docs/FISHER_METRIC_BRIDGE.md b/archive/2026-07-02/docs/FISHER_METRIC_BRIDGE.md
new file mode 100644
index 00000000..15903533
--- /dev/null
+++ b/archive/2026-07-02/docs/FISHER_METRIC_BRIDGE.md
@@ -0,0 +1,75 @@
+# 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.