# RRLS v0.14 — Absolute P≟NP Attempt

## Verdict

**This attempt does not prove \(P=NP\).**

It produces a sharper, machine-auditable statement of where the proposed
rotation/lift/compiler strategy succeeds and where the unresolved complexity remains.

The strongest exact result is:

> Every nonempty local Boolean relation can be rotated so that one allowed local
> state becomes zero, but finding rotations that agree on all shared coordinates
> is exactly the original global constraint-satisfaction problem.

The difficulty is therefore not destroyed by local zeroing. It is transferred into
**global frame synchronization**.

---

## 1. Local Zero-Frame Theorem

Let

\[
R \subseteq \{0,1\}^k
\]

be any nonempty local relation and choose any allowed tuple \(a\in R\). Define

\[
\tau_a(x)=x\oplus a.
\]

Then

\[
\tau_a(a)=0^k,
\]

so

\[
0^k\in \tau_a(R).
\]

RRLS exhaustively checked all 255 nonempty ternary Boolean relations:

\[
\boxed{255/255\text{ locally zeroable}}.
\]

This validates the local geometric intuition completely: every local patch can choose
an origin in which one valid state is zero.

### Why this is not yet a SAT algorithm

For constraints \(R_i\) on scopes \(S_i\), choose local frames \(a_i\in R_i\).
They form one global coordinate system only when they agree on every overlap:

\[
a_i|_{S_i\cap S_j}=a_j|_{S_i\cap S_j}.
\]

Such a compatible family exists **if and only if** the original instance has a global
satisfying assignment.

Proof:

- If \(g\) is a satisfying assignment, take \(a_i=g|_{S_i}\).
- Conversely, compatible \(a_i\) glue to one assignment \(g\), and
  \(g|_{S_i}=a_i\in R_i\).

RRLS independently checked this equivalence on 240 generated small formulas:

\[
\boxed{240/240}.
\]

So the rotation idea is exact, but it moves complexity from the local relations to
their gluing law.

---

## 2. A concrete hidden-holonomy counterexample

Consider

\[
x_1\ne x_2,\qquad x_2\ne x_3,\qquad x_3\ne x_1.
\]

Every local relation is nonempty and can be zeroed. Pairwise arc consistency also
survives. Yet the odd cycle has no global assignment.

Measured result:

- local zeroing: succeeds;
- AC-3 arc consistency: reports consistent;
- global SAT: false;
- incidence-cycle rank: 4.

For this special language, the unresolved cycle has an affine parity invariant and
is solved by 2-SAT/GF(2). This is the cleanest example of the theory working:
the missing higher relation is a cycle holonomy.

For general 3-SAT, transition relations are set-valued and nonlinear; a single Abelian
cycle sum is not sufficient.

---

## 3. The two-axis tractability map

v0.14 now searches two mathematically distinct reasons a problem may collapse.

### Algebraic axis

A grouped local relation language is compiled when it has a common closure operation:

- constant zero / constant one;
- AND: Horn;
- OR: dual-Horn;
- majority: bijunctive / 2-SAT;
- minority: affine / GF(2).

It also detects global variable-complement rotations such as renamable Horn.

### Geometric axis

Even a locally hard relation can be easy when the interaction graph has bounded
treewidth. RRLS performs exact factor elimination while the width remains below a
fixed cap.

This gives a useful distinction:

\[
\boxed{\text{hard local algebra}+\text{easy geometry}\Rightarrow\text{polynomial}}
\]

and

\[
\boxed{\text{easy algebra}+\text{dense geometry}\Rightarrow\text{polynomial}}.
\]

The unresolved region is:

\[
\boxed{\text{Schaefer-hard algebra}+\text{unbounded interaction width}}.
\]

---

## 4. What the new compiler removed

### Hidden majority network

A 60-variable, 900-clause network was generated from translated ternary relations whose
common invariant is majority.

v0.13:

\[
7\text{ nodes},\quad
4\text{ branches},\quad
0.10492\text{ s}.
\]

v0.14:

\[
1\text{ node},\quad
0\text{ branches},\quad
1\text{ algebra dispatch},\quad
0.01951\text{ s}.
\]

Measured speedup:

\[
\boxed{5.38\times}.
\]

### Schaefer-hard relation on a cyclic low-width geometry

The local positive 1-in-3 relation has no Schaefer tractability polymorphism, but the
80-variable cyclic occurrence graph has a small width certificate.

v0.13:

\[
3\text{ nodes},\quad
1\text{ branch},\quad
0.37014\text{ s}.
\]

v0.14:

\[
1\text{ node},\quad
0\text{ branches},\quad
\text{treewidth upper bound }4,\quad
0.02582\text{ s}.
\]

Measured speedup:

\[
\boxed{14.34\times}.
\]

These are genuine examples of:

\[
\text{wrong representation}
\Rightarrow
\text{branching}
\Rightarrow
\text{higher relation}
\Rightarrow
\text{branch-free polynomial collapse}.
\]

---

## 5. What did not collapse

On the 60-variable random-3SAT control, both versions followed the same search tree:

\[
100\text{ nodes},\qquad
51\text{ branch/lift nodes}.
\]

v0.14 records the first representative irreducible core with:

- no common Schaefer polymorphism;
- arc consistency still surviving;
- large cyclic coupling;
- width above the bounded dynamic-programming cap.

The additional theorem audit costs approximately

\[
\boxed{9.6\%}
\]

on this case after self-optimization, while preserving identical search behavior.

Across the random-3SAT width experiment, the min-degree width upper bound grew
empirically as

\[
w \approx 0.6844n+0.8376.
\]

That is not an asymptotic proof, but it explains why fixed-width factor elimination
does not rescue these instances: \(2^w\) becomes exponential when \(w=\Theta(n)\).

---

## 6. Why “compile every local matrix” hits a squeeze

An arity-\(k\) Boolean relation is an arbitrary subset of \(2^k\) tuples, so the number
of possible relations is

\[
\boxed{2^{2^k}}.
\]

Examples:

| arity \(k\) | local rows \(2^k\) | possible relations |
|---:|---:|---:|
| 3 | 8 | 256 |
| 4 | 16 | 65,536 |
| 5 | 32 | 4,294,967,296 |
| 6 | 64 | 18,446,744,073,709,551,616 |
| 8 | 256 | \(2^{256}\) |

This creates the **RRLS bounded-arity squeeze**:

1. Keep arity bounded: every local relation can be catalogued, but global gluing can
   remain NP-complete.
2. Let arity grow until it captures the global instance: arbitrary relation tables and
   vocabulary can grow exponentially or doubly exponentially.

A valid route must therefore find a **compressed nonlocal invariant**, not merely
enumerate larger truth tables.

---

## 7. Why defining a new language is not enough by itself

A language can trivially contain an instruction

```text
SAT(formula)
```

and declare it one unit of work. In that cost model, SAT is “easy” by definition.

That does not prove standard \(P=NP\).

For a valid proof, all of the following must be polynomial in the original input size:

\[
\boxed{
T_{\mathrm{compiler}}
+
L_{\mathrm{compiled}}
+
T_{\mathrm{interpreter}}
+
L_{\mathrm{vocabulary}}
+
L_{\mathrm{intermediate}}
}.
\]

The language must be uniform and polynomially simulable by an ordinary deterministic
machine. Exponential tables, an NP oracle, super-polynomial basis search, or
input-length advice cannot be hidden behind a token.

If RRLS met those conditions and solved SAT exactly for every formula, that would
indeed prove \(P=NP\). The proof gate exists to enforce precisely this standard.

---

## 8. The theorem-level barrier found by the search

For **fixed Boolean constraint languages**, Schaefer’s dichotomy classifies the
tractable closure families and makes the remaining cases NP-complete. RRLS v0.14
implements those Boolean polymorphism tests rather than guessing another local class.

The finite-domain CSP dichotomy extends the same broad lesson: tractability is
controlled by algebraic polymorphisms; otherwise a fixed finite constraint language is
NP-complete.

This does not rule out \(P=NP\). It rules out the easy hope that there is an
unnoticed seventh fixed local Boolean relation class that automatically solves general
3-SAT.

Known knowledge-compilation lower bounds also show that some compact target languages,
such as DNNF, require exponential size for explicit CNF families. Likewise, strong
local-lift hierarchies can require linearly many levels on some CSP families. A proof
must therefore use a representation not covered by those restricted barriers, or show
why RRLS avoids their hypotheses.

---

## 9. Exact remaining target

The remaining problem is now sharply stated:

> Find a fixed, uniform, polynomial-time computable invariant of the global
> frame-synchronization problem that resolves every Schaefer-hard,
> unbounded-width core without branching and without a super-polynomial
> representation.

Formally, for every residual formula \(F\), RRLS needs an operator \(R\) satisfying

\[
R(F)=F'
\]

with strict progress, exact satisfiability preservation, and

\[
T(R),\quad |F'|,\quad
\#\text{applications}
\le \operatorname{poly}(|F|).
\]

The current engine does not possess such an operator.

RRLS uses zero branch nodes as a deliberately conservative sufficient target. This is
not logically necessary: an algorithm may branch and still run in polynomial time if
the **total** branch tree is proved polynomially bounded. No such bound has been proved
for the current general-CNF search.

Therefore:

\[
\boxed{P=NP\text{ remains unproved by RRLS v0.14.}}
\]

But the failed proof is now informative: **local zeroing is complete; global gluing is
the hard coordinate.**

---

## 10. Machine checks in this release

- 450/450 random small 3-SAT formulas matched independent brute force.
- 255/255 nonempty ternary relations were locally zeroable.
- 240/240 generated formulas matched the local-frame/global-assignment equivalence.
- An arc-consistent odd-cycle instance demonstrated that local consistency is
  insufficient.
- Majority-closed hidden relations compiled to 2-SAT without branching.
- Schaefer-hard low-width geometry compiled by exact factor elimination.
- General random 3-SAT still branched, so the proof gate remained closed.

## Primary references

- Clay Mathematics Institute, P vs NP:
  https://www.claymath.org/millennium/p-vs-np/
- T. J. Schaefer, “The Complexity of Satisfiability Problems”:
  https://doi.org/10.1145/800133.804350
- D. Zhuk, “A Proof of the CSP Dichotomy Conjecture”:
  https://arxiv.org/abs/1704.01914
- S. Bova et al., “A Strongly Exponential Separation of DNNFs from CNF Formulas”:
  https://arxiv.org/abs/1411.1995
- G. Schoenebeck, “Linear Level Lasserre Lower Bounds for Certain k-CSPs”:
  https://schoeneb.people.si.umich.edu/papers/Lasserre.pdf