Module proof_rewrite 

The proof-rewrite 2-cells — independent refutation steps commute, and the commutation squares make the space of proof-orderings a contractible CAT(0) cube complex. This is the honest higher structure the symmetry tower pointed at, and it is genuine 2-dimensional homotopy: not a faked π₂, but the coherence theorem for proofs — every way of reordering independent steps is coherently the same, up to all higher homotopies.

The structure

A refutation is a DAG: each step derives a clause from earlier ones. Steps with no dependency either way are independent — swapping two adjacent independent steps yields another valid refutation (checked here against the real PR checker, which is the oracle). The rewrites are the 1-cells; the commutation squares (two disjoint independent swaps done in either order reach the same ordering) are the 2-cells.

Model the executions as a cube complex: vertices = order ideals (the reachable “states”), edges = single steps, and a k-cube for every set of k pairwise-independent steps enabled at a state. Three facts, all checked:

1. Connected (π₀ = 1): any ordering is reachable from any other by commutation moves.
2. The cube condition (Gromov flagness): every pairwise-independent enabled set is jointly a cube — so the complex is CAT(0), hence (Cartan–Hadamard) contractible.
3. Euler characteristic χ = 1: the contractibility invariant, computed cell by cell.

Why this is the same mathematics as concurrency

This is the Mazurkiewicz-trace / higher-dimensional-automata model: independent proof steps commute exactly as independent concurrent operations commute, and the contractible cube complex is the trace’s domain. The homotopy theory of proofs and the homotopy theory of concurrent execution are one theory — the same 2-cells that certify “reordering independent proof steps doesn’t matter” certify “interleaving independent concurrent ops is deterministic.” The symmetry group still acts: Aut(F) permutes this contractible complex, and the homotopy quotient is again K(Aut(F), 1) — the recursion closes.

Structs

ProofPoset

A dependency poset on n proof steps. prec[i][j] means step i must come strictly before step j in any valid ordering (its transitive antecedent). Two steps are independent iff neither precedes the other — they commute. Small n only (≤ 20); it enumerates ideals and cubes, which is the point: it makes the coherence visible and checkable.

Functions

disjoint_double_contradiction

Two var-disjoint contradictions: vars {0,1} and {2,3}, each an unsatisfiable 2-variable block. Its four RUP lemmas (1), (¬1), (3), (¬3) are derived from the originals alone — pairwise independent proof steps, the cleanest place to see the commutation 2-cells on a real refutation.

permutations

Every permutation of 0..k — the orderings to feed the real checker.