feat(multivariate): add sumcheck bridge operations

[codygunton]

Draft status

This draft now carries the reusable CompPoly side of the ArkLib Sumcheck integration. The earlier placeholder/docs-only shape has been replaced with the actual API ArkLib needs.

What changed

• Adds CompPoly.Multivariate.Sumcheck.
• Provides computable CMvPolynomial operations for Sumcheck:
  • partialEvalFirst / partialEvalLast
  • sumOverLast / sumAllButFirst
  • toUnivariate / roundPoly
• Proves evaluation correctness and degree-bound preservation lemmas used by ArkLib.
• Exports the new module from CompPoly.lean.
• Keeps ArkLib-specific degree-bounded wrappers out of CompPoly.

Relationship to ArkLib

ArkLib draft PR Verified-zkEVM/ArkLib#524 now depends on this branch by pinning lakefile.toml to codygunton/CompPoly@2ebbaac3fcabf490698f9d940f8c28d26a592f1e. That fork dependency is intentional while both PRs are drafts. After this PR lands in CompPoly, the ArkLib branch should be repinned back to Verified-zkEVM/CompPoly at the merged commit.

Validation

• lake build CompPoly.Multivariate.Sumcheck
• lake build CompPoly

[github-actions]

🤖 PR Summary

Mathematical Formalization

• CompPoly/Multivariate/Sumcheck.lean: implements core operations for sumcheck protocols, including partial evaluation, finite-domain summation, and degree preservation.
• Establishes multivariate-to-univariate bridge theorems required for individual sumcheck protocol rounds.
• Note: Discrepancy detected—while the PR body describes this as a "staging placeholder," the draft summary indicates that partial evaluation and degree preservation implementations are complete with no sorry placeholders.

Documentation

• docs/wiki/arklib-sumcheck-bridge.md: details the motivation for upstreaming polynomial lemmas from ArkLib.
• Updates the central wiki README with architectural requirements for the sumcheck bridge API.
• Outlines intended API surface for bind₁, fromCMvPolynomial, and CPolynomial constant ring hom helpers.

Infrastructure

• Integrates the sumcheck module into the CompPoly.lean entry point.
• Relocates degree preservation and summation logic from downstream implementations to the core library to support multiple sumcheck variants.

---

Statistics

Metric	Count
📝 Files Changed	4
✅ Lines Added	718
❌ Lines Removed	0

---

Lean Declarations

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

• theorem sumAllButFirst_degreeOf_zero_le [Nontrivial R] {deg : ℕ} (D : Fin m → R) : in CompPoly/Multivariate/Sumcheck.lean
• theorem roundPoly_eval (D : Fin m → R) (k : ℕ) (p : CMvPolynomial (k + 1) R) (x : R) : in CompPoly/Multivariate/Sumcheck.lean
• def sumAllButFirst (D : Fin m → R) : (k : ℕ) → CMvPolynomial (k + 1) R → CMvPolynomial 1 R in CompPoly/Multivariate/Sumcheck.lean
• def partialEvalLast (a : R) (p : CMvPolynomial (n + 1) R) : CMvPolynomial n R in CompPoly/Multivariate/Sumcheck.lean
• theorem partialEvalLast_degreeOf_le [Nontrivial R] {deg : ℕ} (a : R) in CompPoly/Multivariate/Sumcheck.lean
• def roundPoly (D : Fin m → R) (k : ℕ) (p : CMvPolynomial (k + 1) R) : CPolynomial R in CompPoly/Multivariate/Sumcheck.lean
• private lemma partialEvalLast_subst_degreeOf_le [Nontrivial R] (a : R) in CompPoly/Multivariate/Sumcheck.lean
• theorem sumAllButFirst_eval (D : Fin m → R) : in CompPoly/Multivariate/Sumcheck.lean
• def sumOverLast (D : Fin m → R) (p : CMvPolynomial (n + 1) R) : CMvPolynomial n R in CompPoly/Multivariate/Sumcheck.lean
• theorem toUnivariate_toPoly (p : CMvPolynomial 1 R) : in CompPoly/Multivariate/Sumcheck.lean
• private lemma partialEvalFirst_subst_degreeOf_le [Nontrivial R] (a : R) in CompPoly/Multivariate/Sumcheck.lean
• theorem sumOverLast_degreeOf_zero_le [Nontrivial R] {deg : ℕ} (D : Fin m → R) in CompPoly/Multivariate/Sumcheck.lean
• def partialEvalFirst (a : R) (p : CMvPolynomial (n + 1) R) : CMvPolynomial n R in CompPoly/Multivariate/Sumcheck.lean
• theorem partialEvalLast_eval (a : R) (p : CMvPolynomial (n + 1) R) (v : Fin n → R) : in CompPoly/Multivariate/Sumcheck.lean
• private lemma partialEvalFirst_eval₂_degreeOf_le [Nontrivial R] {deg : ℕ} in CompPoly/Multivariate/Sumcheck.lean
• theorem sumOverLast_eval (D : Fin m → R) (p : CMvPolynomial (n + 1) R) (v : Fin n → R) : in CompPoly/Multivariate/Sumcheck.lean
• theorem toUnivariate_natDegree_le {deg : ℕ} in CompPoly/Multivariate/Sumcheck.lean
• private lemma partialEvalFirst_eval₂_monomial_degreeOf_le [Nontrivial R] {deg : ℕ} in CompPoly/Multivariate/Sumcheck.lean
• def CRingHom : R →+* CPolynomial R where in CompPoly/Multivariate/Sumcheck.lean
• theorem toUnivariate_eval (p : CMvPolynomial 1 R) (x : R) : in CompPoly/Multivariate/Sumcheck.lean
• private lemma partialEvalLast_eval₂_monomial_degreeOf_le [Nontrivial R] {deg : ℕ} in CompPoly/Multivariate/Sumcheck.lean
• theorem roundPoly_natDegree_le {deg : ℕ} (D : Fin m → R) {k : ℕ} in CompPoly/Multivariate/Sumcheck.lean
• private def snocFunEquiv (k m : ℕ) : ((Fin k → Fin m) × Fin m) ≃ (Fin (k + 1) → Fin m) where in CompPoly/Multivariate/Sumcheck.lean
• private lemma partialEvalLast_eval₂_degreeOf_le [Nontrivial R] {deg : ℕ} in CompPoly/Multivariate/Sumcheck.lean
• theorem fromCMvPolynomial_bind₁ {m : ℕ} in CompPoly/Multivariate/Sumcheck.lean
• theorem partialEvalFirst_eval (a : R) (p : CMvPolynomial (n + 1) R) (v : Fin n → R) : in CompPoly/Multivariate/Sumcheck.lean
• theorem partialEvalFirst_degreeOf_le [Nontrivial R] {deg : ℕ} (a : R) in CompPoly/Multivariate/Sumcheck.lean
• def toUnivariate (p : CMvPolynomial 1 R) : CPolynomial R in CompPoly/Multivariate/Sumcheck.lean

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

Style and Naming Guidelines

• Naming Conventions: The definition CRingHom (line 31) uses UpperCamelCase. According to the project guidelines for functions and terms, it should use lowerCamelCase (e.g., cRingHom).
• Syntax and Formatting:
  • The code consistently uses the => arrow for anonymous functions (e.g., lines 71, 107, 137, 240). The guidelines specify a preference for the ↦ syntax (fun x ↦ ...).
  • Line Length: Line 600 reaches the 100-character limit. The guidelines request that lines be kept under 100 characters.
  • Copyright Year: The file header in CompPoly/Multivariate/Sumcheck.lean (line 2) lists the copyright year as 2026, which appears to be a typographical error.
  • Authorship: The header lists ArkLib Contributors. Ensure this aligns with project policy, as the guidelines suggest the format Author Name.

Module Layout and Documentation

• Wiki Updates: The PR correctly adheres to the Pull Request Guidelines by updating docs/wiki/README.md and providing a new documentation page (docs/wiki/arklib-sumcheck-bridge.md) to reflect the changes in repo structure and the addition of the sumcheck bridge API.
• Docstrings: All new definitions and major theorems in CompPoly/Multivariate/Sumcheck.lean include appropriate docstrings as required by the Documentation Standards.
• File Placement: The addition of CompPoly/Multivariate/Sumcheck.lean is consistent with the project's organization of bridge layers and multivariate operations.

---

📄 **Per-File Summaries**

• CompPoly.lean: This change adds an import for the sumcheck protocol module to the CompPoly.lean file, integrating multivariate sumcheck functionality into the broader library.
• CompPoly/Multivariate/Sumcheck.lean: This new file implements computable multivariate polynomial operations for sumcheck protocols, including partial evaluation, finite-domain summation, and conversion to univariate polynomials. It introduces several definitions and theorems proving that these operations correctly implement evaluation and preserve degree bounds, with no sorry placeholders used.
• docs/wiki/README.md: The docs/wiki/README.md file has been updated to include references to documentation for the ArkLib Sumcheck bridge. These additions document the upstream API requirements necessary for ArkLib's interaction-native Sumcheck implementation.
• docs/wiki/arklib-sumcheck-bridge.md: This document outlines the design and motivation for a reusable CompPoly API bridge intended to support the ArkLib Sumcheck formalization by upstreaming lemmas related to polynomial substitution, degree bounds, and summation. It details the specific candidate facts required to simplify downstream protocol definitions and manage library dependencies effectively.

---

Last updated: 2026-05-27 18:01 UTC.

[codygunton]

Superseded by #241, which includes this Sumcheck.lean content plus the DegreeBound predicates it builds on. The wiki docs here aren't needed. Closing in favor of #241; the placement/naming of these facts within CompPoly will be revisited separately.