prove a bunch in sigma.lean

[MrBrain295]

No description provided.

[github-actions]

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: prove a bunch in sigma.lean

sorry delta: -6 (6 removed) — net proof progress

Failed to generate AI summary. Please check the per-file summaries and statistics below.

---

Statistics

Metric	Count
📝 Files Changed	1
✅ Lines Added	102
❌ Lines Removed	32

---

Lean Declarations

✏️ Added: 2 declaration(s)

ArkLib/Data/Fin/Sigma.lean (2)

• theorem partialSum_le_sum {m : ℕ} (n : Fin m → ℕ) (i : Fin m) :
• theorem val_embedSum {m : ℕ} {n : Fin m → ℕ} (i : Fin m) (j : Fin (n i)) :

✏️ Affected: 3 declaration(s) (line number changed)

• theorem fflatten_splitSum {A : Sort u} {F : A → Sort v} {m : ℕ} {n : Fin m → ℕ} in ArkLib/Data/Fin/Sigma.lean moved from L313 to L364
• theorem fflatten₂_splitSum {A : Sort u} {B : Sort v} {F : A → B → Sort w} {m : ℕ} {n : Fin m → ℕ} in ArkLib/Data/Fin/Sigma.lean moved from L379 to L436
• theorem vflatten_eq_vappend_last {m : ℕ} {n : Fin (m + 1) → ℕ} in ArkLib/Data/Fin/Sigma.lean moved from L256 to L282

---

sorry Tracking

✅ Removed: 6 `sorry`(s)

ArkLib/Data/Fin/Sigma.lean (6)

• def modSum {m : ℕ} {n : Fin m → ℕ} (k : Fin (∑ j, n j)) : Fin (n (divSum k)) (L521)
• theorem divSum?_is_some_iff_lt_sum {m : ℕ} {n : Fin m → ℕ} {k : ℕ} : (L483)
• theorem fflatten_splitSum {A : Sort u} {F : A → Sort v} {m : ℕ} {n : Fin m → ℕ} (L317)
• theorem fflatten₂_splitSum {A : Sort u} {B : Sort v} {F : A → B → Sort w} {m : ℕ} {n : Fin m → ℕ} (L384)
• theorem sum_le_of_divSum?_eq_some {m : ℕ} {n : Fin m → ℕ} {k : Fin (∑ j, n j)} {i : Fin m} (L510)
• theorem vflatten_eq_vappend_last {m : ℕ} {n : Fin (m + 1) → ℕ} (L264)

---

📋 **Additional Analysis**

The diff is relevant to the ARKLIB contribution guidelines. Below follows the review.

---

📄 **Per-File Summaries**

• ArkLib/Data/Fin/Sigma.lean: Adds the theorem val_embedSum (with a complete induction proof) giving a formula for the underlying Nat value of embedSum i j as the sum of n over earlier indices plus j.val. Moves the three splitSum theorems (vflatten_splitSum, fflatten_splitSum, fflatten₂_splitSum) from unfinished sorry/admit stubs to complete proofs (now each uses embedSum_splitSum to rewrite and then applies the corresponding _embedSum theorem). Replaces the earlier vflatten_eq_vappend_last proof (which ended in sorry) with a fully proved version using vflatten_embedSum and vappend_left/vappend_right. Adds the theorem partialSum_le_sum (the sum of the first i.val+1 terms of n is at most the total sum) and uses it to finish the previously sorry-filled proof of divSum?_is_some_iff_lt_sum. Fills in the sorry in the proof of sum_le_of_divSum?_eq_some using the Fin.eq_false_of_find?_eq_some_of_lt lemma. Finally, completes the modSum definition by proving its Fin (n (divSum k)) membership requirement (the ⟨k - ∑ ... , ?_⟩ term) using Fin.eq_true_of_find?_eq_some.

---

Last updated: 2026-08-05 14:32 UTC.

[github-actions]

Build Timing Report

• Commit: 0a37a22
• Message: prove a bunch in sigma.lean
• Ref: patch-1
• Comparison baseline: febaaa5 from the previous successful PR update.
• Measured on ubuntu-latest with /usr/bin/time -p.
• Commands: clean build rm -rf .lake/build && lake build; warm rebuild lake build; validation wrapper ./scripts/validate.sh.

Measurement	Baseline (s)	Current (s)	Delta (s)	Status
Clean build	1284.51	1423.19	+138.68	ok
Warm rebuild	2.51	2.53	+0.02	ok
Validation wrapper	2.67	2.84	+0.17	ok

Incremental Rebuild Signal

• Warm rebuild saved 1420.66s vs clean (562.53x faster).

This compares a clean project build against an incremental rebuild in the same CI job; it is a lightweight variability signal, not a full cross-run benchmark.

Slowest Current Clean-Build Files

Showing 20 slowest current targets, with comparison against the selected baseline when available.

Current (s)	Baseline (s)	Delta (s)	Path
74.00	58.00	+16.00	ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
68.00	54.00	+14.00	ArkLib/Data/CodingTheory/JohnsonBound/Lemmas.lean
68.00	55.00	+13.00	ArkLib/ProofSystem/Stir/Combine.lean
62.00	54.00	+8.00	ArkLib/Data/CodingTheory/ProximityGap/DG25/MainResults.lean
57.00	49.00	+8.00	ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineSpaces.lean
50.00	34.00	+16.00	ArkLib/Data/CodingTheory/ProximityGap/AHIV22.lean
48.00	49.00	-1.00	ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineLines/BWMatrix.lean
45.00	34.00	+11.00	ArkLib/Data/CodingTheory/BerlekampWelch/Condition.lean
42.00	33.00	+9.00	ArkLib/Data/CodingTheory/ProximityGap/Folding.lean
40.00	35.00	+5.00	ArkLib/OracleReduction/LiftContext/Reduction.lean
33.00	34.00	-1.00	ArkLib/Data/CodingTheory/JohnsonBound/Basic.lean
32.00	22.00	+10.00	ArkLib/Data/CodingTheory/DivergenceOfSets.lean
30.00	26.00	+4.00	ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineLines/JointAgreement.lean
29.00	31.00	-2.00	ArkLib/OracleReduction/Security/RoundByRound.lean
27.00	20.00	+7.00	ArkLib/ToCompPoly/Univariate/Basic.lean
27.00	24.00	+3.00	ArkLib/ProofSystem/Sumcheck/Spec/SingleRound.lean
26.00	21.00	+5.00	ArkLib/Commitments/Functional/KZG/FunctionBinding/EvaluationBindingConflict.lean
26.00	22.00	+4.00	ArkLib/Data/Polynomial/Indicator.lean
26.00	22.00	+4.00	ArkLib/Data/Polynomial/FoldingPolynomial.lean
25.00	24.00	+1.00	ArkLib/Data/CodingTheory/PolishchukSpielman/Degrees.lean

[alexanderlhicks]

Thanks!