feat(SplitFold): add splitNth_eval_comp_pow evaluation lemma

[klausnat]

• Extract splitNth_eval_comp_pow from a local have in RoundConsistency.lean into a standalone lemma in SplitFold.lean
• Refactor RoundConsistency.lean to use the new lemma, removing duplication

First of 4 evaluation-level lemmas needed for #450.

[chatgpt-codex-connector]

Codex usage limits have been reached for code reviews. Please check with the admins of this repo to increase the limits by adding credits.
Credits must be used to enable repository wide code reviews.

[github-actions]

🤖 Gemini PR Summary

Mathematical Formalization

• Added splitNth_eval_comp_pow to SplitFold.lean, establishing the identity relating polynomial split components composed with $X^n$ to their evaluation at $x^n$.
• The implementation contains no sorry or admit placeholders.

Refactoring

• Refactored generalised_round_consistency_completeness in ArkLib/ProofSystem/Fri/RoundConsistency.lean to use the new lemma, eliminating a redundant local have block.
• This is the first of four evaluation-level lemmas planned for Add evaluation-level lemmas for splitNth and foldNth (even/odd decomposition) #450.

---

Statistics

Metric	Count
📝 Files Changed	2
✅ Lines Added	16
❌ Lines Removed	10

---

Lean Declarations

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

• lemma splitNth_eval_comp_pow {n : ℕ} [NeZero n] (f : 𝔽[X]) (x : 𝔽) (i : Fin n) : in ArkLib/Data/Polynomial/SplitFold.lean

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

🎨 **Style Guide Adherence**

Based on the provided style guide, here are the violations found in the diff:

• Line 327: ext e a
  • The variable e violates the Variable Conventions rule: m, n, k, ... : Natural numbers. (In this context, e represents a natural number index/exponent and should be n, m, or k).
  • The variable a violates the Variable Conventions rule: a, b, c, ... : Propositions. (The variable represents an element of a generic type/field, which should be x, y, or z).

---

📄 **Per-File Summaries**

• ArkLib/Data/Polynomial/SplitFold.lean: This change introduces the lemma splitNth_eval_comp_pow, which establishes an identity relating the composition of split polynomial components with $X^n$ to their evaluation at $x^n$. This new theorem bridges coefficient-level definitions with evaluation-level reasoning and contains no sorry placeholders.
• ArkLib/ProofSystem/Fri/RoundConsistency.lean: This change simplifies the proof of generalised_round_consistency_completeness by replacing a local helper lemma with the more general splitNth_eval_comp_pow theorem. It modifies existing proof logic without introducing new definitions or sorry placeholders.

---

Last updated: 2026-04-10 15:06 UTC.