[Show and Tell] Formally Verifying Foundational Computational Group Theory in Lean 4: Operational Schreier-Sims & Backtrack Partitions (Phase 2, Release v0.2.0)

[pCwOrM]

Hello GAP Community,

Following our initial port of modular residue arithmetic, we are pleased to present Phase 2 (Release v0.2.0) of our formal verification initiative: Operational Computational Group Theory and Backtrack Combinatorics in Lean 4 / Mathlib.

• GitHub Repository: pCwOrM/gap-lean4-port
• Official Release v0.2.0: v0.2.0 Release Assets & Notes
• Axiomatic Status: 35 Theorems verified with 0 sorry, 0 admit, 0 external axioms

---

Clarifying the Scope: Algorithm Verification vs. Kernel Emulation

In mathematical software verification, there are two distinct objectives:

1. Runtime & Kernel Verification: Writing a verified C/C++ compiler, AST parser, and memory-model interpreter for the GAP runtime itself.
2. Algorithmic & Mathematical Verification: Formalizing the deep combinatorial algorithms, invariants, and representations developed by the GAP authors (Heiko Theißen, Ákos Seress, Alexander Konovalov, Thomas Breuer) as machine-checked interactive theorems in Lean 4.

Our work focuses rigorously on (2). Rather than relying on non-constructive transfer, Phase 2 implements and machine-checks the executable computational group theory procedures and inductive invariants that form the backbone of GAP's permutation group engine.

---

What Has Been Formalized in Release v0.2.0

1. Stabiliser Chains & Schreier-Sims Sifting (lib/stbc.gi, GAP-0299)

• Module: RequestProject.Gap.Library.Stbc
• Historical GAP Source: lib/stbc.gi (Heiko Theißen & Ákos Seress)
• Constructive Structures:
  • GAP.Stbc.StabLevel: Models each level of a stabiliser chain with base point $\beta_i$, basic orbit $\Delta_i$, strong generators $S_i$, and transversal tree inverse representatives $u_i$.
  • GAP.Stbc.StabChain: The hierarchical tower of stabilisers $[G^{(1)}, G^{(2)}, \dots, G^{(k)}]$.
• Operational Procedures:
  • Single-level coset reduction siftOneLevel: $g \mapsto u_y^{-1} \cdot g$.
  • Full Schreier sifting siftFull / siftedPermutation.
  • Base & Strong Generating Set (BSGS) membership testing: membershipTestKnownBase.
  • Incremental transversal extension: extendSchreierPoint.
• Formally Proved Invariants (0 sorry):
  • siftOneLevel_fixes_basePoint: Proves that single-level sifting strictly fixes the base point $\beta_i$.
  • siftFull_fixes_all_basePoints: Proves that full sifting fixes every base point in the base sequence $(\beta_1, \dots, \beta_k)$.
  • siftedPermutation_mem_subgroup_iff: Proves invariant preservation during coset reduction.
  • membershipTestKnownBase_sound: Proves soundness of the BSGS membership decision procedure.
  • membershipTestKnownBase_iff_mem: Soundness and completeness equivalence: membershipTestKnownBase chain g = true ↔ g ∈ G.
  • extendSchreierPoint_invariant: Machine-checks transversal tree invariant preservation under orbit extension.

2. Ordered Partitions & Cell Refinement for Backtrack Search (lib/partitio.gi, GAP-0332)

• Module: RequestProject.Gap.Library.Partitio
• Historical GAP Source: lib/partitio.gi (Heiko Theißen)
• Structures & Invariants:
  • OrderedPartition: Partition of domain $\Omega$ into ordered, non-empty, pairwise disjoint cells.
  • splitCellByPred: Core cell refinement operation underlying GAP's SplitCell and IsolatePoint.
• Formally Proved Invariants (0 sorry):
  • splitCellByPred_disjoint: Machine-checks that cell splitting yields mutually disjoint subcells.
  • splitCellByPred_union: Proves exact element conservation (subcells partition the original cell).
  • splitCellByPred_length_sum: Proves cardinality conservation $|C_{\text{yes}}| + |C_{\text{no}}| = |C|$.
  • mem_splitCellByPred_iff: Exact predicate-driven membership equivalence.

3. Cyclotomic Extension Rings $\mathbb{Z}/n\mathbb{Z}(\varepsilon_m)$ (lib/zmodnze.gi, GAP-0332)

• Module: RequestProject.Gap.Library.Zmodnze
• Historical GAP Source: lib/zmodnze.gi (Alexander Konovalov)
• Theorems:
  • Formally models elements as coefficient vectors Fin m → GAP.ZModnZObj n with convolution group-ring multiplication mulOp.
  • Proves GAP's exact cardinality theorem (card_eq):
    $$\text{card}(\mathbb{Z}/n\mathbb{Z}(\varepsilon_m)) = n^m$$

4. Constructive Modular Inverses via Extended Euclidean GCD (lib/zmodnz.gi, GAP-0331)

• Module: RequestProject.Gap.Library.Zmodnz
• Historical GAP Source: lib/zmodnz.gi (Thomas Breuer)
• Theorems:
  • Dual architecture: Mathlib ring/field equivalence alongside executable isUnitExec and constructive inverseOpExec via Extended GCD (Nat.gcdA Bézout coefficients).
  • Machine-checked theorem inverseOpExec_correct: Proves that whenever isUnitExec a = true, inverseOpExec a produces a concrete inverse satisfying exact modular multiplication with 0 non-constructive choice.

---

Axiomatic Purity Audit

Every single theorem across the 4 modules has been audited with #print axioms:

• Axioms Used: Exclusively Lean 4 core foundational axioms ([propext, Classical.choice, Quot.sound]).
• External Axioms: 0
• sorry / admit: 0
• @[implemented_by]: 0

---

Independent Verification Instructions

Anyone can independently clone and machine-check the proofs:

git clone https://github.com/pCwOrM/gap-lean4-port.git
cd gap-lean4-port
lake build RequestProject

We hope this provides a rigorous, concrete bridge between computational group theory algorithms and modern interactive theorem proving. Feedback and mathematical discussion from the GAP community are warmly welcomed!

Best regards,

Volkan Dagli & Family (@pCwOrM)
ITouch Systems Formal Verification Lab