feat(fields): add fast Mersenne31 arithmetic

CompPoly.lean

@@ -132,6 +132,9 @@ public import CompPoly.Fields.KoalaBear.Ext6.SexticCertData
 public import CompPoly.Fields.KoalaBear.Ext6.SexticIrreducible
 public import CompPoly.Fields.KoalaBear.Fast
 public import CompPoly.Fields.Mersenne
+public import CompPoly.Fields.Mersenne31
+public import CompPoly.Fields.Mersenne31.Basic
+public import CompPoly.Fields.Mersenne31.Fast
 public import CompPoly.Fields.Montgomery.Basic
 public import CompPoly.Fields.Montgomery.Native32
 public import CompPoly.Fields.Montgomery.Native32Field

CompPoly/Fields/Mersenne.lean

@@ -1,29 +1,16 @@
 /-
 Copyright (c) 2024 ArkLib Contributors. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Quang Dao
+Authors: Quang Dao, Varun Thakore
 -/
 module
 
-public import CompPoly.Fields.PrattCertificate
+public import CompPoly.Fields.Mersenne31
 
 /-!
-  # Mersenne prime field `2^{31} - 1`
+# Deprecated Mersenne31 compatibility import
 
-  This is the field used in Circle STARKs.
+This module re-exports `CompPoly.Fields.Mersenne31` for compatibility with the former import path.
 -/
 
-@[expose] public section
-
-namespace Mersenne31
-
-@[reducible]
-def fieldSize : Nat := 2 ^ 31 - 1
-
-abbrev Field := ZMod fieldSize
-
-theorem is_prime : Nat.Prime fieldSize := by
-  unfold fieldSize
-  pratt
-
-end Mersenne31
+deprecated_module "Use `CompPoly.Fields.Mersenne31` instead" (since := "2026-08-25")

CompPoly/Fields/Mersenne31.lean

@@ -0,0 +1,20 @@
+/-
+Copyright (c) 2024 CompPoly Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Quang Dao, Varun Thakore
+-/
+
+module
+
+public import CompPoly.Fields.Mersenne31.Basic
+public import CompPoly.Fields.Mersenne31.Fast
+
+/-!
+  # Mersenne31 prime field `2^{31} - 1`
+
+  Facade module for the Mersenne31 field. It re-exports the canonical `ZMod` model
+  from `CompPoly.Fields.Mersenne31.Basic` and the native-word implementation from
+  `CompPoly.Fields.Mersenne31.Fast`.
+-/
+
+@[expose] public section

CompPoly/Fields/Mersenne31/Basic.lean

@@ -0,0 +1,48 @@
+/-
+Copyright (c) 2024 CompPoly Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Quang Dao, Varun Thakore
+-/
+
+module
+
+public import CompPoly.Fields.Basic
+public import CompPoly.Fields.PrattCertificate
+
+/-!
+  # Mersenne prime field `2^{31} - 1`
+
+  This is the field used in Circle STARKs.
+-/
+
+@[expose] public section
+
+namespace Mersenne31
+
+/-- The Mersenne31 prime modulus `2^31 - 1`. -/
+@[reducible]
+def fieldSize : Nat := 2 ^ 31 - 1
+
+/-- The canonical mathematical Mersenne31 field, implemented as integers modulo
+`fieldSize`. -/
+abbrev Field := ZMod fieldSize
+
+/-- The Mersenne31 modulus is prime, verified by a Pratt certificate. -/
+theorem is_prime : Nat.Prime fieldSize := by
+  unfold fieldSize
+  pratt
+
+/-- Register primality of `fieldSize` for Mathlib instances such as `ZMod.instField`. -/
+instance : Fact (Nat.Prime fieldSize) := ⟨is_prime⟩
+
+/-- The canonical Mersenne31 carrier is a field because its modulus is prime. -/
+instance : _root_.Field Field := ZMod.instField fieldSize
+
+/-- Mersenne31 has characteristic different from two. -/
+instance : NonBinaryField Field where
+  char_neq_2 := by
+    -- `decide` can discharge this concrete ZMod equality.
+    simpa [Field, fieldSize] using
+      (by decide : (2 : ZMod (2 ^ 31 - 1)) ≠ 0)
+
+end Mersenne31