logicaffeine_proof/

groupoid.rs

//! The **action groupoid** — what symmetry breaking *means*, categorically, as checked code.
//!
//! Symmetry breaking is not a heuristic; it is the computation of `π₀` of a groupoid. A symmetry
//! group `G` acts on the space `X` of assignments (the "possible worlds"). The **action groupoid**
//! `X ⫽ G` has the assignments as objects and the group elements as the (iso)morphisms `α → g·α`:
//! two assignments are *isomorphic* iff related by a symmetry — bisimilar worlds. Symmetry breaking
//! keeps ONE assignment per isomorphism class — it computes the **skeleton**, equivalently
//! `π₀(X ⫽ G)` (the set of orbits = connected components). The exponential→polynomial collapse is
//! exactly `|X| → |π₀(X ⫽ G)|`.
//!
//! This `X ⫽ G` is a **1-groupoid** (h-level 3 in the homotopy-level table). The ∞-tower above it —
//! symmetries *between* symmetry-breakings, then between those, … — is the honest open direction. We
//! build the first rung (this 1-groupoid) solidly and *check* that symmetry breaking is its `π₀`; the
//! next rung (a groupoid of measures-and-their-morphisms) is sketched in the campaign notes. We do
//! not claim to have built an ∞-groupoid — only the 1-truncation that the present theory occupies,
//! and the precise statement of what climbing would mean.

use crate::cdcl::Lit;
use crate::proof::Perm;

/// The action groupoid `X ⫽ G`: assignments over `nv` variables acted on by the group generated by
/// `gens` (literal permutations). Small `nv` only — it enumerates all `2^nv` objects, which is the
/// point: it makes the orbit collapse *visible and checkable*.
pub struct ActionGroupoid {
    nv: usize,
    gens: Vec<Perm>,
}

impl ActionGroupoid {
    pub fn new(nv: usize, gens: Vec<Perm>) -> Self {
        ActionGroupoid { nv, gens }
    }

    /// Act by a (sign-respecting) symmetry on an assignment encoded as a bitmask: variable `v`'s value
    /// is carried to variable `σ(+v).var`, flipped iff `σ(+v)` is negative.
    fn act(&self, g: &Perm, a: u32) -> u32 {
        let mut b = 0u32;
        for v in 0..self.nv {
            let val = (a >> v) & 1;
            let img = g.apply(Lit::pos(v as u32));
            let w = img.var() as usize;
            let new_val = if img.is_positive() { val } else { 1 - val };
            if new_val == 1 {
                b |= 1 << w;
            }
        }
        b
    }

    /// The orbit id of every assignment — `π₀(X ⫽ G)`, computed as the connected components of the
    /// action via union-find. `orbits()[a]` is the canonical representative (smallest member) of `a`'s
    /// orbit.
    pub fn orbits(&self) -> Vec<u32> {
        let total = 1u32 << self.nv;
        let mut parent: Vec<u32> = (0..total).collect();
        fn find(parent: &mut [u32], x: u32) -> u32 {
            let mut r = x;
            while parent[r as usize] != r {
                r = parent[r as usize];
            }
            // path compression
            let mut c = x;
            while parent[c as usize] != r {
                let next = parent[c as usize];
                parent[c as usize] = r;
                c = next;
            }
            r
        }
        for a in 0..total {
            for g in &self.gens {
                let b = self.act(g, a);
                let (ra, rb) = (find(&mut parent, a), find(&mut parent, b));
                if ra != rb {
                    // union by smaller-root so representatives are canonical (smallest)
                    if ra < rb {
                        parent[rb as usize] = ra;
                    } else {
                        parent[ra as usize] = rb;
                    }
                }
            }
        }
        (0..total).map(|a| find(&mut parent, a)).collect()
    }

    /// `|π₀(X ⫽ G)|` — the number of essentially-different worlds, i.e. exactly what symmetry breaking
    /// reduces the search space to.
    pub fn num_orbits(&self) -> usize {
        let reps = self.orbits();
        let mut distinct: Vec<u32> = reps.clone();
        distinct.sort_unstable();
        distinct.dedup();
        distinct.len()
    }

    /// The full group `G` generated by `gens` (closed under composition, including the identity).
    /// Bounded to `cap` elements so a pathological generating set can't blow up; the caller's small
    /// examples are well within it.
    pub fn group_elements(&self, cap: usize) -> Vec<Perm> {
        let mut seen: std::collections::HashSet<Perm> = std::collections::HashSet::new();
        let id = Perm::identity(self.nv);
        seen.insert(id.clone());
        let mut elems = vec![id];
        let mut frontier = elems.clone();
        while !frontier.is_empty() && elems.len() < cap {
            let mut next = Vec::new();
            for e in &frontier {
                for g in &self.gens {
                    let prod = g.compose(e); // g ∘ e
                    if seen.insert(prod.clone()) {
                        next.push(prod.clone());
                        elems.push(prod);
                        if elems.len() >= cap {
                            return elems;
                        }
                    }
                }
            }
            frontier = next;
        }
        elems
    }

    /// `π₁(X ⫽ G)` at the assignment `a` — its **stabilizer**: the group elements that fix `a`
    /// (`g · a = a`). These are the loops at `a` in the action groupoid; the fundamental-group data of
    /// the homotopy type at that component.
    pub fn stabilizer_size(&self, a: u32, group: &[Perm]) -> usize {
        group.iter().filter(|g| self.act(g, a) == a).count()
    }

    /// The size of `a`'s orbit (the connected component of `a`).
    pub fn orbit_size(&self, a: u32) -> usize {
        let reps = self.orbits();
        reps.iter().filter(|&&r| r == reps[a as usize]).count()
    }
}

#[cfg(test)]
mod tests {
    use super::*;

    /// The adjacent variable-transpositions that generate the full symmetric group `S_nv` on the bits.
    fn full_symmetric_gens(nv: usize) -> Vec<Perm> {
        (0..nv.saturating_sub(1))
            .map(|i| {
                let images: Vec<Lit> = (0..nv)
                    .map(|v| {
                        let w = if v == i {
                            i + 1
                        } else if v == i + 1 {
                            i
                        } else {
                            v
                        };
                        Lit::pos(w as u32)
                    })
                    .collect();
                Perm::from_images(images)
            })
            .collect()
    }

    #[test]
    fn symmetry_breaking_is_pi_zero_of_the_action_groupoid() {
        // WHAT SYMMETRY BREAKING MEANS, made checkable. Under the full symmetric group acting on the
        // bits, two assignments are isomorphic iff they have the same Hamming weight — so the `2^n`
        // worlds collapse to exactly `n+1` orbits (weights `0..=n`). That orbit count IS the search
        // space symmetry breaking leaves; the exponential→linear collapse is `2^n → n+1`, computed
        // here as `π₀` of the action groupoid.
        for nv in 3..=8 {
            let g = ActionGroupoid::new(nv, full_symmetric_gens(nv));
            assert_eq!(g.num_orbits(), nv + 1, "S_n on bits ⇒ orbits = Hamming weights = n+1");
            assert!(
                g.num_orbits() < (1usize << nv),
                "exponential collapse: {} orbits vs {} worlds",
                g.num_orbits(),
                1usize << nv
            );
        }
    }

    #[test]
    fn pi_one_of_the_action_groupoid_is_the_stabilizer_and_orbit_stabilizer_holds() {
        // ONE MORE FINITE STEP up the tower: pin the homotopy type of X ⫽ G. π₀ = orbits (already);
        // π₁ at a component = the STABILIZER. The two are bound by the fiber sequence Stab → G → Orbit
        // — the orbit-stabilizer theorem: |G| = |orbit(a)| · |stab(a)| for every assignment a. We check
        // it exhaustively under the full symmetric group on the bits (a small, fully-enumerable group).
        for nv in 3..=5 {
            let g = ActionGroupoid::new(nv, full_symmetric_gens(nv));
            let group = g.group_elements(100_000);
            // |S_n| = n!
            let factorial: usize = (1..=nv).product();
            assert_eq!(group.len(), factorial, "the generated group is S_{nv} of order {nv}!");
            for a in 0..(1u32 << nv) {
                let orbit = g.orbit_size(a);
                let stab = g.stabilizer_size(a, &group);
                assert_eq!(orbit * stab, group.len(), "orbit-stabilizer: |orbit|·|stab| = |G| at a={a}");
            }
        }
    }

    #[test]
    fn the_trivial_group_quotients_nothing_and_a_swap_halves() {
        // Sanity poles of the quotient. No symmetry ⇒ every world is its own orbit (`2^n`). A single
        // variable-swap (a `Z/2` action) pairs `α` with its swap, so the orbit count is the number of
        // swap-symmetric-or-paired worlds — strictly fewer than `2^n` whenever the swap moves anything.
        let nv = 5;
        let none = ActionGroupoid::new(nv, vec![Perm::identity(nv)]);
        assert_eq!(none.num_orbits(), 1 << nv, "trivial action ⇒ no collapse");

        let swap01: Perm = {
            let images: Vec<Lit> =
                (0..nv).map(|v| Lit::pos(if v == 0 { 1 } else if v == 1 { 0 } else { v } as u32)).collect();
            Perm::from_images(images)
        };
        let g = ActionGroupoid::new(nv, vec![swap01]);
        assert!(g.num_orbits() < (1 << nv), "a swap genuinely identifies worlds");
        // Z/2 acting: orbits = fixed points (a₀=a₁) + paired points/2. #fixed = 2^(n-1), #moved = 2^(n-1),
        // so orbits = 2^(n-1) + 2^(n-2) = 3·2^(n-2).
        assert_eq!(g.num_orbits(), 3 * (1 << (nv - 2)), "Z/2 swap ⇒ 3·2^(n-2) orbits");
    }
}