From a45bc5e83284f8550445a8fe32949936ddc087a1 Mon Sep 17 00:00:00 2001
From: Derek Sorensen <d@dhsorens.com>
Date: Fri, 27 Feb 2026 13:11:40 +0000
Subject: [PATCH 1/7] feat: add test suite, refactor tests into a new directory

---
 .github/workflows/lean_action_ci.yml    |  2 ++
 CompPoly/Univariate/Raw.lean            |  9 +++++++-
 lakefile.lean                           |  3 +++
 tests/CompPolyTests.lean                |  1 +
 tests/CompPolyTests/Univariate/Raw.lean | 29 +++++++++++++++++++++++++
 tests/README.md                         | 25 +++++++++++++++++++++
 6 files changed, 68 insertions(+), 1 deletion(-)
 create mode 100644 tests/CompPolyTests.lean
 create mode 100644 tests/CompPolyTests/Univariate/Raw.lean
 create mode 100644 tests/README.md

diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml
index 09cd4ca..dce04a2 100644
--- a/.github/workflows/lean_action_ci.yml
+++ b/.github/workflows/lean_action_ci.yml
@@ -12,3 +12,5 @@ jobs:
     steps:
       - uses: actions/checkout@v4
       - uses: leanprover/lean-action@v1
+      - name: Build tests
+        run: lake build CompPolyTests
diff --git a/CompPoly/Univariate/Raw.lean b/CompPoly/Univariate/Raw.lean
index 3e16ab7..d7a45a4 100644
--- a/CompPoly/Univariate/Raw.lean
+++ b/CompPoly/Univariate/Raw.lean
@@ -1585,7 +1585,14 @@ instance : Neg (CPolynomial.Raw R) := ⟨neg⟩
 instance : Sub (CPolynomial.Raw R) := ⟨sub⟩
 instance : IntCast (CPolynomial.Raw R) := ⟨fun n => C (n : R)⟩
 
-/-- Division with remainder by a monic polynomial using polynomial long division. -/
+/-- Division with remainder by a monic polynomial using polynomial long division.
+
+We use `p.size` as fuel for the recursion. This is always sufficient because
+each division step strictly decreases the size of the remainder (the leading
+term is cancelled by a monic divisor, and `trim` removes any resulting trailing
+zeros). The guard `p.size < q.size` triggers as soon as the remainder is of
+lower degree than the divisor, so the recursion terminates cleanly even when
+cancellation causes the size to drop by more than one in a single step. -/
 def divModByMonicAux [Field R] (p : CPolynomial.Raw R) (q : CPolynomial.Raw R) :
     CPolynomial.Raw R × CPolynomial.Raw R :=
   go (p.size - q.size) p q
diff --git a/lakefile.lean b/lakefile.lean
index f83330e..dd1ee3f 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -10,3 +10,6 @@ require ExtTreeMapLemmas from git "https://github.com/Verified-zkEVM/ExtTreeMapL
 
 @[default_target]
 lean_lib CompPoly
+
+lean_lib CompPolyTests where
+  srcDir := "tests"
diff --git a/tests/CompPolyTests.lean b/tests/CompPolyTests.lean
new file mode 100644
index 0000000..94fa99d
--- /dev/null
+++ b/tests/CompPolyTests.lean
@@ -0,0 +1 @@
+import CompPolyTests.Univariate.Raw
diff --git a/tests/CompPolyTests/Univariate/Raw.lean b/tests/CompPolyTests/Univariate/Raw.lean
new file mode 100644
index 0000000..d8b1035
--- /dev/null
+++ b/tests/CompPolyTests/Univariate/Raw.lean
@@ -0,0 +1,29 @@
+import CompPoly.Univariate.Raw
+
+namespace CompPoly
+namespace CPolynomial.Raw
+
+/-- Regression test for issue #115: `(X^2 - 1) / (X + 1) = X - 1` with zero remainder. -/
+example :
+    divByMonic ((X : CPolynomial.Raw ℚ) ^ 2 - C 1) ((X : CPolynomial.Raw ℚ) + C 1)
+      = #[-(1 : ℚ), 1] := by
+  native_decide
+
+example :
+    modByMonic ((X : CPolynomial.Raw ℚ) ^ 2 - C 1) ((X : CPolynomial.Raw ℚ) + C 1)
+      = #[] := by
+  native_decide
+
+/-- Regression test for review-thread case: `X^3 = (X^2 + 1) * X + (-X)`. -/
+example :
+    divByMonic ((X : CPolynomial.Raw ℚ) ^ 3) ((X : CPolynomial.Raw ℚ) ^ 2 + C 1)
+      = #[(0 : ℚ), 1] := by
+  native_decide
+
+example :
+    modByMonic ((X : CPolynomial.Raw ℚ) ^ 3) ((X : CPolynomial.Raw ℚ) ^ 2 + C 1)
+      = #[(0 : ℚ), -(1 : ℚ)] := by
+  native_decide
+
+end CPolynomial.Raw
+end CompPoly
diff --git a/tests/README.md b/tests/README.md
new file mode 100644
index 0000000..1107590
--- /dev/null
+++ b/tests/README.md
@@ -0,0 +1,25 @@
+# CompPoly tests
+
+This directory contains Lean test modules for regression and behavioral checks.
+
+## Structure
+
+Tests mirror the `CompPoly/` hierarchy under the `CompPolyTests` namespace.
+For example:
+
+- library module: `CompPoly/Univariate/Raw.lean`
+- test module: `tests/CompPolyTests/Univariate/Raw.lean`
+
+## Running tests
+
+Build all tests:
+
+```bash
+lake build CompPolyTests
+```
+
+Build a single test module:
+
+```bash
+lake build CompPolyTests.Univariate.Raw
+```
\ No newline at end of file

From 886dcffe662f112f6b3883df7a872caf9b5516c7 Mon Sep 17 00:00:00 2001
From: Derek Sorensen <d@dhsorens.com>
Date: Fri, 27 Feb 2026 13:16:28 +0000
Subject: [PATCH 2/7] feat: configure CompPolyTests as a test driver

---
 .github/workflows/lean_action_ci.yml | 2 +-
 lakefile.lean                        | 4 +++-
 tests/README.md                      | 2 +-
 3 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml
index dce04a2..f216e93 100644
--- a/.github/workflows/lean_action_ci.yml
+++ b/.github/workflows/lean_action_ci.yml
@@ -13,4 +13,4 @@ jobs:
       - uses: actions/checkout@v4
       - uses: leanprover/lean-action@v1
       - name: Build tests
-        run: lake build CompPolyTests
+        run: lake test
diff --git a/lakefile.lean b/lakefile.lean
index dd1ee3f..4f82666 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -2,7 +2,9 @@ import Lake
 
 open System Lake DSL
 
-package CompPoly where version := v!"0.1.0"
+package CompPoly where
+  version := v!"0.1.0"
+  testDriver := "CompPolyTests"
 
 require "leanprover-community" / mathlib @ git "v4.28.0"
 
diff --git a/tests/README.md b/tests/README.md
index 1107590..20ab1aa 100644
--- a/tests/README.md
+++ b/tests/README.md
@@ -15,7 +15,7 @@ For example:
 Build all tests:
 
 ```bash
-lake build CompPolyTests
+lake test
 ```
 
 Build a single test module:

From 0f3bf001d2c886e5d8341ba91eebbb835a0ccccb Mon Sep 17 00:00:00 2001
From: Derek Sorensen <d@dhsorens.com>
Date: Fri, 27 Feb 2026 13:26:03 +0000
Subject: [PATCH 3/7] feat: fill out a small test suite

---
 tests/CompPolyTests.lean                      |  5 +++
 .../Multivariate/CMvMonomial.lean             | 24 ++++++++++++++
 .../CompPolyTests/Multivariate/Restrict.lean  | 27 +++++++++++++++
 .../Multivariate/VarsDegrees.lean             | 25 ++++++++++++++
 tests/CompPolyTests/Univariate/Basic.lean     | 33 +++++++++++++++++++
 tests/CompPolyTests/Univariate/ToPoly.lean    | 27 +++++++++++++++
 6 files changed, 141 insertions(+)
 create mode 100644 tests/CompPolyTests/Multivariate/CMvMonomial.lean
 create mode 100644 tests/CompPolyTests/Multivariate/Restrict.lean
 create mode 100644 tests/CompPolyTests/Multivariate/VarsDegrees.lean
 create mode 100644 tests/CompPolyTests/Univariate/Basic.lean
 create mode 100644 tests/CompPolyTests/Univariate/ToPoly.lean

diff --git a/tests/CompPolyTests.lean b/tests/CompPolyTests.lean
index 94fa99d..2e72f11 100644
--- a/tests/CompPolyTests.lean
+++ b/tests/CompPolyTests.lean
@@ -1 +1,6 @@
 import CompPolyTests.Univariate.Raw
+import CompPolyTests.Univariate.Basic
+import CompPolyTests.Univariate.ToPoly
+import CompPolyTests.Multivariate.CMvMonomial
+import CompPolyTests.Multivariate.Restrict
+import CompPolyTests.Multivariate.VarsDegrees
diff --git a/tests/CompPolyTests/Multivariate/CMvMonomial.lean b/tests/CompPolyTests/Multivariate/CMvMonomial.lean
new file mode 100644
index 0000000..4db1003
--- /dev/null
+++ b/tests/CompPolyTests/Multivariate/CMvMonomial.lean
@@ -0,0 +1,24 @@
+import CompPoly.Multivariate.CMvMonomial
+
+namespace CPoly
+namespace CMvMonomial
+
+-- TODO: add more arithmetic compatibility checks with `MonoR.evalMonomial`.
+
+example {n : ℕ} (m : CMvMonomial n) : ofFinsupp m.toFinsupp = m := by
+  simp
+
+example {n : ℕ} (m : Fin n →₀ ℕ) : (ofFinsupp m).toFinsupp = m := by
+  simp
+
+example {n : ℕ} (m : CMvMonomial n) : m + 0 = m := by
+  simp [add_zero]
+
+example : CMvMonomial.totalDegree (#m[1, 2] : CMvMonomial 2) = 3 := by
+  native_decide
+
+example : CMvMonomial.degreeOf (#m[3, 4] : CMvMonomial 2) ⟨1, by decide⟩ = 4 := by
+  native_decide
+
+end CMvMonomial
+end CPoly
diff --git a/tests/CompPolyTests/Multivariate/Restrict.lean b/tests/CompPolyTests/Multivariate/Restrict.lean
new file mode 100644
index 0000000..3e01237
--- /dev/null
+++ b/tests/CompPolyTests/Multivariate/Restrict.lean
@@ -0,0 +1,27 @@
+import CompPoly.Multivariate.Restrict
+
+namespace CPoly
+
+open CMvPolynomial
+
+-- TODO: add concrete finite-support examples exercising mixed degree bounds.
+
+example (d : ℕ) : restrictTotalDegree (n := 2) (R := ℚ) d (0 : CMvPolynomial 2 ℚ) = 0 := by
+  simp [restrictTotalDegree_zero]
+
+example (d : ℕ) : restrictDegree (n := 2) (R := ℚ) d (0 : CMvPolynomial 2 ℚ) = 0 := by
+  simp [restrictDegree_zero]
+
+example (d d' : ℕ) (p : CMvPolynomial 2 ℚ) :
+    restrictTotalDegree d (restrictTotalDegree d' p) = restrictTotalDegree (min d d') p := by
+  simp [restrictTotalDegree_restrictTotalDegree]
+
+example (d d' : ℕ) (p : CMvPolynomial 2 ℚ) :
+    restrictDegree d (restrictDegree d' p) = restrictDegree (min d d') p := by
+  simp [restrictDegree_restrictDegree]
+
+example (d d' : ℕ) (p : CMvPolynomial 2 ℚ) :
+    restrictTotalDegree d (restrictDegree d' p) = restrictDegree d' (restrictTotalDegree d p) := by
+  simp [restrictTotalDegree_restrictDegree_comm]
+
+end CPoly
diff --git a/tests/CompPolyTests/Multivariate/VarsDegrees.lean b/tests/CompPolyTests/Multivariate/VarsDegrees.lean
new file mode 100644
index 0000000..983f377
--- /dev/null
+++ b/tests/CompPolyTests/Multivariate/VarsDegrees.lean
@@ -0,0 +1,25 @@
+import CompPoly.Multivariate.VarsDegrees
+
+namespace CPoly
+
+open CMvPolynomial
+
+-- TODO: add nontrivial examples relating `vars`/`degrees` to explicit monomials.
+
+example (i : Fin 3) : (0 : CMvPolynomial 3 ℚ).degreeOf i = 0 := by
+  simp [degreeOf_zero]
+
+example : (0 : CMvPolynomial 3 ℚ).degrees = 0 := by
+  simp [degrees_zero]
+
+example : (0 : CMvPolynomial 3 ℚ).vars = ∅ := by
+  simp [vars_zero]
+
+example : (1 : CMvPolynomial 3 ℚ).degrees = 0 := by
+  simp [degrees_one]
+
+example (p : CMvPolynomial 3 ℚ) (i : Fin 3) :
+    i ∈ p.vars ↔ 0 < p.degreeOf i := by
+  simp [mem_vars_iff_degreeOf_pos]
+
+end CPoly
diff --git a/tests/CompPolyTests/Univariate/Basic.lean b/tests/CompPolyTests/Univariate/Basic.lean
new file mode 100644
index 0000000..4b81755
--- /dev/null
+++ b/tests/CompPolyTests/Univariate/Basic.lean
@@ -0,0 +1,33 @@
+import CompPoly.Univariate.Basic
+
+namespace CompPoly
+namespace CPolynomial
+
+-- TODO: expand this file with more operation-level regression checks.
+
+example (r : ℚ) : (C r).coeff 0 = r := by
+  simpa using coeff_C (R := ℚ) r 0
+
+example (r : ℚ) : (C r).coeff 3 = 0 := by
+  simpa using coeff_C (R := ℚ) r 3
+
+example : (X : CPolynomial ℚ).coeff 1 = 1 := by
+  native_decide
+
+example (p : CPolynomial ℚ) : (divX p).coeff 2 = p.coeff 3 := by
+  simpa using coeff_divX (R := ℚ) p 2
+
+example (p : CPolynomial ℚ) : p + 0 = p := by
+  simp
+
+example (p : CPolynomial ℚ) : 0 + p = p := by
+  simp
+
+example (p : CPolynomial ℚ) : p * 0 = 0 := by
+  simp
+
+example (p : CPolynomial ℚ) : 1 * p = p := by
+  simp
+
+end CPolynomial
+end CompPoly
diff --git a/tests/CompPolyTests/Univariate/ToPoly.lean b/tests/CompPolyTests/Univariate/ToPoly.lean
new file mode 100644
index 0000000..733950b
--- /dev/null
+++ b/tests/CompPolyTests/Univariate/ToPoly.lean
@@ -0,0 +1,27 @@
+import CompPoly.Univariate.ToPoly
+
+namespace CompPoly
+namespace CPolynomial
+
+-- TODO: add focused edge cases for degree/leadingCoeff transport once API settles.
+
+example (p : Polynomial ℚ) : p.toImpl.toPoly = p := by
+  simpa using Raw.toPoly_toImpl (Q := ℚ) (p := p)
+
+example (p : CPolynomial.Raw ℚ) : p.toPoly.toImpl = p.trim := by
+  simp [Raw.toImpl_toPoly]
+
+example (p : CPolynomial ℚ) : p.toPoly.toImpl = p := by
+  simp [toImpl_toPoly_of_canonical]
+
+example (p q : CPolynomial ℚ) : (p + q).toPoly = p.toPoly + q.toPoly := by
+  simp [toPoly_add]
+
+example (p q : CPolynomial ℚ) : (p * q).toPoly = p.toPoly * q.toPoly := by
+  simp [toPoly_mul]
+
+example (r : ℚ) : (C r).toPoly = Polynomial.C r := by
+  simp [C_toPoly]
+
+end CPolynomial
+end CompPoly

From bb73f4abfbcc1eb9bf119bf06263f826a59e4d95 Mon Sep 17 00:00:00 2001
From: Derek Sorensen <d@dhsorens.com>
Date: Fri, 27 Feb 2026 15:42:56 +0000
Subject: [PATCH 4/7] fix: linting errors

---
 scripts/style-exceptions.txt                      |  2 ++
 tests/CompPolyTests/Multivariate/CMvMonomial.lean | 11 +++++++++++
 tests/CompPolyTests/Multivariate/Restrict.lean    | 11 +++++++++++
 tests/CompPolyTests/Multivariate/VarsDegrees.lean | 11 +++++++++++
 tests/CompPolyTests/Univariate/Basic.lean         | 11 +++++++++++
 tests/CompPolyTests/Univariate/Raw.lean           | 11 +++++++++++
 tests/CompPolyTests/Univariate/ToPoly.lean        | 12 ++++++++++++
 7 files changed, 69 insertions(+)

diff --git a/scripts/style-exceptions.txt b/scripts/style-exceptions.txt
index 94c58ea..cd6ad8f 100644
--- a/scripts/style-exceptions.txt
+++ b/scripts/style-exceptions.txt
@@ -2,6 +2,8 @@ lake-manifest.json : line 1 : ERR_COP : Malformed or missing copyright header :
 lake-manifest.json : line 1 : ERR_MOD : Module docstring missing, or too late : ERR_MOD
 lakefile.lean : line 1 : ERR_COP : Malformed or missing copyright header : ERR_COP
 lakefile.lean : line 1 : ERR_MOD : Module docstring missing, or too late : ERR_MOD
+tests/CompPolyTests.lean : line 1 : ERR_COP : Malformed or missing copyright header : ERR_COP
+tests/CompPolyTests.lean : line 1 : ERR_MOD : Module docstring missing, or too late : ERR_MOD
 lean-toolchain : line 1 : ERR_COP : Malformed or missing copyright header : ERR_COP
 lean-toolchain : line 1 : ERR_MOD : Module docstring missing, or too late : ERR_MOD
 lakefile.lean : line 1 : ERR_TAC2 : In the past, importing 'Lake' has led to dramatic slow-downs of the linter (see e.g. mathlib4#13779). Please consider carefully if this import is useful and make sure to benchmark it. If this is fine, feel free to allow this linter. : ERR_TAC2
diff --git a/tests/CompPolyTests/Multivariate/CMvMonomial.lean b/tests/CompPolyTests/Multivariate/CMvMonomial.lean
index 4db1003..24fa300 100644
--- a/tests/CompPolyTests/Multivariate/CMvMonomial.lean
+++ b/tests/CompPolyTests/Multivariate/CMvMonomial.lean
@@ -1,5 +1,16 @@
+/-
+Copyright (c) 2026 CompPoly. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Derek Sorensen
+-/
 import CompPoly.Multivariate.CMvMonomial
 
+/-!
+  # Multivariate Monomial Tests
+
+  First-pass sanity checks for `CompPoly.Multivariate.CMvMonomial`.
+-/
+
 namespace CPoly
 namespace CMvMonomial
 
diff --git a/tests/CompPolyTests/Multivariate/Restrict.lean b/tests/CompPolyTests/Multivariate/Restrict.lean
index 3e01237..f884969 100644
--- a/tests/CompPolyTests/Multivariate/Restrict.lean
+++ b/tests/CompPolyTests/Multivariate/Restrict.lean
@@ -1,5 +1,16 @@
+/-
+Copyright (c) 2026 CompPoly. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Derek Sorensen
+-/
 import CompPoly.Multivariate.Restrict
 
+/-!
+  # Multivariate Restrict Tests
+
+  Basic sanity checks for `restrictTotalDegree` and `restrictDegree`.
+-/
+
 namespace CPoly
 
 open CMvPolynomial
diff --git a/tests/CompPolyTests/Multivariate/VarsDegrees.lean b/tests/CompPolyTests/Multivariate/VarsDegrees.lean
index 983f377..205c4d0 100644
--- a/tests/CompPolyTests/Multivariate/VarsDegrees.lean
+++ b/tests/CompPolyTests/Multivariate/VarsDegrees.lean
@@ -1,5 +1,16 @@
+/-
+Copyright (c) 2026 CompPoly. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Derek Sorensen
+-/
 import CompPoly.Multivariate.VarsDegrees
 
+/-!
+  # Multivariate Vars/Degrees Tests
+
+  Basic sanity checks for `vars`, `degrees`, and `degreeOf`.
+-/
+
 namespace CPoly
 
 open CMvPolynomial
diff --git a/tests/CompPolyTests/Univariate/Basic.lean b/tests/CompPolyTests/Univariate/Basic.lean
index 4b81755..2495cea 100644
--- a/tests/CompPolyTests/Univariate/Basic.lean
+++ b/tests/CompPolyTests/Univariate/Basic.lean
@@ -1,5 +1,16 @@
+/-
+Copyright (c) 2026 CompPoly. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Derek Sorensen
+-/
 import CompPoly.Univariate.Basic
 
+/-!
+  # Univariate Basic Tests
+
+  First-pass sanity checks for key API behavior in `CompPoly.Univariate.Basic`.
+-/
+
 namespace CompPoly
 namespace CPolynomial
 
diff --git a/tests/CompPolyTests/Univariate/Raw.lean b/tests/CompPolyTests/Univariate/Raw.lean
index d8b1035..b4a629d 100644
--- a/tests/CompPolyTests/Univariate/Raw.lean
+++ b/tests/CompPolyTests/Univariate/Raw.lean
@@ -1,5 +1,16 @@
+/-
+Copyright (c) 2026 CompPoly. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Derek Sorensen, Elias Judin
+-/
 import CompPoly.Univariate.Raw
 
+/-!
+  # Univariate Raw Regression Tests
+
+  Lightweight regression checks for `CompPoly.Univariate.Raw`.
+-/
+
 namespace CompPoly
 namespace CPolynomial.Raw
 
diff --git a/tests/CompPolyTests/Univariate/ToPoly.lean b/tests/CompPolyTests/Univariate/ToPoly.lean
index 733950b..f165ad6 100644
--- a/tests/CompPolyTests/Univariate/ToPoly.lean
+++ b/tests/CompPolyTests/Univariate/ToPoly.lean
@@ -1,5 +1,17 @@
+/-
+Copyright (c) 2026 CompPoly. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Derek Sorensen
+-/
 import CompPoly.Univariate.ToPoly
 
+/-!
+  # Univariate ToPoly Tests
+
+  First-pass sanity checks for conversion and transport lemmas in
+  `CompPoly.Univariate.ToPoly`.
+-/
+
 namespace CompPoly
 namespace CPolynomial
 

From 5f65164c322e4db89239b021008ab5c88ead4233 Mon Sep 17 00:00:00 2001
From: Derek Sorensen <d@dhsorens.com>
Date: Fri, 27 Feb 2026 15:46:10 +0000
Subject: [PATCH 5/7] fix: revert comment

---
 CompPoly/Univariate/Raw.lean | 9 +--------
 1 file changed, 1 insertion(+), 8 deletions(-)

diff --git a/CompPoly/Univariate/Raw.lean b/CompPoly/Univariate/Raw.lean
index d7a45a4..3e16ab7 100644
--- a/CompPoly/Univariate/Raw.lean
+++ b/CompPoly/Univariate/Raw.lean
@@ -1585,14 +1585,7 @@ instance : Neg (CPolynomial.Raw R) := ⟨neg⟩
 instance : Sub (CPolynomial.Raw R) := ⟨sub⟩
 instance : IntCast (CPolynomial.Raw R) := ⟨fun n => C (n : R)⟩
 
-/-- Division with remainder by a monic polynomial using polynomial long division.
-
-We use `p.size` as fuel for the recursion. This is always sufficient because
-each division step strictly decreases the size of the remainder (the leading
-term is cancelled by a monic divisor, and `trim` removes any resulting trailing
-zeros). The guard `p.size < q.size` triggers as soon as the remainder is of
-lower degree than the divisor, so the recursion terminates cleanly even when
-cancellation causes the size to drop by more than one in a single step. -/
+/-- Division with remainder by a monic polynomial using polynomial long division. -/
 def divModByMonicAux [Field R] (p : CPolynomial.Raw R) (q : CPolynomial.Raw R) :
     CPolynomial.Raw R × CPolynomial.Raw R :=
   go (p.size - q.size) p q

From 577424fc4dd25f4f3c3f43110fa99953201f6c07 Mon Sep 17 00:00:00 2001
From: Derek Sorensen <d@dhsorens.com>
Date: Fri, 27 Feb 2026 15:55:29 +0000
Subject: [PATCH 6/7] feat: refactor tests out of CompPoly

---
 CompPoly/Univariate/Raw.lean | 22 ----------------------
 1 file changed, 22 deletions(-)

diff --git a/CompPoly/Univariate/Raw.lean b/CompPoly/Univariate/Raw.lean
index a016ee3..1da5565 100644
--- a/CompPoly/Univariate/Raw.lean
+++ b/CompPoly/Univariate/Raw.lean
@@ -1615,28 +1615,6 @@ def modByMonic [Field R] (p : CPolynomial.Raw R) (q : CPolynomial.Raw R) :
     CPolynomial.Raw R :=
   (divModByMonicAux p q).2
 
-/-- Regression test for issue #115: `(X^2 - 1) / (X + 1) = X - 1` with zero remainder. -/
-example :
-    divByMonic ((X : CPolynomial.Raw ℚ) ^ 2 - C 1) ((X : CPolynomial.Raw ℚ) + C 1)
-      = #[-(1 : ℚ), 1] := by
-  native_decide
-
-example :
-    modByMonic ((X : CPolynomial.Raw ℚ) ^ 2 - C 1) ((X : CPolynomial.Raw ℚ) + C 1)
-      = #[] := by
-  native_decide
-
-/-- Regression test for review-thread case: `X^3 = (X^2 + 1) * X + (-X)`. -/
-example :
-    divByMonic ((X : CPolynomial.Raw ℚ) ^ 3) ((X : CPolynomial.Raw ℚ) ^ 2 + C 1)
-      = #[(0 : ℚ), 1] := by
-  native_decide
-
-example :
-    modByMonic ((X : CPolynomial.Raw ℚ) ^ 3) ((X : CPolynomial.Raw ℚ) ^ 2 + C 1)
-      = #[(0 : ℚ), -(1 : ℚ)] := by
-  native_decide
-
 /-- Division of two `CPolynomial.Raw`s. -/
 def div [Field R] (p q : CPolynomial.Raw R) : CPolynomial.Raw R :=
   (C (q.leadingCoeff)⁻¹ • p).divByMonic (C (q.leadingCoeff)⁻¹ * q)

From 7982948346d8468e84ece424c4ed3e42594f9884 Mon Sep 17 00:00:00 2001
From: Derek Sorensen <d@dhsorens.com>
Date: Tue, 3 Mar 2026 15:11:33 +0000
Subject: [PATCH 7/7] fix: warning about native_decide

---
 tests/CompPolyTests/Multivariate/CMvMonomial.lean | 2 ++
 tests/CompPolyTests/Univariate/Raw.lean           | 4 ++++
 2 files changed, 6 insertions(+)

diff --git a/tests/CompPolyTests/Multivariate/CMvMonomial.lean b/tests/CompPolyTests/Multivariate/CMvMonomial.lean
index 24fa300..e66b42b 100644
--- a/tests/CompPolyTests/Multivariate/CMvMonomial.lean
+++ b/tests/CompPolyTests/Multivariate/CMvMonomial.lean
@@ -26,9 +26,11 @@ example {n : ℕ} (m : CMvMonomial n) : m + 0 = m := by
   simp [add_zero]
 
 example : CMvMonomial.totalDegree (#m[1, 2] : CMvMonomial 2) = 3 := by
+  -- TODO avoid using native_decide for soundness issues
   native_decide
 
 example : CMvMonomial.degreeOf (#m[3, 4] : CMvMonomial 2) ⟨1, by decide⟩ = 4 := by
+  -- TODO avoid using native_decide for soundness issues
   native_decide
 
 end CMvMonomial
diff --git a/tests/CompPolyTests/Univariate/Raw.lean b/tests/CompPolyTests/Univariate/Raw.lean
index b4a629d..adf85fa 100644
--- a/tests/CompPolyTests/Univariate/Raw.lean
+++ b/tests/CompPolyTests/Univariate/Raw.lean
@@ -18,22 +18,26 @@ namespace CPolynomial.Raw
 example :
     divByMonic ((X : CPolynomial.Raw ℚ) ^ 2 - C 1) ((X : CPolynomial.Raw ℚ) + C 1)
       = #[-(1 : ℚ), 1] := by
+  -- TODO avoid using native_decide for soundness issues
   native_decide
 
 example :
     modByMonic ((X : CPolynomial.Raw ℚ) ^ 2 - C 1) ((X : CPolynomial.Raw ℚ) + C 1)
       = #[] := by
+  -- TODO avoid using native_decide for soundness issues
   native_decide
 
 /-- Regression test for review-thread case: `X^3 = (X^2 + 1) * X + (-X)`. -/
 example :
     divByMonic ((X : CPolynomial.Raw ℚ) ^ 3) ((X : CPolynomial.Raw ℚ) ^ 2 + C 1)
       = #[(0 : ℚ), 1] := by
+  -- TODO avoid using native_decide for soundness issues
   native_decide
 
 example :
     modByMonic ((X : CPolynomial.Raw ℚ) ^ 3) ((X : CPolynomial.Raw ℚ) ^ 2 + C 1)
       = #[(0 : ℚ), -(1 : ℚ)] := by
+  -- TODO avoid using native_decide for soundness issues
   native_decide
 
 end CPolynomial.Raw