Add new theorems and proofs

[aleph-prover]

This PR contains:

• Proof request: Prove mul_coeff in CompPoly/Univariate/Quotient.lean
• Theorem proofs completed
• All tests passing

[github-actions]

🤖 Gemini PR Summary

Hello,

This pull request focuses on enhancing the CompPoly library by completing the formal proof for polynomial multiplication coefficients and improving code clarity through better name scoping.

Features

• New Proof Module: Introduced CompPoly/Univariate/Quotient_mul_coeff/mul_coeff_prover.lean, which provides the formal proof for the standard coefficient summation formula of polynomial multiplication.

Fixes

• Namespace Resolution: Fully qualified calls to coeff_add as Polynomial.coeff_add in CompPoly/Univariate/Equiv.lean to resolve naming ambiguities and prevent potential build errors.

Refactoring

• Proof Externalization: Streamlined CompPoly/Univariate/Quotient.lean by replacing the local, incomplete mul_coeff implementation with the modular version from the new prover module. This improves maintainability by decoupling the proof logic from the quotient definitions.

---

Status: All tests passed. Ready for review.

---

Analysis of Changes

Metric	Count
📝 Files Changed	3
✅ Lines Added	239
❌ Lines Removed	17

---

sorry Tracking

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

• theorem mul_coeff (p q : CPolynomial R) (i : ℕ) : in CompPoly/Univariate/Quotient.lean

---

🎨 **Style Guide Adherence**

Based on the provided style guide, here are the lines in the code changes that violate the conventions:

CompPoly/Univariate/Quotient_mul_coeff/mul_coeff_prover.lean

• Line 1: (Beginning of file) — "The documentation style" (Violated by missing the mandatory copyright header and module-level docstring//-! -/ header).
• Line 6: Array.foldl f init (Array.range 0) 0 0 = init := rfl — "The style guide" (Violated by excessive whitespace before rfl).
• Line 6: theorem CompPoly.Array.foldl_range_zero — "CompPoly aims to align closely with the established conventions of the Lean community, particularly those used in mathlib" (Violated by using fully qualified names for every declaration instead of namespace blocks).
• Line 9: theorem CompPoly.Array.range_foldl_succ — "CompPoly aims to align closely with the established conventions of the Lean community, particularly those used in mathlib" (Violated by redundant namespace prefixing).
• Line 10: -- try using foldl_push with correct arguments — "The style guide" (Violated by not following mathlib's convention: "Comments should start with a capital letter and end with a period.").
• Line 15: theorem CompPoly.Array.range_foldl_min_succ — "CompPoly aims to align closely with the established conventions of the Lean community, particularly those used in mathlib" (Violated by redundant namespace prefixing).
• Line 21: -- simp should rewrite mins — "The style guide" (Violated by informal comment formatting).
• Line 26: -- rewrite mins then use range_foldl_succ — "The style guide" (Violated by informal comment formatting).
• Line 40: theorem CompPoly.CPolynomial.coeff_add — "CompPoly aims to align closely with the established conventions of the Lean community, particularly those used in mathlib" (Violated by redundant namespace prefixing).
• Line 43: -- remove the trim on the left — "The style guide" (Violated by informal comment formatting).
• Line 45: -- now use the raw coefficient lemma — "The style guide" (Violated by informal comment formatting).
• Line 52: theorem CompPoly.CPolynomial.mulPowX_coeff — "CompPoly aims to align closely with the established conventions of the Lean community, particularly those used in mathlib" (Violated by redundant namespace prefixing).
• Line 57: -- simplify the concatenation lemma and use it to reduce to a replicate lookup — "The style guide" (Violated by informal comment formatting).
• Line 60: -- now the goal is the coefficient of a replicated zero array — "The style guide" (Violated by informal comment formatting).
• Line 68: -- simplify and finish — "The style guide" (Violated by informal comment formatting).
• Line 71: -- simplify the min on the RHS — "The style guide" (Violated by informal comment formatting).
• Line 75: theorem CompPoly.CPolynomial.mul_coeff_partial_step — "CompPoly aims to align closely with the established conventions of the Lean community, particularly those used in mathlib" (Violated by redundant namespace prefixing).
• Line 81: -- fold over an empty range — "The style guide" (Violated by informal comment formatting).
• Line 83: -- coefficient of the zero constant polynomial — "The style guide" (Violated by informal comment formatting).
• Line 93: -- expand the RHS fold using the axiom — "The style guide" (Violated by informal comment formatting).
• Line 95: -- the new term vanishes — "The style guide" (Violated by informal comment formatting).
• Line 97: -- the new term is added via g — "The style guide" (Violated by informal comment formatting).
• Line 177: -- base — "The style guide" (Violated by informal comment formatting).
• Line 181: -- step — "The style guide" (Violated by informal comment formatting).

---

📄 **Per-File Summaries**

• CompPoly/Univariate/Equiv.lean: Fully qualify calls to coeff_add as Polynomial.coeff_add to resolve name ambiguity.
• CompPoly/Univariate/Quotient.lean: This change replaces the local, incomplete mul_coeff theorem with an imported implementation from a dedicated prover module and updates internal references accordingly.
• CompPoly/Univariate/Quotient_mul_coeff/mul_coeff_prover.lean: Provides the proof for the standard coefficient summation formula of polynomial multiplication within the CompPoly library.

---

Last updated: 2026-01-26 22:05 UTC.

[dhsorens]

this is a pull request from logical intelligence into my pull request #58 ; it solves the relevant proof goals and so I will merge it and then clean it up on my PR branch

[dhsorens]

merging