Add "even" and "odd" parts of folding

[ElijahVlasov]

No description provided.

[github-actions]

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: Add "even" and "odd" parts of folding

Mathematical Formalization

Adds the even and odd components of the folding operation used in Proximity Gap coding theory. Two new definitions are introduced:

• foldWordEven domain f — computes the even-indexed part of the fold, using a specified two‑nth root of unity.
• foldWordOdd domain f — computes the odd-indexed part, similarly parameterised by a root of unity.

Both definitions are accompanied by a key decomposition lemma:

• foldWord_k_1_eq_foldWordEven_add_foldWordOdd domain f α — states that foldWord domain f 1 α (the full fold at k=1) equals foldWordEven domain f + α • foldWordOdd domain f. This identity is central to splitting the folding evaluation into even/odd contributions, enabling further analysis of proximity gaps.

All definitions and lemmas are fully proved; no sorry or admit placeholders are present. The changes are concentrated in the single file ArkLib/Data/CodingTheory/ProximityGap/Folding.lean; no other files are modified.

---

Statistics

Metric	Count
📝 Files Changed	1
✅ Lines Added	25
❌ Lines Removed	0

---

Lean Declarations

✏️ Added: 3 declaration(s)

ArkLib/Data/CodingTheory/ProximityGap/Folding.lean (3)

• def foldWordEven [NeZero n] (domain : SmoothCosetFftDomain n F)
• def foldWordOdd [NeZero n] (domain : SmoothCosetFftDomain n F)
• lemma foldWord_k_1_eq_foldWordEven_add_foldWordOdd [NeZero n] {α : F} :

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

Findings from review of the diff against the supplied ArkLib contribution guidelines.

---

📄 **Per-File Summaries**

• ArkLib/Data/CodingTheory/ProximityGap/Folding.lean: Adds two new definitions foldWordEven and foldWordOdd that compute the even and odd parts of the fold, each using a two‑nth root of unity. Also adds lemma foldWord_k_1_eq_foldWordEven_add_foldWordOdd stating that foldWord domain f 1 α equals foldWordEven domain f + α • foldWordOdd domain f. No sorry or admit are present.

---

Last updated: 2026-07-29 17:04 UTC.