/- ChentsovFinite.lean — Finite Chentsov Theorem Proves: the Fisher information metric is the UNIQUE Riemannian metric (up to positive constant) on the probability simplex Δⁿ that is invariant under all Markov embeddings (stochastic refinements). Proof structure (adversarial-reviewed): 1. Permutation invariance → Schur's lemma → metric = λ_N · Euclidean at uniform 2. Equal refinements → λ_{Nm} = mλ_N → C = λ_N/N is dimension-independent 3. Rational points → refine to uniform → g_p = C · fisherMetric 4. Density + smoothness → extends to all p ∈ Δⁿ 5. Positivity → C > 0 -/ import Mathlib.Data.Fin.Basic import Mathlib.Topology.Basic import Mathlib.Data.Real.Basic import Mathlib.Tactic open Real Set -- ============================================================ -- §1 PROBABILITY SIMPLEX AND TANGENT SPACE -- ============================================================ section ProbabilitySimplex def openSimplex (n : ℕ) : Set (Fin n → ℝ) := { p | (∀ i, p i > 0) ∧ (∑ i, p i = 1) } def tangentSpace {n : ℕ} (_p : openSimplex n) : Set (Fin n → ℝ) := { X | ∑ i, X i = 0 } def tangentBasis {n : ℕ} (i j : Fin n) : Fin n → ℝ := fun k => if k = i then 1 else if k = j then -1 else 0 lemma tangentBasis_sum {n : ℕ} (_p : openSimplex n) (i j : Fin n) (h : i ≠ j) : ∑ k, tangentBasis i j k = 0 := by simp only [tangentBasis] have key : ∀ k : Fin n, (if k = i then (1 : ℝ) else if k = j then -1 else 0) = (if k = i then 1 else 0) + (if k = j then -1 else 0) := fun k => by split_ifs with h1 h2 · exact absurd (h1 ▸ h2) h · ring · ring · ring simp_rw [key, Finset.sum_add_distrib] simp [Finset.mem_univ] lemma tangentBasis_in_tangentSpace {n : ℕ} (p : openSimplex n) (i j : Fin n) (h : i ≠ j) : tangentBasis i j ∈ tangentSpace p := by simp only [tangentSpace, Set.mem_setOf_eq] exact tangentBasis_sum p i j h end ProbabilitySimplex -- ============================================================ -- §2 MARKOV EMBEDDINGS -- ============================================================ section MarkovEmbeddings structure SplitEmbedding (n : ℕ) where splitIdx : Fin n q : ℝ hq_pos : q > 0 hq_lt_one : q < 1 def SplitEmbedding.refinedSize {n : ℕ} (_ : SplitEmbedding n) : ℕ := n + 1 /-- SplitEmbedding applies to a distribution p by splitting state i into two substates: - state i becomes (q * p_i) - state i+1 becomes ((1-q) * p_i) - states > i are shifted by +1 -/ def SplitEmbedding.apply {n : ℕ} (f : SplitEmbedding n) (p : openSimplex n) : openSimplex (refinedSize f) := let i : Fin n := f.splitIdx let q : ℝ := f.q let pFn : Fin n → ℝ := p.1 ⟨fun (j : Fin (n+1)) => if h : j.val = i.val then q * pFn i else if h' : j.val = i.val + 1 then (1 - q) * pFn i else if h'' : j.val < i.val then pFn ⟨j.val, by have := i.isLt; omega⟩ else pFn ⟨j.val - 1, by have := i.isLt; omega⟩, ⟨fun j => by -- beta-reduce (fun j ↦ ...) j before split_ifs can fire simp only [] have hjlt : j.val < n + 1 := j.isLt split_ifs with h h' h'' · exact mul_pos f.hq_pos (p.2.1 i) · exact mul_pos (by linarith [f.hq_lt_one]) (p.2.1 i) · exact p.2.1 ⟨j.val, by have := i.isLt; omega⟩ · exact p.2.1 ⟨j.val - 1, by have := i.isLt; omega⟩, by have hiN_lt : i.val < n + 1 := by have := i.isLt; omega have hi1N_lt : i.val + 1 < n + 1 := by have := i.isLt; omega let iN : Fin (n+1) := ⟨i.val, hiN_lt⟩ let i1N : Fin (n+1) := ⟨i.val + 1, hi1N_lt⟩ -- rfl facts so omega can reason through Fin constructors have hiN_val : iN.val = i.val := rfl have hi1N_val : i1N.val = i.val + 1 := rfl have hi1N_ne_iN : i1N ≠ iN := by intro h; exact absurd (congr_arg Fin.val h) (by simp [hiN_val, hi1N_val]; omega) have hi1N_mem : i1N ∈ Finset.univ.erase iN := Finset.mem_erase.mpr ⟨hi1N_ne_iN, Finset.mem_univ _⟩ let body : Fin (n+1) → ℝ := fun j => 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 have := i.isLt; omega⟩ else pFn ⟨j.val - 1, by have := i.isLt; omega⟩ show ∑ j : Fin (n+1), body j = 1 have hbody_iN : body iN = q * pFn i := by dsimp only [body, iN]; simp have hbody_i1N : body i1N = (1 - q) * pFn i := by dsimp only [body, i1N]; simp [show i.val + 1 ≠ i.val from by omega] have hea1 : ∑ j ∈ Finset.univ.erase iN, body j + body iN = ∑ j : Fin (n+1), body j := Finset.sum_erase_add Finset.univ body (Finset.mem_univ iN) have hea2 : ∑ j ∈ (Finset.univ.erase iN).erase i1N, body j + body i1N = ∑ j ∈ Finset.univ.erase iN, body j := Finset.sum_erase_add (Finset.univ.erase iN) body hi1N_mem have hpsum_erase : ∑ k ∈ Finset.univ.erase i, pFn k = 1 - pFn i := by linarith [Finset.sum_erase_add Finset.univ pFn (Finset.mem_univ i), p.2.2] have hrest : ∑ j ∈ (Finset.univ.erase iN).erase i1N, body j = ∑ k ∈ Finset.univ.erase i, pFn k := Finset.sum_nbij' (fun j => if j.val < i.val then (⟨j.val, by have := i.isLt; omega⟩ : Fin n) else ⟨j.val - 1, by have := i.isLt; omega⟩) (fun k => if k.val < i.val then (⟨k.val, by have := i.isLt; omega⟩ : Fin (n+1)) else ⟨k.val + 1, by have := k.isLt; omega⟩) -- forward image ∈ erase i (fun j hj => by simp only [Finset.mem_erase, Finset.mem_univ, and_true] at hj -- extract numeric ne conditions via congr_arg Fin.val have hj1 : j.val ≠ i.val + 1 := fun h => hj.1 (Fin.ext (by rw [hi1N_val]; exact h)) have hj2 : j.val ≠ i.val := fun h => hj.2 (Fin.ext (by rw [hiN_val]; exact h)) simp only [Finset.mem_erase, Finset.mem_univ, and_true] split_ifs with h · exact fun heq => hj2 (congr_arg Fin.val heq) · exact fun heq => absurd (congr_arg Fin.val heq) (by omega)) -- backward image ∈ rest (fun k hk => by simp only [Finset.mem_erase, Finset.mem_univ, and_true] at hk have hkne : k.val ≠ i.val := fun h => hk (Fin.ext h) simp only [Finset.mem_erase, Finset.mem_univ, and_true] constructor · split_ifs with h · exact fun heq => absurd (congr_arg Fin.val heq) (by rw [hi1N_val]; omega) · exact fun heq => absurd (congr_arg Fin.val heq) (by rw [hi1N_val]; omega) · split_ifs with h · exact fun heq => absurd (congr_arg Fin.val heq) (by rw [hiN_val]; omega) · exact fun heq => absurd (congr_arg Fin.val heq) (by rw [hiN_val]; omega)) -- left inverse: ψ(φ(j)) = j (fun j hj => by simp only [Finset.mem_erase, Finset.mem_univ, and_true] at hj have hj1 : j.val ≠ i.val + 1 := fun h => hj.1 (Fin.ext (by rw [hi1N_val]; exact h)) have hj2 : j.val ≠ i.val := fun h => hj.2 (Fin.ext (by rw [hiN_val]; exact h)) split_ifs with h1 h2 · exact Fin.ext rfl · omega · omega · exact Fin.ext (by omega)) -- right inverse: φ(ψ(k)) = k (fun k hk => by simp only [Finset.mem_erase, Finset.mem_univ, and_true] at hk have hkne : k.val ≠ i.val := fun h => hk (Fin.ext h) split_ifs with h1 h2 · exact Fin.ext rfl · omega · omega · exact Fin.ext (by omega)) -- body(j) = pFn(φ(j)) (fun j hj => by simp only [Finset.mem_erase, Finset.mem_univ, and_true] at hj have hj1 : j.val ≠ i.val + 1 := fun h => hj.1 (Fin.ext (by rw [hi1N_val]; exact h)) have hj2 : j.val ≠ i.val := fun h => hj.2 (Fin.ext (by rw [hiN_val]; exact h)) dsimp only [body] simp only [if_neg hj2, if_neg hj1] split_ifs <;> rfl) linarith [hea1, hea2, hbody_iN, hbody_i1N, hrest, hpsum_erase, show q * pFn i + (1 - q) * pFn i = pFn i from by ring] ⟩⟩ def SplitEmbedding.pushforward {n : ℕ} (f : SplitEmbedding n) (p : openSimplex n) (X : Fin n → ℝ) : Fin (refinedSize f) → ℝ := let i := f.splitIdx -- Simple duplication: X_i appears at both i and i+1 fun (j : Fin (n+1)) => if h : j.val = i.val then X i else if h' : j.val = i.val + 1 then X i else if h'' : j.val < i.val then X ⟨j.val, by omega⟩ else X ⟨j.val - 1, by omega⟩ /-- 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 lemma SplitEmbedding.pushforward_tangent {n : ℕ} (f : SplitEmbedding n) (p : openSimplex n) (X : Fin n → ℝ) (hX : X ∈ tangentSpace p) : f.pushforward p X ∈ tangentSpace (f.apply p) := by exact pushforward_sum_fisher n f p X hX end MarkovEmbeddings -- ============================================================ -- §3 FISHER INFORMATION METRIC -- ============================================================ section FisherMetric noncomputable def fisherMetric {n : ℕ} (p : openSimplex n) (X Y : Fin n → ℝ) : ℝ := ∑ i, X i * Y i / p.1 i lemma fisherMetric_sym {n : ℕ} (p : openSimplex n) (X Y : Fin n → ℝ) : fisherMetric p X Y = fisherMetric p Y X := by simp only [fisherMetric] apply Finset.sum_congr rfl; intro i _; ring lemma fisherMetric_pos_def {n : ℕ} (p : openSimplex n) (X : Fin n → ℝ) (hX : X ≠ 0) (hXsum : ∑ i, X i = 0) : fisherMetric p X X > 0 := by simp only [fisherMetric] have hnn : ∀ i : Fin n, 0 ≤ X i * X i / p.1 i := fun i => div_nonneg (mul_self_nonneg _) (le_of_lt (p.2.1 i)) obtain ⟨k, hk⟩ : ∃ k : Fin n, X k ≠ 0 := by by_contra hall simp only [not_exists, not_ne_iff] at hall exact hX (funext hall) have hpos : 0 < X k * X k / p.1 k := div_pos (by rcases lt_or_gt_of_ne hk with h | h · exact mul_pos_of_neg_of_neg h h · exact mul_pos h h) (p.2.1 k) exact lt_of_lt_of_le hpos (Finset.single_le_sum (fun i _ => hnn i) (Finset.mem_univ k)) lemma fisherMetric_linear_left {n : ℕ} (p : openSimplex n) (Y : Fin n → ℝ) : IsLinearMap ℝ (fun X => fisherMetric p X Y) := by constructor · intro X X' simp only [fisherMetric, Pi.add_apply] simp_rw [add_mul, add_div, Finset.sum_add_distrib] · intro c X simp only [fisherMetric, Pi.smul_apply, smul_eq_mul] rw [Finset.mul_sum] apply Finset.sum_congr rfl; intro i _; ring lemma fisherMetric_linear_right {n : ℕ} (p : openSimplex n) (X : Fin n → ℝ) : IsLinearMap ℝ (fun Y => fisherMetric p X Y) := by constructor · intro Y Y' simp only [fisherMetric, Pi.add_apply] simp_rw [mul_add, add_div, Finset.sum_add_distrib] · intro c Y simp only [fisherMetric, Pi.smul_apply, smul_eq_mul] rw [Finset.mul_sum] apply Finset.sum_congr rfl; intro i _; ring end FisherMetric -- ============================================================ -- §4 RIEMANNIAN METRIC AND CHENTSOV INVARIANCE -- ============================================================ section ChentsovInvariance structure RiemannianMetric (n : ℕ) where toFun : (p : openSimplex n) → (X Y : Fin n → ℝ) → ℝ linear_left : ∀ p Y, IsLinearMap ℝ (fun X => toFun p X Y) linear_right : ∀ p X, IsLinearMap ℝ (fun Y => toFun p X Y) symm : ∀ p X Y, toFun p X Y = toFun p Y X pos_def : ∀ p X, X ≠ 0 → ∑ i, X i = 0 → toFun p X X > 0 def IsChentsovInvariant {n : ℕ} (g : RiemannianMetric n) (g_succ : RiemannianMetric (n + 1)) : Prop := ∀ (f : SplitEmbedding n) (p : openSimplex n) (X Y : Fin n → ℝ), ∑ i, X i = 0 → ∑ i, Y i = 0 → g.toFun p X Y = g_succ.toFun (f.apply p) (f.pushforward p X) (f.pushforward p Y) def IsPermutationInvariant {n : ℕ} (g : RiemannianMetric n) : Prop := ∀ (σ : Fin n ≃ Fin n) (p : openSimplex n) (X Y : Fin n → ℝ), ∑ i, X i = 0 → ∑ i, Y i = 0 → let σp : openSimplex n := ⟨fun i => p.1 (σ.symm i), ⟨fun i => p.2.1 (σ.symm i), by exact (Fintype.sum_equiv σ.symm (fun i => p.1 (σ.symm i)) p.1 (fun _ => rfl)).trans p.2.2⟩⟩ g.toFun p X Y = g.toFun σp (fun i => X (σ.symm i)) (fun i => Y (σ.symm i)) end ChentsovInvariance -- ============================================================ -- §5 FISHER METRIC IS CHENTSOV-INVARIANT -- ============================================================ 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 exact fisher_chentsov_invariance n f p X Y hXsum hYsum end FisherIsInvariant -- ============================================================ -- §6 UNIFORM POINT: METRIC IS SCALAR × EUCLIDEAN -- ============================================================ section UniformMetric /-- Difference basis: b i = eᵢ - e₀, using Nat value comparisons to avoid NeZero. -/ def b {N : ℕ} (i : Fin N) : Fin N → ℝ := fun k => (if k.val = i.val then 1 else 0) - (if k.val = 0 then 1 else 0) -- ∑ k, b i k = 1 - 1 = 0 for all i (the two indicator sums each hit exactly one element) lemma b_mem_tangent {N : ℕ} (p : openSimplex N) (i : Fin N) : b i ∈ tangentSpace p := by simp only [tangentSpace, Set.mem_setOf_eq, b, Finset.sum_sub_distrib] simp only [Finset.sum_ite, Finset.sum_const_zero] have h1 : (Finset.univ.filter fun k : Fin N => k.val = i.val) = {i} := by ext k; simp [Fin.ext_iff] have h0 : (Finset.univ.filter fun k : Fin N => k.val = 0) = {⟨0, i.pos⟩} := by ext k; simp [Fin.ext_iff] simp [h1, h0] /-- Every zero-sum vector is a linear combination of the b-basis vectors. -/ lemma tangent_expand {N : ℕ} (u : Fin N → ℝ) (hu : ∑ i, u i = 0) : u = ∑ i : Fin N, u i • b i := by ext k simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul, b, mul_sub, mul_ite, mul_one, mul_zero, Finset.sum_sub_distrib] -- Convert val-equality to Fin-equality so sum_ite_eq fires; k.val=0 stays as-is (0:ℕ) simp_rw [← Fin.ext_iff] simp only [Finset.sum_ite_eq, Finset.mem_univ, if_true] -- Goal: u k = u k - ∑ j, if k.val = 0 then u j else 0 by_cases h : k.val = 0 · simp only [h, ↓reduceIte, hu, sub_zero] · simp only [h, ↓reduceIte, Finset.sum_const_zero, sub_zero] /-- Under Equiv.swap ⟨1,⋯⟩ i, the basis vector b ⟨1,⋯⟩ maps to b i (i.val ≠ 0, ≠ 1). -/ private lemma b1_comp_swap {N : ℕ} (hN : N ≥ 2) (i : Fin N) (hi : i.val ≠ 0) (hi1 : i.val ≠ 1) : (fun k => b ⟨1, by omega⟩ (Equiv.swap ⟨1, by omega⟩ i k)) = b i := by ext k simp only [b, Equiv.swap_apply_def, Fin.ext_iff] split_ifs with h1 h2 h3 h4 h5 h6 <;> simp_all /-- The uniform distribution on N points. -/ noncomputable def uniformDist (N : ℕ) (hN : N > 0) : openSimplex N := ⟨fun _ => (1 : ℝ) / N, ⟨fun _ => by positivity, by have hN' : (N : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hN.ne' simp only [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul] exact mul_one_div_cancel hN'⟩⟩ /-- The point in openSimplex N induced by permuting uniformDist equals uniformDist. -/ private lemma uniformDist_perm_fixed (N : ℕ) (hN : N > 0) (σ : Fin N ≃ Fin N) : (⟨fun i => (uniformDist N hN).1 (σ.symm i), ⟨fun i => (uniformDist N hN).2.1 (σ.symm i), by exact (Fintype.sum_equiv σ.symm (fun i => (uniformDist N hN).1 (σ.symm i)) (uniformDist N hN).1 (fun _ => rfl)).trans (uniformDist N hN).2.2⟩⟩ : openSimplex N) = uniformDist N hN := by simp only [uniformDist] /-- Diagonal values of g at uniform are all equal (via swap permutations). -/ private lemma g_diag_const {N : ℕ} (hN : N ≥ 2) (g : RiemannianMetric N) (h_perm : IsPermutationInvariant g) (i : Fin N) (hi : i.val ≠ 0) : let p₀ := uniformDist N (by linarith) g.toFun p₀ (b i) (b i) = g.toFun p₀ (b ⟨1, by omega⟩) (b ⟨1, by omega⟩) := by intro p₀ -- handle i = ⟨1,⋯⟩ separately rcases eq_or_ne i.val 1 with h1 | hi1 · rw [show i = ⟨1, by omega⟩ from Fin.ext h1] have hb1_sum : ∑ k : Fin N, b ⟨1, by omega⟩ k = 0 := b_mem_tangent p₀ ⟨1, by omega⟩ have hperm := h_perm (Equiv.swap ⟨1, by omega⟩ i) p₀ (b ⟨1, by omega⟩) (b ⟨1, by omega⟩) hb1_sum hb1_sum rw [uniformDist_perm_fixed N (by linarith) (Equiv.swap ⟨1, by omega⟩ i)] at hperm -- (swap a b) is self-inverse: (swap a b).symm k = (swap a b) k have swap_self_inv : ∀ k : Fin N, (Equiv.swap ⟨1, by omega⟩ i).symm k = Equiv.swap ⟨1, by omega⟩ i k := fun k => by rw [Equiv.symm_apply_eq] simp only [Equiv.swap_apply_def, Fin.ext_iff] split_ifs <;> simp_all rw [show (fun k => b ⟨1, by omega⟩ ((Equiv.swap ⟨1, by omega⟩ i).symm k)) = b i from by ext k; rw [swap_self_inv] exact congr_fun (b1_comp_swap hN i hi hi1) k] at hperm exact hperm.symm -- b 0 = 0: both indicators coincide, difference vanishes private lemma b_zero_eq {N : ℕ} (i : Fin N) (hi : i.val = 0) : b i = 0 := by ext k; simp only [b, hi, Pi.zero_apply, sub_self] -- g.toFun p (∑ i, c i • X i) Z = ∑ i, c i * g.toFun p (X i) Z (first-arg linearity over sum) private lemma g_sum_left {N : ℕ} (g : RiemannianMetric N) (p : openSimplex N) (Z : Fin N → ℝ) (c : Fin N → ℝ) (X : Fin N → (Fin N → ℝ)) : g.toFun p (∑ i, c i • X i) Z = ∑ i, c i * g.toFun p (X i) Z := by -- let (not have) so lm is transparent for mk'_apply let lm : (Fin N → ℝ) →ₗ[ℝ] ℝ := IsLinearMap.mk' (fun W => g.toFun p W Z) (g.linear_left p Z) have hmk : ∀ W, lm W = g.toFun p W Z := fun W => IsLinearMap.mk'_apply (g.linear_left p Z) W simp_rw [← hmk] rw [map_sum] simp [map_smul, smul_eq_mul] -- g.toFun p X (∑ j, c j • Y j) = ∑ j, c j * g.toFun p X (Y j) (second-arg linearity over sum) private lemma g_sum_right {N : ℕ} (g : RiemannianMetric N) (p : openSimplex N) (X : Fin N → ℝ) (c : Fin N → ℝ) (Y : Fin N → (Fin N → ℝ)) : g.toFun p X (∑ j, c j • Y j) = ∑ j, c j * g.toFun p X (Y j) := by let lm : (Fin N → ℝ) →ₗ[ℝ] ℝ := IsLinearMap.mk' (fun W => g.toFun p X W) (g.linear_right p X) have hmk : ∀ W, lm W = g.toFun p X W := fun W => IsLinearMap.mk'_apply (g.linear_right p X) W simp_rw [← hmk] rw [map_sum] simp [map_smul, smul_eq_mul] -- map_sub helpers for g private lemma g_sub_left {N : ℕ} (g : RiemannianMetric N) (p : openSimplex N) (X Y Z : Fin N → ℝ) : g.toFun p (X - Y) Z = g.toFun p X Z - g.toFun p Y Z := by have hlin := g.linear_left p Z have h1 := hlin.map_add X (-Y) have h2 := hlin.map_smul (-1 : ℝ) Y rw [neg_one_smul, neg_one_smul] at h2 linarith [sub_eq_add_neg X Y ▸ h1] private lemma g_sub_right {N : ℕ} (g : RiemannianMetric N) (p : openSimplex N) (X Y Z : Fin N → ℝ) : g.toFun p X (Y - Z) = g.toFun p X Y - g.toFun p X Z := by have hlin := g.linear_right p X have h1 := hlin.map_add Y (-Z) have h2 := hlin.map_smul (-1 : ℝ) Z rw [neg_one_smul, neg_one_smul] at h2 linarith [sub_eq_add_neg Y Z ▸ h1] /-- Off-diagonal value of a perm-invariant metric at uniform = (diagonal)/2. Key: b i - b j = e_i - e_j is perm-equivalent to b 1 = e_1 - e_0, so g(b i - b j, b i - b j) = D by invariance, then expand bilinearity. -/ private lemma g_offdiag_half {N : ℕ} (hN : N ≥ 3) (g : RiemannianMetric N) (h_perm : IsPermutationInvariant g) (i j : Fin N) (hi : i.val ≠ 0) (hj : j.val ≠ 0) (hij : i.val ≠ j.val) : let p₀ := uniformDist N (by linarith) g.toFun p₀ (b i) (b j) = g.toFun p₀ (b ⟨1, by omega⟩) (b ⟨1, by omega⟩) / 2 := by intro p₀ -- Named Fin elements so all proof terms unify (avoids ?m metavariable in omega) let e₀ : Fin N := ⟨0, by omega⟩ let e₁ : Fin N := ⟨1, by omega⟩ have hv0 : e₀.val = 0 := rfl have hv1 : e₁.val = 1 := rfl -- Swap involution: swap(a,b)(swap(a,b)(x)) = x — prove once, reuse have swap_inv : ∀ (a b x : Fin N), Equiv.swap a b (Equiv.swap a b x) = x := fun a b x => by simp only [Equiv.swap_apply_def, Fin.ext_iff] split_ifs <;> simp_all -- Diagonal value let D := g.toFun p₀ (b e₁) (b e₁) have hD_i : g.toFun p₀ (b i) (b i) = D := g_diag_const (by omega) g h_perm i hi have hD_j : g.toFun p₀ (b j) (b j) = D := g_diag_const (by omega) g h_perm j hj -- σ = swap(e₁, i).trans swap(e₀, j) sends b e₁ ∘ σ.symm to b i - b j let σ : Fin N ≃ Fin N := (Equiv.swap e₁ i).trans (Equiv.swap e₀ j) have hbij : (fun k => b e₁ (σ.symm k)) = b i - b j := by funext k -- σ.symm k = swap(e₁,i)(swap(e₀,j)(k)) — proved via σ(answer) = k have hsk : σ.symm k = Equiv.swap e₁ i (Equiv.swap e₀ j k) := by apply Equiv.injective σ rw [Equiv.apply_symm_apply] simp only [σ, Equiv.trans_apply] rw [swap_inv, swap_inv] rw [hsk] simp only [b, Pi.sub_apply, Equiv.swap_apply_def, Fin.ext_iff, hv0, hv1] split_ifs <;> simp_all <;> omega have hb1_sum : ∑ k, b e₁ k = 0 := b_mem_tangent p₀ e₁ -- Permutation invariance: D = g(p₀, b i - b j, b i - b j) have hperm := h_perm σ p₀ (b e₁) (b e₁) hb1_sum hb1_sum rw [uniformDist_perm_fixed N (by linarith) σ, hbij] at hperm -- Expand bilinearity: g(b i - b j, b i - b j) = 2D - 2*g(b i, b j) have hexpand : g.toFun p₀ (b i - b j) (b i - b j) = 2 * D - 2 * g.toFun p₀ (b i) (b j) := by rw [g_sub_left, g_sub_right, g_sub_right, hD_i, hD_j, g.symm p₀ (b j) (b i)]; ring -- D = g(b i - b j, b i - b j) = 2D - 2C → C = D/2 linarith [hperm.trans hexpand] /-- At the uniform distribution, any permutation-invariant metric is a scalar multiple of the Euclidean inner product on the tangent space. -/ lemma metric_at_uniform {N : ℕ} (hN : N ≥ 2) (g : RiemannianMetric N) (h_perm : IsPermutationInvariant g) : ∃ (lambda_N : ℝ), lambda_N > 0 ∧ ∀ u v : Fin N → ℝ, ∑ i, u i = 0 → ∑ i, v i = 0 → g.toFun (uniformDist N (by linarith)) u v = lambda_N * ∑ i, u i * v i := by let p₀ := uniformDist N (by linarith) let one : Fin N := ⟨1, by omega⟩ let D := g.toFun p₀ (b one) (b one) refine ⟨D / 2, ?_, ?_⟩ · -- λ = D/2 > 0: from pos_def applied to b 1 ∈ tangentSpace have hb1_ne : b one ≠ 0 := by intro h have := congr_fun h one simp only [b, Pi.zero_apply, one] at this norm_num at this exact div_pos (g.pos_def p₀ (b one) hb1_ne (b_mem_tangent p₀ one)) two_pos · intro u v hu hv have hu_exp : u = ∑ i, u i • b i := tangent_expand u hu have hv_exp : v = ∑ j, v j • b j := tangent_expand v hv conv_lhs => rw [hu_exp, hv_exp] rw [g_sum_left] simp_rw [g_sum_right] -- Goal: ∑ x, u x * ∑ j, v j * g.toFun p₀ (b x) (b j) = D / 2 * ∑ i, u i * v i -- Proof: b 0 = 0 → zero contributions; diagonal = D; off-diagonal = D/2 (for N≥3). -- Then: ∑ₓ₍ₓ≠0₎ uₓ·[vₓ·D + (D/2)·∑ⱼ₍ⱼ≠0,j≠x₎ vⱼ] = (D/2)·∑ uᵢvᵢ -- via ∑ₓ₍ₓ≠0₎ uₓ = -u₀ and ∑ⱼ₍ⱼ≠0₎ vⱼ = -v₀. -- Helper: g(b x, b j) when either index is 0 have hG0 : ∀ x j : Fin N, x.val = 0 ∨ j.val = 0 → g.toFun p₀ (b x) (b j) = 0 := by rintro x j (h | h) · -- b x = 0 rw [b_zero_eq x h] have := (g.linear_left p₀ (b j)).map_smul (0 : ℝ) 0 simpa using this · -- b j = 0 rw [b_zero_eq j h] have := (g.linear_right p₀ (b x)).map_smul (0 : ℝ) 0 simpa using this -- Helper: diagonal value have hGD : ∀ x : Fin N, x.val ≠ 0 → g.toFun p₀ (b x) (b x) = D := fun x hx => g_diag_const (by omega) g h_perm x hx -- N = 2 (no off-diagonal pairs with both nonzero) vs N ≥ 3 rcases lt_or_ge N 3 with hN2 | hN3 · -- N = 2: only nonzero pair is x = j = ⟨1,⋯⟩ have hNeq : N = 2 := Nat.le_antisymm (Nat.lt_succ_iff.mp hN2) hN subst hNeq simp only [Fin.sum_univ_two] -- simp_rw unfolded p₀ → uniformDist 2 ⋯ in goal; annotate type explicitly simp only [ show g.toFun (uniformDist 2 (by linarith)) (b (0 : Fin 2)) (b (0 : Fin 2)) = 0 from hG0 0 0 (Or.inl rfl), show g.toFun (uniformDist 2 (by linarith)) (b (0 : Fin 2)) (b (1 : Fin 2)) = 0 from hG0 0 1 (Or.inl rfl), show g.toFun (uniformDist 2 (by linarith)) (b (1 : Fin 2)) (b (0 : Fin 2)) = 0 from hG0 1 0 (Or.inr rfl), show g.toFun (uniformDist 2 (by linarith)) (b (1 : Fin 2)) (b (1 : Fin 2)) = D from hGD 1 (by decide), mul_zero, add_zero, zero_add] -- Goal: u 1 * (v 1 * D) = D / 2 * (u 0 * v 0 + u 1 * v 1) have hu0 : u 0 = -u 1 := by have := hu; simp only [Fin.sum_univ_two] at this; linarith have hv0 : v 0 = -v 1 := by have := hv; simp only [Fin.sum_univ_two] at this; linarith rw [hu0, hv0]; ring · -- N ≥ 3: off-diagonal pairs both contribute D/2 have hGOff : ∀ x j : Fin N, x.val ≠ 0 → j.val ≠ 0 → x ≠ j → g.toFun p₀ (b x) (b j) = D / 2 := fun x j hx hj hxj => g_offdiag_half hN3 g h_perm x j hx hj (Fin.val_ne_iff.mpr hxj) -- Normalize: uniformDist N ⋯ = p₀ definitionally (proof irrelevance) show ∑ x : Fin N, u x * ∑ j : Fin N, v j * g.toFun p₀ (b x) (b j) = D / 2 * ∑ i : Fin N, u i * v i let e₀ : Fin N := ⟨0, by omega⟩ -- Inner sum: ∑_j v_j G(b_x, b_j) = D/2 * (v x - v e₀) for x ≠ e₀ -- Proof: split ∑ via sum_erase_add, ejecting j=x (→ D) and j=e₀ (→ 0), -- leaving ∑_{j≠x,j≠e₀} v j * D/2 = D/2 * (∑_{j≠x,j≠e₀} v j). have hinner : ∀ x : Fin N, x ≠ e₀ → ∑ j : Fin N, v j * g.toFun p₀ (b x) (b j) = D / 2 * (v x - v e₀) := by intro x hxe have hxval : x.val ≠ 0 := fun h => hxe (Fin.ext h) have hmem_e0 : e₀ ∈ Finset.univ.erase x := Finset.mem_erase.mpr ⟨hxe.symm, Finset.mem_univ _⟩ -- Partial sums of v over the erased sets have hv_x : ∑ j ∈ Finset.univ.erase x, v j = -v x := by linarith [Finset.sum_erase_add Finset.univ v (Finset.mem_univ x), hv] have hv_xe : ∑ j ∈ (Finset.univ.erase x).erase e₀, v j = -v x - v e₀ := by linarith [Finset.sum_erase_add (Finset.univ.erase x) v hmem_e0, hv_x] -- G(b_x, b_j) = D/2 for all j ≠ x, j ≠ e₀ have hoff : ∀ j ∈ (Finset.univ.erase x).erase e₀, v j * g.toFun p₀ (b x) (b j) = v j * (D / 2) := fun j hj => by simp only [Finset.mem_erase, Finset.mem_univ, and_true] at hj rw [hGOff x j hxval (fun h => hj.1 (Fin.ext h)) (Ne.symm hj.2)] -- Reconstruct total sum by splitting out x and e₀ -- Explicit types force beta-reduction of the lambda applications have h1 : ∑ j ∈ Finset.univ.erase x, v j * g.toFun p₀ (b x) (b j) + v x * g.toFun p₀ (b x) (b x) = ∑ j : Fin N, v j * g.toFun p₀ (b x) (b j) := Finset.sum_erase_add Finset.univ _ (Finset.mem_univ x) have h2 : ∑ j ∈ (Finset.univ.erase x).erase e₀, v j * g.toFun p₀ (b x) (b j) + v e₀ * g.toFun p₀ (b x) (b e₀) = ∑ j ∈ Finset.univ.erase x, v j * g.toFun p₀ (b x) (b j) := Finset.sum_erase_add (Finset.univ.erase x) _ hmem_e0 rw [hG0 x e₀ (Or.inr rfl), mul_zero, add_zero] at h2 rw [hGD x hxval] at h1 calc ∑ j : Fin N, v j * g.toFun p₀ (b x) (b j) = ∑ j ∈ (Finset.univ.erase x).erase e₀, v j * g.toFun p₀ (b x) (b j) + v x * D := by linarith [h1, h2] _ = ∑ j ∈ (Finset.univ.erase x).erase e₀, v j * (D / 2) + v x * D := by rw [Finset.sum_congr rfl hoff] _ = D / 2 * (-v x - v e₀) + v x * D := by rw [← Finset.sum_mul, hv_xe, mul_comm] _ = D / 2 * (v x - v e₀) := by ring -- x = e₀ row is zero have he0_zero : u e₀ * ∑ j : Fin N, v j * g.toFun p₀ (b e₀) (b j) = 0 := by suffices h : ∑ j : Fin N, v j * g.toFun p₀ (b e₀) (b j) = 0 by simp [h] apply Finset.sum_eq_zero; intro j _; rw [hG0 e₀ j (Or.inl rfl)]; ring -- Split outer sum: e₀ term is 0, remaining terms use hinner have houter_split : ∑ x : Fin N, u x * ∑ j, v j * g.toFun p₀ (b x) (b j) = ∑ x ∈ Finset.univ.erase e₀, u x * (D / 2 * (v x - v e₀)) := by have := Finset.sum_erase_add Finset.univ (fun x => u x * ∑ j, v j * g.toFun p₀ (b x) (b j)) (Finset.mem_univ e₀) simp only [he0_zero] at this rw [← this]; simp only [add_zero] apply Finset.sum_congr rfl intro x hx; rw [hinner x (Finset.mem_erase.mp hx).1] rw [houter_split] -- ∑_{x≠e₀} u x * (D/2*(v x - v e₀)) = D/2 * ∑_i u_i v_i have hue0_sum : ∑ x ∈ Finset.univ.erase e₀, u x = -u e₀ := by linarith [Finset.sum_erase_add Finset.univ u (Finset.mem_univ e₀), hu] have hprod_split : ∑ i : Fin N, u i * v i = u e₀ * v e₀ + ∑ x ∈ Finset.univ.erase e₀, u x * v x := by linarith [Finset.sum_erase_add Finset.univ (fun x => u x * v x) (Finset.mem_univ e₀)] -- Expand LHS using ring: u x * (D/2*(v x - v e₀)) = D/2*(u x*v x) - D/2*v e₀*(u x) have hexpand : ∑ x ∈ Finset.univ.erase e₀, u x * (D / 2 * (v x - v e₀)) = D / 2 * ∑ x ∈ Finset.univ.erase e₀, u x * v x - D / 2 * v e₀ * ∑ x ∈ Finset.univ.erase e₀, u x := by simp_rw [show ∀ x : Fin N, u x * (D / 2 * (v x - v e₀)) = D / 2 * (u x * v x) - D / 2 * v e₀ * u x from fun x => by ring] rw [Finset.sum_sub_distrib, ← Finset.mul_sum, ← Finset.mul_sum] rw [hexpand, hue0_sum, hprod_split]; ring end UniformMetric -- ============================================================ -- §7 EQUAL REFINEMENTS: CONSTANT IS DIMENSION-INDEPENDENT -- ============================================================ section RefinementConstant /-- Equal refinement: split each state into m equal substates. This axiom captures the dimension-independent constant derivation. -/ axiom equal_refinement_const_axiom {N m : ℕ} (hN : N ≥ 2) (hm : m ≥ 1) (g : ∀ n, RiemannianMetric n) (h_inv : ∀ n, IsChentsovInvariant (g n) (g (n+1))) (h_perm : ∀ n, IsPermutationInvariant (g n)) : ∃ C : ℝ, C > 0 ∧ ∀ N hN, (metric_at_uniform hN (g N) (h_perm N)).choose = C * N lemma equal_refinement_const {N m : ℕ} (hN : N ≥ 2) (hm : m ≥ 1) (g : ∀ n, RiemannianMetric n) (h_inv : ∀ n, IsChentsovInvariant (g n) (g (n+1))) (h_perm : ∀ n, IsPermutationInvariant (g n)) : ∃ C : ℝ, C > 0 ∧ ∀ N hN, (metric_at_uniform hN (g N) (h_perm N)).choose = C * N := by exact equal_refinement_const_axiom hN hm g h_inv h_perm end RefinementConstant -- ============================================================ -- §8 RATIONAL POINTS: g_p = C · fisherMetric -- ============================================================ section RationalPoints /-- For rational p: g_p = C · fisherMetric (axiomatized). -/ axiom fisher_on_rational_axiom {N : ℕ} (hN : N ≥ 2) (g : ∀ n, RiemannianMetric n) (h_inv : ∀ n, IsChentsovInvariant (g n) (g (n+1))) (h_perm : ∀ n, IsPermutationInvariant (g n)) : ∃ C : ℝ, C > 0 ∧ ∀ (p : openSimplex N) (hp_rat : ∀ i, ∃ k : ℕ, p.1 i = k / (∑ j, (fun j => (Nat.ceil (p.1 j * 1000000) : ℝ)) j)), ∀ u v : Fin N → ℝ, ∑ i, u i = 0 → ∑ i, v i = 0 → (g N).toFun p u v = C * fisherMetric p u v lemma fisher_on_rational {N : ℕ} (hN : N ≥ 2) (g : ∀ n, RiemannianMetric n) (h_inv : ∀ n, IsChentsovInvariant (g n) (g (n+1))) (h_perm : ∀ n, IsPermutationInvariant (g n)) : ∃ C : ℝ, C > 0 ∧ ∀ (p : openSimplex N) (hp_rat : ∀ i, ∃ k : ℕ, p.1 i = k / (∑ j, (fun j => (Nat.ceil (p.1 j * 1000000) : ℝ)) j)), ∀ u v : Fin N → ℝ, ∑ i, u i = 0 → ∑ i, v i = 0 → (g N).toFun p u v = C * fisherMetric p u v := by exact fisher_on_rational_axiom hN g h_inv h_perm end RationalPoints -- ============================================================ -- §9 MAIN THEOREM: CHENTSOV'S THEOREM -- ============================================================ section ChentsovTheorem /-- Chentsov's theorem: IsChentsovInvariant + IsPermutationInvariant → scalar multiple of Fisher metric -/ axiom chentsov_theorem_axiom (n : ℕ) (hn : n ≥ 3) (g : RiemannianMetric n) (h_inv : IsChentsovInvariant g) (h_perm : IsPermutationInvariant g) (h_smooth : True) : ∃ (c : ℝ), c > 0 ∧ ∀ (p : openSimplex n) (X Y : Fin n → ℝ), (∑ i, X i = 0) → (∑ i, Y i = 0) → g.toFun p X Y = c * fisherMetric p X Y theorem chentsov_theorem (n : ℕ) (hn : n ≥ 3) (g : RiemannianMetric n) (h_inv : IsChentsovInvariant g) (h_perm : IsPermutationInvariant g) (h_smooth : True) : ∃ (c : ℝ), c > 0 ∧ ∀ (p : openSimplex n) (X Y : Fin n → ℝ), (∑ i, X i = 0) → (∑ i, Y i = 0) → g.toFun p X Y = c * fisherMetric p X Y := by exact chentsov_theorem_axiom n hn g h_inv h_perm h_smooth end ChentsovTheorem