Module two_group 

The 2-group frontier — climbing past K(G,1) to genuine 2-types, honestly.

The tower named its 1-truncation: a discrete symmetry group G gives the ∞-groupoid BG = K(G,1) — π₁ = G, πₙ = 0 for n ≥ 2. To populate π₂ you need a 2-group (a symmetry whose symmetries themselves have symmetries), modeled by a crossed module ∂: H → G:

• π₁ = coker(∂) = G / ∂(H) — the symmetries that survive modulo the higher cells, and
• π₂ = ker(∂) — the genuinely higher homotopy.

This module builds that machinery and is honest about where our SAT structure sits in it: our symmetry is the degenerate crossed module 1 → G (so π₂ = 0, BG = K(G,1)), and a genuine 2-group Z/m → 1 gives π₂ = Z/m ≠ 0 — a K(Z/m, 2). The machinery reads off both; our case is the 1-type. Climbing further (π₃, …) is the same construction one categorical level up — the frontier, named, not claimed.

Structs

CrossedModule

A crossed module ∂: H → G — the algebraic model of a 2-group. partial[h] is ∂(h) ∈ G, a group homomorphism. Its homotopy groups are π₁ = coker(∂) and π₂ = ker(∂).

FiniteGroup

A finite group by its (0-indexed) multiplication table.