feat(fields): add Mersenne31 circle domain skeleton

[adrienlacombe]

Summary

Adds a STWO-style circle-domain skeleton on top of the Mersenne31 field support merged in #257.

Changes

• Adds CompPoly.Fields.Mersenne31.Circle.
• Defines Mersenne31 circle points as pairs satisfying x^2 + y^2 = 1.
• Records the STWO M31 circle generator (2, 1268011823) and proves it lies on the circle.
• Adds point conjugation, antipode, addition, and repeated addition.
• Defines CirclePointIndex modulo 2^31, subgroup generator indices, cosets, conjugate cosets, circle domains, and canonical cosets.
• Proves structural domain facts covering coset size and stepping, conjugate index ordering, domain size, and canonical-domain log size.
• Adds regression tests and exports the new source and test modules through the aggregate imports.

Non-goals

This intentionally does not prove that the generator has order 2^31, and it does not formalize FRI or circle polynomial evaluation. Those remain follow-on work after the domain skeleton stabilizes.

Validation

• lake build CompPoly.Fields.Mersenne31.Circle CompPolyTests.Fields.Mersenne31.Circle
• lake test
• lake build
• lake exe axiomsweep --check
• ./scripts/update-lib.sh
• ./scripts/check-imports.sh
• ./scripts/lint-style.sh
• python3 ./scripts/check-docs-integrity.py
• git diff --check upstream/main..HEAD

All checks pass under Lean v4.33.1.

[github-actions]

🤖 PR Summary

Store the analysis in the variable analysis

---

Statistics

Metric	Count
📝 Files Changed	5
✅ Lines Added	461
❌ Lines Removed	1

---

Lean Declarations

✏️ Added: 63 declaration(s)

CompPoly/Fields/Mersenne31/Circle.lean (48)

• abbrev CirclePointIndex
• abbrev Field
• def OnCircle (x y : Field) : Prop
• def add (p q : Point) : Point where
• def antipode (p : Point) : Point where
• def circleDomain (c : CanonicCoset) : CircleDomain
• def conjugate (c : Coset) : Coset where
• def coset (c : CanonicCoset) : Coset
• def generator : CirclePointIndex
• def generatorX : Field
• def generatorY : Field
• def halfCoset (c : CanonicCoset) : Coset
• def halfOdds (logSize : Nat) (hlogSize : logSize + 2 ≤ logOrder) : Coset
• def indexAt (D : CircleDomain) (i : Nat) : CirclePointIndex
• def logOrder : Nat
• def logSize (D : CircleDomain) : Nat
• def new (halfCoset : Coset) : CircleDomain where
• def nsmul (p : Point) : Nat → Point
• def odds (logSize : Nat) (hlogSize : logSize + 1 ≤ logOrder) : Coset
• def order : Nat
• def pointAt (D : CircleDomain) (i : Nat) : Point
• def size (D : CircleDomain) : Nat
• def subgroup (logSize : Nat) (hlogSize : logSize ≤ logOrder) : Coset
• def subgroupGen (logSize : Nat) : CirclePointIndex
• def toPoint (i : CirclePointIndex) : Point
• def zero : Point where
• theorem circleDomain_logSize (c : CanonicCoset) : c.circleDomain.logSize = c.logSize
• theorem circleDomain_size (c : CanonicCoset) : c.circleDomain.size = 2 ^ c.logSize
• theorem conjugate_indexAt (c : Coset) (i : Nat) :
• theorem conjugate_initialIndex (c : Coset) :
• theorem conjugate_logSize (c : Coset) : c.conjugate.logSize = c.logSize
• theorem conjugate_stepSize (c : Coset) : c.conjugate.stepSize = -c.stepSize
• theorem conjugate_x (p : Point) : (-p).x = p.x
• theorem conjugate_y (p : Point) : (-p).y = -p.y
• theorem ext {p q : Point} (hx : p.x = q.x) (hy : p.y = q.y) : p = q
• theorem generator_onCircle : OnCircle generatorX generatorY
• theorem indexAt_left (D : CircleDomain) (i : Nat) (hi : i < D.halfCoset.size) :
• theorem indexAt_right (D : CircleDomain) (i : Nat) :
• theorem indexAt_succ (c : Coset) (i : Nat) :
• theorem indexAt_zero (c : Coset) : c.indexAt 0 = c.initialIndex
• theorem size_eq_two_mul_halfSize (D : CircleDomain) :
• theorem subgroupGen_logOrder : subgroupGen logOrder = generator
• theorem subgroupGen_zero : subgroupGen 0 = 0
• theorem toPoint_generator : toPoint CirclePointIndex.generator = Circle.generator
• theorem toPoint_zero : toPoint 0 = 0
• theorem zero_add (p : Point) : (0 : Point) + p = p
• theorem zero_x : (0 : Point).x = 1
• theorem zero_y : (0 : Point).y = 0

tests/CompPolyTests/Fields/Mersenne31/Circle.lean (15)

• def smallCanonicCoset : CanonicCoset where
• def smallDomain : CircleDomain
• def smallHalfCoset : Coset
• example (i : Nat) : smallHalfCoset.conjugate.indexAt i = -smallHalfCoset.indexAt i
• example (i : Nat) :
• example : CirclePointIndex.subgroupGen 0 = 0
• example : CirclePointIndex.subgroupGen logOrder = CirclePointIndex.generator
• example : CirclePointIndex.toPoint 0 = 0
• example : CirclePointIndex.toPoint CirclePointIndex.generator = generator
• example : OnCircle (Point.antipode generator).x (Point.antipode generator).y
• example : OnCircle (generator + generator).x (generator + generator).y
• example : OnCircle generatorX generatorY
• example : generator.x = 2
• example : generator.y = 1268011823
• example : smallHalfCoset.indexAt 0 = smallHalfCoset.initialIndex

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📄 **Per-File Summaries**

• CompPoly.lean: A new public import CompPoly.Fields.Mersenne31.Circle was added to the module's public exports. This makes the definitions, theorems, and other declarations from that submodule available to consumers of the CompPoly library.
• CompPoly/Fields/Mersenne31.lean: The facade module CompPoly/Fields/Mersenne31.lean now publicly re-exports CompPoly.Fields.Mersenne31.Circle in addition to the existing Basic and Fast modules. The module-level doc comment has been updated to document that it also re-exports the circle-domain skeleton. No sorry or admit appear in the diff.
• CompPoly/Fields/Mersenne31/Circle.lean: This new file Circle.lean introduces the circle-domain layer for the Mersenne31 field used by STWO. It defines the Point structure on the circle x² + y² = 1, together with its identity, conjugate (negation), antipode, addition, and nsmul (repeated addition). Key theorems establish zero_x, zero_y, conjugate_x/y, and zero_add. The STWO Mersenne31 circle generator is defined with coordinates (2, 1268011823), verified via dec_trivial. The index type CirclePointIndex is an abbreviation for ZMod (2³¹), and its toPoint function maps an index to nsmul of the generator; supporting lemmas include toPoint_zero, toPoint_generator, subgroupGen_zero, and subgroupGen_logOrder. The Coset structure captures a coset with initial index, step size, and log size, providing indexAt, pointAt, a conjugate operation, and related theorems (indexAt_zero, indexAt_succ, conjugate_indexAt, etc.). The CircleDomain structure wraps a half-coset and gives domain-level indexing via indexAt, pointAt, and theorems size_eq_two_mul_halfSize, indexAt_left, indexAt_right. Finally, CanonicCoset specializes to the STWO canonical coset G_{2n} + ⟨G_n⟩, with a halfCoset and circleDomain that satisfy circleDomain_logSize and circleDomain_size. The module docstring notes that the homomorphism property of toPoint will be proved in a follow‑on PR; no sorry or admit appear in the file.
• tests/CompPolyTests.lean: Added a public import for the new CompPolyTests.Fields.Mersenne31.Circle module, which introduces tests or definitions related to the Mersenne31 circle group or its associated field arithmetic. This extends the Mersenne31 coverage in the test suite beyond the existing Fast implementation.
• tests/CompPolyTests/Fields/Mersenne31/Circle.lean: This new file tests/CompPolyTests/Fields/Mersenne31/Circle.lean adds a test suite for the Mersenne31 circle domain. It contains concrete examples proving OnCircle for generator coordinates, group operation results, and antipodes; checks logOrder = 31, order = 2147483648, and properties of CirclePointIndex.toPoint and CirclePointIndex.subgroupGen via simp; defines smallHalfCoset (Coset.halfOdds 3), smallDomain (CircleDomain.new smallHalfCoset), and smallCanonicCoset (with logSize := 4 and decidable proofs for bounds); and includes executable #guard statements validating sizes and a lemma smallDomain.indexAt ... = -smallHalfCoset.indexAt i using CircleDomain.indexAt_right. No sorry or admit appear in this file.

---

Last updated: 2026-09-01 19:33 UTC.