feat(multivariate): add degree-bound and partial-evaluation primitives#241
feat(multivariate): add degree-bound and partial-evaluation primitives#241codygunton wants to merge 3 commits into
Conversation
🤖 PR SummaryMultivariate Polynomials
Status
Statistics
Lean Declarations ✏️ **Added:** 10 declaration(s)
📋 **Additional Analysis**Style and Naming Violations
Module Layout and Organization
Documentation
📄 **Per-File Summaries**
Last updated: 2026-06-23 23:39 UTC. |
- Multivariate/DegreeBound.lean: degree-bound predicates (IndividualDegreeLE, CDegreeLE, CMvDegreeLE) on computable multivariate polynomials. - Multivariate/PartialEval.lean: partialEvalFirst (fix variable 0) with its evaluation and per-variable degree-bound lemmas. - Operations.lean: add the fromCMvPolynomial_bind₁ bridge lemma. These are the generic polynomial facts used by ArkLib's interaction-native oracle bridge and Sumcheck integration. The sumcheck round-polynomial machinery lives in ArkLib, not here.
codygunton
force-pushed
the
cg/multivariate-degree-bound
branch
from
a556bc1 to
6f3eb09
Compare
codygunton
changed the title
alexanderlhicks
left a comment
alexanderlhicks
left a comment
There was a problem hiding this comment.
Review — validated against current master and the ArkLib consumer branch
Verification performed (all locally, with this diff applied):
- Full library build + full
lake testpass on v4.31.0 (master has bumped the toolchain since this PR's last CI run on v4.30.0; the PR is behind but merges cleanly, so re-merging is a formality). #print axiomson all 7 public declarations: onlypropext,Classical.choice,Quot.sound— TCB policy satisfied.lint-style.shpasses;CompPoly.leanregenerated correctly.- Every inline suggestion below was compile-checked against this diff before posting.
ArkLib cross-check (consumer branch cg/mainline-interaction-sumcheck-pr2, tip 1617561d, and the stacked pr3/pr4 tips):
- ArkLib currently carries local copies of
IndividualDegreeLE/CDegreeLE/CMvDegreeLEinArkLib/Data/CompPoly/Basic.lean; onlypartialEvalFirstandpartialEvalFirst_degreeOf_leare consumed from the CompPoly package (Interaction/CompPoly.lean:30,Interaction/SingleRound.lean:35-36). partialEvalFirst_evalandfromCMvPolynomial_bind₁have no external consumers yet (both are still justified: the latter powers bothPartialEvaltheorems, the former is the spec of the definition).- Everything suggested inline is strictly compatible with the ArkLib call sites — notably, I deliberately do not suggest restating
partialEvalFirst_degreeOf_leviaCMvPolynomial.degreeOf, because that would break the exact term-mode application atInteraction/CompPoly.lean:30. Additive corollaries (see inline) give the clean API with zero breakage, and would let ArkLib delete itspartialEvalFirst_individualDegreeLEwrapper and prune the[Nontrivial R]it threads throughSingleRound.
Not anchored inline:
- Namespace/naming:
CompPoly.CDegreeLE/CMvDegreeLEintroduce the first non-test use of theCompPolynamespace (the library otherwise usesCPoly). Either choice works for ArkLib (use sites are unqualified underopen CompPoly CPoly), so this is a deliberate maintainer call — worth a comment in the file either way. Also note the repo's existing degree-bound machinery is lowercase andSet-valued (degreeLE/degreeLTinUnivariate/Linear.lean);CDegreeLEis the first{p // natDegree ≤ d}subtype. PascalCase-for-subtype is Mathlib-idiomatic, so this is defensible. - Headers:
Authors: ArkLib Contributors— repo convention is real names (the originals in ArkLib credit Quang Dao). - Tests:
partialEvalFirstis computable andtests/CompPolyTests/Multivariate/exists — a small evaluation regression test would fit. The new definitions should also be exercised intests/CompPolyTests/Multivariate/TypeclassMinimization.lean, the repo's compile-time regression suite for minimal assumptions (relevant to the inline typeclass comment). - Follow-up golf (assessed, not required): the ~90 lines of private degree helpers reprove what Mathlib's
MvPolynomial.degreeOf_coeff_finSuccEquivprovides; routing through it (plus a smalleval₂↔finSuccEquivbridge, which Mathlib lacks) should collapse the block to ~20-30 lines. Confirmed Mathlib has nodegreeOf_eval₂/bind₁/aevallemma, so the helpers are not redundant as written. Similarly,MvPolynomial.eval_eval₂shortenspartialEvalFirst_evalslightly (validated at 15 lines vs 21). - ArkLib pin: the consumer branch pins CompPoly to a fork rev (
codygunton/CompPoly @ 2ebbaac3) not in upstream; the eventual migration needs a repin plus deletion of the local copies.
Overall: mathematically sound, kernel-safe, green on the current toolchain. The inline items are small and mechanical, each with a verified fix.
| Authors: ArkLib Contributors | ||
| -/ | ||
| import CompPoly.Multivariate.CMvPolynomial | ||
| import CompPoly.Univariate.ToPoly.Impl |
There was a problem hiding this comment.
Unused import (verified: removal compiles). CPolynomial.natDegree lives in CompPoly/Univariate/Basic.lean, which is already transitively imported via CompPoly.Multivariate.CMvPolynomial — ToPoly.Impl pulls in the whole Mathlib Polynomial bridge for nothing.
|
|
||
| namespace CPoly.CMvPolynomial | ||
|
|
||
| variable {n : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] |
There was a problem hiding this comment.
Typeclass assumptions much stronger than needed (verified: the minimized file compiles). Everything in this file needs only [Zero R], and R : Type* matches the rest of the library:
variable {n : ℕ} {R : Type*} [Zero R]
...
def CDegreeLE (R : Type*) [Zero R] (d : ℕ) :=
{ p : CPolynomial R // p.natDegree ≤ d }
def CMvDegreeLE (R : Type*) [Zero R] (n d : ℕ) :=
{ p : CMvPolynomial n R // CMvPolynomial.IndividualDegreeLE (R := R) d p }CPolynomial, CMvPolynomial, natDegree, and Lawful.monomials all require just [Zero R]. As written, every consumer must thread BEq/LawfulBEq/CommSemiring instances it doesn't need (per docs/wiki/typeclass-minimization.md). I checked the ArkLib consumer branch: relaxing is strictly safe — all use sites supply stronger instances. Suggest also adding these three definitions to tests/CompPolyTests/Multivariate/TypeclassMinimization.lean so the minimal assumptions are pinned.
| /-- `p` has individual degree at most `deg` when every monomial exponent is | ||
| bounded by `deg` in every coordinate. -/ | ||
| def IndividualDegreeLE (deg : ℕ) (p : CMvPolynomial n R) : Prop := | ||
| letI := Classical.decEq R |
There was a problem hiding this comment.
Dead code (verified: removal compiles). Nothing in the body needs DecidableEq R — Lawful.monomials is a key list and CMvMonomial.degreeOf never touches R. This looks inherited from the ArkLib original; it embeds a spurious let in the definition that every consumer unfolds past.
Separately (verified), the predicate is equivalent to a bound on the existing CMvPolynomial.degreeOf, and the connection is worth recording here so the new predicate plugs into the existing degreeOf_equiv bridge:
theorem individualDegreeLE_iff {deg : ℕ} (p : CMvPolynomial n R) :
IndividualDegreeLE deg p ↔ ∀ i, CMvPolynomial.degreeOf i p ≤ deg := by
unfold IndividualDegreeLE CMvPolynomial.degreeOf
constructor
· intro h i
exact Finset.sup_le fun m hm => h i m (by simpa using hm)
· intro h i m hm
exact (Finset.le_sup (s := (Lawful.monomials p).toFinset)
(f := fun m => CMvMonomial.degreeOf m i) (by simpa using hm)).trans (h i)| Authors: ArkLib Contributors | ||
| -/ | ||
| import CompPoly.Data.MvPolynomial.Notation | ||
| import CompPoly.Multivariate.DegreeBound |
There was a problem hiding this comment.
Two unused imports (verified: removal compiles). Nothing in this file uses the R[X σ] notation, and nothing here references IndividualDegreeLE or the DegreeBound file. (If you adopt the IndividualDegreeLE-preservation corollary suggested below on the degree lemma, the DegreeBound import becomes genuinely used — otherwise both lines can go.)
| exact (eval_equiv (p := p) (vals := Fin.cons a v)).symm | ||
|
|
||
| /-! ## Degree preservation -/ | ||
|
|
There was a problem hiding this comment.
[Nontrivial R] can be dropped from this public lemma (verified: compiles). Over a subsingleton ring the statement is vacuous — a Lawful polynomial stores no zero coefficients, hence no monomials. The private helpers can keep their [Nontrivial R]:
theorem partialEvalFirst_degreeOf_le {deg : ℕ} (a : R)
(i : Fin n) (p : CMvPolynomial (n + 1) R)
(hDeg : ∀ mono ∈ Lawful.monomials p, mono.degreeOf i.succ ≤ deg) :
∀ mono ∈ Lawful.monomials (partialEvalFirst a p), mono.degreeOf i ≤ deg := by
intro mono hmono
rcases subsingleton_or_nontrivial R with hR | hR
· have hmem : mono ∈ (partialEvalFirst a p).1 := by simpa using hmono
have hne := (partialEvalFirst a p).2 mono
rw [getElem?_pos _ _ hmem,
Subsingleton.elim ((partialEvalFirst a p).1[mono]'hmem) 0] at hne
exact absurd rfl hne
· <original proof body>This matters downstream: on the ArkLib consumer branch, [Nontrivial R] is threaded through partialEvalFirst_individualDegreeLE, stepResidual, and SingleRound.lean's variable block solely to satisfy this hypothesis, over a generic CommSemiring.
Note I'm deliberately not suggesting restating this lemma via CMvPolynomial.degreeOf — that would break ArkLib's exact term-mode application at Interaction/CompPoly.lean:30. Instead, two additive corollaries (both verified) give the clean API with zero breakage:
theorem partialEvalFirst_degreeOf_le' {deg : ℕ} (a : R) (i : Fin n)
(p : CMvPolynomial (n + 1) R) (h : CMvPolynomial.degreeOf i.succ p ≤ deg) :
CMvPolynomial.degreeOf i (partialEvalFirst a p) ≤ deg := ...
theorem partialEvalFirst_individualDegreeLE {deg : ℕ} (a : R)
(p : CMvPolynomial (n + 1) R) (h : IndividualDegreeLE deg p) :
IndividualDegreeLE deg (partialEvalFirst a p) :=
fun i => partialEvalFirst_degreeOf_le a i p (fun mono hmono => h i.succ mono hmono)The second is exactly ArkLib's wrapper in Interaction/CompPoly.lean — upstreaming it lets ArkLib delete that wrapper.
| /-- The computable substitution `bind₁` agrees with Mathlib substitution after | ||
| transporting through `fromCMvPolynomial`. -/ | ||
| theorem fromCMvPolynomial_bind₁ {n m : ℕ} {R : Type*} [CommSemiring R] [BEq R] | ||
| [LawfulBEq R] (f : Fin n → CMvPolynomial m R) (p : CMvPolynomial n R) : |
There was a problem hiding this comment.
Consider spelling the RHS with MvPolynomial.aeval (verified: compiles, no new import):
fromCMvPolynomial (bind₁ f p) =
MvPolynomial.aeval (fun i => fromCMvPolynomial (f i)) (fromCMvPolynomial p)This mirrors CompPoly's own bind₁_eq_aeval and is more discoverable than raw eval₂ C. (MvPolynomial.bind₁ would be the most literal spelling, but it isn't in the current import closure — it lives in Mathlib.Algebra.MvPolynomial.Monad; the aeval form needs nothing new.) I checked there's no existing fromCMvPolynomial_aeval/eval₂ bridge that makes this lemma redundant, so the proof is genuinely needed — a general fromCMvPolynomial_eval₂ next to eval₂_equiv would subsume it and is nice follow-up material.
Nit: double blank line above the docstring (line 458).
2 participants
Summary
Adds the generic computable-polynomial facts that ArkLib's interaction-native protocol work builds on:
Multivariate/DegreeBound.lean— degree-bound predicates (IndividualDegreeLE,CDegreeLE,CMvDegreeLE) on computable multivariate polynomials.Multivariate/PartialEval.lean—partialEvalFirst(fix variable0) with its evaluation lemma and per-variable degree-bound lemma.Operations.lean— thefromCMvPolynomial_bind₁bridge lemma (lives with the otherbind₁/fromCMvPolynomial_*facts).Usage in ArkLib
DegreeBoundis used by the ArkLib oracle bridge (ArkLib/Data/CompPoly/Basic.lean, the core slice) and by the Sumcheck integration.PartialEval(partialEvalFirst) is used by the ArkLib Sumcheck slice.Scope
Follows CompPoly's concept-per-file layout. The sumcheck round-polynomial machinery (
roundPolyand its summation/univariate-collapse helpers) deliberately does not live here — it is protocol-specific, has a single consumer, and lands in ArkLib'sProofSystem/Sumcheck. This PR keeps only the broadly-reusable primitives.Supersedes #235 (closed). Rebased cleanly onto current
master; full CompPoly build passes with no warnings.🤖 Generated with Claude Code