feat(Data/Fin): prove fflatten_embedSum and fflatten₂_embedSum

[aryaethn]

Discharges two sorrys in ArkLib/Data/Fin/Sigma.lean — the functorial-flatten analogues of the
already-proven dflatten_embedSum:

• fflatten_embedSum : fflatten v (embedSum i j) = cast _ (v i j)
• fflatten₂_embedSum : fflatten₂ v (embedSum i j) = cast _ (v i j)

i.e. flattening a nested tuple and indexing at embedSum i j recovers the (i, j) entry, up to the
canonical cast along vflatten_embedSum.

Both proofs mirror the existing dflatten_embedSum: induct on m, case on i with Fin.cases,
reduce with fflatten_succ / fflatten₂_succ + fappend_left / fappend_right (resp. fappend₂_*),
and merge the nested casts with cast_cast — the same dependent-cast family and technique as #586 /
#587.

• Sorry count in the file: 9 → 7. No new declarations, imports, or files; no declaration consumes
  these two lemmas, so nothing downstream is affected.
• validate.sh green (build + Data warning budget + imports/docs/kb).
• Scope note: this touches only fflatten_embedSum / fflatten₂_embedSum (≈ lines 322 / 389),
  outside the region feat: completeness and rbrKnowledgeSoundness of FRI-Binius protocols #383 edits (embedSum_splitSum / dflatten_splitSum, ≈ 131–223), so it should
  not conflict.

[github-actions]

🤖 PR Summary

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

This pull request reduces the sorry count in ArkLib/Data/Fin/Sigma.lean by 2 (from 9 to 7) by proving two lemmas that complete the functorial-flatten analogue of the previously established dflatten_embedSum:

• fflatten_embedSum (fflatten v (embedSum i j) = cast _ (v i j))
• fflatten₂_embedSum (fflatten₂ v (embedSum i j) = cast _ (v i j))

These theorems assert that flattening a nested heterogeneous tuple and then indexing via embedSum recovers the original (i, j) entry, modulo the canonical cast along vflatten_embedSum.

Mathematical Formalization

• Definitions completed: The two sorry placeholders in fflatten_embedSum and fflatten₂_embedSum are now closed. Both proofs follow the same induction-on-m, case-on-i pattern as the existing dflatten_embedSum, using:
  • Fin.cases to split on the outer index
  • fflatten_succ / fflatten₂_succ for reduction
  • fappend_left / fappend_right (and their ₂ variants) for component selection
  • cast_cast to merge dependent category casts along the vflatten_embedSum path.
• API unaffected: No new declarations, imports, or files are introduced; no existing definition consumes these lemmas, so fflatten and fflatten₂ remain unchanged and no downstream code is affected.

Proof Completion (sorries removed)

• Sorry count: ArkLib/Data/Fin/Sigma.lean: 9 → 7. The two removed sorrys were the only changes in the file.

Infrastructure / CI

• validate.sh passes (build within Data warning budget, imports/docs/kb checks pass).

Scope / Conflict Avoidance

• Scope: The edit is confined to lines ~322 (for fflatten_embedSum) and ~389 (for fflatten₂_embedSum), outside the region (lines ~131–223) modified by PR feat: completeness and rbrKnowledgeSoundness of FRI-Binius protocols #383 (embedSum_splitSum / dflatten_splitSum). No merge conflicts are expected.

Remaining Unresolved

The file still contains 7 sorrys (outside the scope of this PR). No new sorry or admit placeholders are introduced.

---

Statistics

Metric	Count
📝 Files Changed	1
✅ Lines Added	24
❌ Lines Removed	2

---

Lean Declarations

• No declarations were added, removed, or affected.

---

sorry Tracking

✅ Removed: 2 `sorry`(s)

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

• theorem fflatten_embedSum {A : Sort u} {F : A → Sort v} {m : ℕ} {n : Fin m → ℕ} (L326)
• theorem fflatten₂_embedSum {A : Sort u} {B : Sort v} {F : A → B → Sort w} {m : ℕ} {n : Fin m → ℕ} (L383)

---

📋 **Additional Analysis**

The diff completes two previously missing proofs. Overall the code is well-structured but has two minor style violations per the ArkLib guidelines, one pre-existing and one newly introduced. No drift from roadmap or documented conventions beyond these points.

---

📄 **Per-File Summaries**

• ArkLib/Data/Fin/Sigma.lean: The file ArkLib/Data/Fin/Sigma.lean now includes complete proofs for the previously sorry-ed theorems fflatten_embedSum and fflatten₂_embedSum. These theorems establish that flattening a nested heterogeneous tuple via fflatten or fflatten₂ and then applying the embedSum injection yields the same result as directly accessing the original nested data, up to a cast.

---

Last updated: 2026-07-05 11:00 UTC.

[alexanderlhicks]

Thanks!