Module kan_complex 

Actually having an ∞-groupoid — not its invariants, the object itself, with its defining property machine-verified.

Everything in progress_complex/cubical computed invariants (Betti numbers) of spaces. That is not the same as possessing the ∞-groupoid: by the homotopy hypothesis the simplicial model of an ∞-groupoid is a Kan complex — a simplicial set in which every horn (a simplex with one face missing) can be filled. Here we build such an object directly: the nerve of a group, whose degree-n simplices are Gⁿ (chains of composable arrows), and we verify the Kan condition — every horn fills — in degrees 2 and 3. The nerve of Aut(F) is exactly BG = K(Aut(F),1), the classifying space the symmetry tower named, so this is that ∞-groupoid, now had as an object.

It is honestly the 1-truncated one: inner horns fill uniquely, the hallmark of the nerve of a 1-groupoid (no genuine higher cells). A non-truncated ∞-groupoid — nontrivial π_{≥2}, inner horns with several fillers, the homology ladder’s higher πₙ assembled into one coherent complex with its k-invariants — is the frontier this does NOT yet reach, and we say so in the test that proves the uniqueness.

Functions

inner_horns_fill_uniquely

Does every compatible inner horn (0 < k < n) fill uniquely? Unique inner fillers are the signature of a 1-truncated nerve — the ∞-groupoid is exactly K(G,1) = BG, no genuine higher cells.

kan_fills

Does the nerve satisfy the Kan condition for horns Λⁿ_k — does every compatible horn fill?

nerve_cohomology_size

The simplicial cohomology |Hⁿ(BG; A)| of the nerve BG = K(G,1), computed from the nerve’s own face maps. By the Eilenberg–MacLane representing property Hⁿ(BG; A) = [BG, K(A,n)]; we confirm it equals the algebraic group cohomology Hⁿ(G; A), so the spectrum represents — on the symmetry’s classifying space — exactly group cohomology, the home of the Postnikov k-invariants.