From 08bba0dcd71e79f0d517740792c9b5a7ca9cecb8 Mon Sep 17 00:00:00 2001
From: Ali Romman <226877337+aliromman@users.noreply.github.com>
Date: Fri, 23 Oct 2026 12:40:57 -0500
Subject: [PATCH] Maintain matching capacity counts incrementally in the census

---
 .../incremental-prefix-capacity/DELTA.diff    |  80 +++
 .../incremental-prefix-capacity/README.md     | 123 ++++
 .../incremental-prefix-capacity/RESULT.json   | 675 ++++++++++++++++++
 .../incremental-prefix-capacity/SOURCES.json  |  42 ++
 .../incremental-prefix-capacity/TASK.json     |  73 ++
 .../incremental-prefix-capacity/TIMINGS.json  | 210 ++++++
 .../incremental-prefix-capacity/VERIFY.json   |  40 ++
 research/incremental-prefix-capacity/census.c | 310 ++++++++
 .../incremental-prefix-capacity/verify.py     | 207 ++++++
 9 files changed, 1760 insertions(+)
 create mode 100644 research/incremental-prefix-capacity/DELTA.diff
 create mode 100644 research/incremental-prefix-capacity/README.md
 create mode 100644 research/incremental-prefix-capacity/RESULT.json
 create mode 100644 research/incremental-prefix-capacity/SOURCES.json
 create mode 100644 research/incremental-prefix-capacity/TASK.json
 create mode 100644 research/incremental-prefix-capacity/TIMINGS.json
 create mode 100644 research/incremental-prefix-capacity/VERIFY.json
 create mode 100644 research/incremental-prefix-capacity/census.c
 create mode 100644 research/incremental-prefix-capacity/verify.py

diff --git a/research/incremental-prefix-capacity/DELTA.diff b/research/incremental-prefix-capacity/DELTA.diff
new file mode 100644
index 0000000000..d43a3add24
--- /dev/null
+++ b/research/incremental-prefix-capacity/DELTA.diff
@@ -0,0 +1,80 @@
+--- pinned/census.c
++++ census.c
+@@ -1,3 +1,7 @@
++/* Incremental matching-capacity state.
++ * Ali Romman, with substantial OpenAI Codex assistance; Apache-2.0.
++ * The predecessor algorithm and notices follow without changes.
++ */
+ /* Source-bound maintained-engine successor with opt-in prefix capacity.
+  * JoyboyBrian, with substantial OpenAI Codex assistance; Apache-2.0.
+  * PR5001 capacity theorem: Ali Romman; all predecessor credit follows.
+@@ -74,25 +78,35 @@
+ }
+ static inline int parity(int x) { return __builtin_popcount((unsigned)x)&1; }
+ static inline mask_t bit(int x) { return (mask_t)1 << x; }
++typedef struct { int size[2],stays[2],occupied_pairs[2]; } Capacity;
++static Capacity capacity[L][N];
++/* Each level owns its state. A sibling overwrites only the next level. */
++static void extend_capacity(int depth,int point,int label,mask_t old_seen) {
++    for(int omitted=0;omitted<N;omitted++) {
++        Capacity *next=&capacity[depth+1][omitted];
++        *next=capacity[depth][omitted];
++        int mask=((1<<N)-1)^(1<<omitted),side=parity(point&mask);
++        next->size[side]++;
++        if(label==omitted) next->stays[side]++;
++        if(old_seen&bit(point^(1<<omitted))) next->occupied_pairs[side]++;
++    }
++}
+ /* The caller supplies a simple path; each omitted functional uses actual splits. */
+ static uint32_t capacity_splits(int depth,int omitted) {
+     int k=depth+1,r=L-k,mask=((1<<N)-1)^(1<<omitted);
+-    int size[2]={0},stays[2]={0},cheap[2]={0},pairs[2]={0},available[2]={0};
+-    int point=0,crossing=0;
+-    size[0]=1;
+-    for(int i=0;i<depth;i++) {
+-        int next=point^(1<<word[i]);
+-        int side=parity(next&mask);
+-        size[side]++;
+-        if(word[i]==omitted) stays[side]++; else crossing++;
+-        point=next;
+-    }
++    const Capacity *state=&capacity[depth][omitted];
++    const int *size=state->size,*stays=state->stays;
++    int cheap[2]={0},pairs[2],available[2];
++    int crossing=depth-stays[0]-stays[1];
+     if(!r) return __builtin_popcount((unsigned)q)==1 ? (uint32_t)1<<size[0] : 0;
+-    for(int vertex=0;vertex<(1<<N);vertex++) if(!(seen&bit(vertex))) {
+-        int side=parity(vertex&mask),mate=vertex^(1<<omitted);
+-        available[side]++;
+-        if(mate==0 || mate==q) cheap[side]++;
+-        else if(!(seen&bit(mate)) && vertex<mate) pairs[side]++;
++    for(int side=0;side<2;side++) {
++        available[side]=(1<<(N-1))-size[side];
++        pairs[side]=(1<<N)/4-size[side]+state->occupied_pairs[side];
++    }
++    int endpoints[2]={0,q};
++    for(int i=0;i<2;i++) {
++        int endpoint=endpoints[i];
++        if(!(seen&bit(endpoint^(1<<omitted)))) cheap[parity(endpoint&mask)]++;
+     }
+     uint32_t splits=0;
+     for(int x=0;x<=r;x++) {
+@@ -168,6 +182,7 @@
+         odd_counts+=(counts[j]&1)?1:-1;
+         q=nq;
+         if (j==old_used) used++;
++        if(capacity_active && fresh) extend_capacity(i,nq,j,old_seen);
+         if (fresh) {
+             seen|=bit(nq);
+             if (p) { O[os++]=nq; oo|=add_same; }
+@@ -265,6 +280,10 @@
+         memset(&run,0,sizeof run); memset(counts,0,sizeof counts);
+         q=used=odd_counts=even_excess=odd_excess=0; es=1; os=0; E[0]=0;
+         seen=1; ee=oo=eo=0; current=&shards[a];
++        if(capacity_active) {
++            memset(capacity,0,sizeof capacity);
++            for(int omitted=0;omitted<N;omitted++) capacity[0][omitted].size[0]=1;
++        }
+         struct timespec start,end; clock_gettime(CLOCK_MONOTONIC,&start);
+         /* Negative necessary budget proves no universal leaf: skip whole shard. */
+         if (!(even_on&&even_budget<0) && !(odd_on&&odd_budget<0) && !(union_on&&union_budget<0)) rec(0);
diff --git a/research/incremental-prefix-capacity/README.md b/research/incremental-prefix-capacity/README.md
new file mode 100644
index 0000000000..1aaf179335
--- /dev/null
+++ b/research/incremental-prefix-capacity/README.md
@@ -0,0 +1,123 @@
+# Incremental matching capacity in the word census
+
+This package answers the first open question in PR #5033. It replaces the
+cube and prefix scans in its opt-in capacity predicate with exact per-depth
+counts. The completion inequality, simple-path gate, search order, counters,
+report format and defaults are unchanged. The new C source preserves all
+predecessor notices. DELTA.diff gives the full source change.
+
+On the complete no-budget n=6, L=14, split (7,7) root shard, seven serialized
+alternating runs gave medians 200.42 ms for the pinned enabled predicate,
+40.73 ms for the incremental enabled predicate, and 20.68 ms for the new
+engine with capacity disabled. The enabled implementation is 4.92 times
+faster in this measurement, but still 1.97 times the disabled runtime.
+Thus the capacity option remains off by default. TIMINGS.json gives all
+samples, compiler, host and reports. These local timings are not CI limits.
+
+Both enabled variants visit exactly 495,919 nodes, find 89,782 restored
+leaves, and make 2,922 capacity prunes. Capacity off visits 506,239 nodes
+with the same restored leaves. There are no universal hits in this domain.
+These results do not establish a seven-label speedup or a new exclusion.
+The complete kappa calculation and selected 60403/20000000 are unchanged.
+
+## Exact state invariant
+
+Fix omitted coordinate v. Let f be the functional with coefficient zero
+at v and one elsewhere. Each class has 2^(n-1) vertices and 2^(n-2) disjoint
+v-matching edges, for n>=2. At prefix depth d, store for each class j:
+
+- a_j: distinct visited vertices;
+- e_j: used path edges in coordinate v;
+- b_j: matching edges with both endpoints visited.
+
+The caller gate requires a simple path. On insertion of new vertex z,
+increment a_f(z). Increment e_f(z) exactly when the new edge uses v.
+Increment b_f(z) exactly when z xor 2^v was already visited. Each matching
+edge is counted once, on insertion of its second endpoint. The initial
+state has a_0=1 and every other count zero. This proves the invariant by
+induction for each prefix.
+
+There are a_j-b_j touched matching edges: a matching edge with two visited
+endpoints contributes two to a_j and one to b_j. Thus
+
+```text
+unused vertices in class j = 2^(n-1) - a_j
+fully unused matching pairs = 2^(n-2) - a_j + b_j
+crossing path edges = d - e_0 - e_1.
+```
+
+The cheap one-vertex matching edges are exactly the unused mates of the
+two path endpoints. Two membership tests count them. Distinct endpoints
+have distinct mates. An internal vertex cannot take a new edge in a simple
+completion. These quantities equal the pinned source's scan results, so
+the unchanged even-interval test returns exactly the same split set.
+When no new vertices remain, the original closing-edge check still applies.
+
+State is stored by depth. A child copies its parent then updates the three
+counts for every omitted coordinate. After return, the parent's row remains
+unchanged. A sibling overwrites the child's row. Each new shard clears the
+array and sets the initial vertex. Closing edges do not add a vertex and
+reach the leaf before a capacity query. The repeat-capable caller bypasses
+capacity exactly as before; its arrays are not updated or consumed.
+
+The new state costs 6*n*L C integers, at most 3,696 bytes with the tested
+four-byte int and the admitted n<=7, L<=22. Each insertion costs O(n).
+Each predicate query keeps the original O(n*L) split loop and removes the
+O(n*(L+2^n)) reconstruction scans. This is an implementation of PR #5001's
+condition, not a stronger pruning theorem.
+
+## Evidence and reproduction
+
+Use CPython 3.12, the standard library and a C11 compiler that supports
+unsigned __int128 and the listed undefined-behavior/bounds sanitizers.
+From the repository root:
+
+```sh
+python3 -I -W error -B research/incremental-prefix-capacity/verify.py
+python3 -I -O -W error -B research/incremental-prefix-capacity/verify.py
+python3 -B scripts/research_package.py --package research/incremental-prefix-capacity
+python3 -I -B research/incremental-prefix-capacity/verify.py --timings
+```
+
+The direct marker is `PASS_INCREMENTAL_PREFIX_CAPACITY`. Normal replay
+checks the complete deterministic RESULT.json. The timing command prints
+new local measurements and does not update the stored receipt. Each native
+process has a fifteen-second limit and fresh output files.
+
+The verifier compares full restored and universal leaf Counters, every
+non-timing report field and exact node counts in twenty configurations:
+(2,4), (3,6), (4,8), (4,10), (5,12), with capacity on/off and budgets on/off.
+Separate checks cover repeat-capable bypass, two disjoint shards and a
+17-node cap. A temporary leaf observer is inserted at the actual source
+leaf boundary; it does not add a production test hook.
+
+The independent PR #5001 split function checks every one of 1,988
+prefix/functional cases at (4,10), with both ordinary and sanitizer builds.
+Four actual source mutations fail: missing occupied-pair count, wrong mate,
+lost parent state and lost final endpoint. The complete source delta and
+all declared input hashes are checked before and after execution.
+
+This equivalence work does not independently prove the predecessor census
+traversal or its matching-capacity theorem. Those remain explicit premises.
+The new count invariant is proved above. No full seven-label run, selected
+cold replay, Lean, Docker, formal-kernel or independent human review is
+claimed. Wall time on another compiler or host can differ.
+
+## Open next questions
+
+- Measure a named production simple-split shard under an explicit node and
+  time budget. Compare enabled and disabled total time before any default
+  change; fewer nodes alone do not justify enablement.
+- Derive a repeat-aware completion theorem before expanding the current
+  simple-path gate. This implementation supplies no such theorem.
+
+## Sources and credit
+
+SOURCES.json pins every consumed file at canonical main
+ff3cc58e370d0f678e529246f8c73e8094e18fcf. The source engine and its notices
+are retained from JoyboyBrian's PR #5033 integration. The mathematical
+predicate is Ali Romman's PR #5001 result. Credit Nick Petalas's matching
+balance and union census, Nicholas Stone's parity correction, Mihir
+Srivastava's handoff, Ross Richardson's prefix model, Aaron Wang/opencode,
+and the retained contributor notices. Ali Romman prepared this incremental
+implementation with substantial OpenAI Codex assistance. Apache-2.0.
diff --git a/research/incremental-prefix-capacity/RESULT.json b/research/incremental-prefix-capacity/RESULT.json
new file mode 100644
index 0000000000..03529ea208
--- /dev/null
+++ b/research/incremental-prefix-capacity/RESULT.json
@@ -0,0 +1,675 @@
+{
+  "status": "PASS_INCREMENTAL_PREFIX_CAPACITY",
+  "complete_domain_modes": [
+    {
+      "n": 2,
+      "length": 4,
+      "flags": [],
+      "report": {
+        "prefix": "",
+        "nodes": 5,
+        "candidate_restored_leaves": 1,
+        "all_restored_leaves": null,
+        "hits": 1,
+        "even_budget_prunes": 0,
+        "odd_budget_prunes": 0,
+        "union_budget_prunes": 0,
+        "prefix_capacity_prunes": 0,
+        "aborted": false,
+        "complete": true
+      },
+      "leaves_sha256": "61f7c686bc038316265ab42cb5d57aa8afecc7ea921764df82c4e57a704a6c06",
+      "hits_sha256": "61f7c686bc038316265ab42cb5d57aa8afecc7ea921764df82c4e57a704a6c06"
+    },
+    {
+      "n": 2,
+      "length": 4,
+      "flags": [
+        "--no-budgets"
+      ],
+      "report": {
+        "prefix": "",
+        "nodes": 5,
+        "candidate_restored_leaves": 1,
+        "all_restored_leaves": 1,
+        "hits": 1,
+        "even_budget_prunes": 0,
+        "odd_budget_prunes": 0,
+        "union_budget_prunes": 0,
+        "prefix_capacity_prunes": 0,
+        "aborted": false,
+        "complete": true
+      },
+      "leaves_sha256": "61f7c686bc038316265ab42cb5d57aa8afecc7ea921764df82c4e57a704a6c06",
+      "hits_sha256": "61f7c686bc038316265ab42cb5d57aa8afecc7ea921764df82c4e57a704a6c06"
+    },
+    {
+      "n": 2,
+      "length": 4,
+      "flags": [
+        "--prefix-capacity"
+      ],
+      "report": {
+        "prefix": "",
+        "nodes": 5,
+        "candidate_restored_leaves": 1,
+        "all_restored_leaves": null,
+        "hits": 1,
+        "even_budget_prunes": 0,
+        "odd_budget_prunes": 0,
+        "union_budget_prunes": 0,
+        "prefix_capacity_prunes": 0,
+        "aborted": false,
+        "complete": true
+      },
+      "leaves_sha256": "61f7c686bc038316265ab42cb5d57aa8afecc7ea921764df82c4e57a704a6c06",
+      "hits_sha256": "61f7c686bc038316265ab42cb5d57aa8afecc7ea921764df82c4e57a704a6c06"
+    },
+    {
+      "n": 2,
+      "length": 4,
+      "flags": [
+        "--prefix-capacity",
+        "--no-budgets"
+      ],
+      "report": {
+        "prefix": "",
+        "nodes": 5,
+        "candidate_restored_leaves": 1,
+        "all_restored_leaves": 1,
+        "hits": 1,
+        "even_budget_prunes": 0,
+        "odd_budget_prunes": 0,
+        "union_budget_prunes": 0,
+        "prefix_capacity_prunes": 0,
+        "aborted": false,
+        "complete": true
+      },
+      "leaves_sha256": "61f7c686bc038316265ab42cb5d57aa8afecc7ea921764df82c4e57a704a6c06",
+      "hits_sha256": "61f7c686bc038316265ab42cb5d57aa8afecc7ea921764df82c4e57a704a6c06"
+    },
+    {
+      "n": 3,
+      "length": 6,
+      "flags": [],
+      "report": {
+        "prefix": "",
+        "nodes": 16,
+        "candidate_restored_leaves": 4,
+        "all_restored_leaves": null,
+        "hits": 4,
+        "even_budget_prunes": 0,
+        "odd_budget_prunes": 0,
+        "union_budget_prunes": 0,
+        "prefix_capacity_prunes": 0,
+        "aborted": false,
+        "complete": true
+      },
+      "leaves_sha256": "5585289ec8e0a0f8823262428d9db0a79d43eede6308563ec5e954603a7da38d",
+      "hits_sha256": "5585289ec8e0a0f8823262428d9db0a79d43eede6308563ec5e954603a7da38d"
+    },
+    {
+      "n": 3,
+      "length": 6,
+      "flags": [
+        "--no-budgets"
+      ],
+      "report": {
+        "prefix": "",
+        "nodes": 16,
+        "candidate_restored_leaves": 4,
+        "all_restored_leaves": 4,
+        "hits": 4,
+        "even_budget_prunes": 0,
+        "odd_budget_prunes": 0,
+        "union_budget_prunes": 0,
+        "prefix_capacity_prunes": 0,
+        "aborted": false,
+        "complete": true
+      },
+      "leaves_sha256": "5585289ec8e0a0f8823262428d9db0a79d43eede6308563ec5e954603a7da38d",
+      "hits_sha256": "5585289ec8e0a0f8823262428d9db0a79d43eede6308563ec5e954603a7da38d"
+    },
+    {
+      "n": 3,
+      "length": 6,
+      "flags": [
+        "--prefix-capacity"
+      ],
+      "report": {
+        "prefix": "",
+        "nodes": 16,
+        "candidate_restored_leaves": 4,
+        "all_restored_leaves": null,
+        "hits": 4,
+        "even_budget_prunes": 0,
+        "odd_budget_prunes": 0,
+        "union_budget_prunes": 0,
+        "prefix_capacity_prunes": 0,
+        "aborted": false,
+        "complete": true
+      },
+      "leaves_sha256": "5585289ec8e0a0f8823262428d9db0a79d43eede6308563ec5e954603a7da38d",
+      "hits_sha256": "5585289ec8e0a0f8823262428d9db0a79d43eede6308563ec5e954603a7da38d"
+    },
+    {
+      "n": 3,
+      "length": 6,
+      "flags": [
+        "--prefix-capacity",
+        "--no-budgets"
+      ],
+      "report": {
+        "prefix": "",
+        "nodes": 16,
+        "candidate_restored_leaves": 4,
+        "all_restored_leaves": 4,
+        "hits": 4,
+        "even_budget_prunes": 0,
+        "odd_budget_prunes": 0,
+        "union_budget_prunes": 0,
+        "prefix_capacity_prunes": 0,
+        "aborted": false,
+        "complete": true
+      },
+      "leaves_sha256": "5585289ec8e0a0f8823262428d9db0a79d43eede6308563ec5e954603a7da38d",
+      "hits_sha256": "5585289ec8e0a0f8823262428d9db0a79d43eede6308563ec5e954603a7da38d"
+    },
+    {
+      "n": 4,
+      "length": 8,
+      "flags": [],
+      "report": {
+        "prefix": "",
+        "nodes": 81,
+        "candidate_restored_leaves": 22,
+        "all_restored_leaves": null,
+        "hits": 22,
+        "even_budget_prunes": 0,
+        "odd_budget_prunes": 0,
+        "union_budget_prunes": 5,
+        "prefix_capacity_prunes": 0,
+        "aborted": false,
+        "complete": true
+      },
+      "leaves_sha256": "ab46ba3e3bcd5817487dfdb70a49e684fde54cee61226e7957e8992ae06a28ef",
+      "hits_sha256": "ab46ba3e3bcd5817487dfdb70a49e684fde54cee61226e7957e8992ae06a28ef"
+    },
+    {
+      "n": 4,
+      "length": 8,
+      "flags": [
+        "--no-budgets"
+      ],
+      "report": {
+        "prefix": "",
+        "nodes": 91,
+        "candidate_restored_leaves": 27,
+        "all_restored_leaves": 27,
+        "hits": 22,
+        "even_budget_prunes": 0,
+        "odd_budget_prunes": 0,
+        "union_budget_prunes": 0,
+        "prefix_capacity_prunes": 0,
+        "aborted": false,
+        "complete": true
+      },
+      "leaves_sha256": "545c82356a180bac011bf7d68ca622e3029f7a678e7e313f822b7b5b5ac203bd",
+      "hits_sha256": "ab46ba3e3bcd5817487dfdb70a49e684fde54cee61226e7957e8992ae06a28ef"
+    },
+    {
+      "n": 4,
+      "length": 8,
+      "flags": [
+        "--prefix-capacity"
+      ],
+      "report": {
+        "prefix": "",
+        "nodes": 81,
+        "candidate_restored_leaves": 22,
+        "all_restored_leaves": null,
+        "hits": 22,
+        "even_budget_prunes": 0,
+        "odd_budget_prunes": 0,
+        "union_budget_prunes": 5,
+        "prefix_capacity_prunes": 0,
+        "aborted": false,
+        "complete": true
+      },
+      "leaves_sha256": "ab46ba3e3bcd5817487dfdb70a49e684fde54cee61226e7957e8992ae06a28ef",
+      "hits_sha256": "ab46ba3e3bcd5817487dfdb70a49e684fde54cee61226e7957e8992ae06a28ef"
+    },
+    {
+      "n": 4,
+      "length": 8,
+      "flags": [
+        "--prefix-capacity",
+        "--no-budgets"
+      ],
+      "report": {
+        "prefix": "",
+        "nodes": 91,
+        "candidate_restored_leaves": 27,
+        "all_restored_leaves": 27,
+        "hits": 22,
+        "even_budget_prunes": 0,
+        "odd_budget_prunes": 0,
+        "union_budget_prunes": 0,
+        "prefix_capacity_prunes": 0,
+        "aborted": false,
+        "complete": true
+      },
+      "leaves_sha256": "545c82356a180bac011bf7d68ca622e3029f7a678e7e313f822b7b5b5ac203bd",
+      "hits_sha256": "ab46ba3e3bcd5817487dfdb70a49e684fde54cee61226e7957e8992ae06a28ef"
+    },
+    {
+      "n": 4,
+      "length": 10,
+      "flags": [],
+      "report": {
+        "prefix": "",
+        "nodes": 566,
+        "candidate_restored_leaves": 110,
+        "all_restored_leaves": null,
+        "hits": 110,
+        "even_budget_prunes": 0,
+        "odd_budget_prunes": 0,
+        "union_budget_prunes": 0,
+        "prefix_capacity_prunes": 0,
+        "aborted": false,
+        "complete": true
+      },
+      "leaves_sha256": "536d9fd18c55d1fb48ecc233c34f9f9722e5f16cff4ee02047ec6067001dbf2c",
+      "hits_sha256": "536d9fd18c55d1fb48ecc233c34f9f9722e5f16cff4ee02047ec6067001dbf2c"
+    },
+    {
+      "n": 4,
+      "length": 10,
+      "flags": [
+        "--no-budgets"
+      ],
+      "report": {
+        "prefix": "",
+        "nodes": 566,
+        "candidate_restored_leaves": 110,
+        "all_restored_leaves": 110,
+        "hits": 110,
+        "even_budget_prunes": 0,
+        "odd_budget_prunes": 0,
+        "union_budget_prunes": 0,
+        "prefix_capacity_prunes": 0,
+        "aborted": false,
+        "complete": true
+      },
+      "leaves_sha256": "536d9fd18c55d1fb48ecc233c34f9f9722e5f16cff4ee02047ec6067001dbf2c",
+      "hits_sha256": "536d9fd18c55d1fb48ecc233c34f9f9722e5f16cff4ee02047ec6067001dbf2c"
+    },
+    {
+      "n": 4,
+      "length": 10,
+      "flags": [
+        "--prefix-capacity"
+      ],
+      "report": {
+        "prefix": "",
+        "nodes": 534,
+        "candidate_restored_leaves": 110,
+        "all_restored_leaves": null,
+        "hits": 110,
+        "even_budget_prunes": 0,
+        "odd_budget_prunes": 0,
+        "union_budget_prunes": 0,
+        "prefix_capacity_prunes": 22,
+        "aborted": false,
+        "complete": true
+      },
+      "leaves_sha256": "536d9fd18c55d1fb48ecc233c34f9f9722e5f16cff4ee02047ec6067001dbf2c",
+      "hits_sha256": "536d9fd18c55d1fb48ecc233c34f9f9722e5f16cff4ee02047ec6067001dbf2c"
+    },
+    {
+      "n": 4,
+      "length": 10,
+      "flags": [
+        "--prefix-capacity",
+        "--no-budgets"
+      ],
+      "report": {
+        "prefix": "",
+        "nodes": 534,
+        "candidate_restored_leaves": 110,
+        "all_restored_leaves": 110,
+        "hits": 110,
+        "even_budget_prunes": 0,
+        "odd_budget_prunes": 0,
+        "union_budget_prunes": 0,
+        "prefix_capacity_prunes": 22,
+        "aborted": false,
+        "complete": true
+      },
+      "leaves_sha256": "536d9fd18c55d1fb48ecc233c34f9f9722e5f16cff4ee02047ec6067001dbf2c",
+      "hits_sha256": "536d9fd18c55d1fb48ecc233c34f9f9722e5f16cff4ee02047ec6067001dbf2c"
+    },
+    {
+      "n": 5,
+      "length": 12,
+      "flags": [],
+      "report": {
+        "prefix": "",
+        "nodes": 8401,
+        "candidate_restored_leaves": 828,
+        "all_restored_leaves": null,
+        "hits": 828,
+        "even_budget_prunes": 0,
+        "odd_budget_prunes": 1175,
+        "union_budget_prunes": 5231,
+        "prefix_capacity_prunes": 0,
+        "aborted": false,
+        "complete": true
+      },
+      "leaves_sha256": "5e222464045f9b7322e600498fe0811e0b96de0c4f9cce023d32621f31ebb62e",
+      "hits_sha256": "5e222464045f9b7322e600498fe0811e0b96de0c4f9cce023d32621f31ebb62e"
+    },
+    {
+      "n": 5,
+      "length": 12,
+      "flags": [
+        "--no-budgets"
+      ],
+      "report": {
+        "prefix": "",
+        "nodes": 17360,
+        "candidate_restored_leaves": 3381,
+        "all_restored_leaves": 3381,
+        "hits": 828,
+        "even_budget_prunes": 0,
+        "odd_budget_prunes": 0,
+        "union_budget_prunes": 0,
+        "prefix_capacity_prunes": 0,
+        "aborted": false,
+        "complete": true
+      },
+      "leaves_sha256": "ad152539cd1fff531c33d46fc16d2a3cb64a3fa9732bc5845667d8539cf87e73",
+      "hits_sha256": "5e222464045f9b7322e600498fe0811e0b96de0c4f9cce023d32621f31ebb62e"
+    },
+    {
+      "n": 5,
+      "length": 12,
+      "flags": [
+        "--prefix-capacity"
+      ],
+      "report": {
+        "prefix": "",
+        "nodes": 8278,
+        "candidate_restored_leaves": 828,
+        "all_restored_leaves": null,
+        "hits": 828,
+        "even_budget_prunes": 0,
+        "odd_budget_prunes": 1058,
+        "union_budget_prunes": 4876,
+        "prefix_capacity_prunes": 240,
+        "aborted": false,
+        "complete": true
+      },
+      "leaves_sha256": "5e222464045f9b7322e600498fe0811e0b96de0c4f9cce023d32621f31ebb62e",
+      "hits_sha256": "5e222464045f9b7322e600498fe0811e0b96de0c4f9cce023d32621f31ebb62e"
+    },
+    {
+      "n": 5,
+      "length": 12,
+      "flags": [
+        "--prefix-capacity",
+        "--no-budgets"
+      ],
+      "report": {
+        "prefix": "",
+        "nodes": 16765,
+        "candidate_restored_leaves": 3381,
+        "all_restored_leaves": 3381,
+        "hits": 828,
+        "even_budget_prunes": 0,
+        "odd_budget_prunes": 0,
+        "union_budget_prunes": 0,
+        "prefix_capacity_prunes": 240,
+        "aborted": false,
+        "complete": true
+      },
+      "leaves_sha256": "ad152539cd1fff531c33d46fc16d2a3cb64a3fa9732bc5845667d8539cf87e73",
+      "hits_sha256": "5e222464045f9b7322e600498fe0811e0b96de0c4f9cce023d32621f31ebb62e"
+    }
+  ],
+  "boundaries": [
+    {
+      "split": [
+        6,
+        5
+      ],
+      "flags": [
+        "--prefix-capacity",
+        "--no-budgets"
+      ],
+      "report": {
+        "prefix_capacity_requested": true,
+        "prefix_capacity_enabled": false,
+        "schema": 1,
+        "n": 5,
+        "length": 12,
+        "split": [
+          6,
+          5
+        ],
+        "groups": "hamming_weight_parity",
+        "even_budget": 10,
+        "odd_budget": 14,
+        "union_budget": 10,
+        "even_budget_enabled": false,
+        "odd_budget_enabled": false,
+        "union_budget_enabled": false,
+        "complete": true,
+        "aborted": false,
+        "requested_shards": 1,
+        "completed_or_partial_shards": 1,
+        "shards": [
+          {
+            "prefix": "",
+            "nodes": 29094,
+            "candidate_restored_leaves": 5457,
+            "all_restored_leaves": 5457,
+            "hits": 144,
+            "even_budget_prunes": 0,
+            "odd_budget_prunes": 0,
+            "union_budget_prunes": 0,
+            "prefix_capacity_prunes": 0,
+            "aborted": false,
+            "complete": true
+          }
+        ],
+        "total": [
+          {
+            "prefix": "",
+            "nodes": 29094,
+            "candidate_restored_leaves": 5457,
+            "all_restored_leaves": 5457,
+            "hits": 144,
+            "even_budget_prunes": 0,
+            "odd_budget_prunes": 0,
+            "union_budget_prunes": 0,
+            "prefix_capacity_prunes": 0,
+            "aborted": false,
+            "complete": true
+          }
+        ]
+      }
+    },
+    {
+      "split": [
+        6,
+        6
+      ],
+      "flags": [
+        "--prefix-capacity",
+        "--no-budgets",
+        "010",
+        "012"
+      ],
+      "report": {
+        "prefix_capacity_requested": true,
+        "prefix_capacity_enabled": true,
+        "schema": 1,
+        "n": 5,
+        "length": 12,
+        "split": [
+          6,
+          6
+        ],
+        "groups": "hamming_weight_parity",
+        "even_budget": 15,
+        "odd_budget": 20,
+        "union_budget": 15,
+        "even_budget_enabled": false,
+        "odd_budget_enabled": false,
+        "union_budget_enabled": false,
+        "complete": true,
+        "aborted": false,
+        "requested_shards": 2,
+        "completed_or_partial_shards": 2,
+        "shards": [
+          {
+            "prefix": "010",
+            "nodes": 3008,
+            "candidate_restored_leaves": 572,
+            "all_restored_leaves": 572,
+            "hits": 139,
+            "even_budget_prunes": 0,
+            "odd_budget_prunes": 0,
+            "union_budget_prunes": 0,
+            "prefix_capacity_prunes": 57,
+            "aborted": false,
+            "complete": true
+          },
+          {
+            "prefix": "012",
+            "nodes": 13760,
+            "candidate_restored_leaves": 2809,
+            "all_restored_leaves": 2809,
+            "hits": 689,
+            "even_budget_prunes": 0,
+            "odd_budget_prunes": 0,
+            "union_budget_prunes": 0,
+            "prefix_capacity_prunes": 183,
+            "aborted": false,
+            "complete": true
+          }
+        ],
+        "total": [
+          {
+            "prefix": "",
+            "nodes": 16768,
+            "candidate_restored_leaves": 3381,
+            "all_restored_leaves": 3381,
+            "hits": 828,
+            "even_budget_prunes": 0,
+            "odd_budget_prunes": 0,
+            "union_budget_prunes": 0,
+            "prefix_capacity_prunes": 240,
+            "aborted": false,
+            "complete": true
+          }
+        ]
+      }
+    },
+    {
+      "split": [
+        6,
+        6
+      ],
+      "flags": [
+        "--prefix-capacity",
+        "--no-budgets",
+        "--cap",
+        "17"
+      ],
+      "report": {
+        "prefix_capacity_requested": true,
+        "prefix_capacity_enabled": true,
+        "schema": 1,
+        "n": 5,
+        "length": 12,
+        "split": [
+          6,
+          6
+        ],
+        "groups": "hamming_weight_parity",
+        "even_budget": 15,
+        "odd_budget": 20,
+        "union_budget": 15,
+        "even_budget_enabled": false,
+        "odd_budget_enabled": false,
+        "union_budget_enabled": false,
+        "complete": false,
+        "aborted": true,
+        "requested_shards": 1,
+        "completed_or_partial_shards": 1,
+        "shards": [
+          {
+            "prefix": "",
+            "nodes": 17,
+            "candidate_restored_leaves": 1,
+            "all_restored_leaves": null,
+            "hits": 1,
+            "even_budget_prunes": 0,
+            "odd_budget_prunes": 0,
+            "union_budget_prunes": 0,
+            "prefix_capacity_prunes": 0,
+            "aborted": true,
+            "complete": false
+          }
+        ],
+        "total": [
+          {
+            "prefix": "",
+            "nodes": 17,
+            "candidate_restored_leaves": 1,
+            "all_restored_leaves": null,
+            "hits": 1,
+            "even_budget_prunes": 0,
+            "odd_budget_prunes": 0,
+            "union_budget_prunes": 0,
+            "prefix_capacity_prunes": 0,
+            "aborted": true,
+            "complete": false
+          }
+        ]
+      }
+    }
+  ],
+  "kernel": {
+    "prefix_functionals": 1988,
+    "mutations": {
+      "missing_occupied_pair": [
+        "01020",
+        0,
+        96,
+        32
+      ],
+      "wrong_mate": [
+        "01020",
+        0,
+        96,
+        32
+      ],
+      "lost_parent_state": [
+        "0",
+        1,
+        112,
+        120
+      ],
+      "lost_final_endpoint": [
+        "0",
+        1,
+        112,
+        240
+      ]
+    }
+  },
+  "census_sha256": "542ca4775439e19efe27578de4687c1cb92dd7abf9f898bbac40521202a80369"
+}
diff --git a/research/incremental-prefix-capacity/SOURCES.json b/research/incremental-prefix-capacity/SOURCES.json
new file mode 100644
index 0000000000..dbf374dc07
--- /dev/null
+++ b/research/incremental-prefix-capacity/SOURCES.json
@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/f7-prefix-capacity-engine/README.md",
+      "usage": "input",
+      "git_blob": "c3d6678f2f563f366a109d1d92262bb8ee02116b",
+      "sha256": "ab5ed05ef6d649c784732a82de9ac00b2cc96d5a322b6e76d3edd0800d1badef"
+    },
+    {
+      "path": "research/f7-prefix-capacity-engine/census.c",
+      "usage": "input",
+      "git_blob": "aba6572c9e16ea473bfd24ffc89b346ff2b3905c",
+      "sha256": "bc3d58245cbff446d7e2c7f73606aafd71fea009ea704a84c785f25be2a358a5"
+    },
+    {
+      "path": "research/f7-prefix-matching-capacity/README.md",
+      "usage": "input",
+      "git_blob": "f5251a7b370d791c1aff734ef805271b807eadfb",
+      "sha256": "dfaacf1af0c1c4f4365f8c03fdcb03a28d7b90e601e8a1204f71b9cab6bfd26c"
+    },
+    {
+      "path": "research/f7-prefix-matching-capacity/verify.py",
+      "usage": "input",
+      "git_blob": "d09ac1fe4364b4f25b16f42483ada0cb331496df",
+      "sha256": "cfb771bcb19eae1d268a45d89bc10acdf56158403b60fdd2e14c8565b5181301"
+    }
+  ]
+}
diff --git a/research/incremental-prefix-capacity/TASK.json b/research/incremental-prefix-capacity/TASK.json
new file mode 100644
index 0000000000..d56c04ec59
--- /dev/null
+++ b/research/incremental-prefix-capacity/TASK.json
@@ -0,0 +1,73 @@
+{
+  "schema_version": 1,
+  "task_id": "census-pruning-audit",
+  "priority_revision": 7,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "original_card": {
+    "id": "census-pruning-audit",
+    "question": "Does the reported word-census parity-pruning error invalidate a specific exclusion we still rely on, and what bounded repair is justified?",
+    "starting_points": [
+      "research/f7-weight-parity-census-correction/README.md",
+      "docs/research/research-family-status.md"
+    ],
+    "methods": [
+      "Independently reconstruct the tiny counterexample and trace one affected exclusion to its exact pruning code.",
+      "Compare corrected and unpruned enumeration on a small exhaustive domain, then audit the changed pruning implication."
+    ],
+    "acceptance_gate": "Pin the old and proposed corrected engines, distinguish a disproved pruning rule from a disproved final bound, and state exactly which downstream exclusions need revalidation. #2973 is an author-checked source archive; neither its new f(7) claim nor all old conclusions are automatically accepted or rejected.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read #2973 error description and MATH.md; manually reconstruct the prefix states of 01021323 before running any large census.",
+      "scope": "Source-binding orientation only; no full enumeration or mathematical validation."
+    },
+    "first_experiment": "Reconstruct the eight prefix states of 01021323 and compare bit-0 versus Hamming-weight parity budgets independently. Trace the reported false prune to one pinned predecessor (#2542, #2634 or #2691), then test a small exhaustive domain. Stop after a source-impact handoff or corrected-prune proof; a full seven-label replay needs a separate resource budget and a named research decision it can change.",
+    "bottleneck_link": "An unsound exclusion can wrongly close a mechanism; correcting its dependency boundary is more useful than extending the same census.",
+    "allowed_variations": [
+      "One predecessor pruning rule, one independently exhaustive small domain, or one downstream dependency audit."
+    ],
+    "scope_change_triggers": [
+      "Launching a larger census before validating the prune and explaining which active decision it changes.",
+      "Treating a small-domain counterexample to the old rule as a counterexample to every reported seven-label bound."
+    ],
+    "overlap_terms": [
+      "2973",
+      "2542",
+      "2634",
+      "2691",
+      "weight parity",
+      "bit-0",
+      "01021323",
+      "census pruning"
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Exact incremental implementation of the existing matching-capacity census predicate.",
+  "scope_change_reason": "Picker fb571b1d095a0b5f5f710da1ece74d61 selected census-pruning-audit. The resolved parity error is not repeated; PR5033 open question 1 requests per-prefix cost reduction.",
+  "bottleneck_link": "Reduce cost of a sound existing census predicate while retaining exact traversal and default-off status.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop on any kernel, leaf, counter, cap or bypass mismatch, or no useful measured cost reduction.",
+  "outcome": "completed",
+  "evidence": "README.md, DELTA.diff, RESULT.json, TIMINGS.json, verify.py",
+  "author": "Ali Romman",
+  "ai_assistance": "Substantial OpenAI Codex assistance; no independent human or kernel review.",
+  "open_questions": [
+    {
+      "question": "Does this predicate save total runtime on a production simple-split shard?",
+      "why_it_matters": "It remains slower than disabled capacity in the measured domain.",
+      "first_step": "Set a node/time budget and compare serialized on/off runs.",
+      "blocked_by": "Separately budgeted production experiment."
+    },
+    {
+      "question": "Can a repeat-aware caller use a stronger capacity test?",
+      "why_it_matters": "The present gate excludes revisits.",
+      "first_step": "Prove a separate repeated-vertex completion theorem.",
+      "blocked_by": "New theorem required."
+    }
+  ],
+  "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4903#discussioncomment-19151175"
+}
diff --git a/research/incremental-prefix-capacity/TIMINGS.json b/research/incremental-prefix-capacity/TIMINGS.json
new file mode 100644
index 0000000000..4096c34a9e
--- /dev/null
+++ b/research/incremental-prefix-capacity/TIMINGS.json
@@ -0,0 +1,210 @@
+{
+  "domain": [
+    6,
+    14
+  ],
+  "split": [
+    7,
+    7
+  ],
+  "runs": 7,
+  "seconds": {
+    "old_on": [
+      0.4744272920070216,
+      0.20104499999433756,
+      0.20042037504026666,
+      0.20119258400518447,
+      0.20027429203037173,
+      0.1999712079996243,
+      0.20003320899559185
+    ],
+    "new_on": [
+      0.2749991660239175,
+      0.03925195802003145,
+      0.04073008301202208,
+      0.03918487502960488,
+      0.04074087494518608,
+      0.03942433401243761,
+      0.041367667028680444
+    ],
+    "new_off": [
+      0.021648416004609317,
+      0.02043391700135544,
+      0.02104154200060293,
+      0.02056454203557223,
+      0.02067612501559779,
+      0.02052608400117606,
+      0.020999333006329834
+    ]
+  },
+  "medians": {
+    "old_on": 0.20042037504026666,
+    "new_on": 0.04073008301202208,
+    "new_off": 0.02067612501559779
+  },
+  "old_on_over_new_on": 4.920696453800737,
+  "new_on_over_new_off": 1.969908915780682,
+  "reports": {
+    "old_on": {
+      "prefix_capacity_requested": true,
+      "prefix_capacity_enabled": true,
+      "schema": 1,
+      "n": 6,
+      "length": 14,
+      "split": [
+        7,
+        7
+      ],
+      "groups": "hamming_weight_parity",
+      "even_budget": 11,
+      "odd_budget": 17,
+      "union_budget": 11,
+      "even_budget_enabled": false,
+      "odd_budget_enabled": false,
+      "union_budget_enabled": false,
+      "complete": true,
+      "aborted": false,
+      "requested_shards": 1,
+      "completed_or_partial_shards": 1,
+      "shards": [
+        {
+          "prefix": "",
+          "nodes": 495919,
+          "candidate_restored_leaves": 89782,
+          "all_restored_leaves": 89782,
+          "hits": 0,
+          "even_budget_prunes": 0,
+          "odd_budget_prunes": 0,
+          "union_budget_prunes": 0,
+          "prefix_capacity_prunes": 2922,
+          "aborted": false,
+          "complete": true
+        }
+      ],
+      "total": [
+        {
+          "prefix": "",
+          "nodes": 495919,
+          "candidate_restored_leaves": 89782,
+          "all_restored_leaves": 89782,
+          "hits": 0,
+          "even_budget_prunes": 0,
+          "odd_budget_prunes": 0,
+          "union_budget_prunes": 0,
+          "prefix_capacity_prunes": 2922,
+          "aborted": false,
+          "complete": true
+        }
+      ]
+    },
+    "new_on": {
+      "prefix_capacity_requested": true,
+      "prefix_capacity_enabled": true,
+      "schema": 1,
+      "n": 6,
+      "length": 14,
+      "split": [
+        7,
+        7
+      ],
+      "groups": "hamming_weight_parity",
+      "even_budget": 11,
+      "odd_budget": 17,
+      "union_budget": 11,
+      "even_budget_enabled": false,
+      "odd_budget_enabled": false,
+      "union_budget_enabled": false,
+      "complete": true,
+      "aborted": false,
+      "requested_shards": 1,
+      "completed_or_partial_shards": 1,
+      "shards": [
+        {
+          "prefix": "",
+          "nodes": 495919,
+          "candidate_restored_leaves": 89782,
+          "all_restored_leaves": 89782,
+          "hits": 0,
+          "even_budget_prunes": 0,
+          "odd_budget_prunes": 0,
+          "union_budget_prunes": 0,
+          "prefix_capacity_prunes": 2922,
+          "aborted": false,
+          "complete": true
+        }
+      ],
+      "total": [
+        {
+          "prefix": "",
+          "nodes": 495919,
+          "candidate_restored_leaves": 89782,
+          "all_restored_leaves": 89782,
+          "hits": 0,
+          "even_budget_prunes": 0,
+          "odd_budget_prunes": 0,
+          "union_budget_prunes": 0,
+          "prefix_capacity_prunes": 2922,
+          "aborted": false,
+          "complete": true
+        }
+      ]
+    },
+    "new_off": {
+      "prefix_capacity_requested": false,
+      "prefix_capacity_enabled": false,
+      "schema": 1,
+      "n": 6,
+      "length": 14,
+      "split": [
+        7,
+        7
+      ],
+      "groups": "hamming_weight_parity",
+      "even_budget": 11,
+      "odd_budget": 17,
+      "union_budget": 11,
+      "even_budget_enabled": false,
+      "odd_budget_enabled": false,
+      "union_budget_enabled": false,
+      "complete": true,
+      "aborted": false,
+      "requested_shards": 1,
+      "completed_or_partial_shards": 1,
+      "shards": [
+        {
+          "prefix": "",
+          "nodes": 506239,
+          "candidate_restored_leaves": 89782,
+          "all_restored_leaves": 89782,
+          "hits": 0,
+          "even_budget_prunes": 0,
+          "odd_budget_prunes": 0,
+          "union_budget_prunes": 0,
+          "prefix_capacity_prunes": 0,
+          "aborted": false,
+          "complete": true
+        }
+      ],
+      "total": [
+        {
+          "prefix": "",
+          "nodes": 506239,
+          "candidate_restored_leaves": 89782,
+          "all_restored_leaves": 89782,
+          "hits": 0,
+          "even_budget_prunes": 0,
+          "odd_budget_prunes": 0,
+          "union_budget_prunes": 0,
+          "prefix_capacity_prunes": 0,
+          "aborted": false,
+          "complete": true
+        }
+      ]
+    }
+  },
+  "compiler": "Apple clang version 17.0.0 (clang-1700.6.3.2)\nTarget: arm64-apple-darwin25.6.0\nThread model: posix\nInstalledDir: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin\n",
+  "python": "3.12.13 (main, May 10 2026, 19:20:41) [Clang 22.1.3 ]",
+  "platform": "macOS-26.6.1-arm64-arm-64bit",
+  "machine": "arm64",
+  "definition": "Serialized alternating process-inclusive runs; no compilation or leaf instrumentation in timings."
+}
diff --git a/research/incremental-prefix-capacity/VERIFY.json b/research/incremental-prefix-capacity/VERIFY.json
new file mode 100644
index 0000000000..afc8e678fc
--- /dev/null
+++ b/research/incremental-prefix-capacity/VERIFY.json
@@ -0,0 +1,40 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/f7-prefix-capacity-engine/README.md",
+    "research/f7-prefix-capacity-engine/census.c",
+    "research/f7-prefix-matching-capacity/README.md",
+    "research/f7-prefix-matching-capacity/verify.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Complete report and leaf equivalence, independent kernel, sanitizer, mutants and boundaries."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "All explicit checks with Python assertions disabled."
+    }
+  ],
+  "notes": "C11, unsigned __int128, and undefined-behavior/bounds sanitizer support are required. Timing is opt-in, not a CI threshold."
+}
diff --git a/research/incremental-prefix-capacity/census.c b/research/incremental-prefix-capacity/census.c
new file mode 100644
index 0000000000..eb5aae8b11
--- /dev/null
+++ b/research/incremental-prefix-capacity/census.c
@@ -0,0 +1,310 @@
+/* Incremental matching-capacity state.
+ * Ali Romman, with substantial OpenAI Codex assistance; Apache-2.0.
+ * The predecessor algorithm and notices follow without changes.
+ */
+/* Source-bound maintained-engine successor with opt-in prefix capacity.
+ * JoyboyBrian, with substantial OpenAI Codex assistance; Apache-2.0.
+ * PR5001 capacity theorem: Ali Romman; all predecessor credit follows.
+ *
+ * Corrected finite canonical restored-word census with a union-support budget.
+ * Derived from Nicholas Stone's corrected_census.c (research/
+ * f7-weight-parity-census-correction, sha256 265ead91...) and the L<=22 gate
+ * extension recorded in PR #3731; preserves the restricted-growth word scope.
+ * New implementation/review with substantial OpenAI Codex assistance.
+ * (The preceding attribution line is retained verbatim from the pinned
+ * predecessor. The union-budget port, the length-22 probes and their
+ * verification were produced by Nick Petalas with AI assistance.)
+ *
+ * E and O ALWAYS mean Hamming-weight parity, never coordinate bit 0.
+ * New DISTINCT states add pair representations; visits add none.
+ * Even excess is (C(|E|,2)-|supp EE|)+(C(|O|,2)-|supp OO|).
+ * Odd excess is |E||O|-|supp EO|. These are monotone, so their necessary
+ * final bounds are sound at intermediate prefixes. Default enables both.
+ *
+ * UNION BUDGET (from research/f7-union-support-audit, PR #3005): let
+ * U = supp EE union supp OO. A completion adds at most
+ * C(S,2)+C(T,2)-C(e,2)-C(o,2) further same-parity pairs, each contributing
+ * at most one new mask, so |U| + that quantity >= 2^(N-1)-1 is necessary.
+ * Because |U| <= |supp EE|+|supp OO|, this dominates the even excess budget
+ * above (the excess form charges an overlapping mask twice). Enabled by
+ * default; --no-union-budget restores the predecessor's even-side test.
+ *
+ * candidate_restored_leaves counts only leaves surviving enabled budgets.
+ * all_restored_leaves is exact only with --no-budgets and complete=true.
+ * A capped run returns 2, complete=false; bad input or output I/O returns 1.
+ * N in [1,7], positive even L<=22. See README.md for proof and commands.
+ */
+#ifndef _POSIX_C_SOURCE
+#define _POSIX_C_SOURCE 200809L
+#endif
+#include <errno.h>
+#include <inttypes.h>
+#include <limits.h>
+#include <stdint.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <time.h>
+
+#ifndef N
+#define N 7
+#endif
+#ifndef L
+#define L 20
+#endif
+#if N < 1 || N > 7 || L < 2 || L > 22 || L % 2
+#error "Requires 1 <= N <= 7 and positive even 2 <= L <= 22"
+#endif
+
+typedef unsigned __int128 mask_t;
+typedef struct { char key[L+1]; int length; uint64_t cap; } Shard;
+typedef struct {
+    uint64_t nodes, candidate_leaves, hits, even_prunes, odd_prunes, union_prunes, capacity_prunes;
+    int aborted;
+    double seconds;
+} Result;
+static int S,T, even_on=1,odd_on=1,union_on=1,even_budget,odd_budget,union_budget;
+static int capacity_on,capacity_active;
+static int word[L], counts[N], E[L+1],O[L+1],es=1,os=0;
+static int q,used,odd_counts,even_excess,odd_excess;
+static mask_t seen=1, ee,oo,eo;
+static Result run;
+static Shard *current;
+static FILE *hitout;
+static int io_error;
+static int rem_even[L],rem_odd[L];
+static inline int pop(mask_t x) {
+    return __builtin_popcountll((uint64_t)x)+__builtin_popcountll((uint64_t)(x>>64));
+}
+static inline int parity(int x) { return __builtin_popcount((unsigned)x)&1; }
+static inline mask_t bit(int x) { return (mask_t)1 << x; }
+typedef struct { int size[2],stays[2],occupied_pairs[2]; } Capacity;
+static Capacity capacity[L][N];
+/* Each level owns its state. A sibling overwrites only the next level. */
+static void extend_capacity(int depth,int point,int label,mask_t old_seen) {
+    for(int omitted=0;omitted<N;omitted++) {
+        Capacity *next=&capacity[depth+1][omitted];
+        *next=capacity[depth][omitted];
+        int mask=((1<<N)-1)^(1<<omitted),side=parity(point&mask);
+        next->size[side]++;
+        if(label==omitted) next->stays[side]++;
+        if(old_seen&bit(point^(1<<omitted))) next->occupied_pairs[side]++;
+    }
+}
+/* The caller supplies a simple path; each omitted functional uses actual splits. */
+static uint32_t capacity_splits(int depth,int omitted) {
+    int k=depth+1,r=L-k,mask=((1<<N)-1)^(1<<omitted);
+    const Capacity *state=&capacity[depth][omitted];
+    const int *size=state->size,*stays=state->stays;
+    int cheap[2]={0},pairs[2],available[2];
+    int crossing=depth-stays[0]-stays[1];
+    if(!r) return __builtin_popcount((unsigned)q)==1 ? (uint32_t)1<<size[0] : 0;
+    for(int side=0;side<2;side++) {
+        available[side]=(1<<(N-1))-size[side];
+        pairs[side]=(1<<N)/4-size[side]+state->occupied_pairs[side];
+    }
+    int endpoints[2]={0,q};
+    for(int i=0;i<2;i++) {
+        int endpoint=endpoints[i];
+        if(!(seen&bit(endpoint^(1<<omitted)))) cheap[parity(endpoint&mask)]++;
+    }
+    uint32_t splits=0;
+    for(int x=0;x<=r;x++) {
+        int added[2]={x,r-x},low=crossing,high=crossing+r+1;
+        if(x>available[0] || r-x>available[1]) continue;
+        if(size[0]+x && size[1]+r-x && low<2) low=2;
+        for(int side=0;side<2;side++) {
+            int one=cheap[side]<added[side]?cheap[side]:added[side];
+            int two=(added[side]-one)/2;
+            if(two>pairs[side]) two=pairs[side];
+            int total=size[side]+added[side];
+            int floor=2*total-2*(stays[side]+one+two);
+            int ceiling=2*total-2*stays[side];
+            if(low<floor) low=floor;
+            if(high>ceiling) high=ceiling;
+        }
+        low+=low&1;
+        if(low<=high) splits|=(uint32_t)1<<(size[0]+x);
+    }
+    return splits;
+}
+static void rec(int i) {
+    if (run.aborted || io_error) return;
+    if (current->cap && run.nodes >= current->cap) { run.aborted=1; return; }
+    run.nodes++;
+    if (i==L) {
+        if (q || used!=N || odd_counts || es!=S || os!=T) return;
+        run.candidate_leaves++;
+        if (pop(ee|oo|eo|1)==(1<<N)) {
+            run.hits++;
+            for (int k=0;k<L;k++) if (fputc('0'+word[k],hitout)==EOF) io_error=1;
+            if (fputc('\n',hitout)==EOF || fflush(hitout)==EOF) io_error=1;
+        }
+        return;
+    }
+    if (odd_counts+2*(N-used)>L-i) return;
+    if(capacity_active && i>0) {
+        for(int omitted=0;omitted<N;omitted++) if(!capacity_splits(i,omitted)) {
+            run.capacity_prunes++; return;
+        }
+    }
+    int limit=used<N ? used+1 : N;
+    for (int j=0;j<limit;j++) {
+        if (run.aborted || io_error) return;
+        if (counts[j]>=L-2*(N-1)) continue;
+        if (i<current->length && j!=current->key[i]-'0') continue;
+        int nq=q^(1<<j),last=(i==L-1);
+        if (last && nq) continue; /* q_L is closure, never a prefix state. */
+        int fresh=!last && !(seen&bit(nq));
+        int p=parity(nq),ns=es+(fresh&&!p),nt=os+(fresh&&p);
+        if (ns>S || nt>T || ns+rem_even[i]<S || nt+rem_odd[i]<T) continue;
+        mask_t add_same=0,add_cross=0;
+        int dc_even=0,dc_odd=0;
+        if (fresh) {
+            const int *same=p?O:E, *cross=p?E:O;
+            int same_size=p?os:es,cross_size=p?es:os;
+            for (int a=0;a<same_size;a++) add_same|=bit(nq^same[a]);
+            for (int a=0;a<cross_size;a++) add_cross|=bit(nq^cross[a]);
+            dc_even=pop(add_same&(p?oo:ee));
+            dc_odd=pop(add_cross&eo);
+            if (union_on) {
+                mask_t nu=(p?oo:ee)|add_same, nc=(p?ee:oo);
+                int future_same=S*(S-1)/2+T*(T-1)/2-ns*(ns-1)/2-nt*(nt-1)/2;
+                if (pop(nu|nc)+future_same<(1<<(N-1))-1) { run.union_prunes++; continue; }
+            }
+            if (even_on && even_excess+dc_even>even_budget) { run.even_prunes++; continue; }
+            if (odd_on && odd_excess+dc_odd>odd_budget) { run.odd_prunes++; continue; }
+        }
+        mask_t old_seen=seen,old_ee=ee,old_oo=oo,old_eo=eo;
+        int old_q=q,old_used=used,old_odd=odd_counts;
+        word[i]=j;
+        counts[j]++;
+        odd_counts+=(counts[j]&1)?1:-1;
+        q=nq;
+        if (j==old_used) used++;
+        if(capacity_active && fresh) extend_capacity(i,nq,j,old_seen);
+        if (fresh) {
+            seen|=bit(nq);
+            if (p) { O[os++]=nq; oo|=add_same; }
+            else { E[es++]=nq; ee|=add_same; }
+            eo|=add_cross;
+            even_excess+=dc_even; odd_excess+=dc_odd;
+        }
+        rec(i+1);
+        if (fresh) {
+            if (p) os--; else es--;
+            even_excess-=dc_even; odd_excess-=dc_odd;
+        }
+        seen=old_seen; ee=old_ee; oo=old_oo; eo=old_eo;
+        counts[j]--; q=old_q; used=old_used; odd_counts=old_odd;
+    }
+}
+static int parse_uint(const char *s,uint64_t *out) {
+    if (!*s || *s<'0' || *s>'9') return 0;
+    errno=0; char *end; unsigned long long n=strtoull(s,&end,10);
+    if (errno || *end) return 0;
+    *out=(uint64_t)n; return 1;
+}
+static int parse_split(const char *s) {
+    const char *comma=strchr(s,',');
+    if (!comma || comma==s || strchr(comma+1,',') || comma-s>3) return 0;
+    char left[4]; memcpy(left,s,(size_t)(comma-s)); left[comma-s]=0;
+    uint64_t a,b;
+    if (!parse_uint(left,&a)||!parse_uint(comma+1,&b)||a<1||b<1||a>L/2||b>L/2||a>(1u<<(N-1))||b>(1u<<(N-1))) return 0;
+    S=(int)a; T=(int)b; return 1;
+}
+static int parse_shard(const char *s,Shard *dst,uint64_t cap) {
+    const char *colon=strchr(s,':');
+    size_t len=colon?(size_t)(colon-s):strlen(s);
+    if (len==1 && s[0]=='-') len=0;
+    if (len>L || (colon && !parse_uint(colon+1,&cap))) return 0;
+    int introduced=0;
+    for (size_t k=0;k<len;k++) {
+        int label=s[k]-'0';
+        if (label<0 || label>=N || label>introduced) return 0;
+        if (label==introduced) introduced++;
+        dst->key[k]=s[k];
+    }
+    dst->key[len]=0; dst->length=(int)len; dst->cap=cap;
+    return 1;
+}
+static void write_result(FILE *f,const char *prefix,Result *r,int comma) {
+    fprintf(f,"    {\"prefix\":\"%s\",\"nodes\":%" PRIu64 ",\"candidate_restored_leaves\":%" PRIu64 ",\"all_restored_leaves\":",prefix,r->nodes,r->candidate_leaves);
+    if (!even_on&&!odd_on&&!r->aborted) fprintf(f,"%" PRIu64,r->candidate_leaves); else fputs("null",f);
+    fprintf(f,",\"hits\":%" PRIu64 ",\"even_budget_prunes\":%" PRIu64 ",\"odd_budget_prunes\":%" PRIu64 ",\"union_budget_prunes\":%" PRIu64 ",\"prefix_capacity_prunes\":%" PRIu64 ",\"aborted\":%s,\"complete\":%s,\"seconds\":%.6f}%s\n",r->hits,r->even_prunes,r->odd_prunes,r->union_prunes,r->capacity_prunes,r->aborted?"true":"false",(!r->aborted&&!io_error)?"true":"false",r->seconds,comma?",":"");
+}
+int main(int argc,char **argv) {
+    Shard shards[128]; Result results[128]; int nshards=0;
+    const char *hits_path=NULL,*json_path=NULL; uint64_t cap=0;
+    if (argc<2||!parse_split(argv[1])) { fprintf(stderr,"usage: %s s,t --hits PATH [--json PATH] [--cap N] [--prefix-capacity] [--no-budgets|--no-even-budget|--no-odd-budget] [PREFIX[:CAP]...]\n",argv[0]); return 1; }
+    for (int a=2;a<argc;a++) {
+        const char *arg=argv[a];
+        if (!strcmp(arg,"--prefix-capacity")) { capacity_on=1; continue; }
+        if (!strcmp(arg,"--no-budgets")) { even_on=odd_on=union_on=0; continue; }
+        if (!strcmp(arg,"--no-even-budget")) { even_on=0; continue; }
+        if (!strcmp(arg,"--no-odd-budget")) { odd_on=0; continue; }
+        if (!strcmp(arg,"--no-union-budget")) { union_on=0; continue; }
+        if (!strcmp(arg,"--hits")||!strcmp(arg,"--json")||!strcmp(arg,"--cap")) {
+            if (++a>=argc) { fprintf(stderr,"missing option argument\n"); return 1; }
+            if (!strcmp(arg,"--hits")) { if(hits_path) return 1; hits_path=argv[a]; }
+            else if (!strcmp(arg,"--json")) { if(json_path) return 1; json_path=argv[a]; }
+            else if (!parse_uint(argv[a],&cap)) { fprintf(stderr,"invalid cap\n"); return 1; }
+            continue;
+        }
+        if (nshards==128 || !parse_shard(arg,&shards[nshards],0)) { fprintf(stderr,"invalid shard: %s\n",arg); return 1; }
+        nshards++;
+    }
+    if (!hits_path || (json_path&&!strcmp(hits_path,json_path))) { fprintf(stderr,"distinct explicit --hits PATH required\n"); return 1; }
+    if (!nshards) { memset(&shards[0],0,sizeof shards[0]); nshards=1; }
+    for(int a=0;a<nshards;a++) {
+        if (!shards[a].cap) shards[a].cap=cap;
+        for(int b=0;b<a;b++) {
+            int common=shards[a].length<shards[b].length?shards[a].length:shards[b].length;
+            if (!strncmp(shards[a].key,shards[b].key,(size_t)common)) { fprintf(stderr,"overlapping shards\n"); return 1; }
+        }
+    }
+    capacity_active=capacity_on && N>=2 && L>=4 && L<=(1<<N) && S==L/2 && T==L/2;
+    even_budget=S*(S-1)/2+T*(T-1)/2-((1<<(N-1))-1);
+    odd_budget=S*T-(1<<(N-1));
+    union_budget=S*(S-1)/2+T*(T-1)/2-((1<<(N-1))-1);
+    for(int i=0;i<L;i++) for(int k=i+2;k<L;k++) if(k&1) rem_odd[i]++; else rem_even[i]++;
+    hitout=fopen(hits_path,"wx");
+    if(!hitout) { perror(hits_path); return 1; }
+    FILE *jsonout=NULL;
+    if(json_path) {
+        jsonout=fopen(json_path,"wx");
+        if(!jsonout) { perror(json_path); fclose(hitout); return 1; }
+    }
+    Result total={0}; int done=0;
+    for(int a=0;a<nshards;a++) {
+        memset(&run,0,sizeof run); memset(counts,0,sizeof counts);
+        q=used=odd_counts=even_excess=odd_excess=0; es=1; os=0; E[0]=0;
+        seen=1; ee=oo=eo=0; current=&shards[a];
+        if(capacity_active) {
+            memset(capacity,0,sizeof capacity);
+            for(int omitted=0;omitted<N;omitted++) capacity[0][omitted].size[0]=1;
+        }
+        struct timespec start,end; clock_gettime(CLOCK_MONOTONIC,&start);
+        /* Negative necessary budget proves no universal leaf: skip whole shard. */
+        if (!(even_on&&even_budget<0) && !(odd_on&&odd_budget<0) && !(union_on&&union_budget<0)) rec(0);
+        clock_gettime(CLOCK_MONOTONIC,&end);
+        run.seconds=(double)(end.tv_sec-start.tv_sec)+1e-9*(double)(end.tv_nsec-start.tv_nsec);
+        results[a]=run; done++;
+        total.nodes+=run.nodes; total.candidate_leaves+=run.candidate_leaves; total.hits+=run.hits;
+        total.even_prunes+=run.even_prunes; total.odd_prunes+=run.odd_prunes; total.union_prunes+=run.union_prunes; total.capacity_prunes+=run.capacity_prunes;
+        total.aborted|=run.aborted; total.seconds+=run.seconds;
+        printf("SHARD %s nodes=%" PRIu64 " candidate_restored_leaves=%" PRIu64 " hits=%" PRIu64 " complete=%s seconds=%.3f\n",current->length?current->key:"-",run.nodes,run.candidate_leaves,run.hits,(!run.aborted&&!io_error)?"true":"false",run.seconds); fflush(stdout);
+        if (run.aborted||io_error) break;
+    }
+    printf("TOTAL N=%d L=%d split=%d,%d nodes=%" PRIu64 " candidate_restored_leaves=%" PRIu64 " hits=%" PRIu64 " complete=%s seconds=%.3f\n",N,L,S,T,total.nodes,total.candidate_leaves,total.hits,(!total.aborted&&!io_error)?"true":"false",total.seconds);
+    if(jsonout) {
+        fprintf(jsonout,"{\n  \"prefix_capacity_requested\":%s,\"prefix_capacity_enabled\":%s,\n",capacity_on?"true":"false",capacity_active?"true":"false");
+        fprintf(jsonout,"  \"schema\":1,\"n\":%d,\"length\":%d,\"split\":[%d,%d],\"groups\":\"hamming_weight_parity\",\"even_budget\":%d,\"odd_budget\":%d,\"union_budget\":%d,\"even_budget_enabled\":%s,\"odd_budget_enabled\":%s,\"union_budget_enabled\":%s,\n  \"complete\":%s,\"aborted\":%s,\"requested_shards\":%d,\"completed_or_partial_shards\":%d,\n  \"shards\":[\n",N,L,S,T,even_budget,odd_budget,union_budget,even_on?"true":"false",odd_on?"true":"false",union_on?"true":"false",(!total.aborted&&!io_error)?"true":"false",total.aborted?"true":"false",nshards,done);
+        for(int a=0;a<done;a++) write_result(jsonout,shards[a].key,&results[a],a+1<done);
+        fputs("  ],\n  \"total\":[\n",jsonout); write_result(jsonout,"",&total,0); fputs("  ]\n}\n",jsonout);
+        if(fclose(jsonout)) io_error=1;
+    }
+    if(fclose(hitout)) io_error=1;
+    if(io_error) { fprintf(stderr,"output I/O failure; result not valid\n"); return 1; }
+    return total.aborted?2:0;
+}
diff --git a/research/incremental-prefix-capacity/verify.py b/research/incremental-prefix-capacity/verify.py
new file mode 100644
index 0000000000..f3b797d031
--- /dev/null
+++ b/research/incremental-prefix-capacity/verify.py
@@ -0,0 +1,207 @@
+"""Check incremental census state against pinned scan and independent splits.
+
+Ali Romman, substantial OpenAI Codex assistance. Apache-2.0.
+"""
+from collections import Counter
+import argparse
+import difflib
+from hashlib import sha256
+import json
+import os
+from pathlib import Path
+import platform
+import runpy
+import statistics
+import subprocess
+import sys
+import tempfile
+import time
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+OLD = ROOT/'research/f7-prefix-capacity-engine/census.c'
+
+def need(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+def canonical(value):
+    return json.dumps(value, sort_keys=True, separators=(',', ':'), allow_nan=False)
+
+def authenticate():
+    for row in json.loads((HERE/'SOURCES.json').read_text())['files']:
+        if row['usage'] == 'input':
+            need(sha256((ROOT/row['path']).read_bytes()).hexdigest() == row['sha256'], 'source bytes')
+    before, after = OLD.read_text(), (HERE/'census.c').read_text()
+    delta = ''.join(difflib.unified_diff(before.splitlines(True), after.splitlines(True),
+                                       fromfile='pinned/census.c', tofile='census.c'))
+    need(delta == (HERE/'DELTA.diff').read_text(), 'complete source delta')
+    return before, after
+
+def command(argv, **kwargs):
+    return subprocess.run(list(map(str, argv)), capture_output=True, text=True, timeout=15, **kwargs)
+
+def compile_c(text, path, n, length, sanitize=False):
+    src = path.with_suffix('.c')
+    src.write_text(text)
+    extra = ['-fsanitize=undefined,bounds', '-fno-sanitize-recover=all'] if sanitize else []
+    out = command([os.environ.get('CC', 'cc'), '-O2', '-Wall', '-Wextra', '-Werror', '-std=c11',
+                   f'-DN={n}', f'-DL={length}', *extra, src, '-o', path])
+    need(out.returncode == 0, 'compile: '+out.stderr)
+
+def stable(value):
+    if isinstance(value, dict):
+        return {k: stable(v) for k, v in value.items() if k != 'seconds'}
+    if isinstance(value, list):
+        return [stable(v) for v in value]
+    return value
+
+def run_census(binary, directory, split, flags):
+    with tempfile.TemporaryDirectory(dir=directory) as tmp:
+        tmp = Path(tmp)
+        start = time.perf_counter()
+        out = command([binary, f'{split[0]},{split[1]}', '--hits', tmp/'hits', '--json', tmp/'run', *flags])
+        seconds = time.perf_counter()-start
+        need(out.returncode in (0, 2), 'census failed: '+out.stderr)
+        data = json.loads((tmp/'run').read_text())
+        need((out.returncode == 2) == data['aborted'] and data['complete'] != data['aborted'], 'cap status')
+        leaves = Counter(line[5:] for line in out.stdout.splitlines() if line.startswith('LEAF '))
+        hits = Counter((tmp/'hits').read_text().splitlines())
+        return dict(report=stable(data), leaves=leaves, hits=hits), seconds
+
+def instrument(source):
+    old = '        run.candidate_leaves++;'
+    need(source.count(old) == 1, 'leaf boundary')
+    return source.replace(old, old+'''\n        fputs("LEAF ",stdout);
+        for(int k=0;k<L;k++) fputc('0'+word[k],stdout);
+        fputc('\\n',stdout);''')
+
+def paths(n, length):
+    rows = []
+    def visit(word, points, highest):
+        if word:
+            for omitted in range(n):
+                rows.append((word, points, omitted))
+        if len(points) == length:
+            return
+        for label in range(min(n-1, highest+1)+1):
+            q = points[-1] ^ (1 << label)
+            if q not in points:
+                visit(word+str(label), points+(q,), max(highest, label))
+    visit('', (0,), -1)
+    return rows
+
+def probe_source(source):
+    return '#define main census_main\n'+source+'''
+#undef main
+int main(void) {
+    char prefix[23]; int omitted;
+    while(scanf("%22s %d",prefix,&omitted)==2) {
+        int depth=(int)strlen(prefix); q=0; seen=1;
+        memset(capacity,0,sizeof capacity);
+        for(int v=0;v<N;v++) capacity[0][v].size[0]=1;
+        for(int i=0;i<depth;i++) {
+            word[i]=prefix[i]-'0'; q^=1<<word[i];
+            extend_capacity(i,q,word[i],seen); seen|=bit(q);
+        }
+        printf("%u\\n",capacity_splits(depth,omitted));
+    }
+    return 0;
+}
+'''
+
+def kernel(after, tmp):
+    rows = paths(4, 10)
+    oracle = runpy.run_path(str(ROOT/'research/f7-prefix-matching-capacity/verify.py'))['feasible_splits']
+    expected = [sum(1 << s for s, _ in oracle(points, 4, 10, omitted)) for _, points, omitted in rows]
+    payload = ''.join(f'{word} {omitted}\n' for word, _, omitted in rows)
+    def probe(source, sanitize=False):
+        binary = tmp/'probe'
+        compile_c(probe_source(source), binary, 4, 10, sanitize)
+        out = command([binary], input=payload)
+        need(out.returncode == 0, 'kernel process: '+out.stderr)
+        return list(map(int, out.stdout.splitlines()))
+    need(probe(after) == expected, 'independent split oracle')
+    need(probe(after, True) == expected, 'sanitized split oracle')
+    mutations = {
+        'missing_occupied_pair': ('next->occupied_pairs[side]++;', 'next->occupied_pairs[side]+=0;'),
+        'wrong_mate': ('old_seen&bit(point^(1<<omitted))', 'old_seen&bit(point)'),
+        'lost_parent_state': ('*next=capacity[depth][omitted];', 'memset(next,0,sizeof *next);'),
+        'lost_final_endpoint': ('int endpoints[2]={0,q};', 'int endpoints[2]={0,0};'),
+    }
+    rejected = {}
+    for label, (old, new) in mutations.items():
+        need(after.count(old) == 1, 'mutation boundary')
+        changed = probe(after.replace(old, new))
+        need(len(changed) == len(expected), 'probe output length')
+        first = next((i for i, (a, b) in enumerate(zip(changed, expected)) if a != b), None)
+        need(first is not None, 'mutation survived: '+label)
+        rejected[label] = [rows[first][0], rows[first][2], expected[first], changed[first]]
+    return dict(prefix_functionals=len(rows), mutations=rejected)
+
+def evidence(before, after, tmp):
+    rows = []
+    for n, length in ((2, 4), (3, 6), (4, 8), (4, 10), (5, 12)):
+        binaries = [tmp/'old', tmp/'new']
+        for source, binary in zip((before, after), binaries):
+            compile_c(instrument(source), binary, n, length)
+        for flags in ([], ['--no-budgets'], ['--prefix-capacity'], ['--prefix-capacity', '--no-budgets']):
+            left, _ = run_census(binaries[0], tmp, (length//2,)*2, flags)
+            right, _ = run_census(binaries[1], tmp, (length//2,)*2, flags)
+            need(left == right, 'complete search/report equivalence')
+            rows.append(dict(n=n, length=length, flags=flags, report=left['report']['total'][0],
+                             leaves_sha256=sha256(canonical(left['leaves']).encode()).hexdigest(),
+                             hits_sha256=sha256(canonical(left['hits']).encode()).hexdigest()))
+    # These use the last domain. Every run starts a fresh process and files.
+    boundaries = []
+    for split, flags in (((6, 5), ['--prefix-capacity', '--no-budgets']),
+                         ((6, 6), ['--prefix-capacity', '--no-budgets', '010', '012']),
+                         ((6, 6), ['--prefix-capacity', '--no-budgets', '--cap', '17'])):
+        left, _ = run_census(binaries[0], tmp, split, flags)
+        right, _ = run_census(binaries[1], tmp, split, flags)
+        need(left == right, 'repeat/shard/cap boundary')
+        boundaries.append(dict(split=split, flags=flags, report=left['report']))
+    result = dict(status='PASS_INCREMENTAL_PREFIX_CAPACITY', complete_domain_modes=rows,
+                  boundaries=boundaries, kernel=kernel(after, tmp),
+                  census_sha256=sha256(after.encode()).hexdigest())
+    return result
+
+def timings(before, after, tmp):
+    binaries = {'old': tmp/'old', 'new': tmp/'new'}
+    for name, source in (('old', before), ('new', after)):
+        compile_c(source, binaries[name], 6, 14)
+    samples = {name: [] for name in ('old_on', 'new_on', 'new_off')}
+    receipts = {}
+    for turn in range(7):
+        order = tuple(samples) if turn % 2 == 0 else tuple(reversed(samples))
+        for label in order:
+            name, mode = label.split('_')
+            flags = ['--no-budgets']+(['--prefix-capacity'] if mode == 'on' else [])
+            result, elapsed = run_census(binaries[name], tmp, (7, 7), flags)
+            samples[label].append(elapsed)
+            receipts.setdefault(label, result['report'])
+            need(receipts[label] == result['report'], 'timing run changed report')
+    need(receipts['old_on'] == receipts['new_on'], 'timing traversal changed')
+    medians = {k: statistics.median(v) for k, v in samples.items()}
+    return dict(domain=[6, 14], split=[7, 7], runs=7, seconds=samples, medians=medians,
+                old_on_over_new_on=medians['old_on']/medians['new_on'],
+                new_on_over_new_off=medians['new_on']/medians['new_off'], reports=receipts,
+                compiler=command([os.environ.get('CC', 'cc'), '--version']).stdout,
+                python=sys.version, platform=platform.platform(), machine=platform.machine(),
+                definition='Serialized alternating process-inclusive runs; no compilation or leaf instrumentation in timings.')
+
+if __name__ == '__main__':
+    parser = argparse.ArgumentParser()
+    parser.add_argument('--emit', action='store_true')
+    parser.add_argument('--timings', action='store_true')
+    args = parser.parse_args()
+    expected = None if args.emit or args.timings else json.loads((HERE/'RESULT.json').read_text())
+    before, after = authenticate()
+    with tempfile.TemporaryDirectory() as tmp:
+        result = timings(before, after, Path(tmp)) if args.timings else evidence(before, after, Path(tmp))
+    need(authenticate() == (before, after), 'sources changed during replay')
+    if args.emit or args.timings:
+        print(json.dumps(result, indent=2))
+    else:
+        need(canonical(result) == canonical(expected), 'complete typed receipt')
+        print(result['status'])