# RRLS v0.28 — Adversarial Proof Gate ## Status **P = NP is not proved.** v0.28 is an adversarial release. Its job is not to make RRLS look good; its job is to locate every place where a claimed polynomial collapse can hide exponential work. The hard proof gate is: 1. one fixed uniform deterministic algorithm; 2. exact SAT correctness on every CNF; 3. all preprocessing/advice/intermediate representations counted; 4. a rigorous polynomial worst-case bound on every input; 5. no truth-table oracle, hidden brute force, float identity, empirical curve fit, or instance-specific exponential search. No current v0.28 route satisfies all five for general CNF. --- # 1. Semantic future automaton: perfect merge + perfect event jump still has a wall A reduced ordered BDD is a useful exact control for the string/collision metaphor. For a fixed variable order it does both operations we wanted: - two prefixes merge iff they induce the same remaining Boolean function; - if testing a variable gives the same low/high future, that variable is skipped completely. So an ROBDD already implements: exact semantic synchronization + exact jump over irrelevant "ticks". The profiler is deliberately exponential at construction time because it uses a full small-n truth vector. It is a diagnostic, not a SAT algorithm. Low-density random 3-SAT, ratio 1.5, best **observed** over natural/reverse/frequency/ min-fill plus random orders: | n | cases | median_nodes | max_nodes | median_width | median_semantic_peak | median_skip | |----:|--------:|---------------:|------------:|---------------:|-----------------------:|--------------:| | 12 | 12 | 83 | 129 | 14 | 19.5 | 1.36778 | | 14 | 10 | 158.5 | 244 | 29 | 39 | 1.74319 | | 16 | 10 | 286.5 | 433 | 50 | 57 | 2.04967 | | 18 | 8 | 492 | 754 | 84 | 104 | 2.21492 | | 20 | 4 | 894 | 1156 | 139 | 160 | 2.08134 | The exact future DAG is not automatically tiny. ### Ordering caveat For one n=8 adversarial formula every one of the 40,320 variable orders was checked: | n | seed | orders_checked | heuristic_nodes | optimal_nodes | optimal_width | worst_nodes | heuristic_over_optimal | seconds | |----:|-------:|-----------------:|------------------:|----------------:|----------------:|--------------:|-------------------------:|----------:| | 8 | 19 | 40320 | 34 | 23 | 5 | 54 | 1.47826 | 7.20923 | The heuristic best had 34 nodes; the true optimum had 23. Therefore larger results are explicitly called *best observed*, never optimal OBDD size. ### Complement/signed future quotient Identifying f and NOT f as one generator plus one polarity bit did not change peak semantic width in the tested corpus: | n | cases | median_plain | median_signed | median_ratio | |----:|--------:|---------------:|----------------:|---------------:| | 12 | 4 | 19.5 | 19.5 | 1 | | 14 | 4 | 33 | 33 | 1 | | 16 | 4 | 46 | 46 | 1 | | 18 | 3 | 93 | 93 | 1 | This exact shortcut does not solve the observed future-width wall. --- # 2. Proof-safe engine: branch-free means branch-free `rrls_v28_proof_attacker.py` executes only certified polynomial routes when `allow_branch=False`. If none applies, the answer is `UNKNOWN`. That is intentional: UNKNOWN is a counterexample to the **current proof language**, not to P=NP. For phase-transition random 3-SAT at ratio 4.26: | n | cases | resolved | UNKNOWN | median_width | max_width | median_seconds | |----:|--------:|-----------:|----------:|---------------:|------------:|-----------------:| | 20 | 8 | 0 | 8 | 14 | 15 | 0.00199215 | | 30 | 8 | 0 | 8 | 20 | 22 | 0.00484193 | | 40 | 8 | 0 | 8 | 28 | 28 | 0.0102151 | | 60 | 8 | 0 | 8 | 40 | 41 | 0.0325596 | | 80 | 8 | 0 | 8 | 54.5 | 56 | 0.0915906 | | 100 | 8 | 0 | 8 | 67 | 69 | 0.176138 | | 120 | 8 | 0 | 8 | 80 | 83 | 0.31568 | Every tested formula from n=20 through n=120 escaped the current polynomial portfolio. The observed min-fill width grew from about 14 to about 80. --- # 3. Logarithmic-width escape hatch failed on the controls If exact factor width is w <= c log_2 n, then a generic Boolean factor has at most 2^w <= n^c states, so such an elimination route would still be polynomial. We explicitly tested c=1,2,3: | n | mult | cap | cases | resolved | median_actual_width | max_actual_width | |----:|-------:|------:|--------:|-----------:|----------------------:|-------------------:| | 20 | 1 | 5 | 6 | 0 | 14 | 14 | | 20 | 2 | 9 | 6 | 0 | 14 | 14 | | 20 | 3 | 13 | 6 | 0 | 14 | 14 | | 30 | 1 | 5 | 6 | 0 | 20.5 | 22 | | 30 | 2 | 10 | 6 | 0 | 20.5 | 22 | | 30 | 3 | 15 | 6 | 0 | 20.5 | 22 | | 40 | 1 | 6 | 6 | 0 | 27.5 | 30 | | 40 | 2 | 11 | 6 | 0 | 27.5 | 30 | | 40 | 3 | 16 | 6 | 0 | 27.5 | 30 | | 60 | 1 | 6 | 6 | 0 | 41 | 44 | | 60 | 2 | 12 | 6 | 0 | 41 | 44 | | 60 | 3 | 18 | 6 | 0 | 41 | 44 | | 80 | 1 | 7 | 6 | 0 | 53.5 | 56 | | 80 | 2 | 13 | 6 | 0 | 53.5 | 56 | | 80 | 3 | 19 | 6 | 0 | 53.5 | 56 | | 100 | 1 | 7 | 6 | 0 | 67.5 | 69 | | 100 | 2 | 14 | 6 | 0 | 67.5 | 69 | | 100 | 3 | 20 | 6 | 0 | 67.5 | 69 | | 120 | 1 | 7 | 6 | 0 | 82 | 84 | | 120 | 2 | 14 | 6 | 0 | 82 | 84 | | 120 | 3 | 21 | 6 | 0 | 82 | 84 | No tested phase-transition random-3SAT instance resolved through these logarithmic-width caps. This is finite evidence about the current instances/order heuristic, not a treewidth lower-bound theorem. --- # 4. The router still crushes large formulas when a real polynomial algebra exists The same proof-safe rules were applied across control families: | family | scale | cases | resolved | SAT | UNSAT | UNKNOWN | median_width | |:----------------|--------:|--------:|-----------:|------:|--------:|----------:|---------------:| | 2SAT | 50 | 2 | 2 | 0 | 2 | 0 | 0 | | 2SAT | 100 | 2 | 2 | 0 | 2 | 0 | 0 | | 2SAT | 200 | 2 | 2 | 0 | 2 | 0 | 0 | | Graph-3Color | 8 | 3 | 3 | 3 | 0 | 0 | 6 | | Graph-3Color | 12 | 3 | 0 | 0 | 0 | 3 | 11 | | Graph-3Color | 16 | 3 | 0 | 0 | 0 | 3 | 19 | | Graph-3Color | 20 | 3 | 0 | 0 | 0 | 3 | 28 | | Horn | 50 | 2 | 2 | 0 | 2 | 0 | 0 | | Horn | 100 | 2 | 2 | 0 | 2 | 0 | 0 | | Horn | 200 | 2 | 2 | 0 | 2 | 0 | 0 | | NAE-3SAT | 20 | 3 | 0 | 0 | 0 | 3 | 10 | | NAE-3SAT | 30 | 3 | 0 | 0 | 0 | 3 | 15 | | NAE-3SAT | 40 | 3 | 0 | 0 | 0 | 3 | 20 | | NAE-3SAT | 60 | 3 | 0 | 0 | 0 | 3 | 28 | | Pigeonhole | 5 | 1 | 1 | 0 | 1 | 0 | 0 | | Pigeonhole | 8 | 1 | 1 | 0 | 1 | 0 | 0 | | Pigeonhole | 12 | 1 | 1 | 0 | 1 | 0 | 0 | | Pigeonhole | 16 | 1 | 1 | 0 | 1 | 0 | 0 | | Positive-1-in-3 | 20 | 3 | 3 | 0 | 3 | 0 | 7 | | Positive-1-in-3 | 30 | 3 | 0 | 0 | 0 | 3 | 10 | | Positive-1-in-3 | 40 | 3 | 0 | 0 | 0 | 3 | 13 | | Positive-1-in-3 | 60 | 3 | 0 | 0 | 0 | 3 | 19 | | Tseitin | 20 | 2 | 2 | 1 | 1 | 0 | 0 | | Tseitin | 40 | 2 | 2 | 1 | 1 | 0 | 0 | | Tseitin | 80 | 2 | 2 | 1 | 1 | 0 | 0 | | Tseitin | 120 | 2 | 2 | 1 | 1 | 0 | 0 | Important controls: - 2-SAT and Horn: resolved through n=200; - Tseitin parity: resolved through the tested 180 edge-variable instances by GF(2); - pigeonhole: resolved through p=16, 240 Boolean variables, by assignment/matching; - renamable Horn was restored to the shared router and passed all 12 constructed n=50/100/200 tests; - NAE-3SAT, larger positive 1-in-3, and larger graph-3color instances become UNKNOWN. Thus the engine is not merely "failing on size." It separates recognized tractable structure from uncompiled residuals. --- # 5. Constraint capture: fewer objects can mean a larger surface The user's non-crossing/ravel intuition maps exactly to factor elimination. When every factor touching variable v is captured into one compound object, the new surface is the union of all incident scopes minus v. For a Boolean surface of width w, a generic exact table has 2^w entries. | family | n | cases | median_boundary | max_boundary | median_digits | |:---------|-----:|--------:|------------------:|---------------:|----------------:| | lowwidth | 100 | 1 | 4 | 4 | 2 | | lowwidth | 500 | 1 | 4 | 4 | 2 | | lowwidth | 1000 | 1 | 4 | 4 | 2 | | lowwidth | 5000 | 1 | 4 | 4 | 2 | | random3 | 20 | 5 | 14 | 15 | 5 | | random3 | 30 | 5 | 21 | 22 | 7 | | random3 | 40 | 5 | 27 | 28 | 9 | | random3 | 60 | 5 | 41 | 42 | 13 | | random3 | 80 | 5 | 54 | 54 | 17 | | random3 | 100 | 5 | 68 | 69 | 21 | | random3 | 120 | 5 | 82 | 83 | 25 | Bounded-window formulas stayed at boundary 4 through n=5000. Random phase-transition 3-SAT reached median boundary 82 at n=120. A generic 82-bit Boolean surface has 2^82 = 4,835,703,278,458,516,698,824,704 possible boundary states. So capture can reduce the number of objects while storing the complexity as boundary "tension." This is a representation statement, not a hardness proof: algebra can compress some large boundaries, as XOR and matching already demonstrate. --- # 6. Boundary functions are not trivially affine after capture For small formulas, a prefix was eliminated exactly and the resulting 14-variable integer completion-count function was profiled modulo 257. | ratio | n | cases | median_support | median_distinct | median_poly_fraction | median_degree | median_rank_fraction | |--------:|----:|--------:|-----------------:|------------------:|-----------------------:|----------------:|-----------------------:| | 1.5 | 14 | 4 | 0.0496216 | 2 | 0.0514832 | 13 | 0.222656 | | 1.5 | 16 | 4 | 0.0688782 | 4 | 0.253601 | 14 | 0.316406 | | 1.5 | 18 | 4 | 0.0684814 | 6 | 0.335358 | 14 | 0.351562 | | 1.5 | 20 | 4 | 0.0658875 | 12 | 0.334167 | 14 | 0.382812 | | 4.26 | 14 | 4 | 0.00012207 | 2 | 0.0146484 | 14 | 0.0117188 | | 4.26 | 16 | 4 | 0.000274658 | 2.5 | 0.012085 | 14 | 0.015625 | | 4.26 | 18 | 4 | 9.15527e-05 | 1.5 | 0.000488281 | 7 | 0.0078125 | | 4.26 | 20 | 4 | 0.000213623 | 2 | 0.0136719 | 7 | 0.0117188 | At ratio 1.5, where many completions remain, median multilinear degree is essentially maximal and coefficient support/rank are nontrivial. At ratio 4.26, low rank/support often reflects the simple fact that very few completions survive. These are exponential diagnostic truth-table experiments. --- # 7. Anti-bias fixation: a real exact compression effect Define the cheap anchor a_v = 0 if positive occurrences of v >= negative occurrences, 1 otherwise. That is the value that locally falsifies the more frequent literal polarity. It is computable in linear time in the input size. On exact 14-coordinate boundary count functions: | ratio | n | cases | improved | median_base | median_anchor | median_reduction | best_reduction | worst_reduction | median_base_degree | median_anchor_degree | improved_fraction | |--------:|----:|--------:|-----------:|--------------:|----------------:|-------------------:|-----------------:|------------------:|---------------------:|-----------------------:|--------------------:| | 1.5 | 16 | 16 | 16 | 3914.5 | 2115 | 0.402116 | 0.740112 | 0.108392 | 14 | 14 | 1 | | 1.5 | 18 | 16 | 16 | 5011 | 2763 | 0.442203 | 0.730877 | 0.0508631 | 14 | 14 | 1 | | 1.5 | 20 | 16 | 14 | 6038.5 | 3913.5 | 0.338118 | 0.642794 | -0.117814 | 14 | 14 | 0.875 | | 2 | 16 | 16 | 16 | 3224 | 1199 | 0.552594 | 0.826606 | 0.16863 | 14 | 14 | 1 | | 2 | 18 | 16 | 15 | 4755.5 | 2151 | 0.58687 | 0.761763 | -0.150588 | 14 | 14 | 0.9375 | | 2 | 20 | 16 | 16 | 6549.5 | 2553.5 | 0.589329 | 0.761268 | 0.254232 | 14 | 14 | 1 | The effect survived different finite fields: | p | n | cases | improved | median_reduction | median_base | median_anchor | improved_fraction | |----:|----:|--------:|-----------:|-------------------:|--------------:|----------------:|--------------------:| | 3 | 16 | 8 | 8 | 0.534735 | 3791.5 | 1726.5 | 1 | | 3 | 18 | 8 | 8 | 0.516588 | 3433 | 1478 | 1 | | 3 | 20 | 8 | 8 | 0.705789 | 5656.5 | 1927 | 1 | | 5 | 16 | 8 | 6 | 0.557796 | 2915.5 | 1457 | 0.75 | | 5 | 18 | 8 | 8 | 0.597974 | 4388 | 1810 | 1 | | 5 | 20 | 8 | 7 | 0.458664 | 5174 | 2747 | 0.875 | | 257 | 16 | 8 | 8 | 0.59292 | 4446 | 1507.5 | 1 | | 257 | 18 | 8 | 8 | 0.543614 | 4737 | 2077 | 1 | | 257 | 20 | 8 | 6 | 0.502627 | 4774 | 2637.5 | 0.75 | and different boundary sizes: | w | cases | improved | median_base | median_anchor | median_reduction | worst | best | improved_fraction | |----:|--------:|-----------:|--------------:|----------------:|-------------------:|----------:|---------:|--------------------:| | 10 | 8 | 8 | 744.5 | 401 | 0.350868 | 0.15903 | 0.624706 | 1 | | 12 | 8 | 7 | 2404.5 | 1166.5 | 0.525496 | -0.182329 | 0.677097 | 0.875 | | 14 | 8 | 8 | 5993 | 2471.5 | 0.588185 | 0.201882 | 0.772878 | 1 | | 16 | 8 | 8 | 12478 | 5402.5 | 0.495971 | 0.404058 | 0.70623 | 1 | On the raw CNF truth functions themselves it also persisted: | n | cases | improved | median_base | median_anchor | median_reduction | worst | best | improved_fraction | |----:|--------:|-----------:|--------------:|----------------:|-------------------:|---------:|---------:|--------------------:| | 14 | 8 | 8 | 1753.5 | 760.5 | 0.494166 | 0.332294 | 0.790857 | 1 | | 16 | 8 | 8 | 5373 | 3208 | 0.432689 | 0.126269 | 0.697579 | 1 | | 18 | 8 | 8 | 18033.5 | 5821.5 | 0.661986 | 0.472149 | 0.845064 | 1 | This is **sparsity compression**, not a degree collapse: median polynomial degree stays maximal. --- # 8. Exact dead-radius lemma Let F have SAT indicator f and let a be any anchor. Define delta(a) = min_{x : f(x)=1} Hamming(a,x). Translate the Boolean function: f_a(y)=f(a XOR y). Write its multilinear/Möbius expansion f_a(y)=sum_S c_S product_{i in S} y_i. For every subset S, c_S = sum_{T subseteq S} (-1)^{|S|-|T|} f_a(1_T). If |S| < delta(a), then every T subseteq S has Hamming weight below delta(a), hence f_a(1_T)=0. Therefore **|S| < delta(a) => c_S = 0.** So a deep infeasible anchor provably creates an empty low-degree Taylor/ANF band. ### Polynomial-time certificate Every clause falsified by a must have at least one variable flipped by any satisfying assignment. If L pairwise-variable-disjoint falsified clauses are found, those required flips are distinct, hence delta(a) >= L. A greedy disjoint-clause packing is polynomial-time and gives an exact lower-bound certificate. Validation: | ratio | n | cases | median_delta | median_L | max_L | median_falsified | median_tightness | violations | |--------:|----:|--------:|---------------:|-----------:|--------:|-------------------:|-------------------:|-------------:| | 1.5 | 14 | 10 | 4 | 3 | 4 | 7 | 0.775 | 0 | | 1.5 | 16 | 10 | 4 | 3 | 4 | 8.5 | 0.75 | 0 | | 1.5 | 18 | 10 | 5 | 3 | 4 | 11 | 0.666667 | 0 | | 2 | 14 | 10 | 4.5 | 3 | 4 | 8 | 0.6 | 0 | | 2 | 16 | 10 | 5 | 3 | 4 | 7 | 0.6 | 0 | | 2 | 18 | 10 | 6 | 4 | 5 | 9.5 | 0.633333 | 0 | | 4.26 | 14 | 10 | 8 | 4 | 4 | 13.5 | 0.5 | 0 | | 4.26 | 16 | 10 | 10 | 4 | 5 | 16.5 | 0.4 | 0 | | 4.26 | 18 | 10 | 10 | 5 | 6 | 18.5 | 0.5 | 0 | No theorem violations occurred. Scaling: | ratio | n | cases | median_L | max_L | median_L_over_n | median_falsified | median_dead_ball_fraction | |--------:|----:|--------:|-----------:|--------:|------------------:|-------------------:|----------------------------:| | 2 | 20 | 12 | 4 | 5 | 0.2 | 11 | 0.00128841 | | 2 | 40 | 12 | 9 | 11 | 0.225 | 23.5 | 9.10829e-05 | | 2 | 60 | 12 | 13 | 14 | 0.216667 | 39 | 1.59181e-06 | | 2 | 80 | 12 | 17 | 20 | 0.2125 | 47.5 | 2.93567e-08 | | 2 | 100 | 12 | 21.5 | 24 | 0.215 | 58.5 | 1.36332e-09 | | 2 | 120 | 12 | 25.5 | 27 | 0.2125 | 70 | 2.65155e-11 | | 2 | 200 | 12 | 43 | 44 | 0.215 | 115 | 2.55191e-17 | | 2 | 400 | 12 | 85 | 89 | 0.2125 | 229 | 4.94075e-33 | | 4.26 | 20 | 12 | 5 | 6 | 0.25 | 18.5 | 0.00590897 | | 4.26 | 40 | 12 | 9 | 11 | 0.225 | 37 | 9.10829e-05 | | 4.26 | 60 | 12 | 15 | 16 | 0.25 | 56.5 | 2.11185e-05 | | 4.26 | 80 | 12 | 18 | 21 | 0.225 | 77 | 1.13307e-07 | | 4.26 | 100 | 12 | 24 | 25 | 0.24 | 99 | 2.75679e-08 | | 4.26 | 120 | 12 | 29.5 | 32 | 0.245833 | 113 | 3.98856e-09 | | 4.26 | 200 | 12 | 48.5 | 51 | 0.2425 | 196 | 2.86179e-14 | | 4.26 | 400 | 12 | 98 | 101 | 0.245 | 380.5 | 4.4781e-26 | The certificate grows roughly linearly in these random ensembles, but the certified ball remains an exponentially tiny fraction of the full cube when L/n < 1/2. So this is a genuine **local event jump**, not a global SAT algorithm. --- # 9. Clause-direct anchored polynomial compiler To ensure the anti-bias improvement was not merely post-hoc truth-table cosmetics, v0.28 compiles the SAT indicator **directly from clauses**. With y=x XOR a, each clause has an exact multilinear indicator and the compiler multiplies them in the Boolean quotient y_i^2=y_i over GF(257). No truth table is used in the production compilation. A hard term cap returns UNKNOWN rather than approximating. Small scaling under an n^4 term budget: | ratio | n | anchor | cases | completed | median_peak | max_peak | median_processed | median_clauses | completion_fraction | |--------:|----:|:---------|--------:|------------:|--------------:|-----------:|-------------------:|-----------------:|----------------------:| | 1.5 | 12 | antibias | 4 | 4 | 552 | 724 | 18 | 18 | 1 | | 1.5 | 12 | zero | 4 | 4 | 866 | 1274 | 18 | 18 | 1 | | 1.5 | 14 | antibias | 4 | 4 | 1623.5 | 2033 | 21 | 21 | 1 | | 1.5 | 14 | zero | 4 | 4 | 2718.5 | 3437 | 21 | 21 | 1 | | 1.5 | 16 | antibias | 3 | 3 | 5261 | 6191 | 24 | 24 | 1 | | 1.5 | 16 | zero | 3 | 3 | 6452 | 7256 | 24 | 24 | 1 | | 1.5 | 18 | antibias | 3 | 3 | 12051 | 12198 | 27 | 27 | 1 | | 1.5 | 18 | zero | 3 | 3 | 16898 | 25577 | 27 | 27 | 1 | | 2 | 12 | antibias | 4 | 4 | 536 | 785 | 24 | 24 | 1 | | 2 | 12 | zero | 4 | 4 | 1190 | 1965 | 24 | 24 | 1 | | 2 | 14 | antibias | 4 | 4 | 1371.5 | 1992 | 28 | 28 | 1 | | 2 | 14 | zero | 4 | 4 | 4575.5 | 5679 | 28 | 28 | 1 | | 2 | 16 | antibias | 3 | 3 | 3601 | 5163 | 32 | 32 | 1 | | 2 | 16 | zero | 3 | 3 | 10163 | 14724 | 32 | 32 | 1 | | 2 | 18 | antibias | 3 | 3 | 12100 | 23851 | 36 | 36 | 1 | | 2 | 18 | zero | 3 | 3 | 18904 | 45833 | 36 | 36 | 1 | | 4.26 | 12 | antibias | 4 | 4 | 530.5 | 680 | 51 | 51 | 1 | | 4.26 | 12 | zero | 4 | 4 | 740 | 990 | 51 | 51 | 1 | | 4.26 | 14 | antibias | 4 | 4 | 1670.5 | 2091 | 60 | 60 | 1 | | 4.26 | 14 | zero | 4 | 4 | 2799 | 3557 | 60 | 60 | 1 | | 4.26 | 16 | antibias | 3 | 3 | 4269 | 4725 | 68 | 68 | 1 | | 4.26 | 16 | zero | 3 | 3 | 9394 | 14194 | 68 | 68 | 1 | | 4.26 | 18 | antibias | 3 | 3 | 11348 | 21013 | 77 | 77 | 1 | | 4.26 | 18 | zero | 3 | 3 | 21419 | 26344 | 77 | 77 | 1 | Selected n=20 runs: | ratio | seed | anchor | status | peak_terms | processed | clauses | cap | seconds | |--------:|-------:|:---------|:---------|-------------:|------------:|----------:|-------:|----------:| | 2 | 0 | zero | SAT | 92890 | 40 | 40 | 160000 | 1.05973 | | 2 | 0 | antibias | SAT | 32808 | 40 | 40 | 160000 | 0.487047 | | 2 | 1 | zero | SAT | 21304 | 40 | 40 | 160000 | 0.219689 | | 2 | 1 | antibias | SAT | 22850 | 40 | 40 | 160000 | 0.321048 | | 4.26 | 0 | zero | SAT | 60222 | 85 | 85 | 160000 | 1.88777 | | 4.26 | 0 | antibias | SAT | 18234 | 85 | 85 | 160000 | 0.311796 | | 4.26 | 1 | zero | UNSAT | 48407 | 83 | 85 | 160000 | 1.04635 | | 4.26 | 1 | antibias | UNSAT | 23764 | 84 | 85 | 160000 | 0.509598 | The anti-bias origin often reduces actual live compilation size substantially. It still has no universal polynomial bound. --- # 10. Rigorous exponential counterexample to the anchored-polynomial language Consider the connected 3-CNF family F_m = AND_{i=1..m} NAE(z,x_i,y_i) with each NAE encoded as (z OR x_i OR y_i) AND (NOT z OR NOT x_i OR NOT y_i). There are n=2m+1 variables. Every variable has balanced positive/negative occurrence count, so the anti-bias tie rule chooses the zero anchor. Restrict z=0. Each relation becomes x_i OR y_i, whose multilinear polynomial is x_i + y_i - x_i y_i. The m variable pairs are disjoint, so product_i (x_i + y_i - x_i y_i) contains exactly 3^m distinct monomials with no z. No z-containing monomial can cancel one of them. Therefore the full anchored indicator has at least **3^m = 3^((n-1)/2)** nonzero monomials. This is a rigorous exponential lower bound for this representation on a connected 3-CNF family. Finite compiler check: | m | n | anchor | poly_terms | lower_bound_3m | ratio_to_lower | hybrid_status | hybrid_width | |----:|----:|---------:|-------------:|-----------------:|-----------------:|:----------------|---------------:| | 1 | 3 | 0 | 6 | 3 | 2 | SAT | 2 | | 2 | 5 | 0 | 20 | 9 | 2.22222 | SAT | 2 | | 3 | 7 | 0 | 60 | 27 | 2.22222 | SAT | 2 | | 4 | 9 | 0 | 176 | 81 | 2.17284 | SAT | 2 | | 5 | 11 | 0 | 516 | 243 | 2.12346 | SAT | 2 | | 6 | 13 | 0 | 1520 | 729 | 2.08505 | SAT | 2 | | 7 | 15 | 0 | 4500 | 2187 | 2.05761 | SAT | 2 | | 8 | 17 | 0 | 13376 | 6561 | 2.03871 | SAT | 2 | The same family has structural width 2 and is easy for the structural route. This is a central v0.28 lesson: > complexity can move between representations; a universal solver must switch > languages rather than assume one coordinate basis is globally compact. --- # 11. Generator market and obstruction search The exact generator market compares algebraic, structural, anchored-polynomial, frontier, residual, and small brute-oracle routes while keeping UNKNOWN first-class. Finite scheduled corpus summary: | family | cases | unknown_cases | disagreements | median_seconds | |:-----------|--------:|----------------:|----------------:|-----------------:| | 3color | 3 | 0 | 0 | 0.0158866 | | lowwidth | 1 | 0 | 0 | 1.05872 | | nae3 | 3 | 0 | 0 | 0.0281981 | | pigeonhole | 3 | 0 | 0 | 0.0105681 | | planted3 | 3 | 0 | 0 | 0.126714 | | random3 | 3 | 0 | 0 | 0.0969081 | | tseitin | 2 | 0 | 0 | 0.346539 | | xor3 | 2 | 0 | 0 | 0.0849889 | No disagreements were observed on that scheduled finite corpus, but this does **not** open the P=NP gate. A deliberate obstruction search asked for formulas where all primary configured generators return UNKNOWN: | n | cases | all_primary_unknown | unknown_fraction | median_seconds | |----:|--------:|----------------------:|-------------------:|-----------------:| | 24 | 6 | 0 | 0 | 0.0716062 | | 30 | 6 | 0 | 0 | 0.313166 | | 36 | 6 | 5 | 0.833333 | 0.69835 | | 40 | 6 | 6 | 1 | 0.870827 | At n=40 all 6/6 scanned cases produced an all-primary-UNKNOWN obstruction under the configured budgets. One n=40 obstruction snapshot had: | case | n | tick | live_frontier_states | syntactic_future_classes | future_variables | semantic_future_classes | syntax_to_semantic_ratio | frontier_to_semantic_ratio | largest_syntax_group_same_semantics | semantic_modelcount_classes | seconds | |:------------------|----:|-------:|-----------------------:|---------------------------:|-------------------:|--------------------------:|---------------------------:|-----------------------------:|--------------------------------------:|:--------------------------------------------|----------:| | hard40_seed282000 | 40 | 63 | 84394 | 38191 | 11 | 1 | 38191 | 84394 | 38191 | ((0, 38191),) | 0.132395 | | hard36_seed286600 | 36 | 23 | 9799 | 3258 | 18 | 5 | 651.6 | 1959.8 | 3251 | ((0, 3251), (1, 2), (2, 2), (3, 1), (3, 2)) | 0.690279 | The hard40 snapshot's 38,191 syntactic residuals were all the **same UNSAT semantic future** according to the exponential semantic oracle. Then the polynomial residual router classified all 38,191 of those residual descriptions: | case | n | syntactic_residuals | recognized | recognized_fraction | SAT | UNSAT | UNKNOWN | breakdown | seconds | |:------------------|----:|----------------------:|-------------:|----------------------:|------:|--------:|----------:|:----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|----------:| | hard40_seed282000 | 40 | 38191 | 38191 | 1 | 0 | 38191 | 0 | {('UNSAT', 'structural', 'low-width exact bucket elimination'): 29867, ('UNSAT', 'algebraic', '2-SAT/SCC'): 1, ('UNSAT', 'algebraic', 'GF(2)/rank'): 8323} | 17.654 | | hard36_seed286600 | 36 | 3258 | 1423 | 0.436771 | 7 | 1416 | 1835 | {('UNSAT', 'algebraic', 'GF(2)/rank'): 490, ('UNSAT', 'structural', 'low-width exact bucket elimination'): 925, ('UNKNOWN', 'unknown', 'uncompiled wide residual'): 1835, ('UNSAT', 'algebraic', '2-SAT/SCC'): 1, ('SAT', 'structural', 'low-width exact bucket elimination'): 7} | 7.7416 | This is tantalizing but not a proof: reaching/enumerating that snapshot had already generated many histories. The missing algorithm is a polynomial path to the semantic certificate *before* that population explosion. --- # 12. Counterexample minimization hardens the proof gate A 170-clause all-primary-UNKNOWN formula was greedily minimized while preserving that property. Result: original clauses = 170 minimized clauses = 30 all primary generators UNKNOWN = True measured structural width = 9 The minimized formula sat just beyond the configured width-8 structural budget. When that single budget was raised to 9: status = SAT time = 0.002519 s. An exact residual solver with a larger state cap also solved it with model count 16,900,632,960 and peak residual state count 4,948. This is exactly why a counterexample to a **budget** is not a complexity lower bound. The adversarial lab records both. --- # 13. Complexity ledger Route-local representation sizes are tracked separately: | case | family | variables | clauses | input_description_bits | winner | algebraic-router | hybrid-width8 | semantic-residual-lite | sparse-frontier | |:---------------|:-----------|------------:|----------:|-------------------------:|:-----------------------|-------------------:|----------------:|-------------------------:|------------------:| | lowwidth:100:1 | lowwidth | 100 | 185 | 4817 | hybrid-width8 | nan | 32 | 4096 | 976 | | pigeonhole:6:1 | pigeonhole | 30 | 141 | 2087 | algebraic-router | 11 | 11 | 20 | 522 | | random3:30:1 | random3 | 30 | 128 | 2565 | semantic-residual-lite | nan | nan | 1468 | 7873 | | xor3:40:1 | xor3 | 40 | 128 | 2950 | hybrid-width8 | 36 | 36 | 512 | 56 | Counts such as "GF(2) features", "frontier states", and "factor table cells" are not automatically comparable units. v0.28 therefore forbids selecting a universal complexity winner by comparing arbitrary route-local proxy numbers. --- # 14. Current P=NP proof gate The gate remains CLOSED. What is missing is a fixed polynomial-time semantic promotion rule Q such that for every CNF F: F -> Q(F) and throughout the entire computation: - every representation has polynomial description size; - every transform/promotion is polynomial-time; - every event/collapse is exact; - no branch tree of exponential depth/width is required; - no exponential truth table/advice/precomputation is hidden; - SAT/nonemptiness of the final representation is polynomial-time. The strongest v0.28 positive ingredients are: 1. exact algebra/structure routing; 2. deep-anchor dead-radius certificates; 3. exact event-jump semantics; 4. anti-bias anchored compilation as a useful local coordinate choice; 5. semantic future collapse when a tractable certificate is found. The strongest negative results are: 1. proof-safe random 3-SAT remains UNKNOWN; 2. log-width elimination does not capture the random hard controls; 3. semantic future DAGs are not automatically tiny; 4. capture stores complexity in boundary width; 5. signed/complement merging did not help the tested corpus; 6. the anchored-polynomial representation has an explicit exponential connected family. That is the wall v0.29 must attack.