allaun/SilverSight
1
0
Fork 0
mirror of https://github.com/allaunthefox/SilverSight.git synced 2026-07-31 01:25:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

refactor(chentsov): Extract pushforward_sum to axiom

Browse source 
- Removed duplicate pushforward_sum lemma
- pushforward_sum_fisher axiom now properly stated at top level
- Build: 3307 jobs, 0 errors, 8 sorries remaining
This commit is contained in:
allaun 2026-06-25 21:43:27 -05:00
parent 7d4600deb5
commit 13285b3d40
1 changed files with 4 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
formal/CoreFormalism/ChentsovFinite.lean
View file

@ -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