feat(SplitFold): add even/odd evaluation lemmas for splitNth

[klausnat]

Motivation

In this PR we add evaluation-level lemmas relating splitNth, to connect the spec to FRI-style folding, where the even/odd split shows up as f(x) vs f(-x).

Changes

Adds three lemmas (n = 2 specialization):

• splitNth_two_eval is reusable pointwise even/odd decomposition.
• splitNth_two_eval_add
• splitNth_two_eval_sub

Built on the existing splitNth_eval_comp_pow.

Notes

As for fourth lemma from the issue #450, foldNth_two_eval, we should first define foldNth
(mentioned in the module docstring, but not defined).

Solves partially #450

[github-actions]

🤖 PR Summary

Mathematical Formalization

• Adds $n=2$ evaluation lemmas splitNth_two_eval, splitNth_two_eval_add, and splitNth_two_eval_sub to formalize even/odd polynomial decomposition.
• Connects splitNth specifications to FRI-style folding by relating polynomial evaluations at $x$ and $-x$.
• Extends the splitNth_eval_comp_pow framework to facilitate specialized use cases in proof protocols.

Refactoring

• Performs minor stylistic and formatting improvements in ArkLib/Data/Polynomial/SplitFold.lean.

---

Statistics

Metric	Count
📝 Files Changed	1
✅ Lines Added	28
❌ Lines Removed	7

---

Lean Declarations

✏️ **Added:** 3 declaration(s)

• lemma splitNth_two_eval_add {𝔽 : Type} [CommRing 𝔽] (f : 𝔽[X]) (x : 𝔽) : in ArkLib/Data/Polynomial/SplitFold.lean
• lemma splitNth_two_eval_sub {𝔽 : Type} [CommRing 𝔽] (f : 𝔽[X]) (x : 𝔽) : in ArkLib/Data/Polynomial/SplitFold.lean
• lemma splitNth_two_eval {𝔽 : Type} [CommSemiring 𝔽] (f : 𝔽[X]) (y : 𝔽) : in ArkLib/Data/Polynomial/SplitFold.lean

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

Style and Naming Guidelines

• Indentation: The theorem declarations for the newly added lemmas (splitNth_two_eval, splitNth_two_eval_add, and splitNth_two_eval_sub) use 4-space indentation for the theorem assertion and 6-space indentation for continuation lines. According to the style guide and the existing patterns in the file, indentation increments should be 2 spaces.
• Documentation Standards: The docstrings for the new lemmas use backticks for mathematical notation (e.g., `n = 2` and `f(x) + f(-x) = 2 · f₀(x²)`). The project's Documentation Standards require the use of LaTeX for math expressions (e.g., $ n = 2 $, $ f(x) + f(-x) = 2 \cdot f_0(x^2) $).

---

📄 **Per-File Summaries**

• ArkLib/Data/Polynomial/SplitFold.lean: This update introduces new theorems for polynomial evaluation in the specific case of $n=2$ splitting, characterizing the even and odd components of a polynomial. The changes also include minor formatting cleanups in existing proofs and do not introduce any sorry or admit placeholders.

---

Last updated: 2026-06-08 07:53 UTC.

[ElijahVlasov]

Is this in any way better than what was done here long ago (and was removed):

ArkLib/ArkLib/Data/Polynomial/EvenAndOdd.lean

Line 451 in 181ae87

lemma poly_fold_k_eq_2 {f : F[X]} {r : F} :

?

[ElijahVlasov]

Is this in any way better than what was done here long ago (and was removed):

ArkLib/ArkLib/Data/Polynomial/EvenAndOdd.lean

Line 451 in 181ae87

lemma poly_fold_k_eq_2 {f : F[X]} {r : F} :

?

And here:

ArkLib/ArkLib/Data/Polynomial/EvenAndOdd.lean

Line 407 in 181ae87

lemma even_y_odd_eq_folding_polynomial {f : Polynomial F} :

[klausnat]

Thanks @ElijahVlasov

But file EvenAndOdd was removed because SplitFold replaced it.

In this PR I am adding eval-lemmas in SplitFold (filling the gap).

also it was built on a different abstraction (evenPart/oddPart/evenize) rather than splitNth, which is what SplitFold.lean uses today.

Also there were no f(x) ± f(-x) evaluation identities, it had only lower-level pieces (even_eval, evenPart_x_eval_eq).

in my PR they are in the FRI-ready form on the current splitNth API, and SplitFold.lean had no
evaluation-level lemmas at all before.

[aryaethn]

These three even/odd lemmas are exactly what #450 needs. Two things that might help move it along:

1. Looks like it needs a rebase. The diff predates a recent change to this file — main now uses Polynomial.eval_finsetSum (the eval_finset_sum spelling in the diff context no longer exists), so it likely won't merge cleanly as-is. The few whitespace-only reversions on otherwise untouched lines could also be dropped to keep the diff focused on the new lemmas.

2. The remaining #450 item (foldNth_two_eval) follows directly from these. The foldNth named in the module docstring is realized by FoldingPolynomial.polyFold — polyFold_eq_sum_of_splitNth already gives polyFold f n r = ∑ i, C (rⁱ) * splitNth f n i — so the main result composes with your splitNth_two_eval_add / splitNth_two_eval_sub. I checked this compiles on top of your branch (current main, [Field 𝔽]):

lemma foldNth_two_eval (f : 𝔽[X]) (x β : 𝔽) (hx : x ≠ 0) (h2 : (2 : 𝔽) ≠ 0) :
    (FoldingPolynomial.polyFold f 2 β).eval (x ^ 2) =
      (f.eval x + f.eval (-x) + β * (f.eval x - f.eval (-x)) * x⁻¹) * (2 : 𝔽)⁻¹ := by
  rw [polyFold_eq_sum_of_splitNth, eval_finsetSum, Fin.sum_univ_two]
  simp only [Fin.val_zero, Fin.val_one, pow_zero, pow_one, eval_mul, eval_C, one_mul]
  rw [splitNth_two_eval_add f x, splitNth_two_eval_sub f x]
  field_simp

Happy to send this as a follow-up PR once yours lands, or you're welcome to fold it in here — whichever you prefer.

(Minor, optional: the module docstring lists foldNth n f α under "Main definitions", but there's no such def yet — only polyFold. Might be worth adding a foldNth alias or adjusting the docstring so the name resolves.)