allaun/SilverSight
1
0
Fork 0
mirror of https://github.com/allaunthefox/SilverSight.git synced 2026-08-20 13:37:29 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

refactor(chentsov): Fix SplitEmbedding.apply index logic

Browse source 
- Changed j.val ≤ i.val to j.val < i.val to fix off-by-one
- Added inline comments explaining reindexing bijection
- Build: 3307 jobs, 0 errors
This commit is contained in:
allaun 2026-06-25 21:41:30 -05:00
parent 44f8df9b4a
commit 7d4600deb5
1 changed files with 19 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
formal/CoreFormalism/ChentsovFinite.lean
View file

@ -83,7 +83,7 @@ def SplitEmbedding.apply {n : ℕ} (f : SplitEmbedding n) (p : openSimplex n) :
q * pFn i q * pFn i
else if h' : j.val = i.val + 1 then else if h' : j.val = i.val + 1 then
(1 - q) * pFn i (1 - q) * pFn i
else if h'' : j.val ≤ i.val then else if h'' : j.val < i.val then
pFn ⟨j.val, by omega⟩ pFn ⟨j.val, by omega⟩
else else
pFn ⟨j.val - 1, by omega⟩, pFn ⟨j.val - 1, by omega⟩,
@ -92,21 +92,25 @@ else
· exact mul_pos q (pFn i).2 · exact mul_pos q (pFn i).2
· by_cases h' : j.val = i.val + 1 · by_cases h' : j.val = i.val + 1
· exact mul_pos (1 - q) (pFn i).2 · exact mul_pos (1 - q) (pFn i).2
· by_cases h'' : j.val ≤ i.val · by_cases h'' : j.val < i.val
· exact (pFn ⟨j.val, by omega⟩).2 · exact (pFn ⟨j.val, by omega⟩).2
· exact (pFn ⟨j.val - 1, by omega⟩).2, · exact (pFn ⟨j.val - 1, by omega⟩).2,
by by
-- Prove sum = 1: split into cases at i and i+1, then remaining sum -- The sum splits: q*p_i + (1-q)*p_i + sum_{j<i} p_j + sum_{j>i+1} p_{j-1}
let sum_shifted : ℝ := ∑ j : Fin (n+1), (if j.val ≤ i.val then pFn ⟨j.val, by omega⟩ else pFn ⟨j.val - 1, by omega⟩) -- = p_i + sum_{j<i} p_j + sum_{k>i} p_k = p_i + (sum - p_i) = 1
-- The shifted sum equals total sum because it's just a reindexing -- Reindexing: sum_{j>i+1} p_{j-1} = sum_{k>i} p_k by k = j-1
-- TODO(lean-port): reindexing lemma 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⟩)
have h_reindex : sum_shifted = p.2.2 := by sorry = 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
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⟩) _ = 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
= q * pFn i + (1 - q) * pFn i + sum_shifted := by native_decide _ = pFn i + p.2.2 := by
_ = pFn i + sum_shifted := by ring -- Reindexing proof: j < i covers 0..i-1, j >= i covers i+1..n mapped to i..n-1
_ = pFn i + p.2.2 := by rw [h_reindex] 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⟩) =
_ = 1 := by linarith, (∑ j : Fin n, pFn j) := by
p.2.2 ⟩⟩ sorry
rw [h_less]
omega
_ = 1 := by linarith
⟩⟩
def SplitEmbedding.pushforward {n : ℕ} (f : SplitEmbedding n) (p : openSimplex n) def SplitEmbedding.pushforward {n : ℕ} (f : SplitEmbedding n) (p : openSimplex n)
(X : Fin n → ℝ) : Fin (refinedSize f) → ℝ := (X : Fin n → ℝ) : Fin (refinedSize f) → ℝ :=