What this programme is about
Zero-knowledge proof systems verify computation by compiling algorithms into systems of quadratic equations called rank-one constraint systems, or R1CS. Each equation has the shape A · B = C, where A, B, and C are linear sums of program variables and hidden witness wires. This programme asks what mathematical relations a set budget of quadratic rows and witness wires can enforce. Outside pure algebra, these bounds govern the size and running time of circuits for hash functions like SHA-256, integer range checks, and bitwise adders. A tight lower bound proves that a gadget implementation can't shrink further. An impossibility theorem tells circuit designers when an operation requires auxiliary witness wires or extra quadratic rows.
What has been settled
For prime fields, MF-158 proves a single R1CS row implements one of four geometric relations, an apparently new classification in R1CS expressiveness. Textbook gadgets are optimal: MF-160 proves IsZero, n-ary AND, n-ary OR, and XOR4 require two rows over F_p, where textbook circomlib lacked prior optimality proofs. For three inputs, MF-159 realizes XOR3 and MAJ3 in one row with zero allocations, halving standard library counts. Zero-testing without witnesses is impossible: ML-050 proves degree-at-most-two equations can't enforce z = [x = 0] without an inverse helper when |F| ≥ 4, while MF-091 fuses IsZero and a multiplexer into three rows, the exact minimum over |F| ≥ 5.
On F₂⁴, MF-059 classifies all 65,536 Boolean functions by minimum witness width, placing 32, 1,120, 63,872, and 512 functions at widths 0, 1, 2, and 3. Four-input AND requires width 3. For width 2, MF-003 delivers the first exact relational negative with phantom witnesses: two Boolean witnesses can't realize AND4 across any finite number of rows in the arbitrary-nonempty-fibre affine-C model. An initial over-broad scope was retracted before selector-closure restored the all-row theorem, and ML-020 confirms the two-witness route is unsatisfiable for all row counts. For width 3, MF-051 rules out three product rows with even fibres.
In linear graph systems over GF(2), MF-064 proves an exact conservation law for forests, where apparent vertex-row savings N - E match created gauge dimensions.
What is still open
Several core bounds and gadget classifications remain unresolved. The parity-degree conjecture MF-013 posits a degree bound of 2m - a + 1 in odd-multiplicity F₂ systems; only a constant nonzero fibre-trace subcase is verified. For modular addition over F_p, ML-085 conjectures an auxiliary-free bound of at least two quadratic rows from quadratic root counts, without an unconditional proof. In arithmetic gadgets, ML-080 catalogs rationality gaps for n-bit range checks with n ≥ 3 and notes the conic obstruction leaving 32-bit addition between 32 and 33 rows. In Boolean systems, MF-058 and ML-020 leave seven singular three-witness three-row orbits unknown for AND4, MF-061 leaves the identity-C sentinel unproved on SHA instances, and MF-012 leaves carry-system pinning conjectural.
How to read the evidence
Exhaustive computational checks and algebraic receipts dominate this register, alongside written paper proofs and certified solver runs. Exhaustive searches cover finite Boolean spaces completely, eliminating small counterexamples without manual calculation errors. Algebraic receipts supply concrete polynomial identities you can evaluate directly. Trust is high for bounded classifications. Uncertified arithmetic estimates remain rough templates awaiting compiler verification.