Multilinear folding completeness

[ElijahVlasov]

This PR introduces iterated folding operation as defined in the WHIR paper, proves it completeness, and its multilinear counterpart.

[github-actions]

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: Multilinear folding completeness

The overview should be written directly, starting with the substantive content or headers. No meta prefaces.

---

Statistics

Metric	Count
📝 Files Changed	5
✅ Lines Added	876
❌ Lines Removed	0

---

Lean Declarations

✏️ Added: 49 declaration(s)

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

• lemma iteratedFoldWord_zero {α : Fin 0 → F} :
• noncomputable def iteratedFoldWord (domain : SmoothCosetFftDomain n F)
• private lemma div_two_pow_div_two (d k : ℕ) :
• theorem foldWord_k_1' [NeZero n] {α : F} :
• theorem iteratedFoldWord_mem_code_of_mem_code {d : ℕ}

ArkLib/Data/CodingTheory/ProximityGap/Folding/Multilinear.lean (6)

• lemma foldWord_eq_evalOnPoints_powAlgHom [NeZero n] {α : F}
• private lemma aeval_split_mem {n : ℕ} [NeZero n] {R : Type} [Field R]
• private lemma aeval_substFun_comp {k : ℕ} [NeZero (n - k)] (γ : Fin (k + 1) → F)
• private lemma aeval_substFun_mem [NeZero n] {gg : F⦃≤ 1⦄[X (Fin n)]}
• private noncomputable def substFun (m : ℕ) (β : Fin m → F) (i : Fin n) :
• theorem iteratedFoldWord_eq_evalOnPoints_powAlgHom [NeZero n] {α : Fin k → F}

ArkLib/Data/Domain/CosetFftDomain/Subdomain.lean (9)

• def sqFoldMapGen {i : ℕ} (u : Fin (2 ^ n)) : Fin (2 ^ (n - i))
• lemma evalOnPoints_pow_of_two_eq_evalOnPoints_subdomain
• lemma evalOnPoints_sq_eq_evalOnPoints_subdomain [NeZero n] {p : Polynomial F} :
• lemma sqFoldMapGen_eq_sqFoldMapGen_of_pow_apply_eq_pow_apply
• lemma subdomain_one_comp
• lemma subdomain_sqFoldMapGen_eq_pow_domain [NeZero n] {i : ℕ} {j : Fin (2 ^ n)} :
• lemma subdomain_zero_eq_self {n : ℕ} {ω : SmoothCosetFftDomain n F} :
• private lemma subdomain_embed_comp {k : ℕ} (hk : k + 1 ≤ n)
• private lemma subdomain_eval (ω : D) (j : ℕ)

ArkLib/Data/MvPolynomial/EvenAndOdd.lean (29)

• lemma aeval_shift_mem_restrictDegree
• lemma aeval_shift_monomial_mem {n : ℕ} [NeZero n]
• lemma even_and_odd_eval
• lemma even_and_odd_formula'
• lemma even_and_odd_formula
• lemma powAlgHom_eq_even_add_odd_powAlgHom
• lemma powAlgHom_eq_even_add_odd
• lemma shiftedPowAlgHom_eq_powAlgHom_comp_sq_x
• noncomputable def even (p : R⦃≤ 1⦄[X (Fin n)]) :
• noncomputable def even_pred (p : R⦃≤ 1⦄[X (Fin n)]) : R⦃≤ 1⦄[X (Fin (n - 1))]
• noncomputable def odd (p : R⦃≤ 1⦄[X (Fin n)]) :
• noncomputable def odd_pred (p : R⦃≤ 1⦄[X (Fin n)]) : R⦃≤ 1⦄[X (Fin (n - 1))]
• noncomputable def shiftedPowAlgHom :
• private lemma aeval_shift_monomial_nonzero_case
• private lemma aeval_shift_monomial_zero_case {n : ℕ} [NeZero n]
• private lemma even_mem (p : R⦃≤ 1⦄[X (Fin n)]) :
• private lemma formula_for_monomial
• private lemma formula_generic
• private lemma mul_C_mem_restrictDegree
• private lemma odd_mem (p : R⦃≤ 1⦄[X (Fin n)]) :
• private lemma powAlgHom_aeval_shift (q : MvPolynomial (Fin (n - 1)) R) :
• private lemma shiftDown_shiftUp_eq (q : MvPolynomial (Fin n) R) :
• private lemma substMinus_mem_restrictDegree
• private lemma substNoX0_eq_self_of_even
• private lemma substNoX0_eq_self_of_odd
• private lemma substPlus_mem_restrictDegree
• private noncomputable def shiftDown (q : MvPolynomial (Fin n) R) : MvPolynomial (Fin (n - 1)) R
• private noncomputable def substMinus (p : MvPolynomial (Fin n) R) :
• private noncomputable def substPlus (p : MvPolynomial (Fin n) R) :

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

The diff introduces significant new functionality but contains several violations of the project's style and documentation guidelines. The most notable issues are missing or improperly formatted docstrings, a missing module docstring in EvenAndOdd.lean, incorrect naming of definitions even_pred/odd_pred, and likely line-length violations. Additionally, the BibTeX entry for the cited paper [ACFY24] is not included in the diff (should be added to blueprint/src/references.bib). Below is a detailed list of findings organized by category.

---

📄 **Per-File Summaries**

• ArkLib.lean: Two new module imports were added to ArkLib.lean: ArkLib.Data.CodingTheory.ProximityGap.Folding.Multilinear and ArkLib.Data.MvPolynomial.EvenAndOdd. These extend the library's coverage of coding theory proximity gaps and multivariate polynomial theory, respectively.
• ArkLib/Data/CodingTheory/ProximityGap/Folding.lean: The diff introduces several additions to Folding.lean:

1. A new theorem foldWord_k_1' provides an explicit formula for foldWord when k = 1 that avoids Lagrange interpolation, stated as a function-level version.
2. A noncomputable definition iteratedFoldWord implements an iterative version of folding, achieving k steps by repeatedly applying the k = 1 folding.
3. A lemma iteratedFoldWord_zero simplifies the definition for k = 0.
4. A private lemma div_two_pow_div_two is added as a helper for arithmetic on degrees.
5. A key theorem iteratedFoldWord_mem_code_of_mem_code establishes perfect completeness: if a word f belongs to a Reed–Solomon code of degree d, then its iteratedFoldWord (with a parameter α and under the conditions k ≤ n and 2^k ∣ d) belongs to the folded RS code of degree d / (2^k). The proof uses the existing foldWord_mem_code_of_mem_code and a helper subdomain_one_comp.

• ArkLib/Data/CodingTheory/ProximityGap/Folding/Multilinear.lean: This commit adds the file ArkLib/Data/CodingTheory/ProximityGap/Folding/Multilinear.lean, which provides an equivalent formulation of the folding completeness of Reed-Solomon codes in terms of multilinear polynomials, following Lemma 4.15 of [ACFY24].

It introduces:

• foldWord_eq_evalOnPoints_powAlgHom: a lemma showing that a single folding step of the foldWord can be expressed as evalOnPoints of a powAlgHom after a substitution that separates the first variable.
• iteratedFoldWord_eq_evalOnPoints_powAlgHom: the main theorem, establishing that the iteratedFoldWord after k folds equals evalOnPoints on the subdomain k of a powAlgHom applied to a g.1 composed with a substitution that replaces the first k variables by constants and shifts the remaining ones.
• Three private lemmas (substFun, aeval_substFun_comp, aeval_split_mem, aeval_substFun_mem) that handle the technical substitution and degree-restriction bookkeeping needed for the proof.

No sorry, admit, or other incomplete proofs are present.

The file depends on several imported modules for polynomial algebra, domain theory, and coding-theoretic foundations, and it operates in the ProximityGap namespace.

• ArkLib/Data/Domain/CosetFftDomain/Subdomain.lean: This diff adds several new lemmas and definitions to ArkLib/Data/Domain/CosetFftDomain/Subdomain.lean that establish relationships between evaluations on a smooth coset FFT domain and its subdomains. It introduces sqFoldMapGen, a generalized modular reduction map from Fin (2^n) to Fin (2^(n-i)). The main new result is evalOnPoints_pow_of_two_eq_evalOnPoints_subdomain, which relates ReedSolomon.evalOnPoints for a composed polynomial on the full domain to its evaluation on the subdomain, with a special case evalOnPoints_sq_eq_evalOnPoints_subdomain for squaring. Complementary lemmas subdomain_sqFoldMapGen_eq_pow_domain and sqFoldMapGen_eq_sqFoldMapGen_of_pow_apply_eq_pow_apply relate subdomain values to powers of the original domain. A subdomain_one_comp lemma shows that iterating subdomains corresponds to taking higher-index subdomains under an index identification, and a subdomain_zero_eq_self lemma states that the zeroth subdomain is itself.
• ArkLib/Data/MvPolynomial/EvenAndOdd.lean: This new file defines even-odd decompositions for multilinear polynomials over a field of characteristic not two. It defines private helpers substPlus and substMinus (substitutions of 1/-1 for the first variable) and uses them to define public functions even and odd on the subtype R⦃≤ 1⦄[X (Fin n)] (polynomials of degree ≤1 in each variable). It proves the main decomposition lemma even_and_odd_formula ((even p).1 + X₀*(odd p).1 = p.1) and a shifted version even_and_odd_formula', plus an evaluation lemma even_and_odd_eval. It then defines even_pred and odd_pred (projecting to degree-1 polynomials over Fin (n-1) by eliminating variable 0) and relates them to a power-algebra homomorphism powAlgHom via powAlgHom_eq_even_add_odd and powAlgHom_eq_even_add_odd_powAlgHom. All lemmas assume ¬CharP R 2 and that p lies in the degree‑≤‑1 restriction. The file contains no sorry or admit.

---

Last updated: 2026-07-10 12:04 UTC.

[alexanderlhicks]

AI-generated review. This review was produced by Codex and has not been written by a human reviewer. Every finding below was checked against exact head 2fa10aaa3e100bbbc24af3f6bd76d7efdc82b2eb, the referenced paper, and the current ArkLib interfaces.

Conclusion: changes are needed before this should land. The recurrence, univariate degree-bound theorem, and even/odd algebra are meaningful, axiom-clean progress, but the advertised multilinear result is only the full-rate m = n specialization of WHIR Claim 4.15, pp. 26–27. It does not yet formalize the paper's independent code parameter m ≤ n.

Validation performed

• Ran ./scripts/validate.sh at this exact SHA: all 4,050 Lean jobs and repository gates passed. I also refreshed GitHub checks on 2026-07-19; all reported checks pass.
• Ran #print axioms on the principal new fold/MLE declarations: only standard Lean/Mathlib axioms were reported, with no sorryAx.
• Compared the public statements to WHIR Definition 4.14 and Claim 4.15 and to ArkLib's existing ReedSolomon.smoothCode, mem_rs_code_iff_exists_mle, ProximityGap.foldWord, and proof-system Fold.fold_k surfaces.
• Tested integration against current main and the related PRs: this work overlaps #657's binary-fold insertion and places Reed–Solomon corollaries in a domain module, so semantic integration is required rather than a mechanical merge.

Required outcome

1. Generalize the MLE statement to independent m and n, with a paper-shaped smoothCode wrapper.
2. Preserve ArkLib's dependency direction by moving coding-theory corollaries out of CosetFftDomain/Subdomain.
3. Prove/document equivalence with the existing STIR/WHIR fold APIs and #657's explicit-root theorem.

Series-wide context: of the seven WHIR items directly targeted by PRs #534/#603/#616/#657 (Definition 4.14, Claim 4.15, Definitions 4.16–4.18, Claim 4.19, Claim 4.22), only Claim 4.19 is currently both paper-faithful and axiom-clean end-to-end. This PR advances Claim 4.15, but does not yet close it, and it does not close a numbered STIR result.

[alexanderlhicks]

AI-generated inline feedback — paper fidelity (blocking). Here g has variables Fin n, where the same n fixes the domain cardinality 2^n. I validated this against WHIR Claim 4.15, pp. 26–27: the paper starts from RS[F,L,m] with independent k ≤ m ≤ n and returns an (m-k)-variate MLE. Thus the present theorem covers only m = n. Please quantify m independently and add a paper-shaped wrapper starting from f ∈ ReedSolomon.smoothCode domain m; ArkLib's mem_rs_code_iff_exists_mle already exposes a Fin m witness. Add at least one test/example with m < n to prevent this conflation from returning.

[alexanderlhicks]

AI-generated inline feedback — layering (blocking for integration). I validated the import graph against current ArkLib: coding theory imports domain infrastructure, while this new import makes CosetFftDomain/Subdomain depend on ReedSolomon. Please retain only generic subdomain/power lemmas here and move ReedSolomon.evalOnPoints corollaries to Data/CodingTheory/ProximityGap/Folding/Multilinear.lean (or another coding-theory module). This also avoids the content conflict observed when stacking this PR after #603.

[alexanderlhicks]

AI-generated inline feedback — canonical fold API. I checked current ArkLib and the related heads: main already has ProximityGap.foldWord, the proof-system development has Fold.fold_k, and #657 adds an axiom-clean explicit-root binary theorem. Please prove the exact equivalence/migration lemma for iteratedFoldWord and make downstream Claims 4.20–4.23 use one canonical surface. WHIR Definition 4.14 defines the k-fold recursively, so two unbridged recurrences are not enough to establish faithful reuse.

[alexanderlhicks]

AI-generated inline feedback — proof documentation. The powers of two here are not coprime. I checked the proof immediately below: it cancels a common power-of-two factor using the divisibility relation. Please rewrite the comment to describe that cancellation; the present explanation states a false number-theoretic fact.