Struct ProofPoset 

pub struct ProofPoset {
    pub n: usize,
    /* private fields */
}

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.

Fields

n: usize

Implementations

impl ProofPoset

pub fn new(n: usize, edges: &[(usize, usize)]) -> Self

Build from direct dependency edges (i, j) = “i must precede j”, then transitively close.

pub fn precedes(&self, i: usize, j: usize) -> bool

pub fn independent(&self, i: usize, j: usize) -> bool

Neither step precedes the other: they commute, and that commutation is a 2-cell.

pub fn ideals(&self) -> Vec<u64>

All order ideals — the vertices of the cube complex.

pub fn enabled(&self, ideal: u64) -> Vec<usize>

The steps enabled at ideal: not yet taken, with every predecessor already taken.

pub fn euler_characteristic(&self) -> i64

Euler characteristic of the commutation cube complex: a k-cube for every state and every pairwise-independent set of k steps enabled there. χ = 1 ⟺ contractible (with the cube condition below ruling out the alternatives).

pub fn satisfies_cube_condition(&self) -> bool

Gromov’s cube condition (flagness): every pairwise-independent set of enabled steps is jointly addable — the 1-skeleton of a cube is always filled to the solid cube. A simply connected cube complex satisfying this is CAT(0), hence contractible. For a commutation poset it holds structurally; we check it as confirmation (and as a guard on enabled/independent).

pub fn execution_complex(&self) -> CubicalComplex

The execution complex of this commutation poset, as a CubicalComplex: states (order ideals) are corners in {0,1}ⁿ, and at each state the enabled steps — which are automatically pairwise independent — span a cube. This is the proof-rewrite complex of proof_rewrite handed to the same general homology engine that produced π₁, π₂, π₃ from concurrency, so the whole ladder runs through one engine, from π₀ = symmetry breaking on up.

pub fn linear_extensions(&self) -> Vec<Vec<usize>>

All linear extensions (valid total orderings) of the poset.

pub fn canonical_extension(&self) -> Vec<usize>

The canonical (lexicographically-least) linear extension — the orbit representative under commutation. This is symmetry breaking applied to the orderings: one schedule per trace, the π₀ representative, exactly as a lex-leader picks one assignment per symmetry orbit.

pub fn is_complex_automorphism(&self, perm: &[usize]) -> bool

Does the step-relabeling perm (perm[i] = image of step i) preserve the whole order — both precedence and commutation? Such a perm is a cellular automorphism of the cube complex: it carries cubes to cubes and is exactly how a symmetry of F acts on the space of its proofs.

pub fn acts_freely_on_extensions(&self, perm: &[usize]) -> bool

Does perm act freely on the linear extensions — fixing none? A free cellular action of a group on a contractible complex has homotopy quotient BG (the Borel construction degenerates), which is how symmetry-breaking the proof complex recovers a classifying space.

pub fn extensions_connected_by_commutation(&self) -> bool

Are all linear extensions connected by adjacent-independent commutation moves? (π₀ = 1 of the reordering graph — the coherence base: every ordering is reachable from every other.)