Module gf2 

The general linear group GL(n,2) and the invertibility constant — where the reciprocal SAT-threshold sum comes home.

A uniformly random n×n matrix over GF(2) is invertible with probability Π_{j=1}^n (1 − 2⁻ʲ), which → φ(½) = 0.2887880951. The reciprocal first-moment SAT-threshold sum is −log₂ φ(½) exactly, so the two meet at this one constant. And it is not a coincidence — it is a symmetry break:

• The invertible matrices are exactly the group GL(n,2).
• GL(n,2) acts simply transitively on ordered bases of GF(2)ⁿ (a matrix is invertible iff its rows are a basis). So by orbit–stabilizer with a trivial stabilizer, |GL(n,2)| = the number of ordered bases = Π_{i=0}^{n-1} (2ⁿ − 2ⁱ) — each factor counting the vectors that avoid the span built so far. That step-by-step quotient is the symmetry-broken enumeration; dividing by 2^{n²} gives the Euler partial product.

Structs

SolutionSpace

The complete solution space of a GF(2) linear system A x = b, in symmetry-broken form: one particular solution x₀ plus a basis of the kernel. Every solution is x₀ ⊕ (a GF(2) combination of the kernel basis), so the entire affine coset — all 2^{n−rank} solutions — is generated from this compressed witness. The kernel is the symmetry group of the solution set (the translations that preserve Ax), x₀ is one witness, and the basis are its generators: this is the exact, polynomial, linear analog of hypercube::model_orbit. The harder the break (the bigger the kernel), the more solutions; an invertible system has a trivial kernel — no symmetry, a unique witness.

Functions

count_invertible_gf2_bruteforce

Brute-force count of invertible n×n GF(2) matrices, over all 2^{n²} of them. Feasible for n ≤ 4.

gl_order

|GL(n,2)| via the orbit–stabilizer (ordered-basis) factorization Π_{i=0}^{n-1}(2ⁿ − 2ⁱ). Each factor 2ⁿ − 2ⁱ is the count of vectors outside the i-dimensional span of the basis chosen so far — the symmetry-broken enumeration of the bases on which GL(n,2) acts simply transitively. Valid up to n = 10 before the u128 product overflows.

invertibility_density

The Euler partial product Π_{j=1}^n (1 − 2⁻ʲ) — the exact invertibility density |GL(n,2)| / 2^{n²}.

is_invertible_gf2

Is an n×n GF(2) matrix (each row packed as the low n bits of a u64) invertible? Gaussian elimination over GF(2): invertible iff it reduces to full rank n.

solve_gf2

Solve a GF(2) system A x = b (each row a coefficient bit-vector in the low n bits, rhs the right-hand sides) for its entire solution space via Gaussian elimination to reduced row echelon form. Returns the symmetry-broken SolutionSpace (particular solution + kernel basis), or None iff the system is inconsistent. Generalizes crate::xorsat::solve, which returns just one witness.