Proof for divX_mul_X_add

[aleph-prover]

Proven lemmas: 3/3

The goal is to prove the polynomial identity divX p * X + C (p.coeff 0) = p for any CPolynomial p over a nontrivial ring/semiring R: informally, dividing by X and then multiplying back by X recovers all higher-degree terms, and the missing constant term is restored by adding C(p₀). The proof was decomposed into two coefficient “shift” lemmas about multiplication by X, and then a final step that compares coefficients on both sides. First, coeff_mul_X_zero shows that the constant coefficient of p * X is 0. Second, coeff_mul_X_succ shows that for every n, the (n+1)-st coefficient of p * X equals the n-th coefficient of p (multiplication by X shifts coefficients up by one). With these in hand, the main theorem divX_mul_X_add is proved by coefficient extensionality: check k = 0 separately (the X-multiple contributes 0 and C(p₀) contributes p₀), and check k = n+1 using the shift lemma plus the defining coefficient rule for divX.

Progress: all 3 sub-problems out of 3 are solved (both shift lemmas and the final coefficient-extensionality argument). There is no remaining mathematical gap; what’s left is only to integrate/clean up the proven Lean code so the file compiles smoothly with the intended imports and instances. One interesting technical challenge handled along the way is that only one term in the convolution sum for coeff(p * X) can survive (because coeff X j is 0 unless j = 1), so the proof collapses a finite sum to a single index using a “sum equals single term” argument, together with small arithmetic facts about n+1−i. Another minor gotcha is disambiguating similarly named lemmas for coeff_X coming from different namespaces, which the proof resolves by using the appropriate qualified lemma when rewriting.

[github-actions]

🤖 Gemini PR Summary

This Pull Request completes the formal proof of the polynomial identity divX p * X + C (p.coeff 0) = p within the CompPoly library. This identity establishes that dividing a polynomial by $X$, multiplying it back by $X$, and adding the original constant term recovers the original polynomial.

Features

• Main Theorem Implementation: Proved divX_mul_X_add, demonstrating that for any polynomial $p$ over a nontrivial (semi)ring, the relation between divX and multiplication by $X$ holds via coefficient extensionality.
• Auxiliary Coefficient Lemmas:
  • coeff_mul_X_zero: Proves that the constant coefficient of $p * X$ is always $0$.
  • coeff_mul_X_succ: Proves that the $(n+1)$-th coefficient of $p * X$ is equal to the $n$-th coefficient of $p$ (modeling the coefficient shift).
• Summation Logic: Implemented the logic to collapse the convolution sum for coeff (p * X), handling the index simplification where coeff X j is non-zero only at $j=1$.

Refactoring

• Code Cleanup: Removed redundant whitespace in CompPoly/Univariate/ToPoly.lean to adhere to formatting standards.
• Namespace Resolution: Standardized the use of qualified names for coeff_X to resolve ambiguity between conflicting namespaces.

Technical Notes

The proof handles the edge case of index $k=0$ separately from $k=n+1$. It successfully manages the arithmetic of $n+1-i$ within the finite sum index range and leverages the specific properties of the divX coefficient definition to bridge the gap between shifted coefficients.

---

Analysis of Changes

Metric	Count
📝 Files Changed	2
✅ Lines Added	50
❌ Lines Removed	2

---

sorry Tracking

✅ **Removed:** 1 `sorry`(s)

• lemma divX_mul_X_add [Nontrivial R] (p : CPolynomial R) : divX p * X + C (p.coeff 0) = p in CompPoly/Univariate/Basic.lean

---

🎨 **Style Guide Adherence**

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

• Line 265, 294, 318: "Every definition and major theorem should have a docstring." (Theorems coeff_mul_X_succ, coeff_mul_X_zero, and divX_mul_X_add are missing docstrings).
• Line 268: "Avoid parentheses where possible." (The double parentheses in change ((p.val * X.val).coeff (n + 1) = p.val.coeff n) are redundant; a single pair or none are required depending on context).
• Line 274: "Prefer fun x ↦ ... over λ x, ...." (The code uses fun i => ... instead of the preferred ↦ arrow for a mathematical function).
• Line 335: "Avoid parentheses where possible." (The parentheses around (coeff_divX (p := p) (i := n)) are redundant for the simpa using tactic).

---

📄 **Per-File Summaries**

• CompPoly/Univariate/Basic.lean: This change completes the proof of the identity divX p * X + C (p.coeff 0) = p by establishing auxiliary lemmas for the coefficients of polynomials multiplied by X.
• CompPoly/Univariate/ToPoly.lean: Remove a redundant blank line between theorem definitions to improve code formatting.

---

Last updated: 2026-02-13 15:29 UTC.