diff --git a/research/eight-source-lift-obstruction/OBSTRUCTION-RESULT.json b/research/eight-source-lift-obstruction/OBSTRUCTION-RESULT.json
new file mode 100644
index 0000000000..2de73c0a4f
--- /dev/null
+++ b/research/eight-source-lift-obstruction/OBSTRUCTION-RESULT.json
@@ -0,0 +1,74 @@
+{
+  "status": "PASS_PROJECTION_MATCHING_OBSTRUCTION",
+  "word": "341236425430103051216402",
+  "distinct_projected_states": 24,
+  "coverage": 128,
+  "unique_difference_matching": [
+    [
+      22,
+      24
+    ],
+    [
+      86,
+      30
+    ],
+    [
+      122,
+      70
+    ],
+    [
+      123,
+      0
+    ],
+    [
+      121,
+      66
+    ],
+    [
+      83,
+      113
+    ],
+    [
+      87,
+      98
+    ],
+    [
+      85,
+      8
+    ],
+    [
+      21,
+      81
+    ],
+    [
+      5,
+      26
+    ],
+    [
+      4,
+      114
+    ]
+  ],
+  "matching_size": 11,
+  "lifted_state_lower_bound": 35,
+  "minimum_vertex_cover_size": 11,
+  "closed_lift_word_length_lower_bound": 36,
+  "exhaustive_small_lift_subsets": 65805,
+  "universal_small_lifts": 41439,
+  "rejected_controls": 4,
+  "known_universal_upper_word": "01020103010201034546454745464547",
+  "nonuniversal_28_word": "5643251350361472024502071341",
+  "nonuniversal_28_missing_masks": [
+    19,
+    25,
+    27,
+    30,
+    51,
+    57,
+    59,
+    83,
+    89,
+    121
+  ],
+  "scope": "General written matching lemma and one fixed-projection exclusion; f(8) remains unresolved."
+}
diff --git a/research/eight-source-lift-obstruction/README.md b/research/eight-source-lift-obstruction/README.md
new file mode 100644
index 0000000000..009bc108a4
--- /dev/null
+++ b/research/eight-source-lift-obstruction/README.md
@@ -0,0 +1,205 @@
+# 八源 28 步问题：投影提升的匹配障碍（部分结果）
+
+## Reviewer summary (English)
+
+**Partial result; the eight-source 28-step question remains open. No new kappa.**
+This package proves a general projection obstruction and excludes one particular
+seven-source optimal projection. It does not exclude all 28-step words.
+
+For a nonempty projected set `Q`, let `G(Q)` have an edge `{u,v}` exactly when
+`u XOR v` has this unique unordered representation in `Q`. For a lift
+`P ⊆ Q × F₂` projecting onto `Q`, let `S` be the projected states whose fibers
+contain both layers. If `P + P` is the whole ambient space, `S` must cover every
+edge of `G(Q)`: otherwise the unique pair has only one layer parity and misses
+one of the two lifted differences. Hence
+`|P| = |Q| + |S| ≥ |Q| + τ(G(Q)) ≥ |Q| + ν(G(Q))`.
+This is a written proof for arbitrary dimension; the finite tests below are
+corroboration rather than its justification.
+
+For the 24-step seven-source word `341236425430103051216402`, all 24 prefix
+states are distinct and their differences cover `F₂⁷`. An explicit matching of
+11 unique-difference edges and a vertex cover of size 11 certify `τ = ν = 11`.
+Every universal lift with exactly this projected state set therefore needs at
+least 35 distinct states, or at least 36 steps for a closed singleton path.
+**The 36-step lower bound is conditional on this fixed projection, not a global
+bound on f(8), and attainability at 36 is not asserted.**
+
+The checker also verifies an exact static lift criterion against direct XOR
+enumeration on all 65,805 nonempty sets in dimensions 2–4, checks the known
+32-step Gray upper construction, and rejects four false controls. In particular,
+revisited projections invalidate the tempting general bound that the number of
+double-layer states is at most the number of new-coordinate calls.
+
+The exploratory logs are incomplete searches. The 28-step SMT run returned
+`unknown` after its timeout, not `unsat`. Normal and optimized standard-library
+checks reproduce `OBSTRUCTION-RESULT.json`; commands are in section 6.
+The detailed proof, certificates, attribution and limitations follow below.
+
+状态：**原问题尚未解决**。本轮得到一个一般必要条件、一个完整的固定投影排除证明，以及可复现的精确检查。没有证明所有 28 步候选不存在，没有把随机搜索或求解器超时当成排除证据，也没有提高已知的 `28 <= f(8) <= 32`。
+
+Prepared for Nicholas Stone with substantial OpenAI Codex assistance, 2026-10-24, Asia/Shanghai. New text/code: Apache-2.0. No independent human or proof-kernel review, and no historical novelty claim.
+
+## 1. 问题及已知前提
+
+在八维二进制空间中，从零开始，每一步翻转一个坐标，最终返回零。记长度为 L 的单坐标序列为 w，终点前的前缀状态集合为 P。通用性条件为
+
+\[
+P+P=\mathbb F_2^8.
+\]
+
+这里加法就是 XOR。源码与贡献背景见 [PR5234](https://github.com/CrocSwap/integer-mult-bounds/pull/5234) 和 [PR3058](https://github.com/CrocSwap/integer-mult-bounds/pull/3058)。本轮以 canonical main `1a3ced60b2f7a46bc70280a04f2eeb8ca027c700` 为来源；对应 README 路径为 `research/eight-source-singleton-floor/README.md` 和 `research/connector-covering-code/README.md`。
+
+conorholds 的 PR3058 证明 f(7)=24；本轮引用这一结果，没有重新运行其中排除较短序列的完整计算证明，也不将其视为所有最优 24 步序列的分类。Nick Petalas 的 PR5234 通过逐坐标删除推出 L>=28，并证明 28 步候选的次数只能是 `(4,4,4,4,4,4,2,2)`，允许重新编号。这些是前序结果，不是本轮贡献。Ross Richardson/PR943 的模型、Douglas Colkitt/PR1185 的 Gray 构造及原有贡献者保留署名。
+
+因此，28 步候选删去任一出现四次的坐标后，都会得到一个通用的七源 24 步序列。但其不同前缀状态数不一定是 24，不能未经证明就假定投影是简单环。
+
+## 2. 一般匹配障碍：完整证明
+
+设 Q 是 \(\mathbb F_2^n\) 的一个非空子集。对每个非零差值 d，记其无序表示集合
+
+\[
+R_d=\{\{u,v\}\subseteq Q:u\ne v,\ u+v=d\}.
+\]
+
+定义图 G(Q)：顶点是 Q；若 \(R_{u+v}=\{\{u,v\}\}\)，就在 u、v 之间连边。也就是说，边的差值在 Q 中只有这一种无序表示。
+
+考虑任意投影恰好等于 Q 的提升 \(P\subseteq Q\times\mathbb F_2\)。定义双层状态集合
+
+\[
+S=\{q\in Q:(q,0)\in P\text{ 且 }(q,1)\in P\}.
+\]
+
+**引理。** 如果 \(P+P=\mathbb F_2^{n+1}\)，则 S 是 G(Q) 的顶点覆盖。因而
+
+\[
+|P|=|Q|+|S|\ \ge\ |Q|+\tau(G(Q))\ \ge\ |Q|+\nu(G(Q)),
+\]
+
+其中 τ 是最小顶点覆盖大小，ν 是最大匹配大小。无需假定 G(Q) 是二分图。
+
+**证明。** 取 G(Q) 的任意一条边 {u,v}，令 d=u+v。由于其无序表示唯一，P 中产生差值 `(d,0)` 或 `(d,1)` 的点对，其投影只能是 u、v。若 u、v 均不属于 S，那么它们各只有一个提升，设为 `(u,a)`、`(v,b)`，因此只能产生 `(d,a+b)`，缺少另一个提升差值。这与通用性矛盾，所以至少一个端点属于 S。每条边均如此，S 必须是顶点覆盖。每个 q 的非空纤维有一个或两个点，故 `|P|=|Q|+|S|`。匹配的边两两不共顶点，每条边都需要一个覆盖顶点，故任何匹配大小都是 |S| 的下界。证毕。
+
+**对本题的后果。** 假定存在一个 28 步解。对六个出现四次的坐标 j，分别删除 j，得到投影集合 Q_j；每一个都必须满足
+
+\[
+|Q_j|+\nu(G(Q_j))\le 28.
+\]
+
+例如，若某个 Q_j 有 24 个不同状态，而且可以给出五条互不相交的唯一差值边，那么该候选立即被排除。对于只有 23 个不同状态的投影，需要六条这样的边；对于 22 个状态，需要七条。只找到一个违反条件的坐标就足够。
+
+这个条件只是必要条件。尚未证明所有七源 24 步投影都违反它，更没有证明存在满足它的实际 28 步闭合路径。
+
+## 3. 一个完整排除的七维最优投影
+
+本轮计算得到以下七源序列：
+
+```text
+341236425430103051216402
+```
+
+其长度为 24，坐标 0--4 各出现四次，5、6 各出现两次，终态为零。它有 24 个不同前缀状态，差集覆盖全部 128 个七位掩码。引用 f(7)=24，可以称它为七源最优序列。
+
+按访问顺序，其状态为
+
+```text
+0, 8, 24, 26, 30, 22, 86, 70, 66, 98, 114, 122,
+123, 121, 120, 112, 113, 81, 83, 87, 85, 21, 5, 4
+```
+
+下表是 11 条互不相交的唯一差值边。数字是二进制状态的十进制编码，不是序列位置。
+
+| u | v | u XOR v |
+|---:|---:|---:|
+|22|24|14|
+|86|30|72|
+|122|70|60|
+|123|0|123|
+|121|66|59|
+|83|113|34|
+|87|98|53|
+|85|8|93|
+|21|81|68|
+|5|26|31|
+|4|114|118|
+
+逐一枚举 Q 的全部 276 个无序点对，可以检查这些差值各自只有表中所列的一种表示，且 22 个端点互不相同。因此 ν>=11。
+
+另外，集合 `{24,26,66,81,83,85,86,87,70,114,123}` 覆盖 G(Q) 的全部边。因此 τ=ν=11；这里两个方向都有显式证书，不依赖通用顶点覆盖求解器。
+
+由引理，任何具有这个**固定投影集合**的八维通用状态集，都至少需要 `24+11=35` 个不同状态。长度 L 的闭合路径至多有 L 个不同前缀状态，而闭合单坐标路径的长度为偶数，因此
+
+\[
+L\ge36.
+\]
+
+特别地，在上述七源序列中任意插入四次新坐标调用，都不可能得到八源 28 步解。这里的 36 是固定投影条件下的下界，不是 f(8) 的下界，也没有宣称 36 可达。
+
+## 4. 精确的静态提升判据
+
+匹配条件还可补充为一个精确的集合层面判据。对每个不在 S 中的 q，令 c(q) 为其唯一提升的最后一位。
+
+P 通用当且仅当：
+
+1. S 非空，从而能产生纯新坐标差值 `(0,1)`；
+2. 对每个非零 d，以下至少一项成立：R_d 中有一对触及 S；或者所有表示都不触及 S，但这些表示的 `c(u) XOR c(v)` 同时取到 0 和 1。
+
+理由是逐个检查 `(d,0)` 与 `(d,1)`：触及双层状态的一对自动产生两种；否则只能由单层端点的颜色奇偶决定。零差值 `(0,0)` 自动存在。
+
+这是对固定提升集合 P 的充要条件，不是长度为 28 的路径可实现性条件。即使颜色分配满足它，仍须证明状态能按所需单坐标次数和闭合顺序访问。
+
+## 5. 必须保留的重复状态边界
+
+不能一般地说“双层状态数不超过新坐标调用次数”。反例是三维闭合序列
+
+```text
+2010120101
+```
+
+新坐标 2 只调用两次，但删除它后的投影重复遍历二维方块；四个投影状态全部在两层出现，故 |S|=4。它实际上访问全部八个三维状态。
+
+始终成立的是 `|S|=|P|-|Q|<=L-|Q|`。只有投影具有 24 个不同状态且 L=28 时，才能推出 |S|<=4。验证程序专门拒绝错误的通用上界。
+
+## 6. 验证与搜索结果
+
+必要条件的普遍性来自第 2 节证明。有限计算的用途是核对证书、判据实现以及失败边界。
+
+```sh
+python3 -I -W error -B research/eight-source-lift-obstruction/verify_obstruction.py
+python3 -I -O -W error -B research/eight-source-lift-obstruction/verify_obstruction.py
+```
+
+标准库即可。本轮 CPython 3.12.14 普通/优化执行输出一致，记录在 `OBSTRUCTION-RESULT.json`：
+
+- 检查七源序列、全部 276 对状态、11 边匹配及 11 顶点覆盖证书。
+- 枚举提升后维数为 2、3、4 的全部 65,805 个非空状态子集；其中 41,439 个通用。静态提升判据与直接差集枚举完全一致，所有通用实例都满足唯一差值边覆盖条件。
+- 复核已知的 32 步 Gray 上界构造。
+- 使用单独的连续区间 XOR 枚举，交叉核对一个 28 步搜索样本的差集；它只覆盖 246 个掩码，明确不是解。
+- 四个错误控制全部被拒绝，包括非唯一差值、重复匹配端点、无效端点以及错误的双层状态上界。
+
+`experiments/` 保存探索代码和日志，均不作为完整排除证书：
+
+- 28 步交换退火约 8,985 万次候选评估，最好覆盖 246/256；评估不保证互异。
+- 对 4,965 个采样得到的七源通用序列枚举四次新调用插入方式，评估 87,135,750 个提升，最好覆盖 242/256。七源父序列并未穷尽，也未去重，不能排除全部 28 步解。
+- 完整 28 步 SMT 模型在 180 秒后返回 `unknown`，原因为超时，不能记为 UNSAT。使用 Z3 5.3.1，仅探索脚本需要此依赖；把 z3-solver 安装到脚本旁的 `deps/` 即可复跑。
+- 附加的四种 30 步次数形状的启发式探测，以及对覆盖 255/256 的两个样本的局部改进，均未找到通用序列。这也不排除 30 步解。
+
+探索程序用固定随机种子、墙钟停止条件，所以不同机器的评估数量和最佳结果可能不同。数学证书和标准库验证程序不依赖这些随机结果。未运行全域穷举、独立求解器 UNSAT 证书检查、完整七源最优解分类或形式化证明。
+
+## 7. Open next questions / 精确剩余任务与接续方式
+
+目前仍只有已知界 `28 <= f(8) <= 32`。下一步要回答的是：是否存在一个可实现的七源 24 步投影，其唯一差值图允许足够小的顶点覆盖，并且四次新坐标切换能满足第 4 节的所有颜色条件？
+
+完整排除可以走两条路线：证明所有实际七源 24 步投影必有 `|Q|+τ(G(Q))>28`；或者保留满足这一必要条件的投影，再对四次切换位置作完整、带证书的剩余搜索。前一命题尚未建立，也可能过强；不能将它作为已证剪枝。匹配筛选失败只表示未排除，不表示存在合法提升。
+
+**Open next question:** Can all realizable seven-source 24-step projections be
+excluded by the matching/cover bound, or can any surviving projection support a
+28-step lift? This decides the next obstruction needed to settle the 28-step
+case. A feasible first step is to enumerate canonical seven-source parents,
+retain the full projected state sets (including repeated visits), and certify
+matching witnesses before exhaustively checking insertion positions. The blocker
+is the missing complete parent enumeration or a uniform theorem replacing it.
+Static color feasibility alone does not establish chronological path feasibility.
+
+This submission is an isolated partial research result. The earlier projection
+recurrence PR5416 concerns a different question. No selected result, frozen
+predecessor, shared checker or production code is changed.
diff --git a/research/eight-source-lift-obstruction/experiments/lift.cpp b/research/eight-source-lift-obstruction/experiments/lift.cpp
new file mode 100644
index 0000000000..5c37f2bf45
--- /dev/null
+++ b/research/eight-source-lift-obstruction/experiments/lift.cpp
@@ -0,0 +1,24 @@
+#define main anneal_main
+#include "search.cpp"
+#undef main
+int main(){
+ mt19937_64 rng(150725); vector<int>w; for(int i=0;i<7;i++)for(int j=0;j<(i<5?4:2);j++)w.push_back(i);
+ auto st=chrono::steady_clock::now(); int best=0,parents=0;long long lifts=0;
+ while(chrono::duration<double>(chrono::steady_clock::now()-st).count()<90){
+  shuffle(w.begin(),w.end(),rng);int cur=coverage(w);
+  for(int t=0;t<40000;t++){
+   int a=rng()%24,b=rng()%24;swap(w[a],w[b]);int c=coverage(w);double T=.1+2*pow(1-t/40000.,2);
+   if(c>=cur||generate_canonical<double,53>(rng)<exp((c-cur)/T))cur=c;else swap(w[a],w[b]);
+   if(cur!=128)continue;
+   parents++;
+   for(int a=0;a<24;a++)for(int b=a;b<24;b++)for(int c=b;c<24;c++)for(int d=c;d<24;d++){
+    vector<int>v;for(int i=0;i<24;i++){for(int x:{a,b,c,d})if(x==i)v.push_back(7);v.push_back(w[i]);}
+    int cov=coverage(v);lifts++;
+    if(cov>best){best=cov;cout<<"best "<<best<<" parents "<<parents<<" lifts "<<lifts<<" word ";for(int x:v)cout<<x;cout<<endl;}
+    if(cov==256)return 0;
+   }
+   break;
+  }
+ }
+ cout<<"INCOMPLETE sampled parents "<<parents<<" lifts "<<lifts<<" best "<<best<<endl;
+}
diff --git a/research/eight-source-lift-obstruction/experiments/lift.log b/research/eight-source-lift-obstruction/experiments/lift.log
new file mode 100644
index 0000000000..5d14c42e04
--- /dev/null
+++ b/research/eight-source-lift-obstruction/experiments/lift.log
@@ -0,0 +1,37 @@
+best 152 parents 1 lifts 1 word 7777216351340643521034012024
+best 166 parents 1 lifts 2 word 7772716351340643521034012024
+best 171 parents 1 lifts 3 word 7772176351340643521034012024
+best 182 parents 1 lifts 4 word 7772167351340643521034012024
+best 184 parents 1 lifts 5 word 7772163751340643521034012024
+best 187 parents 1 lifts 8 word 7772163513740643521034012024
+best 189 parents 1 lifts 12 word 7772163513406473521034012024
+best 190 parents 1 lifts 16 word 7772163513406435217034012024
+best 195 parents 1 lifts 17 word 7772163513406435210734012024
+best 196 parents 1 lifts 39 word 7727163513406435217034012024
+best 200 parents 1 lifts 40 word 7727163513406435210734012024
+best 201 parents 1 lifts 74 word 7721673513740643521034012024
+best 204 parents 1 lifts 82 word 7721673513406435217034012024
+best 206 parents 1 lifts 83 word 7721673513406435210734012024
+best 209 parents 1 lifts 85 word 7721673513406435210347012024
+best 211 parents 1 lifts 350 word 7271673513740643521034012024
+best 213 parents 1 lifts 357 word 7271673513406435271034012024
+best 216 parents 1 lifts 358 word 7271673513406435217034012024
+best 218 parents 1 lifts 359 word 7271673513406435210734012024
+best 219 parents 1 lifts 361 word 7271673513406435210347012024
+best 221 parents 1 lifts 612 word 7217673513406435210734012024
+best 222 parents 1 lifts 614 word 7217673513406435210347012024
+best 223 parents 1 lifts 634 word 7217637513406435210347012024
+best 226 parents 1 lifts 863 word 7216737513406435210734012024
+best 228 parents 1 lifts 5305 word 2176735134064735210340120724
+best 229 parents 1 lifts 5515 word 2176375134064735210340120724
+best 230 parents 1 lifts 7285 word 2167375134064735210340127024
+best 231 parents 1 lifts 7286 word 2167375134064735210340120724
+best 232 parents 3 lifts 43104 word 4137253467432010520127461730
+best 234 parents 5 lifts 72668 word 7604305232643215701417207314
+best 236 parents 18 lifts 311878 word 3240142715030642731727630154
+best 237 parents 154 lifts 2688614 word 4746074502172304321316120753
+best 239 parents 154 lifts 2688691 word 4746074502123043217316120753
+best 240 parents 1426 lifts 25013236 word 4745301341237514760207120263
+best 241 parents 1967 lifts 34508061 word 4704502134212563731073761402
+best 242 parents 3092 lifts 54250857 word 0740251763714513420264732013
+INCOMPLETE sampled parents 4965 lifts 87135750 best 242
diff --git a/research/eight-source-lift-obstruction/experiments/refine30.cpp b/research/eight-source-lift-obstruction/experiments/refine30.cpp
new file mode 100644
index 0000000000..ddb7af9195
--- /dev/null
+++ b/research/eight-source-lift-obstruction/experiments/refine30.cpp
@@ -0,0 +1,21 @@
+#define main anneal_main
+#include "search.cpp"
+#undef main
+int main(){
+ vector<string>seeds={"404623713412310507205215604053","035420602417513104317142306021"};
+ mt19937_64 rng(77202);long long trials=0;int best=255;auto st=chrono::steady_clock::now();
+ while(chrono::duration<double>(chrono::steady_clock::now()-st).count()<90){
+  vector<int>w;for(char c:seeds[rng()%seeds.size()])w.push_back(c-'0');int cur=coverage(w);
+  for(int t=0;t<100000;t++){
+   auto v=w;int a=rng()%30,b=rng()%30;if(a>b)swap(a,b);
+   int move=rng()%3;
+   if(move==0)swap(v[a],v[b]);
+   else if(move==1)reverse(v.begin()+a,v.begin()+b+1);
+   else rotate(v.begin()+a,v.begin()+a+1,v.begin()+b+1);
+   int c=coverage(v);double T=.15+.8*pow(1-t/100000.,2);trials++;
+   if(c>=cur||generate_canonical<double,53>(rng)<exp((c-cur)/T)){w=v;cur=c;}
+   if(cur==256){cout<<"WITNESS trials "<<trials<<" word ";for(int a:w)cout<<a;cout<<endl;return 0;}
+  }
+ }
+ cout<<"INCOMPLETE trials "<<trials<<" no witness"<<endl;
+}
diff --git a/research/eight-source-lift-obstruction/experiments/refine30.log b/research/eight-source-lift-obstruction/experiments/refine30.log
new file mode 100644
index 0000000000..8a8683e12b
--- /dev/null
+++ b/research/eight-source-lift-obstruction/experiments/refine30.log
@@ -0,0 +1 @@
+INCOMPLETE trials 96800000 no witness
diff --git a/research/eight-source-lift-obstruction/experiments/search.cpp b/research/eight-source-lift-obstruction/experiments/search.cpp
new file mode 100644
index 0000000000..d3bbc1ed33
--- /dev/null
+++ b/research/eight-source-lift-obstruction/experiments/search.cpp
@@ -0,0 +1,31 @@
+#include <algorithm>
+#include <array>
+#include <chrono>
+#include <cmath>
+#include <iostream>
+#include <random>
+#include <vector>
+using namespace std;
+int coverage(const vector<int>& w){
+ unsigned long long seen[4]={1,0,0,0}; int p[32],q=0;
+ for(int i=0;i<(int)w.size();i++){p[i]=q;q^=1<<w[i];}
+ for(int i=0;i<(int)w.size();i++)for(int j=0;j<i;j++){int x=p[i]^p[j];seen[x>>6]|=1ULL<<(x&63);}
+ return __builtin_popcountll(seen[0])+__builtin_popcountll(seen[1])+__builtin_popcountll(seen[2])+__builtin_popcountll(seen[3]);
+}
+int main(int argc,char**argv){
+ int seconds=argc>1?atoi(argv[1]):30; int dim=argc>2?atoi(argv[2]):8; int len=4*dim-4; mt19937_64 rng(20261024); vector<int>w;
+ for(int i=0;i<dim;i++)for(int j=0;j<(i<dim-2?4:2);j++)w.push_back(i);
+ auto start=chrono::steady_clock::now();int best=0;long long n=0; vector<int>bw;
+ while(chrono::duration<double>(chrono::steady_clock::now()-start).count()<seconds){
+  shuffle(w.begin(),w.end(),rng);int cur=coverage(w);
+  for(int t=0;t<20000;t++){
+   int a=rng()%len,b=rng()%len;if(w[a]==w[b])continue;
+   swap(w[a],w[b]);int c=coverage(w);double temp=0.15+2.5*pow(1-t/20000.0,2);
+   if(c>=cur||generate_canonical<double,53>(rng)<exp((c-cur)/temp))cur=c;else swap(w[a],w[b]);n++;
+   if(cur>best){best=cur;bw=w;cout<<"best "<<best<<" trials "<<n<<" word ";for(int v:bw)cout<<v;cout<<endl;}
+   if(best==(1<<dim))return 0;
+  }
+ }
+ cout<<"INCOMPLETE heuristic only trials "<<n<<" best "<<best<<endl;
+ return 0;
+}
diff --git a/research/eight-source-lift-obstruction/experiments/search.log b/research/eight-source-lift-obstruction/experiments/search.log
new file mode 100644
index 0000000000..ade7dac669
--- /dev/null
+++ b/research/eight-source-lift-obstruction/experiments/search.log
@@ -0,0 +1,22 @@
+best 194 trials 1 word 3142310521702316424505603457
+best 199 trials 2 word 3142310521705316424502603457
+best 201 trials 4 word 3142360521705316424502103457
+best 210 trials 14 word 3142360501705216424532103457
+best 211 trials 49 word 3742360410305216527542103451
+best 215 trials 63 word 4732560410305216327542103541
+best 218 trials 64 word 4732560430105216327542103541
+best 222 trials 88 word 4732065430105216327542103541
+best 223 trials 1626 word 4013520327560534257140214613
+best 226 trials 5306 word 3246230250545317414506172310
+best 228 trials 5560 word 3246203250545317414506172301
+best 230 trials 19954 word 4017351253613542302142570406
+best 231 trials 22532 word 5072052365304531642471314201
+best 233 trials 22612 word 1072052365304531642471314205
+best 235 trials 24638 word 1027025631430536452741312405
+best 236 trials 43665 word 7106454315456120307142302352
+best 237 trials 43820 word 7106454315456120307124302352
+best 239 trials 661788 word 2731052402651532156074341034
+best 241 trials 662687 word 2731052402651325156074314034
+best 242 trials 662700 word 2731052402615325156074314034
+best 246 trials 3842766 word 5643251350361472024502071341
+INCOMPLETE heuristic only trials 89853147 best 246
diff --git a/research/eight-source-lift-obstruction/experiments/search30-0.log b/research/eight-source-lift-obstruction/experiments/search30-0.log
new file mode 100644
index 0000000000..48277cad4d
--- /dev/null
+++ b/research/eight-source-lift-obstruction/experiments/search30-0.log
@@ -0,0 +1,23 @@
+best 214 trials 1 word 314231052160231642457560345607
+best 216 trials 18 word 314230154160231640457562326507
+best 218 trials 60 word 315263154103201602475464326507
+best 221 trials 66 word 315263154103201602473464526507
+best 225 trials 314 word 043241602031536421765014357265
+best 230 trials 336 word 043421602031532461765014357265
+best 231 trials 396 word 340421602031532461765014357265
+best 233 trials 1401 word 534501764365120421623063075241
+best 234 trials 1409 word 534501704365120421623603675241
+best 238 trials 1412 word 534501704365120321623640675241
+best 240 trials 1592 word 534501734365120321620460675241
+best 242 trials 1604 word 534501734365120321620460675214
+best 243 trials 6264 word 542625012031765614356703421403
+best 244 trials 9108 word 426524012460735314536716021530
+best 245 trials 9142 word 426254012460735314536716021530
+best 246 trials 9247 word 426524012460735314536716025130
+best 248 trials 77981 word 654652010245743140536372101263
+best 249 trials 165501 word 023632412636520174510454750613
+best 251 trials 270444 word 650124263421307565035647131204
+best 252 trials 271161 word 650124236421307565035647131204
+best 253 trials 1173523 word 653410142640104250673235632175
+best 254 trials 8214633 word 027426134267054312365051461503
+INCOMPLETE heuristic only trials 29299984 best 254
diff --git a/research/eight-source-lift-obstruction/experiments/search30-1.log b/research/eight-source-lift-obstruction/experiments/search30-1.log
new file mode 100644
index 0000000000..99778a3c51
--- /dev/null
+++ b/research/eight-source-lift-obstruction/experiments/search30-1.log
@@ -0,0 +1,27 @@
+best 203 trials 1 word 304121042160230531355470245607
+best 209 trials 7 word 304120140160230531355470245627
+best 217 trials 22 word 034102150160230531345470245627
+best 219 trials 33 word 534102150160230531345470240627
+best 220 trials 150 word 205134051263420401705310623547
+best 225 trials 193 word 205130454703256201204710613543
+best 227 trials 205 word 205130454703256207204110613543
+best 229 trials 478 word 250130407543265247151040120363
+best 231 trials 566 word 250130407543250246151740120363
+best 232 trials 1966 word 357501420615214304273540306021
+best 234 trials 2156 word 725010341630214035470542350621
+best 235 trials 2219 word 725010341630214035670542350412
+best 237 trials 3071 word 041201543072324123760501350546
+best 238 trials 3129 word 043203541271024123760501350546
+best 239 trials 3222 word 041203543270124321760501350564
+best 243 trials 3485 word 043520414762124321060503150573
+best 244 trials 4106 word 041502430763214232640501350571
+best 245 trials 41005 word 401207253065131431642507402305
+best 246 trials 41050 word 403207253065131431642507402105
+best 248 trials 43863 word 403207253065131431642504702105
+best 249 trials 109780 word 453403160103201067252415357042
+best 251 trials 111596 word 453403160102301067251345250742
+best 252 trials 127839 word 434204360750512050713015423261
+best 253 trials 129823 word 434204360750521050710315423261
+best 254 trials 753891 word 437030240307102512165453145260
+best 255 trials 11457379 word 404623713412310507205215604053
+INCOMPLETE heuristic only trials 14036146 best 255
diff --git a/research/eight-source-lift-obstruction/experiments/search30-2.log b/research/eight-source-lift-obstruction/experiments/search30-2.log
new file mode 100644
index 0000000000..1e4c8a261a
--- /dev/null
+++ b/research/eight-source-lift-obstruction/experiments/search30-2.log
@@ -0,0 +1,24 @@
+best 199 trials 1 word 203121041160120531347450234607
+best 204 trials 4 word 203121041160140531347450232607
+best 208 trials 45 word 243121051470140501673430232610
+best 210 trials 79 word 243412051070140501673431232610
+best 211 trials 98 word 243012050170140501673431232614
+best 214 trials 109 word 243012050170140501613431232674
+best 215 trials 119 word 241032050170141501613430232674
+best 216 trials 120 word 214032050170141501613430232674
+best 217 trials 123 word 214032050170141510613430232674
+best 221 trials 150 word 214031450270102510613430236714
+best 223 trials 347 word 612340530741342410621025130107
+best 225 trials 403 word 600342031721345210641045132170
+best 226 trials 657 word 130162437015234012046514010327
+best 232 trials 1652 word 651014273413612043215040701302
+best 234 trials 4086 word 141623015724134024053036017102
+best 243 trials 4259 word 141603015724134024503063217012
+best 244 trials 4600 word 143603015724134024503061210712
+best 247 trials 4838 word 143603051724134024503016210712
+best 249 trials 129026 word 030603052301761412041472132451
+best 252 trials 130080 word 030703052301761412041462312415
+best 253 trials 535126 word 046040721513124313052610230174
+best 254 trials 2382137 word 632012342070405040714613152131
+best 255 trials 10406196 word 035420602417513104317142306021
+INCOMPLETE heuristic only trials 29899998 best 255
diff --git a/research/eight-source-lift-obstruction/experiments/search30-3.log b/research/eight-source-lift-obstruction/experiments/search30-3.log
new file mode 100644
index 0000000000..e3cdd75bb2
--- /dev/null
+++ b/research/eight-source-lift-obstruction/experiments/search30-3.log
@@ -0,0 +1,23 @@
+best 192 trials 1 word 203121031160120521245370234607
+best 193 trials 41 word 203120101260120510245371234637
+best 215 trials 58 word 103150201260120510242371234637
+best 216 trials 115 word 123010501214023260242071351637
+best 220 trials 131 word 123010051241023260243071351267
+best 222 trials 153 word 123010250241023160243071351267
+best 224 trials 162 word 123014250201023160243071351267
+best 225 trials 515 word 130152317321060312140260502427
+best 229 trials 673 word 130152317301261032140260502427
+best 230 trials 1266 word 412506010720163203470312512132
+best 232 trials 4201 word 402370351214210252160321070316
+best 235 trials 4275 word 402370351214210252160123070316
+best 236 trials 6146 word 042130751214213510260320723016
+best 238 trials 6954 word 410230751216312501240230731026
+best 239 trials 7038 word 410230751216312501340320721026
+best 240 trials 7294 word 610320751316312501240320720124
+best 241 trials 8544 word 160320751316312501243012072024
+best 242 trials 14178 word 161230751306315210243020721024
+best 243 trials 28256 word 732104132601305423267120150210
+best 245 trials 78216 word 216027030251420123615030713241
+best 246 trials 157980 word 630214071021652324230521307101
+best 247 trials 1837219 word 304201713210513403016252127260
+INCOMPLETE heuristic only trials 28324407 best 247
diff --git a/research/eight-source-lift-obstruction/experiments/search30.cpp b/research/eight-source-lift-obstruction/experiments/search30.cpp
new file mode 100644
index 0000000000..6d71f2e752
--- /dev/null
+++ b/research/eight-source-lift-obstruction/experiments/search30.cpp
@@ -0,0 +1,32 @@
+#include <algorithm>
+#include <array>
+#include <chrono>
+#include <cmath>
+#include <iostream>
+#include <random>
+#include <vector>
+using namespace std;
+int coverage(const vector<int>& w){
+ unsigned long long seen[4]={1,0,0,0}; int p[32],q=0;
+ for(int i=0;i<(int)w.size();i++){p[i]=q;q^=1<<w[i];}
+ for(int i=0;i<(int)w.size();i++)for(int j=0;j<i;j++){int x=p[i]^p[j];seen[x>>6]|=1ULL<<(x&63);}
+ return __builtin_popcountll(seen[0])+__builtin_popcountll(seen[1])+__builtin_popcountll(seen[2])+__builtin_popcountll(seen[3]);
+}
+int main(int argc,char**argv){
+ int seconds=argc>1?atoi(argv[1]):30; int dim=argc>2?atoi(argv[2]):8; int len=4*dim-4; int pattern=argc>3?atoi(argv[3]):-1; mt19937_64 rng(20261024); vector<int>w;
+ for(int i=0;i<dim;i++)for(int j=0;j<(i<dim-2?4:2);j++)w.push_back(i);
+ if(pattern>=0){w.clear();for(int i=0;i<8;i++){int c=i<pattern?6:(i<7-pattern?4:2);for(int j=0;j<c;j++)w.push_back(i);}len=w.size();}
+ auto start=chrono::steady_clock::now();int best=0;long long n=0; vector<int>bw;
+ while(chrono::duration<double>(chrono::steady_clock::now()-start).count()<seconds){
+  shuffle(w.begin(),w.end(),rng);int cur=coverage(w);
+  for(int t=0;t<20000;t++){
+   int a=rng()%len,b=rng()%len;if(w[a]==w[b])continue;
+   swap(w[a],w[b]);int c=coverage(w);double temp=0.15+2.5*pow(1-t/20000.0,2);
+   if(c>=cur||generate_canonical<double,53>(rng)<exp((c-cur)/temp))cur=c;else swap(w[a],w[b]);n++;
+   if(cur>best){best=cur;bw=w;cout<<"best "<<best<<" trials "<<n<<" word ";for(int v:bw)cout<<v;cout<<endl;}
+   if(best==(1<<dim))return 0;
+  }
+ }
+ cout<<"INCOMPLETE heuristic only trials "<<n<<" best "<<best<<endl;
+ return 0;
+}
diff --git a/research/eight-source-lift-obstruction/experiments/search7.log b/research/eight-source-lift-obstruction/experiments/search7.log
new file mode 100644
index 0000000000..7f05b2377d
--- /dev/null
+++ b/research/eight-source-lift-obstruction/experiments/search7.log
@@ -0,0 +1,7 @@
+best 110 trials 1 word 314213052160231342460540
+best 115 trials 2 word 314213052160235342460140
+best 120 trials 5 word 314213052160235342460410
+best 122 trials 27 word 314213052264135432064010
+best 125 trials 484 word 414205314032620130543216
+best 127 trials 1179 word 210463205130261034214345
+best 128 trials 13228 word 341236425430103051216402
diff --git a/research/eight-source-lift-obstruction/experiments/smt.log b/research/eight-source-lift-obstruction/experiments/smt.log
new file mode 100644
index 0000000000..938c8d5289
--- /dev/null
+++ b/research/eight-source-lift-obstruction/experiments/smt.log
@@ -0,0 +1,2 @@
+built
+{"status": "unknown", "seconds": 180.0163176609999, "version": "5.3.1", "reason": "timeout"}
diff --git a/research/eight-source-lift-obstruction/experiments/smt.py b/research/eight-source-lift-obstruction/experiments/smt.py
new file mode 100644
index 0000000000..c24ae552a1
--- /dev/null
+++ b/research/eight-source-lift-obstruction/experiments/smt.py
@@ -0,0 +1,24 @@
+import sys,json,time
+sys.path.insert(0,str(__import__('pathlib').Path(__file__).parent/'deps'))
+import z3
+n=8;L=28
+s=z3.Solver();s.set(timeout=180000)
+q=[z3.BitVec('q'+str(i),n) for i in range(L)]+[z3.BitVecVal(0,n)]
+s.add(q[0]==0)
+edges=[[q[t]^q[t+1]==(1<<j) for j in range(n)] for t in range(L)]
+for es in edges:s.add(z3.Or(es))
+for j in range(n):s.add(z3.PbEq([(edges[t][j],1) for t in range(L)],4 if j<6 else 2))
+# Rotate to an occurrence of the distinguished twice-used coordinate 6.
+s.add(edges[0][6])
+# Six frequent coordinates can be renamed by first occurrence.
+for j in range(1,6):
+ for t in range(L):s.add(z3.Implies(edges[t][j],z3.Or([edges[k][j-1] for k in range(t)])))
+for d in range(1,1<<n):
+ s.add(z3.Or([q[i]^q[j]==d for i in range(L) for j in range(i) if ((i-j)&1)==(d.bit_count()&1)]))
+print('built',flush=True);start=time.monotonic();r=s.check()
+out={'status':str(r),'seconds':time.monotonic()-start,'version':z3.get_version_string()}
+if r==z3.sat:
+ m=s.model();states=[m.eval(x).as_long() for x in q[:-1]]+[0]
+ out['word']=[(states[t]^states[t+1]).bit_length()-1 for t in range(L)]
+else:out['reason']=s.reason_unknown() if r==z3.unknown else 'UNSAT in solver; independent proof certificate not checked'
+print(json.dumps(out),flush=True)
diff --git a/research/eight-source-lift-obstruction/verify_obstruction.py b/research/eight-source-lift-obstruction/verify_obstruction.py
new file mode 100644
index 0000000000..b057d8f1e4
--- /dev/null
+++ b/research/eight-source-lift-obstruction/verify_obstruction.py
@@ -0,0 +1,132 @@
+"""Exact corroboration of a projection matching obstruction, stdlib only."""
+from collections import Counter, defaultdict
+from itertools import combinations
+import json
+
+WORD = '341236425430103051216402'
+MATCHING = [(22,24),(86,30),(122,70),(123,0),(121,66),(83,113),
+            (87,98),(85,8),(21,81),(5,26),(4,114)]
+VERTEX_COVER = {24,26,66,81,83,85,86,87,70,114,123}
+
+def need(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+def prefixes(word):
+    out=[]; q=0
+    for a in word:
+        out.append(q); q ^= 1 << int(a)
+    need(q == 0, 'word must restore')
+    return out
+
+def differences(points):
+    return {a ^ b for a in points for b in points}
+
+def representations(points):
+    r=defaultdict(list)
+    for a,b in combinations(sorted(points),2):
+        r[a ^ b].append((a,b))
+    return r
+
+def check_matching(points, matching):
+    r=representations(points); used=set()
+    for a,b in matching:
+        need(a in points and b in points and a!=b,'invalid endpoint')
+        need(a not in used and b not in used,'not a matching')
+        need(r[a ^ b] == [tuple(sorted((a,b)))], 'difference is not unique')
+        used.update((a,b))
+    return len(matching)
+
+def lift_criterion(P,n):
+    mask=(1<<n)-1
+    Q={x & mask for x in P}
+    S={q for q in Q if q in P and q+(1<<n) in P}
+    need(len(P)==len(Q)+len(S),'fiber cardinality')
+    if not S:
+        return False,Q,S
+    R=representations(Q)
+    for d in range(1,1<<n):
+        pairs=R[d]
+        if any(a in S or b in S for a,b in pairs):
+            continue
+        colors={((0 if a in P else 1) ^ (0 if b in P else 1)) for a,b in pairs}
+        if colors!={0,1}:
+            return False,Q,S
+    return True,Q,S
+
+def rejected(fn):
+    try:
+        fn()
+    except ValueError:
+        return 1
+    raise ValueError('negative control accepted')
+
+def main():
+    Q=set(prefixes(WORD))
+    need(len(WORD)==24 and len(Q)==24,'simple projected word')
+    need(sorted(Counter(WORD).values())==[2,2,4,4,4,4,4],'counts')
+    need(differences(Q)==set(range(128)),'seven-source universal')
+    k=check_matching(Q,MATCHING)
+    need(k==11,'matching size')
+    need(len(VERTEX_COVER)==11 and all(a in VERTEX_COVER or b in VERTEX_COVER
+         for pairs in representations(Q).values() if len(pairs)==1
+         for a,b in pairs),'matching cover dual certificate')
+    gray=[i^(i>>1) for i in range(16)]+[0]
+    half=[(a^b).bit_length()-1 for a,b in zip(gray,gray[1:])]
+    upper=half+[i+4 for i in half]
+    need(len(upper)==32 and differences(prefixes(upper))==set(range(256)),
+         'known 32-step upper construction')
+    near='5643251350361472024502071341'
+    near_states=prefixes(near); near_differences=differences(near_states)
+    intervals={0}
+    for i in range(len(near)):
+        d=0
+        for c in near[i:]:
+            d^=1<<int(c); intervals.add(d)
+    need(intervals==near_differences,'independent interval oracle')
+    need(len(near)==28 and sorted(Counter(near).values())==[2,2,4,4,4,4,4,4],
+         '28-step sample counts')
+    need(len(near_differences)==246,'sample is not universal')
+    domain=valid=0
+    for n in range(1,4):
+        ambient=1<<(n+1)
+        for bits in range(1,1<<ambient):
+            P={x for x in range(ambient) if bits>>x&1}
+            pred,Q0,S=lift_criterion(P,n)
+            actual=differences(P)==set(range(ambient))
+            need(pred==actual,'exact static lifting equivalence')
+            if actual:
+                valid+=1
+                for pairs in representations(Q0).values():
+                    if len(pairs)==1:
+                        a,b=pairs[0]
+                        need(a in S or b in S,'unique-edge cover')
+            domain+=1
+    # A repeated projected state may split without a new-coordinate call at
+    # that state. Therefore |S| <= number of new-coordinate calls is false.
+    repeated='2010120101'
+    P=set(prefixes(repeated)); _,Q0,S=lift_criterion(P,2)
+    need(len(S)==4 and repeated.count('2')==2,'revisit counterexample')
+    controls=0
+    controls+=rejected(lambda:check_matching(Q,[(0,8)]))
+    controls+=rejected(lambda:check_matching(Q,[MATCHING[0],MATCHING[0]]))
+    controls+=rejected(lambda:check_matching(Q,[(0,127)]))
+    controls+=rejected(lambda:need(len(S)<=repeated.count('2'),'false split bound'))
+    need(not lift_criterion({0,1,2,3},2)[0],'one-layer negative fixture')
+    print(json.dumps({
+        'status':'PASS_PROJECTION_MATCHING_OBSTRUCTION',
+        'word':WORD,'distinct_projected_states':len(Q),'coverage':128,
+        'unique_difference_matching':MATCHING,
+        'matching_size':k,'lifted_state_lower_bound':len(Q)+k,
+        'minimum_vertex_cover_size':len(VERTEX_COVER),
+        'closed_lift_word_length_lower_bound':2*((len(Q)+k+1)//2),
+        'exhaustive_small_lift_subsets':domain,'universal_small_lifts':valid,
+        'rejected_controls':controls,
+        'known_universal_upper_word':''.join(map(str,upper)),
+        'nonuniversal_28_word':near,
+        'nonuniversal_28_missing_masks':sorted(set(range(256))-near_differences),
+        'scope':'General written matching lemma and one fixed-projection exclusion; f(8) remains unresolved.'
+    },indent=2))
+
+if __name__=='__main__':
+    main()