Add a direct computable CMvPolynomial/CPolynomial univariate bridge

[quangvdao]

Posted by Cursor assistant (model: GPT-5.4) on behalf of the user (Quang Dao) with approval.

Summary

• add CompPoly.Multivariate.UnivariateEquiv with a direct computable bridge CMvPolynomial 1 R ≃+* CPolynomial R
• implement the bridge through direct eval₂-based definitions instead of the existing noncomputable MvPolynomial / Polynomial transport path
• prove compatibility with the existing finSuccEquiv composite and keep the regression tests and docs in sync

Main API

• CompPoly.CPolynomial.cRingHom
• CPoly.CMvPolynomial.toUnivariate
• CPoly.CMvPolynomial.ofUnivariate
• CPoly.CMvPolynomial.univariateRingEquiv
• CPoly.CMvPolynomial.coeff_toUnivariate
• CPoly.CMvPolynomial.coeff_ofUnivariate
• CPoly.CMvPolynomial.univariateRingEquiv_eq_finSucc_composite

Validation

• ./scripts/check-imports.sh
• lake build
• lake test
• ./scripts/lint-style.sh
• python3 ./scripts/check-docs-integrity.py

[github-actions]

🤖 Gemini PR Summary

Mathematical Formalization

• Computable Isomorphism: Adds CPoly.CMvPolynomial.univariateRingEquiv, a computable ring isomorphism between CMvPolynomial 1 R and CPolynomial R. This bypasses the existing noncomputable transport path through MvPolynomial and Polynomial.
• Direct Implementation: Implements the bridge via toUnivariate and ofUnivariate using eval₂-based definitions rather than abstract noncomputable isomorphisms.
• Coefficient Correspondence: Provides CPoly.CMvPolynomial.coeff_toUnivariate and CPoly.CMvPolynomial.coeff_ofUnivariate to characterize coefficient mapping across the isomorphism.
• Consistency Proofs: Includes CPoly.CMvPolynomial.univariateRingEquiv_eq_finSucc_composite, proving the new direct bridge is equivalent to the existing finSuccEquiv composite.
• Additional API: Introduces CPoly.CPolynomial.cRingHom for computable ring homomorphisms in the univariate context.

Infrastructure & Testing

• Library Integration: Updates CompPoly.lean to export the CompPoly.Multivariate.UnivariateEquiv module.
• Regression Testing: Adds tests/CompPolyTests/Multivariate/UnivariateEquiv.lean to validate the ring isomorphism and coefficient mappings.
• Placeholder Check: No sorry or admit placeholders were introduced in this PR.

Documentation

• Repository Mapping: Updates docs/wiki/repo-map.md to include the new UnivariateEquiv module.
• Bridge Documentation: Modifies docs/wiki/representations-and-bridges.md to formalize the role of the direct computable bridge for single-variable multivariate polynomials.

---

Statistics

Metric	Count
📝 Files Changed	6
✅ Lines Added	452
❌ Lines Removed	0

---

Lean Declarations

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

• lemma toUnivariate_add [Nontrivial R] (p q : CMvPolynomial 1 R) : in CompPoly/Multivariate/UnivariateEquiv.lean
• def ofUnivariate (p : CompPoly.CPolynomial R) : CMvPolynomial 1 R in CompPoly/Multivariate/UnivariateEquiv.lean
• lemma univariateRingEquiv_symm_apply [Nontrivial R] (p : CompPoly.CPolynomial R) : in CompPoly/Multivariate/UnivariateEquiv.lean
• lemma toUnivariate_ofUnivariate [Nontrivial R] (p : CompPoly.CPolynomial R) : in CompPoly/Multivariate/UnivariateEquiv.lean
• def univariateMonomial (n : ℕ) : CMvMonomial 1 in CompPoly/Multivariate/UnivariateEquiv.lean
• def toUnivariate [Nontrivial R] (p : CMvPolynomial 1 R) : CompPoly.CPolynomial R in CompPoly/Multivariate/UnivariateEquiv.lean
• def univariateRingEquiv [Nontrivial R] : CMvPolynomial 1 R ≃+* CompPoly.CPolynomial R where in CompPoly/Multivariate/UnivariateEquiv.lean
• lemma coeff_ofUnivariate (p : CompPoly.CPolynomial R) (i : ℕ) : in CompPoly/Multivariate/UnivariateEquiv.lean
• lemma ofUnivariate_toUnivariate [Nontrivial R] (p : CMvPolynomial 1 R) : in CompPoly/Multivariate/UnivariateEquiv.lean
• lemma univariateRingEquiv_apply [Nontrivial R] (p : CMvPolynomial 1 R) : in CompPoly/Multivariate/UnivariateEquiv.lean
• lemma coeff_C_mul_X_pow (c : R) : in CompPoly/Multivariate/UnivariateEquiv.lean
• def cRingHom : R →+* CMvPolynomial 1 R where in CompPoly/Multivariate/UnivariateEquiv.lean
• lemma cRingHom_apply (r : R) : cRingHom (R in CompPoly/Multivariate/UnivariateEquiv.lean
• theorem univariateRingEquiv_eq_finSucc_composite [Nontrivial R] : in CompPoly/Multivariate/UnivariateEquiv.lean
• lemma coeff_toUnivariate [Nontrivial R] (p : CMvPolynomial 1 R) (i : ℕ) : in CompPoly/Multivariate/UnivariateEquiv.lean
• lemma toUnivariate_mul [Nontrivial R] (p q : CMvPolynomial 1 R) : in CompPoly/Multivariate/UnivariateEquiv.lean
• lemma coeff_sum {ι : Type*} (s : Finset ι) (f : ι → CPolynomial R) (i : ℕ) : in CompPoly/Multivariate/UnivariateEquiv.lean

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

🎨 **Style Guide Adherence**

The following violations of the style guide were found:

• CompPoly/Multivariate/UnivariateEquiv.lean:2: Copyright (c) 2026 CompPoly. All rights reserved. violates Copyright (c) 2024 Author Name. All rights reserved. (Incorrect year and missing author name).
• CompPoly/Multivariate/UnivariateEquiv.lean:83: simpa using (coeff_zero (R := R) (i := i)) violates Avoid parentheses where possible. Use <| (pipe left) and |> (pipe right) to reduce nesting. (Parentheses around the term are redundant).
• CompPoly/Multivariate/UnivariateEquiv.lean:152: def toUnivariate [Nontrivial R] (p : CMvPolynomial 1 R) : CompPoly.CPolynomial R := violates Every definition and major theorem should have a docstring.
• CompPoly/Multivariate/UnivariateEquiv.lean:156: def ofUnivariate (p : CompPoly.CPolynomial R) : CMvPolynomial 1 R := violates Every definition and major theorem should have a docstring.
• CompPoly/Multivariate/UnivariateEquiv.lean:226: lemma coeff_toUnivariate [Nontrivial R] (p : CMvPolynomial 1 R) (i : ℕ) : violates Every definition and major theorem should have a docstring.
• CompPoly/Multivariate/UnivariateEquiv.lean:247: lemma coeff_ofUnivariate (p : CompPoly.CPolynomial R) (i : ℕ) : violates Every definition and major theorem should have a docstring.
• CompPoly/Multivariate/UnivariateEquiv.lean:269: lemma toUnivariate_ofUnivariate [Nontrivial R] (p : CompPoly.CPolynomial R) : violates Every definition and major theorem should have a docstring.
• CompPoly/Multivariate/UnivariateEquiv.lean:277: lemma ofUnivariate_toUnivariate [Nontrivial R] (p : CMvPolynomial 1 R) : violates Every definition and major theorem should have a docstring.
• tests/CompPolyTests/Multivariate/UnivariateEquiv.lean:2: Copyright (c) 2026 CompPoly. All rights reserved. violates Copyright (c) 2024 Author Name. All rights reserved. (Incorrect year and missing author name).
• tests/CompPolyTests/Multivariate/UnivariateEquiv.lean:72: (fun e : CMvPolynomial 1 ℚ ≃+* CPolynomial ℚ => e p) violates Functions: Prefer fun x ↦ ... over λ x, ... (Uses => instead of the preferred ↦ syntax).

---

📄 **Per-File Summaries**

• CompPoly.lean: This change updates the top-level CompPoly.lean file to import the UnivariateEquiv module. This expansion likely integrates definitions and theorems concerning the equivalence between multivariate and univariate polynomials into the main library.
• docs/wiki/repo-map.md: This documentation update adds a repository map entry for the bridge between single-variable multivariate polynomials and univariate polynomials. It directs contributors to CompPoly/Multivariate/UnivariateEquiv.lean for work related to this specific ring isomorphism.
• docs/wiki/representations-and-bridges.md: This update adds documentation for a new computable ring isomorphism between multivariate polynomials in one variable and univariate polynomials. It specifies the location and role of UnivariateEquiv.lean as a dedicated bridge within the library's multivariate polynomial representation.
• tests/CompPolyTests.lean: This change updates the test suite by importing the UnivariateEquiv module, thereby integrating tests for the equivalence between multivariate and univariate polynomials. It does not introduce new definitions, theorems, or sorry placeholders within this specific file.
• tests/CompPolyTests/Multivariate/UnivariateEquiv.lean: This new test file introduces a suite of examples to verify the computable equivalence between single-variable multivariate polynomials (CMvPolynomial 1 R) and univariate polynomials (CPolynomial R). It validates the core properties of the ring isomorphism and its coefficient mappings, ensuring consistency with existing library definitions without using any sorry or admit placeholders.
• CompPoly/Multivariate/UnivariateEquiv.lean: This file introduces new definitions and theorems to establish a direct, computable ring equivalence between one-variable multivariate polynomials (CMvPolynomial 1) and canonical univariate polynomials (CPolynomial). It provides the toUnivariate and ofUnivariate maps along with proofs of their inverse relationship and compatibility with existing noncomputable transport paths. No sorry or admit placeholders are introduced.

---

Last updated: 2026-03-30 15:44 UTC.

[github-actions]

Build Timing Report

• Commit: 783bace
• Message: Merge e2849f5 into 94ccb6f
• Ref: quang/cmvpoly-univariate-equiv
• Comparison baseline: c584d70 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; test path lake test.

Measurement	Baseline (s)	Current (s)	Delta (s)	Status
Clean build	246.21	243.48	-2.73	ok
Warm rebuild	1.28	1.61	+0.33	ok
Test path	19.79	20.71	+0.92	ok

Incremental Rebuild Signal

• Warm rebuild saved 241.87s vs clean (151.23x 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
84.00	85.00	-1.00	CompPoly/Fields/Binary/BF128Ghash/XPowTwoPowModCertificate.lean
53.00	62.00	-9.00	CompPoly/Fields/Binary/Tower/Abstract/Basis.lean
49.00	48.00	+1.00	CompPoly/Bivariate/ToPoly.lean
30.00	25.00	+5.00	CompPoly/Fields/Binary/BF128Ghash/Impl.lean
27.00	28.00	-1.00	CompPoly/Univariate/Raw/Proofs.lean
24.00	22.00	+2.00	CompPoly/Univariate/Lagrange.lean
21.00	23.00	-2.00	CompPoly/Fields/Binary/AdditiveNTT/NovelPolynomialBasis.lean
20.00	22.00	-2.00	CompPoly/Fields/Binary/Tower/Support/Preliminaries.lean
18.00	19.00	-1.00	CompPoly/Fields/Binary/AdditiveNTT/Intermediate.lean
18.00	14.00	+4.00	CompPoly/Univariate/Quotient/Core.lean
17.00	16.00	+1.00	CompPoly/Univariate/Basic.lean
16.00	15.00	+1.00	CompPoly/Fields/Binary/Tower/Abstract/Core.lean
14.00	16.00	-2.00	CompPoly/Fields/Binary/AdditiveNTT/Domain.lean
13.00	14.00	-1.00	CompPoly/Fields/Binary/Common.lean
12.00	11.00	+1.00	CompPoly/Fields/Binary/AdditiveNTT/Correctness.lean
11.00	9.30	+1.70	CompPoly/Multilinear/Basic.lean
10.00	9.50	+0.50	CompPoly/Data/Nat/Bitwise.lean
10.00	12.00	-2.00	CompPoly/Fields/Binary/Tower/TensorAlgebra.lean
10.00	12.00	-2.00	CompPoly/Fields/Binary/Tower/Abstract/Split.lean
10.00	12.00	-2.00	CompPoly/Fields/Binary/BF128Ghash/XPowTwoPowGcdCertificate.lean

[github-actions]

🤖 Initial AI review without external context

🤖 AI Review

Overall Summary:

1. TL;DR

The PR is in fantastic shape, featuring sound mathematical formalization and robust testing across the board. The reviewers found no critical misformalizations or major Mathlib issues, and praised the idiomatic bridging of executable and noncomputable math. There is only one minor suggestion regarding an overly strong typeclass assumption to review.

2. Checklist Coverage

No explicit specification checklist was provided for this review. All files were evaluated against general Lean 4 and mathematical formalization best practices.

3. Key Lean 4 / Mathlib Issues & Nitpicks

No critical Lean 4 or Mathlib blockers were found. The reviewers did highlight the following minor technical observations:

• Overly Strong Typeclass Assumption (CompPoly/Multivariate/UnivariateEquiv.lean): The variable [Nontrivial R] block inside CompPoly.CPolynomial cascades and forces [Nontrivial R] on toUnivariate and univariateRingEquiv. Mathematically, embedding constants into polynomials (C : R → R[X]) and evaluating them is well-defined even for the trivial ring. Unless the core implementation inherently requires this constraint to maintain representation invariants (e.g., ensuring leading_coeff ≠ 0), this constraint could likely be dropped. (Note: This is a minor detail, as cryptography/CompPoly applications generally operate over nontrivial fields anyway).
• Excellent Computability Trick (CompPoly/Multivariate/UnivariateEquiv.lean): Explicitly redeclaring cRingHom directly via the underlying computable C function to bypass the noncomputable CMvPolynomial.CRingHom bundling is a highly commendable, well-documented workaround. It is a very idiomatic Lean 4 strategy for maintaining computability.

4. Overall Verdict

Approved

---

📄 **Review for `CompPoly.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Multivariate/UnivariateEquiv.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:

• Potentially overly strong typeclass assumption: The variable [Nontrivial R] block inside CompPoly.CPolynomial encompasses cRingHom and its associated lemmas, which cascades and forces [Nontrivial R] on toUnivariate and univariateRingEquiv. Mathematically, embedding constants into polynomials (C : R → R[X]) and evaluating them is well-defined even for the trivial ring where 0 = 1. Unless the core implementation of CPolynomial R intrinsically requires [Nontrivial R] to maintain representation invariants (e.g., maintaining leading_coeff ≠ 0), you could likely drop this constraint. This is only a minor detail given that cryptography/CompPoly applications operate almost exclusively over nontrivial fields anyway.
• Excellent computability trick: Explicitly redeclaring cRingHom directly via the underlying computable C function to bypass the noncomputable CMvPolynomial.CRingHom bundling is a great, well-documented workaround. Very idiomatic for Lean 4 formal verification bridging executable and noncomputable math.

📄 **Review for `tests/CompPolyTests.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `tests/CompPolyTests/Multivariate/UnivariateEquiv.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

[dhsorens]

this looks good to me!