Completing the Cohomological Extension Package: Section Cocycles and Splitting Criterion for Mathlib

Mathlib's GroupExtension/Defs. lean documents two explicit TODO items: a bijection between N-conjugacy classes of splittings and H¹, and a bijection between equivalence classes of group extensions and H², both for abelian kernel N. Neither is currently formalized. This technical note documents a proposed Mathlib contribution that constitutes Phase 1 of completing these TODOs: the section cocycle associated to a set-theoretic section of a group extension, the splitting criterion (splitsᵢffₜrivialcocycle), and supporting infrastructure including the section difference function, the conjugation action via sections, and the multiplicative 2-cocycle identity. All theorems are fully verified by the Lean type checker with zero sorry. We describe the proposed API surface, design decisions (nam