# RRLS v0.17 — The Fiber Occupancy Wall ## Status **P = NP is not proved.** v0.17 finds the sharpest formulation of the RRLS wall so far. The key result is: > Making the defining equation geometrically simple is not enough. > The irreducible operation is deciding whether its solution fiber is empty. --- ## 1. Any Boolean function can already be lifted into one clean coordinate For any Boolean formula/function F(x), define T_F(x,b) = (x, b XOR F(x)). This map is a bijection and an involution: T_F(T_F(x,b)) = (x,b). A circuit for T_F only needs to compute F and XOR its result into one auxiliary bit. So RRLS's original dream step complicated relation -> simple higher coordinate does not by itself solve SAT. The transformed problem still asks exists x : F(x)=1. The complexity survives as **fiber occupancy / existential projection**. The included exact finite tests verify bijectivity and involution for generated CNFs. --- ## 2. Fiber-Centering Lemma Let S_F = {x : F(x)=1}. Suppose a uniform polynomial-time compiler outputs an efficiently invertible bijection G_F such that F is satisfiable iff 0^n is in G_F(S_F). Then SAT is in P: 1. compile G_F; 2. compute x* = G_F^(-1)(0^n); 3. evaluate F(x*). If the equivalence holds, F(x*) tells us SAT immediately. Therefore a universal "rotate the solution onto the zero axis" compiler is not a free geometric trick. It is already a polynomial-time SAT algorithm. This makes the user's zero-axis intuition mathematically precise: the missing step is not moving a *known* solution to zero; it is finding the transform that knows which fiber contains a solution. --- ## 3. Straightening is tiny once the witness is known If x* is a satisfying assignment, then G(x) = x XOR x* maps x* to 0. This requires at most n NOT gates. Measured on random satisfiable 3-SAT near clause ratio 4.26: | n | cases | median_checks | max_checks | median_fraction | median_discovery_seconds | median_NOT_gates | max_NOT_gates | median_checks_per_gate | |----:|--------:|----------------:|-----------------:|------------------:|---------------------------:|-------------------:|----------------:|-------------------------:| | 10 | 5 | 407 | 683 | 0.397461 | 0.000514552 | 5 | 6 | 81.4 | | 12 | 5 | 561 | 3700 | 0.136963 | 0.000735726 | 3 | 8 | 187 | | 14 | 5 | 4125 | 13187 | 0.25177 | 0.00565913 | 6 | 6 | 687.5 | | 16 | 5 | 13000 | 31250 | 0.198364 | 0.0280706 | 6 | 8 | 2166.67 | | 18 | 5 | 72524 | 184019 | 0.276657 | 0.0890565 | 8 | 10 | 9065.5 | | 20 | 3 | 313786 | 676356 | 0.29925 | 0.400641 | 10 | 10 | 31378.6 | | 22 | 3 | 1.6466e+06 | 2.89968e+06 | 0.392579 | 1.90535 | 10 | 15 | 164660 | At n=22, the median brute-force discovery cost in the tested sample was about 1,646,596 assignment checks, while the final centering map needed only about 10 NOT gates. This is not an asymptotic lower bound on SAT. It is an exact demonstration of the compiler trap: tiny final coordinate transform != cheap discovery of that transform. The expensive work can be hidden entirely in orientation selection. --- ## 4. Bijections preserve the fiber's cardinality For every bijection G, |G(S_F)| = |S_F|. So reversible coordinate transforms never remove the existential/counting invariant. They only rearrange the solution geometry. Every nonempty fiber can in principle be permuted into a visually simple canonical set, but synthesizing such a canonical permutation can require exactly the information we were trying to compute. This distinguishes two different goals: equation straightening fiber straightening. The first is easy in general via T_F. The second is the actual complexity-theoretic problem. --- ## 5. Closure stress test: local simplicity can explode under conjunction v0.17 incrementally conjoined random 3-SAT clauses and measured exact ANF/Fourier structure. Representative n=14 random 3-CNF: | constraints | solutions | anf_terms | walsh_nonzero | affine | |--------------:|------------:|------------:|----------------:|:---------| | 1 | 14336 | 3 | 8 | False | | 2 | 12544 | 9 | 64 | False | | 3 | 10752 | 21 | 104 | False | | 4 | 9184 | 81 | 544 | False | | 6 | 6720 | 168 | 746 | False | | 8 | 5328 | 380 | 3098 | False | | 10 | 3904 | 468 | 3842 | False | | 12 | 2680 | 590 | 4128 | False | | 16 | 1226 | 1518 | 12732 | False | | 20 | 711 | 2154 | 16384 | False | | 24 | 424 | 3120 | 14828 | False | | 32 | 193 | 2802 | 16384 | False | | 40 | 88 | 3378 | 13284 | False | | 60 | 5 | 1536 | 16384 | False | After around 20 clauses, the Walsh support reached all 16,384 frequencies. The same experiment on XOR constraints behaves differently: | constraints | solutions | anf_terms | walsh_nonzero | affine | |--------------:|------------:|------------:|----------------:|:---------| | 1 | 8192 | 3 | 1 | True | | 2 | 4096 | 10 | 4 | True | | 3 | 2048 | 26 | 8 | True | | 4 | 1024 | 78 | 16 | True | | 6 | 256 | 514 | 64 | True | | 8 | 64 | 1596 | 256 | True | | 10 | 16 | 2228 | 1024 | True | | 12 | 4 | 1256 | 4096 | True | | 14 | 0 | 0 | 1 | True | ANF and Fourier support may themselves become large, but the relation remains affine and is still represented compactly by a row-reduced GF(2) matrix. Therefore the correct invariant is not generic sparsity. It is **algebraic closure under the operations the solver performs**. --- ## 6. Three independent walls now meet at the same point ### Backdoor wall Modern SAT backdoor-depth theory constructs obstruction trees of arbitrarily high depth into Horn/Krom classes. Shallow branching into tractable islands is not universal. ### Extension-synthesis wall RRLS vocabulary tokens are analogous to extension variables in strong proof systems. Naming relations can make representations exponentially shorter, but finding the right definitions can itself be hard. ### Fiber-occupancy wall Even a polynomial reversible transformation can expose F as a single output coordinate without making `exists x F(x)` easy. These are three views of the same missing resource: a polynomially computable global invariant that decides nonemptiness while remaining closed under composition/projection. --- ## 7. Local basis rotation has already been pushed very far in theory Holographic algorithms / Holant theory formalize invertible basis transformations of local constraint tensors. They discover genuinely surprising tractable coordinate systems, including affine/product/matchgate-style families. But Boolean Holant/#CSP dichotomy theorems also identify broad families that remain #P-hard outside the tractable holographic orbits. This does not itself settle decision SAT or P vs NP. It does tell us that "search for one better local basis" is not an unexploited universal trick. Any RRLS breakthrough now has to be **nonlocal and instance-global**, or prove a new closure theorem outside those classified local transformations. --- ## 8. New theorem target: Fiber Canonicalization The cleanest sufficient theorem I can formulate is: There exists one uniform polynomial-time algorithm C which maps every CNF F to a representation R_F such that: 1. R_F exactly represents the solution fiber of F; 2. |R_F| is polynomial in |F|; 3. nonemptiness of R_F is decidable in polynomial time; 4. conjunction and existential projection needed during compilation are polynomial; 5. every intermediate representation stays polynomial-size; 6. C itself uses only polynomial time/advice. Then SAT is in P and therefore P=NP. This is not proved. v0.17's purpose is to prevent weaker claims from being mistaken for this theorem. --- ## 9. What a real next candidate must do A candidate wall-break operator must provide more than a compact coordinate map. It must produce a **fiber invariant** whose zero/nonzero status can be computed polynomially and which survives composition. Known successful examples: XOR -> rank / consistency over GF(2) 2-SAT -> SCC contradiction Horn -> closure conflict matching -> augmenting-path / Hall structure The unknown object would be the analogue of "rank" for arbitrary SAT. That is now the target.