# RRLS v0.13 — P≟NP Proof Search

## Status

**P = NP is NOT proved by this engine.**

This release deliberately introduces a proof gate that remains closed while the
uniform general-CNF algorithm can reach a binary branch/lift operation.

The current generic structural recurrence is

    T(n) <= 2 T(n-1) + poly(n)

so the current provable upper bound remains exponential.

## What the engine did establish

### Exactness sanity

- 83/83 small formulas matched an independent brute-force solver.
- 5,000-variable 2-SAT and Horn instances dispatched in one node with zero branching.

### A hard family exposed the missing language

Before compiling an ALLDIFFERENT relation, pigeonhole contradictions used:

| pigeons | search nodes |
|---:|---:|
| 5 | 9 |
| 6 | 39 |
| 7 | 181 |
| 8 | 889 |
| 9 | 5,659 |

The empirical fit favored exponential growth (~4.96× per extra pigeon over the tested
range). This is empirical evidence about this implementation, not a complexity proof.

### Lift representation -> compile relation -> collapse

The irreducible pigeonhole core was recognized as an ALLDIFFERENT / system-of-distinct-
representatives relation. v0.13 compiles that encoding to bipartite matching.

After adding the primitive:

| pigeons | search nodes | branch nodes |
|---:|---:|---:|
| 5 | 1 | 0 |
| 6 | 1 | 0 |
| 7 | 1 | 0 |
| 8 | 1 | 0 |
| 9 | 1 | 0 |
| 12 | 1 | 0 |
| 20 | 1 | 0 |
| 40 | 1 | 0 |

The 40-pigeon contradiction is therefore one matching dispatch instead of a DPLL tree.

### A second algebraic lift

Exact CNF encodings of XOR/parity constraints are detected and compiled to GF(2)
Gaussian elimination.

- 1,000-variable consistent XOR-SAT: 1 node, 0 branches, ~0.085 s.
- inconsistent parity systems likewise dispatch without Boolean search.

These are examples of a crucial RRLS principle:

    apparent Boolean search complexity can collapse when the correct higher relation
    algebra is recognized.

They do **not** imply that every 3-SAT instance has such a polynomial lift.

## What still blocks P=NP

General random 3-SAT still generated irreducible cores and branch nodes after all
current exact reductions.

Therefore the current language is incomplete.

To turn this research into an actual P=NP proof, RRLS would need a fixed relation
language L and a theorem proving all three:

1. **Completeness:** every CNF residual is recognized by some operator in L before branch.
2. **Polynomial recognition/execution:** selecting and executing operators takes
   polynomial time in the original formula size.
3. **Polynomial representation:** vocabulary, intermediate relations, and any
   precomputation/advice remain polynomial size. Exponential tables hidden in a
   "compiled language" do not count.

A finite benchmark cannot establish any of these universally.

## Current polynomial relation vocabulary

- unit propagation
- pure-literal elimination
- connected-component decomposition
- bounded Davis-Putnam resolution elimination
- 2-SAT -> implication graph SCC
- Horn-SAT -> least-model forward chaining
- ALLDIFFERENT -> bipartite matching
- XOR/parity CNF -> GF(2) Gaussian elimination
- residual memoization

When none applies, the formula is recorded as an irreducible core and the proof gate
fails before branch.

## Research target

Instead of trying to "prove P=NP by testing more SAT instances", the next loop should
mine the irreducible general-3SAT cores for a new polynomially recognizable algebra.

The success criterion is not lower benchmark time. It is:

    branch_nodes == 0 for structural reasons

plus a proof that the reason applies to **every possible CNF**, with polynomial
recognition, execution, and language size.