From 13ab6beb0136f745e631e6754d0a17bb7d2c1d07 Mon Sep 17 00:00:00 2001 From: allaun Date: Fri, 26 Jun 2026 00:00:35 -0500 Subject: [PATCH] fix(chentsov): Remove sorry placeholder from axiom parameters - chentsov_theorem_axiom now takes explicit IsChentsovInvariant g argument - theorem chentsov_theorem updated to match - Build: 3307 jobs, 0 errors, 0 sorries in ChentsovFinite --- formal/CoreFormalism/ChentsovFinite.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/formal/CoreFormalism/ChentsovFinite.lean b/formal/CoreFormalism/ChentsovFinite.lean index 1b4b295a..6c8b7275 100644 --- a/formal/CoreFormalism/ChentsovFinite.lean +++ b/formal/CoreFormalism/ChentsovFinite.lean @@ -710,7 +710,7 @@ 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 sorry) + (h_inv : IsChentsovInvariant g) (h_perm : IsPermutationInvariant g) (h_smooth : True) : ∃ (c : ℝ), c > 0 ∧ ∀ (p : openSimplex n) (X Y : Fin n → ℝ), @@ -718,7 +718,7 @@ axiom chentsov_theorem_axiom (n : ℕ) (hn : n ≥ 3) (g : RiemannianMetric n) g.toFun p X Y = c * fisherMetric p X Y theorem chentsov_theorem (n : ℕ) (hn : n ≥ 3) (g : RiemannianMetric n) - (h_inv : IsChentsovInvariant g sorry) + (h_inv : IsChentsovInvariant g) (h_perm : IsPermutationInvariant g) (h_smooth : True) : ∃ (c : ℝ), c > 0 ∧ ∀ (p : openSimplex n) (X Y : Fin n → ℝ),