Module polycalc_zm 

Nullstellensatz over the rings ℤ/m — composite moduli, zero divisors and all, at arbitrary degree. The characteristic axis (crate::polycalc_gfp) covered every field; this module covers what is left of “GF(N) for any N”: the moduli where no field exists (ℤ/6) and the prime powers where the ring is not the field (ℤ/4, with its nilpotent 2).

Three facts shape the module:

• Completeness needs no division. The partition-of-unity construction — the engine of “no finite formula is structureless” — only ever adds, subtracts, and multiplies: the atom (1 − x) + x = 1 is a ring identity, the signed point indicators cancel by additive inverses, and multilinear representations of cube functions are unique over any commutative ring (the Möbius transform is unipotent). So every UNSAT formula has a degree-≤ n certificate over every ℤ/m, m ≥ 2 — hardness-as-structurelessness has no witness at any finite n over any modulus. The honest boundary is unchanged: the certificate lives in the 2ⁿ basis, and the asymptotic cost-growth statements (the certified degree lower bounds) are exactly the results pointing the other way.
• Refutation needs real ring linear algebra. Gaussian elimination dies without inverses, so span membership over ℤ/m is decided by a Howell-style echelon: gcd pivoting (every pivot normalized, by a unit, to a divisor of m) plus annihilator completion (each pivot row spawns its (m/d)-multiple, which lives strictly below it) — validated against an exhaustive all-combinations oracle on small systems and against the field engine at prime m.
• Composite moduli intersect, they do not add. For squarefree m, CRT splits the coefficient ring, so a ℤ/6 refutation is exactly a GF(2) refutation and a GF(3) refutation at the same degree — the composite ring is the conjunction of its prime parts, weaker than either. Dual witnesses generalize with the normalization L(1) ≠ 0 (a zero divisor is fine): a prime witness lifts to a ring witness by scaling with m/p.

Re-exports

pub use crate::polycalc::Mono;

Structs

NsCertificateZm

A constructive Nullstellensatz certificate over ℤ/m: Σ_C p_C · g_C = 1 in the multilinear ring.

Functions

build_ns_certificate_zm

The uniform completeness construction over ℤ/m — partition-of-unity charging, valid over any commutative ring because it never divides. Returns a constructive certificate proving UNSAT or a satisfying assignment proving SAT: a total, certifying decision over every modulus m ≥ 2 — so “structureless” (no certificate at any degree ≤ n) has no witness among finite formulas over any ℤ/m. The honest cost is unchanged: the certificate lives in the 2ⁿ monomial basis (existence, not efficiency), and num_vars ≤ 20 bounds the explicit-corner construction.

check_ns_lower_bound_polys_zm

Re-check a ring pseudo-expectation (zero trust): L(1) ≢ 0 (mod m) — over a ring the normalization cannot demand a unit, and a zero-divisor value like m/p is honest — and ⟨L, mono·g⟩ ≡ 0 for every admitted generator product. Soundness is one line and field-free: a degree-d refutation 1 = Σ λ·prod would force L(1) = Σ λ·L(prod) = 0. So true certifies that no degree-d refutation over ℤ/m exists. Degree-bounded enumeration — num_vars ≤ 63.

check_ns_lower_bound_zm

check_ns_lower_bound_polys_zm for a CNF. An empty clause admits no lower bound at any degree.

clause_polynomial_zm

The clause polynomial over ℤ/m — the signed false-indicator, exactly as over the fields: a positive literal contributes 1 − x (over ℤ/6: 1 + 5x), a negative one contributes x; the product is 1 on falsifying corners and 0 elsewhere over every commutative ring.

lift_prime_witness_to_zm

Lift a prime-field pseudo-expectation to the ring: for p | m, the functional L(x) = (m/p) · L_p(x mod p) satisfies every ℤ/m constraint — (m/p)·c·v depends on c only mod p, so each pairing is (m/p) · ⟨L_p, prod mod p⟩ = 0 — and carries the zero-divisor normalization L(1) = m/p ≠ 0. One prime witness therefore certifies the ring lower bound: the composite modulus inherits the hardness of each of its prime parts (the witness face of the CRT conjunction).

ns_refutes_polys_zm

Does a degree-d Nullstellensatz refutation over the ring ℤ/m exist for a polynomial generator system — is 1 in the ℤ/m-span of { mono·g : deg ≤ d }? Decided by the Howell echelon (validated against the exhaustive all-combinations oracle and against the field engine at prime m). Degree-bounded enumeration — num_vars ≤ 63.

ns_refutes_zm

ns_refutes_polys_zm for a CNF (signed clause false-indicators as generators). An empty clause is 1 = 0 outright.

partition_of_unity_zm

The partition of unity Σ_a δ_a over ℤ/m — the constant 1 at every n over every modulus.

pou_atom_zm

The partition-of-unity atom (1 − x_v) + x_v — the constant 1 in every commutative ring, zero divisors notwithstanding: the identity needs only additive inverses.

zm_poly_degree

The degree of a multilinear ℤ/m polynomial (0 for the zero polynomial).

Type Aliases

ZmPoly

A multilinear polynomial over ℤ/m: monomial → nonzero coefficient in 1..m (absent = 0).