Research · Papers · What rank-one constraints can express · MF-003
An impossibility theorem for four-input AND in two-witness relational R1CS
Over F₂, no system Aj(x,z)Bj(x,z)=Cj(x,z) (1≤j≤r, z∈F₂^2) with affine Aj,Bj,Cj,D and Zx≠∅ satisfies D(x,z)=x1 x2 x3 x4 for all z∈Zx
Published 2026-08-29
For everyone
Plain summary
Four-input AND outputs 1 only when all four inputs are 1. This result proves you cannot compute four-input AND using two hidden Boolean bits, an affine decoder, and any finite number of rank-one quadratic equations. The encoding allows multiple valid hidden settings per input, provided every input has at least one valid assignment.
The proof is backed by 955,369,472 equation-pair iterations, an exhaustive census of admissible rows, and independent replays of a selector-closure calculation. An earlier scope correction narrowed the claim before the selector-closure replay proved impossibility for all finite row counts. The register records this as the first exact negative result for relational R1CS with non-unique phantom witnesses, noting no independent prior-art search.
Result
Work over F_2. Let x = (x1, x2, x3, x4) and f(x) = x1 x2 x3 x4. Let z = (z1, z2) ∈ F_2^2 be two Boolean witnesses. For a finite row count r, consider rows Aj(x, z) Bj(x, z) = Cj(x, z), 1 ≤ j ≤ r, where Aj, Bj, and Cj are arbitrary affine forms. Let D(x, z) be an arbitrary affine decoder, and define the witness fibre Zx = {z ∈ F_2^2 : Aj(x, z) Bj(x, z) = Cj(x, z) for every j}.
The arbitrary-nonempty-fibre affine-C model requires Zx ≠ ∅ for every x, and represents f when D(x, z) = f(x) for all z ∈ Zx.
Theorem: For every finite r, no such two-witness system represents f(x) = x1 x2 x3 x4.
The impossibility holds for arbitrary affine factors, arbitrary affine C-sides, an affine decoder, and arbitrary nonempty witness multiplicities, including even multiplicity.
Setting and definitions
All variables and equations are over F_2. An affine form is a constant plus a sum of variables. A rank-one quadratic row equates the product of two affine forms to an arbitrary affine right-hand side. The witness fibre Zx contains all witness pairs satisfying every row for a given public input x. The relation may be many-to-one: fibre size and parity may vary with x, provided Zx is nonempty and the affine decoder D(x, z) evaluates to f(x) for all z ∈ Zx.
Method
The initial two-witness search evaluated 955,369,472 equation-pair iterations across two independent implementations. The exact semilattice census admitted arbitrary affine C-sides and evaluated the intersection of all 16 target-compatible rows. That intersection left two positive-pin wrong points, ruling out three or more rows in the two-witness model.
Scope restoration used an exact selector-closure calculation. A Python replay used grouped 65,536-bit coverage, and a C++ replay verified individual selectors followed by the full GL(4,2) action. Across a catalog of 128 affine forms, 2,732 products, 83,456 relations, and 13,424 viable rows, 0 of 65,536 selectors survived. A separate census of 119,333,776 relation pairs ruled out the three-witness, two-row case under its own hypotheses.
All associated verification receipts and raw computational outputs are available in this paper's downloadable evidence pack.
Discussion
The scope evolved across verification phases. An initial correction retracted the claim of arbitrary nonempty witness multiplicity at all row counts: positive-even two-witness fibres were eliminated for all r, arbitrary-positive fibres were eliminated through four rows, and odd or proper-mixed fibres at five or more rows remained UNKNOWN.
The selector-closure calculation resolved that gap. Independent replays verified the full selector space, establishing impossibility across all finite row counts for arbitrary nonempty fibres, including odd and proper-mixed cases. The separate three-witness, two-row census operates under distinct hypotheses, moving the open frontier to three witnesses and three rows.
This result settles expressiveness for two-witness relational R1CS with phantom witnesses. It does not extend to larger witness counts or modified relation formats. The register claims this as the first exact expressiveness negative in this setting, without an independent literature search.
For everyone — the takeaway
What this means
Computing a four-way AND is impossible with two hidden bits in this constraint format. Even if you allow inputs to map to multiple hidden states and add any finite number of quadratic equations, an addition-based decoder cannot extract the correct output. A separate test showed that three hidden bits cannot compute it in two equations either. That leaves three hidden bits with three equations as the next unsolved boundary. The register claims priority for this exact negative result, though it records no literature survey to confirm it.
Attribution and prior art
Prior art: This is presented as the first exact negative result regarding the expressive power of relational R1CS with phantom witnesses. No separate prior-art search or additional qualification is stated.
Register references
Entry: MF-003.
Receipts: DL phantom_pair_and4_certificate.json; CONT phantom_pair_even_recheck.json (digest 08ae596a…); phantom_pair_a2m3_semilattice_results.json; Package-3 package3_replay_receipt.json; CONT lens_l3b_verification_report.md (SHA-256 a06180bb5723dcc760b56375d046377f24f0bafcebbc8b67358e5edfe7feae14); lens_l3b_verification_receipt.json (SHA-256 56954be356773a60b27c5610afa21c029783e62a51965a60e12c17511c0273c9); lens_r2a_catalyst_verification_report.md; lens_r2a_catalyst_verification_receipt.json; lens_r2a_independent_audit.json.
Prior art: the register does not record this.
Every artifact named above is bundled in, or hashed by, this paper's evidence pack below.
Evidence pack
Everything needed to check this entry against its receipts: the register text, a manifest with a SHA-256 hash for every named receipt, and 8 of 9 receipt files bundled (36 KB). Anything not bundled is still hashed in the manifest and lives in the compute-box working trees.
Changelog
Last reviewed 2026-08-29
- 2026-08-13Partially retracted: the corrected theorem remains proved, but the phrase “arbitrary nonempty witness multiplicity” at every row count was over-broad. Two-witness positive-even fibres are dead at every row count by the semilattice theorem, arbitrary-positive fibres only through four rows, and odd/proper-mixed two-witness fibres at five or more rows remain unknown.
- 2026-08-13Restored on 2026-08-13: independent replay checks confirm that two-witness affine-C AND₄ is impossible at any finite row count for arbitrary nonempty fibres (0/65,536 surviving selectors across 13,424 viable rows, 83,456 relations, 2,732 products, and 128 affine forms). The Return-8 partial retraction remains valid for the semilattice argument.
- 2026-08-29Published on this site.