Module modp 

Linear algebra over GF(p) — the mod-p generalization of the GF(2) parity cut (crate::xorsat).

A system of congruences Σ aᵢ·xᵢ ≡ c (mod p) is decided in polynomial time by Gaussian elimination with modular inverses, and it is certified: an inconsistent system yields a re-checkable linear-dependency refutation — a combination of the original equations whose left side cancels to 0 while the right side is some nonzero residue, i.e. 0 ≡ r ≢ 0 (mod p). A consistent system yields a satisfying assignment over GF(p).

This matters because the parity cut only speaks GF(2). The mod-p counting principles (Count_p: “partition a set whose size is not a multiple of p into p-blocks”) are resolution-hard, and a polynomial-calculus proof over the wrong characteristic cannot refute them either — but Gaussian elimination over the right GF(p) decides them instantly. A genuinely new invariant, the parity crush carried to every prime.

Structs

ModpEquation

A congruence Σ (a·x) ≡ rhs (mod p). Coefficients and rhs are reduced mod p. p must be prime (so every nonzero element is invertible, via Fermat).

ModpRecovery

A mod-m linear system recovered from an opaque Boolean CNF: the one-hot groups (each a ℤ/m variable, with the boolean var ids listed in value order) plus the congruences fitted to the forbidden-combination clauses. The recovered system is equisatisfiable to the source CNF, so the modular verdict carries back — over the prime field solve when modulus is prime, over the composite ring crate::modm::solve otherwise. See recover_from_cnf.

SolutionSpaceP

The complete solution space of a GF(p) linear system A x = b, in symmetry-broken form: one particular solution x₀ plus a basis of the kernel (null space). Every solution is x₀ + a GF(p) combination of the kernel basis, so all p^{n−rank} solutions are generated from this compressed witness. The kernel is the translation symmetry of the solution coset — the GF(p) analogue of crate::gf2::SolutionSpace, and the substrate of the affine SAT-side break: a variable the kernel never moves is forced to a single value.

Enums

ModpOutcome

The outcome of solving a mod-p linear system.

Functions

cycle_system

The canonical scalable mod-p obstruction: a cycle of differences xᵢ − x_{i+1} ≡ 1 (mod p) around an n-cycle. Summing all n equations telescopes the left side to 0 and the right to n, so the system is inconsistent exactly when n is not a multiple of p — the mod-p counting fact. For even n with p > 2 ∤ n it is satisfiable over GF(2) yet refuted over GF(p): a family the parity cut cannot see. (x − y is written x + (p−1)y.)

gl_order_p

|GL(n,p)| over GF(p) via the orbit–stabilizer (ordered-basis) factorization Π_{i=0}^{n-1}(pⁿ − pⁱ). GL(n,p) acts simply transitively on ordered bases of GF(p)ⁿ, so each factor pⁿ − pⁱ counts the vectors outside the i-dimensional span built so far — the same symmetry break as over GF(2), now across the field. The p = 2 case is gf2::gl_order.

invertibility_density_p

The invertibility density over GF(p): Π_{j=1}^n (1 − p⁻ʲ) = |GL(n,p)| / p^{n²}. As the field grows the density → 1 (fewer linear collisions); p = 2 is the densest-collision regime, the smallest constant φ(½) ≈ 0.28879.

is_invertible_modp

Is an n×n matrix over GF(p) invertible? Gaussian elimination with modular pivots: full rank n. p must be prime.

is_prime

is_refutation

Re-check a refutation: the chosen combination of equations has every variable coefficient ≡ 0 and a nonzero right-hand side mod p — a solver-free certificate of inconsistency.

recover_from_cnf

Lift an opaque Boolean CNF onto ℤ/m. Recognize the canonical one-hot encoding of a mod-m linear system — each variable a group of m bits with an at-least-one clause and the full pairwise at-most-one, plus all-negative “forbidden combination” clauses pinning the congruences — and recover the system over ℤ/m. The modulus m is the group size; it may be prime (a field) or composite (a ring), and [fit_congruence] handles both. Returns None (declining, never guessing) unless every clause fits the pattern and every forbidden set is exactly the complement of a single congruence: then the recovered system is equisatisfiable to the CNF, so the modular solver’s verdict transfers (UNSAT certificate carries; a SAT model is re-checked against the clauses by the caller). The m = 2 case is the parity cut; this is that cut generalized to every modulus — the obstruction GF(2) is blind to, decided in polynomial time where resolution (CDCL, Z3, Kissat) needs 2^Ω(n).

satisfies

Re-check a satisfying assignment: every congruence holds mod p.

solve

Decide a mod-p linear system by Gaussian elimination over GF(p). Returns a satisfying assignment, or an inconsistency-witnessing combination of the original equations. p must be prime.

solve_space

Solve a GF(p) system for its entire solution space via Gaussian elimination to reduced row echelon form, returning the symmetry-broken SolutionSpaceP (particular solution + kernel basis), or None iff the system is inconsistent. Generalizes solve, which returns just one witness, to the full coset — the GF(p) analogue of crate::gf2::solve_gf2. p must be prime.