Module modm 

Linear algebra over ℤ/m for composite m, by the Chinese Remainder Theorem — the multiplicative symmetry break. A system Σ aᵢ·xᵢ ≡ c (mod m) over a squarefree modulus m = p₁·…·p_t factors, through the ring isomorphism ℤ/m ≅ GF(p₁) × … × GF(p_t), into one independent system over each prime field — each decided by crate::modp::solve — and the per-field solutions are recombined by CRT. The factorization of the modulus is the symmetry that splits the problem; the prime fields are the irreducible pieces:

• consistent mod m ⟺ consistent over every prime factor pᵢ, and the recombined residues give an assignment over ℤ/m that re-checks (satisfies);
• inconsistent mod m ⟺ some prime factor’s system is inconsistent, and that prime together with its GF(p) refutation combination is the re-checkable witness (crate::modp::is_refutation).

This is crate::modp (the prime-field cut, itself the prime generalization of the GF(2) parity cut) carried up onto the composites by multiplication. Prime-power moduli p^k need the residue ring ℤ/p^k (a different object — p is a zero divisor), a separate rung; this module is exact and complete for squarefree m.

Structs

SolutionSpaceM

The complete solution space of a ℤ/pᵏ linear system, in symmetry-broken form: a particular solution plus a generating set of the kernel submodule (each generator is a column of the Smith transform V scaled by its pivot’s freedom q/gcd(dₜ,q)). The prime-power analogue of crate::modp::SolutionSpaceP over a local ring — and the substrate of the scalable forced/linked break: a variable the kernel never moves is forced.

Enums

AllowedOutcome

The per-variable allowed-value congruence of a ℤ/m system, for any composite m. By CRT over the prime-power components, each variable’s solution-projection is a coset x_g ≡ residue (mod modulus) — the tightest congruence the system forces on it. Generalizes forcing: modulus = m is a single value (fully forced), 1 < modulus < m is partial (confined to a value-subset), modulus = 1 is free. Within each prime-power component the coset modulus is gcd(p^k, kernel column at g) from solve_space_prime_power; the components recombine by CRT. Inconsistent if any component is.

ForcedM

The forced-value structure of a ℤ/m system over a squarefree m.

ModmOutcome

The outcome of deciding a linear system over ℤ/m.

PrimePowerSpace

The outcome of solve_space_prime_power.

Functions

allowed_residues

See AllowedOutcome. None only on Smith overflow.

cycle_system

The scalable composite obstruction: the n-cycle of differences xᵢ − x_{i+1} ≡ 1 (mod m), inconsistent exactly when m ∤ n (summing telescopes the left to 0, the right to n). The coefficient −1 is written m − 1. Reuses crate::modp::cycle_system’s shape across the field.

forced_values_prime_power

Which variables a ℤ/m system forces, for any composite m — by CRT over its prime-power components (ℤ/m ≅ ∏ ℤ/pᵢ^{kᵢ}), each solved scalably by Smith normal form (solve_space_prime_power): a variable is forced mod m iff its kernel never moves it in every component, and the value is the CRT of the residues. This is the Smith-form generalization that replaces the old bounded brute force — no size cap; None only on Smith overflow. Inconsistent when any component is.

forced_values_squarefree

Which variables a squarefree ℤ/m system forces to a single value, by CRT of the GF(pᵢ) solution spaces (ℤ/m ≅ ∏ GF(pᵢ)): a variable is forced mod m iff it is forced mod every prime factor (crate::modp::solve_space — its kernel never moves it), and the value is the CRT of those residues. None if m is not squarefree (the prime-power case needs Smith normal form, not handled here). This is the substrate of the composite affine SAT-side break.

is_refutation

Re-check a refutation over ℤ/modulus: the chosen combination of equations has every variable coefficient ≡ 0 and a nonzero right-hand side mod modulus — a solver-free certificate that the system is inconsistent over that quotient ring (and hence over any ℤ/m with modulus | m).

prime_power_factorize

The prime-power factorization of m (m = ∏ pᵢ^{kᵢ}), or None if m < 2.

satisfies

Re-check a satisfying assignment over ℤ/m: every congruence holds mod m.

solve

Decide a linear system over ℤ/m for any m ≥ 2, closing every composite modulus. By CRT, ℤ/m ≅ ∏ ℤ/pᵢ^{kᵢ}: solve each prime-power component (solve_prime_power) and recombine the residues. Consistent mod m ⟺ consistent over every prime-power factor; the first inconsistent factor is the witness (and certifies UNSAT mod m, since that factor divides m). Returns None only if m < 2, or a component is too large / overflows the integer Smith reduction.

solve_prime_power

Decide a linear system over the residue ring ℤ/pᵏ. For k = 1 this is the prime field, handed to the proven crate::modp::solve. For k ≥ 2 the ring has zero divisors, so we diagonalize over the integers — U·A·V = D with U, V unimodular (Smith-style: gcd row/column reduction) — after which each dₜ·yₜ ≡ (U·b)ₜ (mod pᵏ) is an independent 1-D congruence, solvable iff gcd(dₜ, pᵏ) ∣ (U·b)ₜ. U yields both the satisfying assignment (x = V·y) and, on failure, the re-checkable refutation (a row of U, scaled to annihilate the coefficients mod pᵏ). Returns None only if the integer entries would exceed [GROWTH_CAP].

solve_space_prime_power

Solve a ℤ/pᵏ system for its full solution space via Smith normal form U·A·V = D — the scalable analogue of crate::modp::solve_space over a prime-power ring (where p is a zero-divisor, so field Gaussian fails). Returns the particular solution plus the kernel generators (so a variable the kernel never moves is forced), or Inconsistent. None only when the integer Smith reduction overflows [GROWTH_CAP]. k = 1 delegates to the prime-field solver.

solve_squarefree

Decide a linear system over ℤ/m for squarefree m, via CRT over the prime fields. Returns None only when m is not squarefree (the prime-power ring is a separate rung). The first prime factor whose system is inconsistent is reported as the witness — by CRT, the whole composite system is then inconsistent.

squarefree_primes

The distinct prime factors of m, in increasing order — or None if m < 2 or m is not squarefree (some p² | m). Squarefreeness is exactly the condition under which ℤ/m is a product of fields, so the CRT-over-prime-fields decision procedure below is complete.