Prove distanceLE_mvPolynomial_degreeLE

[MrBrain295]

No description provided.

[github-actions]

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: Prove distanceLE_mvPolynomial_degreeLE

sorry delta: -1 (1 removed) — net proof progress

Summary

Mathematical Formalization

• ArkLib/Data/MvPolynomial/Degrees.lean: Adds theorem totalDegree_le_card_mul_of_mem_restrictDegree bounding the total degree of a polynomial in finitely many variables (type σ) where each variable's degree is ≤ n. The bound is Fintype.card σ * n. Proof is included.

Proof Completion (sorries removed)

• Core change in ArkLib/OracleReduction/OracleInterface.lean: The proof of distanceLE_mvPolynomial_degreeLE is now complete, replacing a previous sorry. The proof uses Fintype.fieldOfDomain to obtain a field structure, then applies MvPolynomial.totalDegree_le_card_mul_of_mem_restrictDegree and MvPolynomial.card_zeros_le_of_totalDegree_le. New imports ArkLib.Data.MvPolynomial.Degrees and ArkLib.Data.MvPolynomial.SchwartzZippelCounting are added.

Protocols / Soundness

• ArkLib/Data/MvPolynomial/SchwartzZippelCounting.lean: Adds two zero-counting theorems:
  • MvPolynomial.card_zeros_le_of_totalDegree_le_fin: For a nonzero polynomial f over a finite field F, in s variables, with total degree ≤ D, the number of zeros is bounded by D * |F|^(s-1).
  • MvPolynomial.card_zeros_le_of_totalDegree_le: Generalizes the bound to any finite index type ι (by reduction to Fin s), yielding D * |F|^(|ι|-1). The |F|^0 case is not handled. Both theorems include their proofs.

Infrastructure / CI

No changes.

Documentation

No changes.

Refactoring

No changes.

No sorries or admits remain in the changed files.

---

Statistics

Metric	Count
📝 Files Changed	3
✅ Lines Added	68
❌ Lines Removed	1

---

Lean Declarations

✏️ Added: 3 declaration(s)

ArkLib/Data/MvPolynomial/Degrees.lean (1)

• theorem totalDegree_le_card_mul_of_mem_restrictDegree [Fintype σ] (p : MvPolynomial σ R) (n : ℕ)

ArkLib/Data/MvPolynomial/SchwartzZippelCounting.lean (2)

• theorem MvPolynomial.card_zeros_le_of_totalDegree_le_fin
• theorem MvPolynomial.card_zeros_le_of_totalDegree_le

---

sorry Tracking

✅ Removed: 1 `sorry`(s)

ArkLib/OracleReduction/OracleInterface.lean (1)

• theorem distanceLE_mvPolynomial_degreeLE {σ : Type} [Fintype σ] [DecidableEq σ] : (L370)

---

📋 **Additional Analysis**

The diff adds a new lemma totalDegree_le_card_mul_of_mem_restrictDegree to Degrees.lean, a new file SchwartzZippelCounting.lean containing two counting theorems, and a completion of a previously-sorry'd theorem distanceLE_mvPolynomial_degreeLE in OracleInterface.lean, along with necessary imports. The submission is well-structured, follows the project's naming and formatting conventions, and addresses a documented goal (Schwartz-Zippel zero counting). No style or compliance issues were found. Given the described workflow, the output should be a concise bullet point report listing adherence to the instructions, as the deployment-supplied instructions do not specify a particular format beyond 'follow whatever the instructions request' and defaulting to bullet points. The diff is relevant and the review is complete.

---

📄 **Per-File Summaries**

• ArkLib/Data/MvPolynomial/Degrees.lean: Adds a new theorem totalDegree_le_card_mul_of_mem_restrictDegree to ArkLib/Data/MvPolynomial/Degrees.lean. It states that for a polynomial with finitely many variables whose individual degrees are all at most n, its total degree is bounded by Fintype.card σ * n, and includes the proof of the bound.
• ArkLib/Data/MvPolynomial/SchwartzZippelCounting.lean: The diff adds a new ZeroCount section containing two theorems. MvPolynomial.card_zeros_le_of_totalDegree_le_fin bounds the number of zeros of a nonzero polynomial f over a finite field F in s variables with total degree ≤ D by D * |F|^(s-1). MvPolynomial.card_zeros_le_of_totalDegree_le extends this bound to any finite index type ι by using Fintype.equivFin to reduce to the Fin s case, yielding D * |F|^(|ι|-1).
• ArkLib/OracleReduction/OracleInterface.lean: The proof of distanceLE_mvPolynomial_degreeLE has been completed, replacing the previous sorry; it now uses Fintype.fieldOfDomain to obtain a field structure, then applies MvPolynomial.totalDegree_le_card_mul_of_mem_restrictDegree and MvPolynomial.card_zeros_le_of_totalDegree_le to establish the distance bound. Two new imports were added: ArkLib.Data.MvPolynomial.Degrees and ArkLib.Data.MvPolynomial.SchwartzZippelCounting.

---

Last updated: 2026-08-05 00:33 UTC.

[github-actions]

Build Timing Report

• Commit: febaaa5
• Message: Prove distanceLE_mvPolynomial_degreeLE
• Ref: patch-1
• Comparison baseline: d89e507 from the previous successful PR update.
• Measured on ubuntu-latest with /usr/bin/time -p.
• Commands: clean build rm -rf .lake/build && lake build; warm rebuild lake build; validation wrapper ./scripts/validate.sh.

Measurement	Baseline (s)	Current (s)	Delta (s)	Status
Clean build	1470.17	1284.51	-185.66	ok
Warm rebuild	2.59	2.51	-0.08	ok
Validation wrapper	2.95	2.67	-0.28	ok

Incremental Rebuild Signal

• Warm rebuild saved 1282.00s vs clean (511.76x faster).

This compares a clean project build against an incremental rebuild in the same CI job; it is a lightweight variability signal, not a full cross-run benchmark.

Slowest Current Clean-Build Files

Showing 20 slowest current targets, with comparison against the selected baseline when available.

Current (s)	Baseline (s)	Delta (s)	Path
58.00	74.00	-16.00	ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
55.00	66.00	-11.00	ArkLib/ProofSystem/Stir/Combine.lean
54.00	69.00	-15.00	ArkLib/Data/CodingTheory/JohnsonBound/Lemmas.lean
54.00	63.00	-9.00	ArkLib/Data/CodingTheory/ProximityGap/DG25/MainResults.lean
49.00	50.00	-1.00	ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineLines/BWMatrix.lean
49.00	61.00	-12.00	ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineSpaces.lean
35.00	41.00	-6.00	ArkLib/OracleReduction/LiftContext/Reduction.lean
34.00	46.00	-12.00	ArkLib/Data/CodingTheory/BerlekampWelch/Condition.lean
34.00	39.00	-5.00	ArkLib/Data/CodingTheory/JohnsonBound/Basic.lean
34.00	44.00	-10.00	ArkLib/Data/CodingTheory/ProximityGap/AHIV22.lean
33.00	44.00	-11.00	ArkLib/Data/CodingTheory/ProximityGap/Folding.lean
31.00	28.00	+3.00	ArkLib/OracleReduction/Security/RoundByRound.lean
26.00	22.00	+4.00	ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineLines/JointAgreement.lean
24.00	18.00	+6.00	ArkLib/Data/CodingTheory/PolishchukSpielman/Degrees.lean
24.00	31.00	-7.00	ArkLib/ProofSystem/Sumcheck/Spec/SingleRound.lean
22.00	24.00	-2.00	ArkLib/Data/Polynomial/Indicator.lean
22.00	24.00	-2.00	ArkLib/Data/Polynomial/FoldingPolynomial.lean
22.00	29.00	-7.00	ArkLib/Data/CodingTheory/DivergenceOfSets.lean
21.00	23.00	-2.00	ArkLib/Data/Domain/CosetFftDomain/Subdomain.lean
21.00	32.00	-11.00	ArkLib/Commitments/Functional/KZG/FunctionBinding/EvaluationBindingConflict.lean