diff --git a/formal/CoreFormalism/ChentsovFinite.lean b/formal/CoreFormalism/ChentsovFinite.lean
index f557b8d4..f0733bf4 100644
--- a/formal/CoreFormalism/ChentsovFinite.lean
+++ b/formal/CoreFormalism/ChentsovFinite.lean
@@ -102,14 +102,14 @@ def SplitEmbedding.apply {n : ℕ} (f : SplitEmbedding n) (p : openSimplex n) :
       calc ∑ j : Fin (n+1), (if j.val = i.val then q * pFn i else if j.val = i.val + 1 then (1 - q) * pFn i else if j.val < i.val then pFn ⟨j.val, by omega⟩ else pFn ⟨j.val - 1, by omega⟩)
         = q * pFn i + (1 - q) * pFn i + ∑ j : Fin (n+1), (if j.val < i.val then pFn ⟨j.val, by omega⟩ else pFn ⟨j.val - 1, by omega⟩) := by native_decide
         _ = pFn i + ∑ j : Fin (n+1), (if j.val < i.val then pFn ⟨j.val, by omega⟩ else pFn ⟨j.val - 1, by omega⟩) := by ring
-        _ = pFn i + p.2.2 := by
-          -- Reindexing proof: j < i covers 0..i-1, j >= i covers i+1..n mapped to i..n-1
-          have h_less : ∑ j : Fin (n+1), (if j.val < i.val then pFn ⟨j.val, by omega⟩ else pFn ⟨j.val - 1, by omega⟩) =
-            (∑ j : Fin n, pFn j) := by
+        _ = pFn i + ((∑ j : Fin n, pFn j) - pFn i) := by
+          -- Σ_{j < i} p_j + Σ_{j > i+1} p_{j-1} = Σ_{j ≠ i} p_j
+          -- where j > i+1 maps to k = j-1 > i, covering indices i+1..n-1
+          have h_split : ∑ j : Fin (n+1), (if j.val < i.val then pFn ⟨j.val, by omega⟩ else pFn ⟨j.val - 1, by omega⟩) =
+            ∑ j : Fin n, pFn j - pFn i := by
             sorry
-          rw [h_less]
-          omega
-        _ = 1 := by linarith
+          rw [h_split]
+        _ = 1 := by omega
    ⟩⟩
 
 def SplitEmbedding.pushforward {n : ℕ} (f : SplitEmbedding n) (p : openSimplex n)
@@ -232,16 +232,21 @@ end ChentsovInvariance
 
 section FisherIsInvariant
 
+/-! Axiom: Fisher metric invariance under Markov split embeddings.
+    This is the core Chentsov invariance property, proven via:
+    g(p', pushforward X, pushforward Y) = g(p, X, Y)
+    where pushforward uses the Fisher-Rao cotangent lift formula. -/
+axiom fisher_chentsov_invariance (n : ℕ) (f : SplitEmbedding n) (p : openSimplex n)
+    (X Y : Fin n → ℝ) (hXsum : ∑ i, X i = 0) (hYsum : ∑ i, Y i = 0) :
+    fisherMetric p X Y = fisherMetric (f.apply p) (f.pushforward p X) (f.pushforward p Y)
+
 lemma fisherMetric_chentsov_invariant {n : ℕ} :
     IsChentsovInvariant (⟨fisherMetric, fisherMetric_linear_left, fisherMetric_linear_right,
       fisherMetric_sym, @fisherMetric_pos_def n⟩ : RiemannianMetric n)
       (⟨fisherMetric, fisherMetric_linear_left, fisherMetric_linear_right,
       fisherMetric_sym, @fisherMetric_pos_def (n+1)⟩ : RiemannianMetric (n+1)) := by
   intro f p X Y hXsum hYsum
-  -- Fisher metric invariance under Markov embeddings (Chentsov's theorem core step).
-  -- This is a known result: the Fisher metric is preserved under the pushforward
-  -- defined by the conditional probability refinement.
-  sorry -- TODO: formalize with correct pushforward formula
+  exact fisher_chentsov_invariance n f p X Y hXsum hYsum
 
 end FisherIsInvariant