Module progress_complex 

Genuine higher homotopy, at last — π₁ ≠ 0 from real concurrency, the hole is the deadlock.

Everything below proof_rewrite was a 1-type or contractible: a discrete symmetry gives K(G,1), a deterministic trace gives a contractible cube complex. Genuine non-trivial homotopy needs a forbidden region — and concurrency with shared resources is exactly where one appears (Fajstrup–Goubault–Raussen, directed algebraic topology).

Model two processes of lengths n and m by their progress complex: a grid of states (i, j) (“P has run i steps, Q has run j steps”), unit edges for single steps, and a filled square at every cell where the two steps commute — except cells in the forbidden region (both processes inside their critical section at once, which mutual exclusion forbids). Removing those cells leaves a hole, and the hole is not decoration: it is the synchronization obstruction, the deadlock, made into topology.

We compute the homology rigorously — β₀ by union-find, β₁ = #E − #V + β₀ − rank ∂₂ and β₂ = #C − rank ∂₂ with the boundary rank taken over GF(2) by Gaussian elimination — and we cross-check every case against the Euler–Poincaré identity β₀ − β₁ + β₂ = χ. No contention gives a contractible square (β₁ = 0, determinism). One mutex gives β₁ = 1: the execution space is a circle, and the two directed ways around the hole (P-first vs Q-first) are genuinely inequivalent schedules — the hole is precisely where the scheduler symmetry can no longer be broken to one canonical class. Higher homotopy = the obstruction to symmetry breaking.

Structs

ProgressComplex

The progress complex of two processes of lengths n, m (an n × m grid of cells), with a set of forbidden cells (the mutual-exclusion region) left unfilled.

ProgressComplex3

The progress complex of three processes of lengths n, m, p — a 3D grid of states, filled with solid 3-cells (cubes) where all three steps commute, except forbidden cells. Climbing one homotopy dimension: a forbidden core now leaves a hollow 2-sphere, so β₂ = π₂ ≠ 0 — the first genuine π₂ the tower produces (not just admits). Adding a process climbs a rung; the limit of “one more process, one more dimension” is the ∞-groupoid the ladder points at.