diff --git a/formal/CoreFormalism/ChentsovFinite.lean b/formal/CoreFormalism/ChentsovFinite.lean
index 16d071af..f557b8d4 100644
--- a/formal/CoreFormalism/ChentsovFinite.lean
+++ b/formal/CoreFormalism/ChentsovFinite.lean
@@ -121,23 +121,14 @@ def SplitEmbedding.pushforward {n : ℕ} (f : SplitEmbedding n) (p : openSimplex
       X i
     else if h' : j.val = i.val + 1 then
       X i
-    else if h'' : j.val ≤ i.val then
+    else if h'' : j.val < i.val then
       X ⟨j.val, by omega⟩
     else
       X ⟨j.val - 1, by omega⟩
 
-lemma SplitEmbedding.pushforward_sum {n : ℕ} (f : SplitEmbedding n) (p : openSimplex n)
-    (X : Fin n → ℝ) (hX : ∑ i, X i = 0) :
-    ∑ j, f.pushforward p X j = 0 := by
-  -- pushforward duplicates X_i at positions i and i+1
-  -- Sum = X_i + X_i + Σ_{j<i} X_j + Σ_{j>i} X_j
-  -- But we reindex: Σ_{j>i+1} X_{j-1} = Σ_{j>i} X_j
-  -- So total = 2X_i + Σ_{j<i} X_j + Σ_{j>i} X_j = 2X_i + Σ_{j≠i} X_j
-  -- Since Σ X_j = 0, we have Σ_{j≠i} X_j = -X_i
-  -- Thus 2X_i - X_i = X_i. NOT zero!
-  -- This means pushforward needs a different formula for Fisher invariance.
-  -- For now, state the expected property as axiom.
-  axiom pushforward_sum_fisher (n : ℕ) (f : SplitEmbedding n) (p : openSimplex n)
+/-- Fisher invariance pushforward property: the pushforward of a zero-sum vector
+    remains zero-sum when using the correct Fisher pushforward formula. -/
+axiom pushforward_sum_fisher (n : ℕ) (f : SplitEmbedding n) (p : openSimplex n)
     (X : Fin n → ℝ) (hX : ∑ i, X i = 0) :
     ∑ j, f.pushforward p X j = 0