x: Sequential composition General.lean

[NhlanhlaHasane]

Updates to OracleReduction/Composition/Sequential/General.lean

Related PR

Depends on / related to #501

[github-actions]

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: x: Sequential composition General.lean

Mathematical Formalization

• ArkLib/Data/Polynomial/SplitFold.lean adds new definitions and lemmas for polynomial splitting and folding, specifically targeting the FRI protocol's algebraic core.
  • New definition: foldNth (n : ℕ) (f : 𝔽[X]) (β : 𝔽) [NeZero n] : 𝔽[X], defined as ∑_{i : Fin n} β ^ i.val * splitNth f n i. A trivial lemma foldNth_eq_sum_splitNth is provided.
  • New lemmas for n=2 case:
    • splitNth_monomial_even, splitNth_monomial_odd: Relate the splitNth of even/odd-degree monomials in 𝔽[X] to lower-degree monomials.
    • splitNth_two_eval_add, splitNth_two_eval_sub: Relate f.eval x plus/minus f.eval (-x) to (splitNth f 2 0).eval (x ^ 2) and (splitNth f 2 1).eval (x ^ 2), respectively.
    • foldNth_two_eval (final target): Gives a closed-form expression for (foldNth 2 f β).eval (x ^ 2) in terms of f.eval x, f.eval (-x), x, and β, assuming x ≠ 0 and 2 ≠ 0.
  • Refactor: The proof of splitNth_def was rewritten to use a more modular block of have statements instead of a single calc block. No new lemmas or definitions are introduced by this refactor.

Documentation

• ArkLib/OracleReduction/Basic.lean received an extensive module-level docstring (/-! block) explaining the concept of an Interactive Oracle Reduction (IOR), its role in SNARKs, and the key defined concepts (Prover, Verifier, OracleVerifier, OracleInterface, embed, Execution, Soundness, Completeness). It describes the architecture and the intended reading order of related files. The diff is purely documentation; no definitions, theorems, or implementations are changed.

Proof Completion (sorries removed)

• None. No sorry or admit statements were added or removed in any modified file.

Protocols / Soundness

• Unchanged. No files dealing with protocol soundness or completeness were directly modified.

Infrastructure / CI

• Unchanged.

Refactoring

• None beyond the proof-level refactoring in ArkLib/Data/Polynomial/SplitFold.lean noted above.

Summary of key changes: The main mathematical additions are in SplitFold.lean (new foldNth function and n=2 evaluation lemmas); the docstring in Basic.lean is purely structural/navigational. The review can concentrate on SplitFold.lean for algebraic correctness.

---

Statistics

Metric	Count
📝 Files Changed	2
✅ Lines Added	352
❌ Lines Removed	61

---

Lean Declarations

✏️ Added: 7 declaration(s)

ArkLib/Data/Polynomial/SplitFold.lean (7)

• def foldNth (n : ℕ) (f : 𝔽[X]) (β : 𝔽) [NeZero n] : 𝔽[X]
• lemma foldNth_eq_sum_splitNth {n : ℕ} [NeZero n] (f : 𝔽[X]) (β : 𝔽) :
• lemma foldNth_two_eval (f : 𝔽[X]) (x β : 𝔽)
• lemma splitNth_monomial_even (a : 𝔽) (k : ℕ) :
• lemma splitNth_monomial_odd (a : 𝔽) (k : ℕ) :
• lemma splitNth_two_eval_add (f : 𝔽[X]) (x : 𝔽) :
• lemma splitNth_two_eval_sub (f : 𝔽[X]) (x : 𝔽) :

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

The diff introduces new lemmas and documentation in SplitFold.lean and a large module docstring in OracleReduction/Basic.lean. Adherence to the ArkLib style guide is generally good, but two violations are identified. No project‑framework information is present in the diff, so progress against such a framework cannot be assessed.

---

📄 **Per-File Summaries**

• ArkLib/Data/Polynomial/SplitFold.lean: This diff makes the following changes to the file ArkLib/Data/Polynomial/SplitFold.lean:

1. Refactor of splitNth_def proof. The proof of splitNth_def inside the h : e % n ≥ b % n branch was rewritten to replace a single large calc-style rewrite with a more modular sequence of have statements (e.g., eq1, eq2, eq3), and the h' (the ¬ e % n ≥ b % n) branch was also restructured in a similar fashion. No new lemmas or definitions are introduced by this change.

2. New definition: foldNth. Defines a new function foldNth (n : ℕ) (f : 𝔽[X]) (β : 𝔽) [NeZero n] : 𝔽[X] as the sum over i : Fin n of β ^ i.val * splitNth f n i. A trivially true lemma foldNth_eq_sum_splitNth is also added.

3. New lemmas. Four new lemmas are added for the case n = 2, establishing evaluation-level identities for FRI folding:

• splitNth_monomial_even (a : 𝔽) (k : ℕ) : splitNth (monomial (2 * k) a) 2 0 = monomial k a.
• splitNth_monomial_odd (a : 𝔽) (k : ℕ) : splitNth (monomial (2 * k + 1) a) 2 1 = monomial k a.
• splitNth_two_eval_add (f : 𝔽[X]) (x : 𝔽) : f.eval x + f.eval (-x) = 2 * (splitNth f 2 0).eval (x ^ 2).
• splitNth_two_eval_sub (f : 𝔽[X]) (x : 𝔽) : f.eval x - f.eval (-x) = 2 * x * (splitNth f 2 1).eval (x ^ 2).
• foldNth_two_eval (f : 𝔽[X]) (x β : 𝔽) (hx : x ≠ 0) (h2 : (2 : 𝔽) ≠ 0) : (foldNth 2 f β).eval (x ^ 2) = (f.eval x + f.eval (-x) + β * (f.eval x - f.eval (-x)) * x⁻¹) * (2 : 𝔽)⁻¹.

No sorry or admit is introduced.

• ArkLib/OracleReduction/Basic.lean: Added a comprehensive module-level docstring (/-! block) to ArkLib/OracleReduction/Basic.lean. The documentation explains the concept of an Interactive Oracle Reduction (IOR) and its role as the core building block for SNARKs, outlines the key definitions (Prover, Verifier, OracleVerifier, OracleInterface, embed, Execution, Soundness, Completeness) with their signatures and intended semantics, clarifies the three-layer separation of interaction, execution, and security, and describes how this file relates to other files in the library (e.g., Composition.lean, Lifting.lean, and concrete protocols). The diff does not modify any existing definitions or introduce any sorry/admit; it only enriches the file with conceptual documentation.

---

Last updated: 2026-07-07 01:08 UTC.