Module polycalc_gfp 

Nullstellensatz over any prime field GF(p) and over GF(4) — the characteristic axis of the algebraic proof system that crate::polycalc fixes at GF(2).

Each characteristic is a genuinely different proof system: the mod-p counting principles fall to degree 1 over GF(p) yet carry growing degree over GF(q) for every other prime q — the pairwise incomparability that makes “which field?” a real dial, not a convention. Extension fields, by contrast, add nothing: a certificate over GF(pᵏ) projects coefficient-wise through any GF(p)-linear functional fixing 1, so NS degree depends only on the characteristic (the GF(4) engine here exists to prove that collapse, constructively). The GF(2) engine stays as the specialized fast path — its coefficient-free bitset representation packs 64 basis columns per word — and this general engine is pinned to it by a p = 2 differential test.

Everything crate::polycalc certifies has its analogue here, now with explicit coefficients: signed clause false-indicators (1 − x, which characteristic 2 silently conflates with 1 + x), the field-generic partition of unity ((1 − x) + x = 1 holds in every field, so constructive completeness is not a GF(2) artifact), degree-d refutation decisions, and dual-witness degree lower bounds with zero-trust re-checking.

Re-exports

pub use crate::polycalc::Mono;

Structs

NsCertificateGfp

A constructive Nullstellensatz certificate over f: one coefficient polynomial g_C per input clause with Σ_C p_C · g_C = 1 in the multilinear ring over f — the coefficient-explicit generalization of crate::polycalc::NsCertificate.

Enums

NsField

The coefficient field of the general engine. Elements are u64-encoded: Prime(p) uses the residues 0..p; Gf4 uses 2-bit pairs a + b·ω in the basis {1, ω} with ω² = ω + 1 (value a | b<<1).

Functions

build_ns_certificate_gfp

The uniform completeness construction over f — the partition-of-unity charging of crate::polycalc::build_ns_certificate, field-generic because its every ingredient is: the signed point indicators sum to 1 in any field (partition_of_unity_gfp), and p_C · δ_a = δ_a whenever p_C(a) = 1 (multilinear representations on the cube are unique over any field). Returns a constructive NsCertificateGfp proving UNSAT or a satisfying assignment proving SAT. Bounded to num_vars ≤ 20 (the explicit-corner construction).

check_ns_lower_bound_gfp

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

check_ns_lower_bound_polys_gfp

Re-check a ns_lower_bound_witness_polys_gfp certificate (zero trust in the producer): L(1) = 1 and ⟨L, m·g⟩ = 0 over f for every admitted generator product. true ⟹ the system genuinely has no degree-d Nullstellensatz refutation over f. Degree-bounded enumeration — num_vars ≤ 63.

clause_polynomial_gfp

The clause polynomial over f — the signed false-indicator: a positive literal x contributes 1 − x (over GF(3): 1 + 2x, not 1 + x — over GF(2) the two coincide, which is exactly the sign the general engine must make explicit), a negative literal ¬x contributes x. The product is 1 exactly on the clause’s falsifying corners and 0 elsewhere, over every field.

exactly_one_linear_generators_gfp

The linear encoding of exactly-one constraints over f: for each group G the degree-1 generator (Σ_{v∈G} x_v) − 1 plus the pairwise products x_u·x_v, deduplicated — the signed generalization of crate::polycalc::exactly_one_linear_generators (over GF(2) the two coincide, since −1 = 1). This is the encoding the modular-counting degree bounds are stated against; over GF(p) the point generators telescope — Σ_i P_i = −n when every edge meets exactly p points — so a counting family with p ∤ n collapses at degree 1 over its own characteristic.

gfp_poly_degree

The degree of a multilinear polynomial: its largest monomial’s popcount (0 for the zero polynomial).

gfp_solve

Solve a linear system Σ aᵢ·x_{vᵢ} = rhs over f by incremental-echelon Gaussian elimination with modular-inverse pivot normalization. Each equation is a sparse coefficient vector over nvars unknowns plus its right-hand side. Returns a solution (free variables 0) or None on inconsistency. The field-general sibling of the GF(2) engine’s bit-packed gf2_solve: rows join an echelon basis one at a time (memory stays O(rank · nvars) however many equations stream through), each stored row is pivot-normalized with every entry strictly below its pivot column, so back-substitution in increasing pivot order reads a solution off directly.

ns_certificate_at_degree_gfp

A degree-d certificate EXTRACTION over f: where ns_refutes_polys_gfp only decides span membership, this runs the same incremental echelon with provenance — each basis row remembers the combination of original generator products it is — and reads the certificate g_C = Σ λ_{C,m}·m off the target’s reduction, exactly the technique of crate::modp::solve’s refutation combinations. Returns None when no degree-d refutation exists. The extracted certificate is what the GF(4) → GF(2) projection (project_gf4_certificate_to_gf2) operates on. Provenance rows cost O(rank · products) memory — meant for the small-census scale, not the witness frontier.

ns_lower_bound_witness_gfp

ns_lower_bound_witness_polys_gfp for a CNF (signed clause false-indicators as generators). An empty clause is an immediate refutation — no lower bound at any degree.

ns_lower_bound_witness_on_basis_gfp

ns_lower_bound_witness_polys_gfp restricted to a sub-basis: the functional L is sought only on monomials passing in_basis (L = 0 elsewhere), while the constraints ⟨L, m·g⟩ = 0 still range over all admitted generator products — so any Some is a fully valid, check_ns_lower_bound_polys_gfp-verifiable witness, and None means only “no witness on this sub-basis”. The structure probe of the GF(2) engine, carried to every characteristic: which candidate supports hold a family’s lower bound, field by field. Degree-bounded enumeration — num_vars ≤ 63.

ns_lower_bound_witness_polys_gfp

A degree-d pseudo-expectation over f for an arbitrary generator system: a functional L on the degree-≤ d monomials with L(1) = 1 and L(m·g) = 0 for every admitted generator product, returned as its nonzero values (monomial, value). Some(L) certifies NS-degree > d over f (re-checkable by check_ns_lower_bound_polys_gfp, zero trust in the solver); None means a degree-d refutation exists — the exact witness↔refutation duality of the GF(2) engine, at every characteristic. Degree-bounded enumeration — num_vars ≤ 63.

ns_refutes_gfp

ns_refutes_polys_gfp for a CNF: the generators are the signed clause false-indicators. An empty clause is 1 = 0 outright.

ns_refutes_polys_gfp

Does a degree-d Nullstellensatz refutation over f exist for an arbitrary polynomial generator system — is 1 in the f-span of { m·g : deg(m·g) ≤ d }? The general-field sibling of crate::polycalc::ns_refutes_polys, answered by incremental-echelon span membership (memory O(rank · basis) however many generator products stream through). Degree-bounded enumeration — num_vars ≤ 63.

partition_of_unity_gfp

The partition of unity Σ_{a ∈ {0,1}ⁿ} δ_a over f, by direct summation — the constant 1 at every n over every field (pou_atom_gfp is the closed-form reason).

pou_atom_gfp

The partition-of-unity atom on variable v: (1 − x_v) + x_v, the constant 1 in every field — the identity is characteristic-free, so the completeness construction it powers is not a GF(2) artifact.

project_gf4_certificate_to_gf2

The GF(4) → GF(2) coefficient projection — the constructive half of the extension-field collapse. λ : a + b·ω ↦ a is the GF(2)-linear functional fixing 1; because every clause polynomial has prime-subfield (0/1) coefficients, applying λ coefficient-wise to a GF(4) certificate identity Σ_C p_C · g_C = 1 commutes with the clause factors and lands on a GF(2) certificate of no larger degree. So nothing proved over GF(4) needed the extension: NS degree depends only on the characteristic. Returns None unless the certificate is over Gf4.

reynolds_gfp

The Reynolds operator L ↦ |G|⁻¹ · Σ_{g∈G} g·L over f — the characteristic-0 averaging trick, available exactly when |G| is invertible, i.e. gcd(|G|, char) = 1. Returns None when char | |G| (the annihilation branch: the group-sum kills L(1) and no normalization can restore it), and the averaged functional otherwise. Averaging a valid pseudo-expectation of a G-invariant generator system yields a valid, G-invariant one — the branch the GF(2) engine can never take on an even group. Pass the full closed group.

symmetrize_gfp

The unnormalized group-sum symmetrization Σ_{g∈G} g·L of a functional over f — coefficients genuinely ADD, where the GF(2) engine could only toggle. On the constant monomial it evaluates to |G| · L(1), which is the whole dichotomy: zero (annihilation) iff char | |G|. Pass the full closed group, not a generating set.

Type Aliases

GfpPoly

A multilinear polynomial over an NsField: monomial → nonzero coefficient (absent = 0). The coefficient-explicit generalization of crate::polycalc::Poly, whose GF(2) monomial-set form is the special case “every present coefficient is 1”.