Folding Polynomial definition and Fact 4.6 proof from STIR paper

[ElijahVlasov]

No description provided.

[github-actions]

🤖 Gemini PR Summary

Mathematical Formalization

• Bivariate Folding Polynomial: Defines foldingPolynomial, formalizing the existence and uniqueness of a bivariate polynomial $Q(X, Y)$ such that $f(Z) = Q(q(Z), Z)$, corresponding to Fact 4.6 (Proposition 6.3) of the STIR paper. Includes proofs for associated degree bounds and substitution properties.
• Polynomial Decomposition: Establishes a framework for decomposing polynomials into even and odd parts, bridging standard polynomial arithmetic with proximity protocol folding techniques.
• Generalized Splitting: Replaces localized splitNth definitions with a generalized polyFold API for consistent $n$-th degree decompositions.

FRI Protocol Integration

• Logic Refinement: Updates the FRI specification to use FoldingPolynomial.polyFold instead of the legacy foldNth implementation.
• Completeness Proofs: Simplifies generalised_round_consistency_completeness by leveraging Lagrange interpolation and the new polyFold API.
• Witness Verification: Expands the witness_lift lemma to establish rigorous degree bounds during FRI round transitions, ensuring soundness properties are maintained.

Refactoring & Generalization

• Universe Polymorphism: Updates bivariate polynomial implementations to use arbitrary universe levels (Type*) for broad semiring compatibility.
• API Ergonomics: Refactors round consistency checks in the ArkLib namespace to utilize function-based point representations rather than lists, increasing flexibility for evaluations in proofs.

Proof Status

• All definitions and lemmas, including the core foldingPolynomial logic and witness_lift proofs, are fully established. No sorry or admit placeholders are present in this PR.

---

Statistics

Metric	Count
📝 Files Changed	7
✅ Lines Added	1512
❌ Lines Removed	256

---

Lean Declarations

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

• lemma foldNth_zero {s : ℕ} {α : 𝔽} : foldNth (2 ^ s) 0 α = 0 in ArkLib/Data/Polynomial/SplitFold.lean
• lemma foldNth_degree_le' {n : ℕ} {f : 𝔽[X]} {α : 𝔽} [inst : NeZero n] : in ArkLib/Data/Polynomial/SplitFold.lean
• lemma foldNth_degree_le {n : ℕ} {f : 𝔽[X]} {α : 𝔽} [inst : NeZero n] : in ArkLib/Data/Polynomial/SplitFold.lean

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

• theorem folding_polynomial_deg_x {q f : F[X]} : in ArkLib/Data/Polynomial/FoldingPolynomial.lean
• lemma eq_zero_of_folding_polynomial_eq_zero {q f : F[X]} in ArkLib/Data/Polynomial/FoldingPolynomial.lean
• lemma folding_polynomial_eq_map_of_f_degree_lt_q_degree {q f : F[X]} in ArkLib/Data/Polynomial/FoldingPolynomial.lean
• lemma f_eq_evenPart_plus_x_oddPart {f : Polynomial F} : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• lemma evenPart_x_eval_eq {f : Polynomial F} {s : F} : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• lemma polyFold_eq_sum_of_splitNth {𝔽 : Type} [Field 𝔽] in ArkLib/Data/Polynomial/SplitFold.lean
• lemma folding_polynomial_deg_x_bound {q f : F[X]} {t : ℕ} in ArkLib/Data/Polynomial/FoldingPolynomial.lean
• lemma evenPart_even {f : Polynomial F} : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• lemma evenize_coeff {f : Polynomial F} {n : ℕ} : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• lemma oddPart_by_2 : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• lemma poly_fold_k_eq_2 {f : F[X]} {r : F} : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• lemma folding_polynomial_C_q {q : F} {f : F[X]} : in ArkLib/Data/Polynomial/FoldingPolynomial.lean
• def EvenPoly (f : Polynomial F) : Prop in ArkLib/Data/Polynomial/EvenAndOdd.lean
• lemma deevenize_evenize {f : Polynomial F} : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• theorem folding_polynomial_is_unique {q f : F[X]} {Q : F[X][Y]} in ArkLib/Data/Polynomial/FoldingPolynomial.lean
• lemma folding_polynomial_eq_sum_splitNth {𝔽 : Type} [Field 𝔽] in ArkLib/Data/Polynomial/SplitFold.lean
• lemma folded_poly_degree_bound {Q : F[X][Y]} {q : F[X]} {t : ℕ} in ArkLib/Data/Polynomial/FoldingPolynomial.lean
• lemma oddPart_even {f : Polynomial F} : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• lemma foldingPolynomial_C_f {f : F} {q : F[X]} : in ArkLib/Data/Polynomial/FoldingPolynomial.lean
• lemma substitution_property_of_folding_polynomial {q f : F[X]} : in ArkLib/Data/Polynomial/FoldingPolynomial.lean
• lemma even_poly_has_even_degree {f : F[X]} in ArkLib/Data/Polynomial/EvenAndOdd.lean
• lemma deevenize_zero : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• lemma eq_evenize_deevenize {f : Polynomial F} (hEven : EvenPoly f) : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• lemma evenPart_def : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• lemma folding_polynomial_is_the_reminder {q f : F[X]} : in ArkLib/Data/Polynomial/FoldingPolynomial.lean
• lemma evenPart_coeff {f : Polynomial F} {n : ℕ} : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• lemma deevenize_coeff {f : Polynomial F} {n : ℕ} : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• lemma polyFold_natDegree_le {f : F[X]} {k : ℕ} {r : F} : in ArkLib/Data/Polynomial/FoldingPolynomial.lean
• lemma oddPart_coeff {f : Polynomial F} {n : ℕ} : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• lemma evenize_eval {f : Polynomial F} {s : F} : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• lemma evenize_is_even {f : Polynomial F} : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• lemma evenize_eq_comp_x_squared {f : Polynomial F} : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• lemma foldingPolynomial_zero {q : F[X]} : in ArkLib/Data/Polynomial/FoldingPolynomial.lean
• lemma polyFold_zero_eq_zero {k : ℕ} {r : F} : in ArkLib/Data/Polynomial/FoldingPolynomial.lean
• lemma oddPart_def : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• lemma even_eval {f : Polynomial F} {s : F} (hEven : EvenPoly f) : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• lemma even_y_odd_eq_folding_polynomial {f : Polynomial F} : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• theorem folding_polynomial_is_unique' {q f : Polynomial F} {Q : Polynomial (Polynomial F)} in ArkLib/Data/Polynomial/FoldingPolynomial.lean
• lemma oddPart_x_eval_eq {f : Polynomial F} {s : F} : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• lemma evenPart_by_2 : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• lemma deevenize_comp_x_squared {f : Polynomial F} (hEven : EvenPoly f) : in ArkLib/Data/Polynomial/EvenAndOdd.lean
• theorem folding_polynomial_deg_y_bound {q f : F[X]} (h : 0 < q.degree) : in ArkLib/Data/Polynomial/FoldingPolynomial.lean

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

🎨 **Style Guide Adherence**

The provided code changes contain several violations of the style guide. Since there are more than 20 violations in total, they are grouped by rule below with representative examples.

Indentation and Spacing

• Rule: "Indentation: Use 2 spaces for indentation."
  • Count: ~45 violations.
  • Examples:
    • ArkLib/Data/Polynomial/EvenAndOdd.lean:41: 4 spaces used instead of 2.
    • ArkLib/Data/Polynomial/EvenAndOdd.lean:99: 4 spaces used for match block.
    • ArkLib/Data/Polynomial/FoldingPolynomial.lean:206: 10 spaces used for induction'.
• Rule: "Avoid parentheses where possible. ... [Delimiters]" (This includes avoiding extra spaces inside delimiters like [], ()).
  • Count: ~25 violations.
  • Examples:
    • ArkLib/Data/Polynomial/FoldingPolynomial.lean:123: [ Polynomial.eq_C_of_degree_le_zero h₁ ] contains unnecessary spaces inside brackets.
    • ArkLib/Data/Polynomial/FoldingPolynomial.lean:129: ( not_le_of_gt ( lt_of_lt_of_le ( Polynomial.degree_C_le ) h₃ ) ) contains excessive nesting and spaces inside parentheses.
• Rule: "Avoid empty lines inside definitions or proofs."
  • Count: 8 violations.
  • Examples:
    • ArkLib/Data/Polynomial/FoldingPolynomial.lean:159: Empty line within a proof.
    • ArkLib/ProofSystem/Fri/RoundConsistency.lean:150: Empty line with trailing spaces inside a proof.
• Rule: "Keep lines under 100 characters."
  • Count: 5 violations.
  • Examples:
    • ArkLib/Data/Polynomial/FoldingPolynomial.lean:354: Line exceeds 100 characters.
    • ArkLib/Data/Polynomial/FoldingPolynomial.lean:504: Line exceeds 100 characters.

Function and Binder Syntax

• Rule: "Prefer fun x ↦ ... over λ x, ...." (Standard mathlib convention uses ↦ for fun binders).
  • Count: 18 violations.
  • Examples:
    • ArkLib/Data/Polynomial/EvenAndOdd.lean:117: Uses fun n => instead of fun n ↦.
    • ArkLib/Data/Polynomial/FoldingPolynomial.lean:127: Uses fun h₃ h₄ => instead of fun h₃ h₄ ↦.

Tactic and Operator Formatting

• Rule: "Avoid using ; to separate tactics unless writing short, single-line tactic sequences." (Also used to mark unnecessary semicolons at line ends).
  • Count: 12 violations.
  • Examples:
    • ArkLib/Data/Polynomial/EvenAndOdd.lean:241: · symm ; apply hEven uses a semicolon to separate two distinct tactic calls.
    • ArkLib/Data/Polynomial/FoldingPolynomial.lean:154: rw [ Polynomial.div_def ]; uses a semicolon at the end of a line.
• Rule: "Place by at the end of the line preceding the tactic block."
  • Count: 8 violations.
  • Examples:
    • ArkLib/Data/Polynomial/EvenAndOdd.lean:72: := by is placed on its own line.
    • ArkLib/Data/Polynomial/FoldingPolynomial.lean:68: := followed by a line break before foldingPolynomialAux.
• Rule: "Place [operators] before a line break rather than at the start of the next line."
  • Count: 2 violations.
  • Line 78 & 80 of EvenAndOdd.lean: Commas are placed at the start of the next line.

Documentation and Naming

• Rule: "Use LaTeX for math: $ f(x) = y $" and "Use backticks for Lean names: `List.map`."
  • Count: 15 violations.
  • Examples:
    • ArkLib/Data/Polynomial/EvenAndOdd.lean:15: Math expression f = a_0 + ... not in LaTeX.
    • ArkLib/Data/Polynomial/EvenAndOdd.lean:17: Lean names evenPart and oddPart not in backticks.
• Rule: "Prop-valued Classes: Use UpperCamelCase. If the class is an adjective, use the Is prefix."
  • Line 86 of EvenAndOdd.lean: def EvenPoly describes an adjective property and should be IsEvenPoly.
• Rule: "Theorems and Proofs: snake_case" (applied to naming semantics).
  • Line 163 of EvenAndOdd.lean: really_glorious_lemma is non-descriptive and violates the naming dictionary logic.

---

📄 **Per-File Summaries**

• ArkLib.lean: This change updates the ArkLib library by importing new modules for even/odd polynomial decompositions and folding polynomials. It expands the library's polynomial API by making these components available in the main namespace.
• ArkLib/Data/Polynomial/Bivariate.lean: This change generalizes the type parameter F to arbitrary universe levels by updating its declaration to Type*. This ensures that the definitions in the file are compatible with semirings in any universe.
• ArkLib/Data/Polynomial/EvenAndOdd.lean: This file introduces new definitions and theorems for decomposing a polynomial into even and odd parts, establishing their basic properties and providing a bridge to the FoldingPolynomial framework used in FRI protocols.
• ArkLib/Data/Polynomial/SplitFold.lean: This PR refactors the file to integrate with a generalized folding framework by replacing the local foldNth definition and its properties with new theorems that relate splitNth decomposition to FoldingPolynomial.polyFold.
• ArkLib/ProofSystem/Fri/RoundConsistency.lean: Refactors the roundConsistencyCheck definition to represent points as a function rather than a list and significantly simplifies the proof of generalised_round_consistency_completeness by leveraging Lagrange.eq_interpolate and the FoldingPolynomial API.
• ArkLib/ProofSystem/Fri/Spec/SingleRound.lean: This file replaces the foldNth function with FoldingPolynomial.polyFold across the FRI round specification and significantly expands the proof of the witness_lift lemma to rigorously establish polynomial degree bounds. These changes modify existing definitions and proofs to align with the refined folding logic without introducing any sorry or admit placeholders.
• ArkLib/Data/Polynomial/FoldingPolynomial.lean: This file formalizes the existence and uniqueness of the bivariate folding polynomial $Q(X, Y)$ such that $f(Z) = Q(q(Z), Z)$, as described in Proposition 6.3 of Ben-Sasson and Sudan (2008). It introduces the foldingPolynomial definition, proves its associated degree bounds and substitution properties, and provides the polyFold function used in proximity protocols like FRI. The implementation is complete and contains no sorry placeholders.

---

Last updated: 2026-03-09 16:04 UTC.

[alexanderlhicks]

/review

External:
https://eprint.iacr.org/2020/654.pdf
https://eprint.iacr.org/2024/1586.pdf
https://eprint.iacr.org/2024/390.pdf
https://eprint.iacr.org/2023/1705.pdf

Internal:
ArkLib/Data/CodingTheory/
ArkLib/Data/Polynomial

Comments:
Please review for correctness with respect to ArkLib internals and the external reference papers (in particular STIR i.e.https://eprint.iacr.org/2024/390.pdf and WHIR i.e. https://eprint.iacr.org/2024/1586.pdf). Identify any possible improvements to the declarations to improve their accuracy and correctness.

[github-actions]

🤖 AI Review (with external context)

🤖 AI Review

Overall Summary:
Here is the synthesized Executive Summary for the Pull Request author:

1. TL;DR

The mathematical translation of FRI's polynomial splitting and folding mechanisms is structurally sound, seamlessly connecting to the uniqueness theorem and Mathlib's Lagrange API. However, the PR currently fails to compile due to a type mismatch and a missing import, and contains a critical mathematical edge case (missing a non-zero parameter hypothesis) that violates the preconditions of bivariate decomposition.

2. Checklist Coverage

Overall, the PR covers the core mathematical specification well, but reviewers flagged a few missing requirements and edge cases:

• ✅ Bivariate Polynomial Decomposition: Edge cases for constant/zero polynomials, homomorphic evaluations at (q(Z), Z), and uniqueness bounds are well-handled.
• ⚠️ Bivariate Polynomial Degrees: Fractional degree bounds safely use Nat division. Note that degreeX and natDegreeY return 0 for the zero polynomial (instead of -∞); while this didn't cause failures in the current diff, you must be careful when proving strict inequalities like deg_Y(Q) < deg(q).
• ❌ k-wise Polynomial Folding: The folding parameter requirement ($k > 0$) is correctly enforced in some files (SplitFold.lean, RoundConsistency.lean) but critically missing from the base definitions in FoldingPolynomial.lean.
• ❌ Equivalence of Split and Fold: While the sum-based splitNth representation is verified against the generic polynomial folding sum, the specific direct bridging lemma polyFold f k r = foldNth k f r was flagged as missing from FoldingPolynomial.lean.
• ✅ Even/Odd Decomposition: Successfully verified. oddPart is constructed precisely so that deevenize behaves mathematically as intended.

3. Critical Misformalizations

• Missing [NeZero k] Precondition (FoldingPolynomial.lean): The definition of polyFold and the lemma polyFold_natDegree_le currently allow $k = 0$. When $k = 0$, $X^k = 1$, which attempts to decompose against a constant polynomial. This mathematically violates the preconditions of Fact 4.6. You must add a [NeZero k] typeclass requirement to polyFold, mirroring the assumption already correctly utilized in SplitFold.lean.
• Type Mismatch in queryVerifier (SingleRound.lean): In the invocation of RoundConsistency.roundConsistencyCheck, the variable pts is passed as (List.get pts). List.get pts returns a function (Fin pts.length → F × F), whereas the consistency check strictly expects a List (F × F). Revert this to passing pts directly to fix the compilation error.
• Missing Equivalence Theorem (FoldingPolynomial.lean): To fully satisfy the specification checklist, you need to add a lemma explicitly proving polyFold f k r = foldNth k f r to bridge the sum-based split representation and the bivariate folding representation.

4. Key Lean 4 / Mathlib Issues

• Bad Simp Lemma Normal Form (EvenAndOdd.lean): The lemma @[simp] even_y_odd_eq_folding_polynomial uses X * X instead of X ^ 2 on the LHS. Because X ^ 2 is the standard normal form for polynomials in Mathlib, the simp lemma will fail to trigger automatically, forcing manual rw [sq] hacks downstream. Update the LHS to use X ^ 2.
• Missing Import (SingleRound.lean): The PR introduces FoldingPolynomial.polyFold into the round specification but forgets to import the FoldingPolynomial namespace at the top of the file, breaking compilation.
• Inconsistent Degree Bound Types (FoldingPolynomial.lean): In folding_polynomial_deg_y_bound, natDegreeY (which is of type ℕ) is compared against q.degree (which is WithBot ℕ). Standardize this to q.natDegree (with a hypothesis 0 < q.natDegree) to remain consistent with your other uniqueness lemmas.
• Shadowing and Redundant Variables (2 files affected: Bivariate.lean, RoundConsistency.lean): Explicit binders like {F : Type u} [Semiring F] in definitions are shadowing the identical variables already declared in the variable section block. This creates unnecessary verbosity and potential typeclass diamonds. Safely remove the explicit binders from definitions where they are already in scope.
• Unidiomatic Formatting (2 files affected: FoldingPolynomial.lean, RoundConsistency.lean): There are multiple instances of trailing semicolons at the end of tactics (e.g., by_cases hq : f.degree < q.degree ;) and trailing commas in rw blocks (e.g., rw [heq,]). These are remnants of Lean 3 / Coq style and should be removed.

5. Overall Verdict

Changes Requested

---

📄 **Review for `ArkLib.lean`**

Verdict: Approved

Checklist Verification:

• ⚠️ Bivariate Polynomial Decomposition (Fact 4.6 / BS08): Cannot be determined from the diff. The diff only adds the import ArkLib.Data.Polynomial.FoldingPolynomial statement to the main module ArkLib.lean, but the actual file contents containing the formalization are not included in the provided diff.
• ⚠️ Bivariate Polynomial Degrees (deg_X and deg_Y): Cannot be determined from the diff for the same reason.
• ⚠️ k-wise Polynomial Folding (polyFold): Cannot be determined from the diff.
• ⚠️ Equivalence of Split and Fold: Cannot be determined from the diff.
• ⚠️ Even/Odd Decomposition and Deevenization: Cannot be determined from the diff.

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `ArkLib/Data/Polynomial/Bivariate.lean`**

Verdict: Needs Minor Revisions

Checklist Verification:

• ⚠️ Bivariate Polynomial Decomposition: Not addressed or modified in this diff.
• ⚠️ Bivariate Polynomial Degrees: The definitions degreeX and natDegreeY currently return 0 for the zero polynomial (via Polynomial.natDegree and Finset.sup), rather than -∞. This is flagged as a [Major] issue in the checklist because it invalidates strict inequalities like deg_Y(Q) < deg(q). However, since these definitions are not modified by the current diff, this is just noted for context and is not scored as a defect in this review.
• ⚠️ k-wise Polynomial Folding: Not addressed or modified in this diff.
• ⚠️ Equivalence of Split and Fold: Not addressed or modified in this diff.
• ⚠️ Even/Odd Decomposition and Deevenization: Not addressed or modified in this diff.

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:

• Shadowing Variables: At the top of the section, you successfully updated the global variables to be universe-polymorphic with variable {F : Type u} [Semiring F]. However, definitions like coeff, weightedDegree, natWeightedDegree, and rootMultiplicity₀ still explicitly bind {F : Type u} [Semiring F] in their signatures. This shadows the section variables and makes the signatures unnecessarily verbose. You can safely simplify these definitions by dropping the redundant explicit binders:

  def coeff (f : F[X][Y]) (i j : ℕ) : F := (f.coeff j).coeff i

  (Note: rootMultiplicity requires a stronger [CommSemiring F] assumption, so it will still need its own instance binder, but you can still omit {F : Type u}).
• Variable / Universe Naming Clash: In weightedDegree and natWeightedDegree, the parameters are named (u v : ℕ). While Lean 4 successfully disambiguates the term variable u from the universe level u (introduced via universe u), it can be slightly confusing for human readers. Consider using different parameter names for the degrees to avoid this visual clash.

📄 **Review for `ArkLib/Data/Polynomial/EvenAndOdd.lean`**

Verdict: Changes Requested

Checklist Verification:

• Bivariate Polynomial Decomposition (Fact 4.6 / BS08): ⚠️ Cannot be fully evaluated from this diff alone as the general definitions (foldingPolynomial, polyFold) reside in a different file (FoldingPolynomial.lean). However, the application of the uniqueness theorem for $q(X) = X^2$ in this diff is correctly done.
• Bivariate Polynomial Degrees (deg_X and deg_Y): ✅ Verified. The fractional degree bound for $q(X)=X^2$ is correctly implemented using Nat division (f.natDegree / 2).
• k-wise Polynomial Folding (polyFold): ✅ Verified. The parameter $k=2$ in poly_fold_k_eq_2 is strictly positive. The representation mathematically aligns with evaluating the outer variable $Y$ at $r$.
• Equivalence of Split and Fold: ✅ Verified for $n=2$ via even_y_odd_eq_folding_polynomial. The required degree bounds for the uniqueness theorem are correctly established in deevenize_natDegree_le_natDegree_div_2.
• Even/Odd Decomposition and Deevenization: ✅ Verified. oddPart is constructed such that $f(X) = E(X^2) + X \cdot O(X^2)$, meaning oddPart f is an even polynomial containing the shifted coefficients. Consequently, deevenize behaves mathematically exactly as intended when applied to oddPart f.

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:

• Bad Simp Lemma Normal Form: In @[simp] lemma even_y_odd_eq_folding_polynomial, the LHS uses X * X instead of X ^ 2. In Lean 4, X ^ 2 is the standard normal form for polynomials. Because the LHS is not in normal form, the simp lemma will fail to trigger automatically on normalized expressions.
  This issue forces a manual un-simplification in the proof of poly_fold_k_eq_2:

  have h : (X : F[X]) ^ 2 = X * X := by ring
  rw [h]
  simp -- Now it finally triggers

  Fix: Update the LHS of even_y_odd_eq_folding_polynomial to use (X ^ 2). This will allow you to completely remove the have h : ... := by ring; rw [h] hack in poly_fold_k_eq_2.

Nitpicks:

• Mathematical Readability of Bivariate Variables: In the RHS of even_y_odd_eq_folding_polynomial, the expression X * (C (deevenize <| oddPart f)) uses X (via Polynomial.X) for the outer polynomial variable. While this is type-theoretically correct (since the type is Polynomial (Polynomial F)), mathematically this represents the second indeterminate $Y$. To a reader, seeing X * C(...) looks like $X \cdot O(X)$ rather than the intended $Y \cdot O(X)$. Consider using a local notation like local notation "Y" => Polynomial.X to make the theorem statement align with the math.
• Unidiomatic Proof Script: If you ever need to rewrite powers to multiplications elsewhere, prefer using rw [sq] or rw [pow_two] instead of the clunky have h : ... = ... := by ring; rw [h] pattern.

📄 **Review for `ArkLib/Data/Polynomial/FoldingPolynomial.lean`**

Verdict: Changes Requested

Checklist Verification:

• ✅ Verify handling of edge case q constant or zero: Handled correctly. foldingPolynomialAux safely defaults to map C f when q.degree ≤ 0.
• ✅ Proper ring homomorphism for evaluation at (q(Z), Z): substitution_property_of_folding_polynomial correctly leverages Q.map (compRingHom q) and .eval X to represent this substitution mathematically.
• ✅ Uniqueness lemma strictly bounds equality: Both folding_polynomial_is_unique and folding_polynomial_is_unique' assert strict equality Q = foldingPolynomial q f given the bounds.
• ✅ Definitions of degreeX and natDegreeY handle zero correctly: Handled successfully via natDegree yielding 0 for the zero polynomial.
• ✅ Fractional degree bound uses integer division: f.natDegree / q.natDegree safely utilizes Nat division (where x / 0 = 0).
• ❌ Verify k > 0 is assumed for folding: The definition of polyFold and the lemma polyFold_natDegree_le do not require k > 0 (or [NeZero k]). If k = 0, q(X) = X^0 = 1, making it a constant polynomial, which mathematically violates the preconditions of the bivariate decomposition.
• ✅ Fold aligns with substituting r into Y: The operation .eval (C r) correctly evaluates the outer variable Y at the constant r, yielding the expected univariate folded polynomial in X.
• ❌ Equivalence of Split and Fold: The PR does not contain a theorem establishing the formal equivalence between polyFold (the bivariate formulation) and foldNth / splitNth (the sum-based representation from SplitFold.lean).
• ⚠️ Even/Odd Decomposition: Not applicable to this file directly.

Critical Misformalizations:

• Missing Equivalence of Split and Fold: The formalization checklist specifically asks to check the equivalence between the sum-based split representation and the bivariate folding polynomial. This PR does not include any theorem linking polyFold to foldNth (from SplitFold.lean). You need to add a lemma proving polyFold f k r = foldNth k f r to bridge these two representations, which is a core step for verifying FRI correctness.
• Missing [NeZero k] Assumption in polyFold: The definition of polyFold and polyFold_natDegree_le allow k = 0. When k = 0, X^k = 1, which means the folding operation attempts to decompose against a constant polynomial. Although Lean's natural division trivially makes the bound f.natDegree / 0 = 0 hold, this mathematically violates the preconditions of bivariate decomposition (Fact 4.6). You should add a [NeZero k] typeclass requirement to polyFold, mirroring the assumption already present on foldNth.

Lean 4 / Mathlib Issues:

• Inconsistent Degree Bounds Comparison: In folding_polynomial_deg_y_bound, the statement compares natDegreeY (which is ℕ) with q.degree (which is WithBot ℕ):
  natDegreeY (foldingPolynomial q f) < q.degree.
  While Lean allows this via coercion, it is unidiomatic and inconsistent with your other lemmas (e.g., folded_poly_degree_bound and folding_polynomial_is_unique) which strictly compare ℕ with ℕ using q.natDegree. Changing this to q.natDegree (and the hypothesis to 0 < q.natDegree) will standardize your degree boundaries.

Nitpicks:

• Typo in Lemma Names: The lemmas satisfies_composition_property_implies_is_the_reminder and folding_polynomial_is_the_reminder contain a typo: reminder should be spelled remainder.
• Trailing Semicolons: The proofs contain numerous trailing semicolons (e.g., by_cases hq : f.degree < q.degree ;). This is a remnant of Lean 3 / Coq style and is unidiomatic in Lean 4. You can safely remove them.
• Spacing in Parentheses: Spaces inside parentheses, such as ( Nat.pos_of_ne_zero _ ), are not standard in Lean 4 formatting. Prefer (Nat.pos_of_ne_zero _).
• Inconsistent Type Notation: In folding_polynomial_is_unique', the types are written explicitly as Polynomial F and Polynomial (Polynomial F). For consistency with the rest of the file, consider using the local notations F[X] and F[X][Y].

📄 **Review for `ArkLib/Data/Polynomial/SplitFold.lean`**

Verdict: Approved

Checklist Verification:

• Equivalence of Split and Fold: ✅ The lemma folding_polynomial_eq_sum_splitNth successfully formally links the generic FoldingPolynomial.foldingPolynomial with the explicit algebraic sum over splitNth f n i.
• Degree Bounds of Split: ✅ The proof of folding_polynomial_eq_sum_splitNth explicitly verifies the strict degree bounds required by the uniqueness theorem. It utilizes natDegree_sum_le_of_forall_le to bound degreeX by f.natDegree / n (via splitNth_degree_le), and proves natDegreeY < n strictly using Nat.lt_of_le_pred and omega.
• k-wise Polynomial Folding (polyFold): ✅ The lemma polyFold_eq_sum_of_splitNth verifies that polyFold f n r corresponds exactly to substituting r into the folded polynomial to yield the univariate sum ∑ i, C (r ^ i.val) * splitNth f n i. Additionally, the assumption [inst : NeZero n] enforces that the folding parameter $n > 0$, handling the degenerate edge case safely.
• Other items: ⚠️ Items pertaining to Even/Odd Decomposition and handling of constant polynomials inside FoldingPolynomial.lean are outside the scope of this diff, though the dependencies used here behave safely.

Critical Misformalizations:
None. The translation of the FRI polynomial splitting and folding mechanisms into Lean perfectly aligns with the mathematical definitions described in STIR/WHIR, and seamlessly connects them to the uniqueness theorem.

Lean 4 / Mathlib Issues:
None. The use of the @[simp] attribute is idiomatic here (unrolling an opaque algorithm into a computable sum), and typeclass assumptions ([Field 𝔽], [NeZero n]) are appropriate and sound.

Nitpicks:

1. Explicit Instance Passing: In rw [splitNth_def (f := f) (inst := inst)], passing (inst := inst) is slightly unidiomatic. Because [NeZero n] is already in the local context, typeclass resolution will infer it automatically. You can just write rw [splitNth_def (f := f)].
2. Redundant Braces in by block: The expression apply Nat.lt_of_le_pred (by { apply Nat.zero_lt_of_ne_zero; aesop }) uses unnecessary curly braces and tactics. It can be simplified down to apply Nat.lt_of_le_pred (by exact Nat.pos_of_neZero n) or similar, since n > 0 is an immediate consequence of NeZero n.
3. conv Block Verbosity: In polyFold_eq_sum_of_splitNth, the conv block used to rewrite mul_comm under the sum binder is perfectly valid, but slightly heavy. A simple simp_rw [mul_comm] would also achieve the same result compactly.

📄 **Review for `ArkLib/ProofSystem/Fri/RoundConsistency.lean`**

Verdict: Approved

Checklist Verification:

• ✅ Bivariate Polynomial Decomposition (Fact 4.6 / BS08): The code correctly mirrors the mathematical evaluation properties. The substitution of the challenge into the folding polynomial's second variable evaluates precisely to (polyFold f n γ).eval (s₀ ^ n).
• ✅ k-wise Polynomial Folding (polyFold): The folding parameter n is strictly required to be non-zero via the [NeZero n] typeclass assumption. This correctly enforces the bounds and prevents the trivial $X^0 = 1$ edge case from violating the bivariate decomposition preconditions.
• ✅ Equivalence of Split and Fold: The proof explicitly rewrites using polyFold_eq_sum_of_splitNth. This successfully bridges the formal mathematical equivalence between the sum-based split representation ∑ i, γ^i * splitNth f n i and the bivariate polyFold.

Critical Misformalizations:
None. The formalization of the completeness of the FRI round consistency check is mathematically sound. The transition from lists to indexed functions (Fin n → 𝔽 × 𝔽) correctly tracks vector dimension through the type system and perfectly aligns with Mathlib's Lagrange API.

Lean 4 / Mathlib Issues:
None. The removal of the ad-hoc poly_eq_of lemma in favor of Mathlib's Lagrange.eq_interpolate is a great idiomatic improvement that drastically simplified the code. The conv tracking and Eq.trans manual bridging are expertly written.

Nitpicks:

• Trailing comma in rw: Around line 125, the code contains rw [heq,]. While Lean 4's rwRuleSeq parser technically accepts an optional trailing comma, it is non-standard style and should be cleaned up to rw [heq].
• Diamond Potential: This is pre-existing, but roundConsistencyCheck includes both [CommSemiring 𝔽] [NoZeroDivisors 𝔽] from the module's variable block and an explicit [Field 𝔽] in its own signature. This can cause typeclass diamonds (though harmless here since it's just a definition). Notice how in generalised_round_consistency_completeness, you successfully bypassed this by re-binding {𝔽 : Type} to shadow the section variable and drop the redundant semiring instances. It is worth doing the same for the definition if you experience unification issues downstream.

📄 **Review for `ArkLib/ProofSystem/Fri/Spec/SingleRound.lean`**

Verdict: Changes Requested

Checklist Verification:

• k-wise Polynomial Folding (polyFold)
  • ✅ Verify folding parameter is positive: The folding parameter k is supplied as 2 ^ (s i).1 (and similar variants). Because s i has type ℕ+, its value is ≥ 1, making the folding parameter at least 2. This naturally satisfies the precondition k > 0.
  • ⚠️ Check folded polynomial evaluation aligns: The PR replaces foldNth with FoldingPolynomial.polyFold, but the definition of polyFold is not included in this diff or the provided imports, meaning its mathematical evaluation logic cannot be fully verified in the scope of this file.

(Other checklist items are not applicable to this specific file's changes).

Critical Misformalizations:

• Type Mismatch in queryVerifier: In the invocation of RoundConsistency.roundConsistencyCheck, the variable pts (which is explicitly constructed and typed as List (F × F) just lines prior) is passed as (List.get pts). In Lean 4, List.get pts returns a function of type Fin pts.length → F × F, whereas roundConsistencyCheck strictly expects a List (F × F). This will result in a compilation error (expected List (F × F), found Fin pts.length → F × F).
  Correction: Revert to passing pts directly:

  guard (RoundConsistency.roundConsistencyCheck x₀ pts β)

Lean 4 / Mathlib Issues:

• Missing Import for FoldingPolynomial: The PR introduces FoldingPolynomial.polyFold and FoldingPolynomial.polyFold_natDegree_le in witness_lift, foldProver, and finalFoldProver. However, the FoldingPolynomial namespace is not imported at the top of the file (the current imports still reference the old ArkLib.Data.Polynomial.SplitFold). You must add the correct import (e.g., import ArkLib.Data.Polynomial.Folding) so the file can compile.
• Good Fix: The removal of sorry in queryCodeword and replacement with by omega perfectly closes an incomplete proof.

Nitpicks:

• The updated proof of witness_lift is quite dense and relies on heavy manual index arithmetic. Once the FoldingPolynomial API is fully integrated, consider extracting the degree bound logic into a dedicated lemma (e.g., Witness.polyFold_mem) to keep the FRI round specification declarative and clean.

[alexanderlhicks]

I haven't gone through the current draft yet, but just as a sanity check: #363 was merged around the time you opened this PR and affects definitions for relHammingBall and closeCodewordsRel.

[ElijahVlasov]

I haven't gone through the current draft yet, but just as a sanity check: #363 was merged around the time you opened this PR and affects definitions for relHammingBall and closeCodewordsRel.

This draft is not affected by that PR. Here we don't do any information theory, only polynomial stuff.