Machine-Checked Computational Group Theory in Lean 4: Operational Schreier-Sims Stabilizer Chains, BSGS Sifting, and Backtrack Ordered Partitions

Abstract

gap-lean4-port (Release v0.2.0): Formally Machine-Checked Computational Group Theory in Lean 4 and Mathlib4 This repository and research package contains the complete, standalone formalization of foundational computational discrete algebra and permutation group algorithms verified in the Lean 4 interactive theorem prover (v4.34.1) against Mathlib4 with zero unproven axioms (sorry). While modern interactive proof assistants possess extensive abstract algebraic hierarchies, constructive and operational permutation group algorithms—such as Charles Sims' 1970 Schreier-Sims algorithm, transversal lookup trees, and backtrack ordered partition refinement—have remained largely absent from dependent type theory. This project bridges that gap by directly modeling and formally verifying the operational algorithms of the GAP (Groups, Algorithms, Programming) computational algebra library. Key Machine-Verified Theorems (35 Theorems, 0 sorry, 0 admit) Operational Schreier-Sims Stabilizer Chains (lib/stbc.gi, GAP-0299): Transversal invariance, single & multi-level sifting, base point fixation theorem, and BSGS membership soundness/completeness. Backtrack Ordered Partitions (lib/partitio.gi, GAP-0332): Cell refinement (splitCellByPred), disjointness, cardinality conservation, and predicate exactness. Cyclotomic Extension Rings (lib/zmodnze.gi, GAP-0332): Exact cardinality theorem |Z/nZ(eps_m)| = n^m. Constructive Modular Inverses & Residues (lib/zmodnz.gi, GAP-0331): Canonical GAP representation, executable Extended Euclidean GCD inverse, and unit characterization. Axiomatic Purity & Verification Audit Audited via Lean 4's #print axioms command. Depends exclusively on standard Lean 4 foundations: [propext, Classical.choice, Quot.sound]. Build & Verification Instructions $ git clone https://github.com/pCwOrM/gap-lean4-port.git $ cd gap-lean4-port $ lake build RequestProject