# RRLS exact-cover lift: exclusivity, certificates, and a measured limit 5 September 2026. Extension to the RRLS proof-audit engine. The target was to restore the exact-cover constraints that a parity-only representation discards, then determine whether the resulting algebraic lift rejects additional impossible matchings with independently checkable evidence. The target was met on the recorded experiment. This is not a proof of P = NP or P ≠ NP, and it is not evidence for additional physical dimensions. The implementation applies established polynomial infeasibility-certificate ideas. Degree-bounded searches for identities of the form 1 = sum of polynomial multiples are central to the Nullstellensatz linear algebra approach. This project does not claim to have invented that method. [De Loera, Lee, Malkin, and Margulies, Computing Infeasibility Certificates for Combinatorial Problems through Hilbert's Nullstellensatz](https://www.math.ucdavis.edu/~deloera/researchsummary/jsc09_issac08.final.pdf). ## 1. Exact formulation Let X, Y, Z each contain n vertices and let T be a listed set of m distinct triples in X × Y × Z. Introduce a Boolean selection variable x_e for each triple e. A perfect three-dimensional matching selects exactly one incident triple at every vertex. For each vertex v define, over GF(2), \[ f_v(x)=1+\sum_{e\ni v}x_e. \] For every pair of distinct triples sharing a vertex define \[ g_{ef}(x)=x_ex_f. \] Calculations take place in the Boolean quotient ring \[ \mathcal B_m=GF(2)[x_1,\ldots,x_m]/\langle x_i^2-x_i\rangle. \] Multiplication of squarefree monomials is therefore set union of their supports. Polynomial addition is symmetric difference. Both operations are exact integer/bit operations in the implementation. **Theorem 1.** The Boolean solutions of all equations f_v = 0 and g_ef = 0 are precisely the perfect matchings of T. **Proof.** The equation f_v = 0 requires an odd number of selected triples at v. The equations g_ef = 0 forbid selecting any two incident triples together, so at most one can be selected. Odd and at most one means exactly one. Conversely, a perfect matching satisfies both requirements. ∎ The parity-only formulation omits the g-equations and permits three, five, or another odd number of selected triples at a vertex. Adding monomials to that weakened formulation does not restore the omitted restriction. ## 2. Why the previous parity lift cannot improve **Theorem 2.** If Ax = 1 is consistent over GF(2), every linearization obtained solely by multiplying those equations by monomials, with Boolean square reduction, is consistent at every degree. **Proof.** Choose a solution a in GF(2)^m. Assign the coordinate for every monomial x_S the product of its selected entries a_S. Each original equation evaluates to zero, so every polynomial multiple also evaluates to zero. Square reduction is valid because each a_i is a bit. These values satisfy the entire lifted system. ∎ This statement specifically concerns GF(2). It does not assert the same result for an arbitrary non-Boolean solution over another field. In the GF(2) setting, no amount of monomial multiplication can refute a system already having a Boolean solution. ## 3. The bounded lift and its proof object At product degree D, the engine generates every squarefree monomial multiple x_S f_v with |S| + 1 ≤ D and every x_S g_ef with |S| + 2 ≤ D. The latter are omitted in the parity-only control. Each product is reduced in the Boolean ring and treated as a linear equation in monomial coordinates. The degree convention bounds the degree before Boolean square reduction. Claims about the degree-2 system below refer to exactly this generated system, not every proof calculus bearing a similar name. Gaussian elimination uses Python integer bitsets. Every row carries a second bitset identifying its source polynomial multiples. A row equal to the constant polynomial 1 produces the certificate \[ \boxed{\sum_j x_{S_j}h_j(x)=1,\qquad h_j\in\{f_v,g_{ef}\}.} \] **Theorem 3: certificate soundness.** Such an identity proves that T has no perfect matching. **Proof.** By Theorem 1, every perfect matching makes each h_j zero. The left-hand side would then be zero while the right-hand side remains one. This is impossible. ∎ `verify_exact_cover.py` constructs the permitted equations from the original triples and expands each indicated multiple independently. It checks the input binding, vertex or conflicting pair, multiplier, product-degree bound, and final symmetric difference. It does not import Gaussian elimination, the lift builder, SciPy, or the matching solver. The method reports UNSAT only with a checked certificate. NO_REFUTATION means that the completed bounded lift did not find one. BUDGET means that construction or elimination stopped at a resource limit. Neither status is SAT. ## 4. A three-term explanation of the improvement Consider the four triples \[ T=\{000,001,010,100\}. \] Each pairwise projection has a perfect matching. Selecting all four triples satisfies every parity equation: each coordinate value occurs either once or three times. Nevertheless, there is no perfect 3D matching because no two listed triples are coordinatewise disjoint. Write a for the selection variable of 001 and b for that of 010. Their unique coordinate-1 vertices force a = 1 and b = 1, while their shared first-coordinate vertex forbids selecting both. The corresponding polynomials are 1+a, 1+b, and ab. The exact identity is \[ \boxed{ab+a(1+b)+(1+a)=1\quad\text{over }GF(2).} \] This degree-2 certificate uses the missing exclusivity equation. Without it the parity model is consistent and Theorem 2 applies. ## 5. Exact boundary relations for independent ground truth The reference algorithm processes first-coordinate vertices in order. Its state after k steps is the exact relation \[ B_k=\{(Y',Z'): \text{some compatible selection covers the first }k \text{ vertices of }X\text{ and exactly }Y',Z'\}. \] Start with B_0 = {(∅,∅)}. For each triple (k,y,z), extend a state only when y and z are unused. Preserve every resulting pair of used-vertex sets. The final state (Y,Z) is reachable if and only if a perfect matching exists. A SAT proof supplies selected triple indices, checked directly. An UNSAT proof supplies all boundary layers; an independent implementation recomputes every transition and rejects omitted or invented reachable states. This is a concrete implementation of preserving a compatibility relation instead of only a local yes/no answer. It is not polynomial in general. The possible state count has upper bound \[ \sum_{k=0}^{n}\binom nk^2=\binom{2n}{n}, \] which grows exponentially. The reference provides bounded, exact decisions for these small experiments; its cost is not hidden inside the measured algebraic filter. ## 6. Exhaustive and fixed-sample results Every subset of the eight triples in the 2 × 2 × 2 universe was tested, for 256 instances. Exhaustive enumeration of potential matchings agreed with the boundary solver. | Exhaustive binary universe | Result | |---|---:| | Instances with no perfect matching | 81 | | Refuted by parity-only degrees 1, 2, or 3 | 73 | | Refuted by degree 2 with exclusivity | 81 | | Matchable instances falsely rejected | 0 of 175 | The larger experiment selected 100 UNSAT and 25 SAT instances at each n in {3,4,5,6}. Every selected instance passed all three pairwise matching tests. Subsets were drawn with an edge count uniform between 2n and 4n, using fixed seeds 9100000+n. Exact boundary decisions determined selection into the predeclared quotas. The 500-instance sample is deliberately conditioned on pairwise feasibility and truth value; it is not a population prevalence estimate or a reproduction of the attachment's unavailable 1,000-instance dataset. | Part size n | Selected UNSAT | Parity-only degree 1 rejects | Exclusivity degree 2 rejects | UNSAT cases with feasible witnesses for all four fields and LP | |---|---:|---:|---:|---:| | 3 | 100 | 20 | 100 | 11 | | 4 | 100 | 22 | 100 | 5 | | 5 | 100 | 18 | 100 | 11 | | 6 | 100 | 11 | 100 | 3 | | Total | 400 | 71 | 400 | 30 | Thus the degree-2 lift refuted 329 instances that parity alone could not refute. It also refuted all 30 selected impossible instances with verified feasible witnesses for GF(2), GF(3), GF(5), GF(7), and the continuous nonnegative incidence equations. None of the 100 SAT controls was falsely rejected. Degree 3 with exclusivity found no additional UNSAT cases in this sample. The field feasibility witnesses are checked directly modulo their prime. SciPy's LP solver is used only to propose a nonnegative feasible vector; rational reconstruction is accepted only when exact Fraction arithmetic verifies Ax = 1 and x ≥ 0. Floating-point LP infeasibility is not used as an infeasibility certificate. This distinguishes an exact successful relaxation witness from an unverified numerical solver message. ### Cost and budget accounting Each mode ran three times on each selected input, in forward/reverse/forward order, after one excluded initial warm-up per mode. Times include algebra construction, source provenance, elimination, and checking any refutation. They exclude input I/O, interpreter imports, sample selection, reference boundary solving, and LP scouting. The table reports medians across the 500 per-instance timing medians; the final column sums those per-instance medians. | Mode | Refutations | No refutation | Budget stops | Median ms | Sum ms | |---|---:|---:|---:|---:|---:| | Parity, degree 1 | 71 | 429 | 0 | 0.104 | 53.884 | | Parity, degree 2 | 71 | 429 | 0 | 1.215 | 775.314 | | Parity, degree 3 | 71 | 421 | 8 | 13.282 | 13,256.092 | | Exclusivity, degree 2 | 400 | 100 | 0 | 0.762 | 610.207 | | Exclusivity, degree 3 | 400 | 88 | 12 | 4.186 | 4,988.976 | Budget stops are retained as budget stops, including on known SAT controls. Completed parity-only runs had identical rejection results at all tested degrees, as predicted by Theorem 2. The degree-2 exclusivity route cost more than parity degree 1 and supplied substantially stronger rejections. Increasing to degree 3 added cost without additional rejections in this selected sample. For m selection variables and c conflicting pairs, a column upper bound is \[ C_D=\sum_{k=0}^{\min(m,D)}\binom mk, \] and a generated-row upper bound is \[ R_D=3n\sum_{k=0}^{D-1}\binom mk+c\sum_{k=0}^{D-2}\binom mk, \] using zero for binomial terms outside 0..m. These are polynomial for a fixed D, but the exponent grows with D. The experiment caps columns at 50,000, generated rows at 100,000, and an estimated 64-bit word-work counter at 10,000,000 per mode. That work counter includes estimated bitset row/provenance XOR costs and product generation, not every allocation, sort, hash lookup, or interpreter operation. Elapsed time covers those implementation costs. None of these measurements is a universal bit-complexity theorem. ## 7. A certified limit: the cyclic table of order eight After the fixed comparison, a separate structural challenge used complete cyclic tables \[ T_n=\{(i,j,(i+j)\bmod n):0\le i,j