Fiber Architecture for Group Extensions in Lean 4: Cocycles, Splitting, and the Cohomological Bridge

We present a machine-checked formalization of the section 2-cocycle, splitting criterion, and embedding-problem equivalence for group extensions in Lean 4, built on Mathlib's GroupExtension API. The formalization is organized around a fiber architecture that decomposes extensions into layers: fibers over quotient elements (N-torsors), set-theoretic sections (always exist), and homomorphic splittings (may not exist). The central results are: (1) the splitting criterion---an extension splits if and only if some section has trivial cocycle; (2) the embedding-problem equivalence---an abstract embedding problem (the central lifting problem in inverse Galois theory) is solvable if and only if the associated extension splits, if and only if the cocycle obstruction vanishes; (3) the 2-coc