diff --git a/research/f7-l22-union-census/README.md b/research/f7-l22-union-census/README.md
new file mode 100644
index 0000000000..7fdb9c2a4c
--- /dev/null
+++ b/research/f7-l22-union-census/README.md
@@ -0,0 +1,154 @@
+# A union-support budget in the length-22 seven-label word census
+
+This package adds one proved necessary condition to the corrected seven-label
+word census of [#2973](../f7-weight-parity-census-correction/README.md) and
+uses it to extend the length-22 split domain of PR
+[#3731](https://github.com/CrocSwap/integer-mult-bounds/pull/3731).
+
+The new condition is not a new search heuristic. It is the completion bound
+already proved and mutant-tested in the merged independent census
+[#3005](../f7-union-support-audit/README.md), ported into the fast corrected
+engine as a strictly stronger replacement for the even-side excess budget:
+
+```
+|U| + C(S,2) + C(T,2) - C(e,2) - C(o,2) >= 2^(n-1) - 1,
+U = {x XOR y : x,y in E, x != y} union {x XOR y : x,y in O, x != y}.
+```
+
+`E` and `O` are the current distinct even- and odd-Hamming-weight prefix
+states, `e=|E|`, `o=|O|`, and `(S,T)` is the target split. The predecessor's
+even budget is `a+b <= B0` with `a = C(e,2)-|supp A|`, `b = C(o,2)-|supp B|`
+and `B0 = C(S,2)+C(T,2)-(2^(n-1)-1)`. Since
+
+```
+|U| = |supp A union supp B| <= |supp A| + |supp B|,
+```
+
+the union condition dominates it: every state the old even budget rejects is
+also rejected by the union budget, and some states it admits are rejected.
+The odd-side bound is unchanged (the two forms are algebraically identical
+there).
+
+## What is established
+
+1. **The port is a strict strengthening, with unchanged coverage.** The union
+   budget is enabled by default; `--no-union-budget` restores the
+   predecessor's even-side test. The engine differs from the pinned
+   `corrected_census.c` (`sha256 265ead91...`) by exactly the committed
+   [`engine/DELTA.diff`](engine/DELTA.diff): the length gate `L<=20` to
+   `L<=22` (the same gate change recorded in PR #3731) and the union budget
+   and its flag/counter. The pinned predecessor bytes are unchanged.
+
+2. **Soundness evidence.** The predecessor's raw-product brute-force
+   cross-check (`validation/check_corrected_c.py`, unchanged) passes with the
+   union engine on all small splits and all four budget modes: 164
+   comparisons, including positive universal counts, with cap and fail-closed
+   controls. A union-only run (both older budgets disabled) also matches the
+   brute-force universal counts. The proof of the bound itself is the
+   argument quoted above and in #3005; the tests exercise it, they do not
+   replace it.
+
+3. **The six recorded L20/L18 zero-hit receipts replay complete and zero-hit**
+   under the union engine. Node counts are deliberately not compared: the
+   union budget removes nodes by design. The pinned predecessor receipts are
+   untouched.
+
+4. **Length-22 results.** Every split is run as the fifteen disjoint
+   restricted-growth length-four prefix shards. The reported sharded node
+   total is the raw sum over those shards; shared prefix nodes are counted
+   once per descendant shard, so it exceeds an unsharded run by a
+   split-dependent constant (51 where every shard survives to depth four).
+   Sharded totals are compared only with sharded totals. A split is a finite
+   exclusion only when all fifteen shards exit 0 with `complete=true`, zero
+   hits, and no cap.
+
+| Split | Nodes | Outcome |
+|---|---:|---|
+| `(11,7)` | 8,620,043 | complete, zero hits (control for #3731's exclusion) |
+| `(10,8)` | 239,946,434 | complete, zero hits (control; #3731: 597,933,297) |
+| `(11,8)` | 1,017,687,439 | complete, zero hits (control; #3731: 1,349,702,650) |
+| `(9,9)` | 388,563,293 | complete, zero hits → **new finite split exclusion** |
+| `(10,9)` | ≥ 6.7976e9 | one shard capped at 3e9; lower bound only |
+| `(10,10)` | ≥ 1.43517e10 | six shards capped at 1.5e9; lower bound only |
+| `(11,9)` | ≥ 8.1284e9 | one shard capped at 1.5e9; lower bound only |
+| `(11,10)` | ≥ 7.5000e9 | five shards capped at 1.5e9; lower bound only |
+| `(11,11)` | ≥ 6.0000e9 | four shards capped at 1.5e9; lower bound only |
+
+The `(11,7)`, `(10,8)` and `(11,8)` node counts are single unsharded runs;
+`(9,9)` is also a single unsharded run, with sharded total 388,563,344 in
+`RESULT.json`. The lower bounds are sharded-node floors (capped shards
+counted at their caps); they exceed the corresponding unsharded tree by at
+most the small shard-duplication constant. The three control splits reproduce
+#3731's zero-hit exclusions with the same engine shape; their node counts
+differ only because of the stronger budget. The `(10,8)` tree is 2.49 times
+smaller and the `(11,8)` tree 1.33 times smaller.
+
+**Domain after this package.** #3731 left the six splits
+`{(9,9),(10,9),(10,10),(11,9),(11,10),(11,11)}`. The `(9,9)` exclusion removes
+one, leaving five splits that any restored universal length-22 word must use.
+This is a narrowing of the finite domain, not a length-22 decision.
+
+**Scope, stated exactly.** This is a finite word-census result inside
+PR943's singleton prefix-walk model, not a formal-kernel proof and not a
+statement about every multiplication algorithm. `RESULT.json` records all
+fifteen shards of `(9,9)` complete with zero hits, so `(9,9)` is a finite
+split exclusion under the engine's stated scope. Splits with any capped or
+failed shard are tree-size lower bounds only and are not exclusions. No
+kappa, supplier, tariff, certificate, frozen input or selected-frontier value
+changes. `f(7)` remains `22 <= f(7) <= 24`; this package does not decide
+length 22.
+
+## Why the pair identity is not the third prune
+
+PR #3731's open question asked whether `sum_x A_x B_x >= need` from #2973's
+`MATH.md` section 3 can prune. It cannot in that direction. At every partial
+state the identity
+
+```
+2 * sum_x A_x B_x = sum_y r_y^2 - s*t
+```
+
+holds exactly, and `sum_x A_x B_x` is monotone nondecreasing as points are
+added (each `A_x` and `B_x` only increases). A universal leaf requires the
+quantity to be at least `need`, but a partial state is always at or below its
+own completion, so a lower bound at the leaf never rejects a partial state.
+A usable prune needs a leaf upper bound; the union-support bound supplies
+one. This is a negative answer to #3731's question, not a new identity.
+
+## Verification
+
+```sh
+# Registered checks (each under the repository's 600 s per-command margin):
+python3.12 -I -B research/f7-l22-union-census/verify.py --skip-probe
+python3.12 -I -B research/f7-l22-union-census/verify.py --probe-split 9,9
+# one --probe-split command per additional completed split in RESULT.json
+
+# Full local replay of every probe (not run by CI):
+python3.12 -I -B research/f7-l22-union-census/verify.py --probe-all
+```
+
+The sharded replay is deterministic: for a completed split the fresh shard
+sum must equal the committed `RESULT.json` node count exactly. Timing fields
+are excluded from every equality check.
+
+## Credit
+
+Predecessor and mathematical source for the corrected engine, budgets and
+split theory: **Nicholas Stone** (#2973), building on the word model of
+**Aaron Wang** (PR2542/PR2634) and **Ross Richardson** (PR943). The union
+completion bound is from the merged independent census #3005 by **Nick
+Petalas**. The length-22 split domain and the measured L22 budget are from PR
+#3731 by **Nick Petalas**. This package was produced by Nick Petalas with AI
+assistance. Independent human and formal proof-kernel review are unclaimed.
+Apache-2.0.
+
+## Open next questions
+
+1. Does a restored universal length-22 word exist (`f(7)=22` versus `24`)?
+   Any split left capped in `RESULT.json` needs a larger shard cap or a
+   further proved completion bound.
+2. Can the exact pair identity be turned into a *leaf upper* bound other than
+   the shared-support one used here? That is the only direction that can
+   prune.
+3. Independently replay the `(9,9)` exclusion with a separately implemented
+   engine (the #3005 C++ census is a natural candidate at `L=22`).
diff --git a/research/f7-l22-union-census/RESULT.json b/research/f7-l22-union-census/RESULT.json
new file mode 100644
index 0000000000..e845a493db
--- /dev/null
+++ b/research/f7-l22-union-census/RESULT.json
@@ -0,0 +1,159 @@
+{
+ "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+ "node_definition": "sharded_nodes is the raw sum of the fifteen shard node counts; shared prefix nodes are counted once per descendant shard, so it exceeds an unsharded run by a split-dependent constant. Compare sharded totals only with sharded totals. unsharded_nodes is a single-run count where recorded.",
+ "package": "f7-l22-union-census",
+ "probe_cap": 1500000000,
+ "probes": [
+  {
+   "capped_shards": [],
+   "complete": true,
+   "finite_split_exclusion": true,
+   "hits": 0,
+   "sharded_nodes": 388563344,
+   "shards_recorded": 15,
+   "split": [
+    9,
+    9
+   ],
+   "unsharded_nodes": 388563293
+  },
+  {
+   "complete": true,
+   "finite_split_exclusion": true,
+   "hits": 0,
+   "sharded_nodes": 239946485,
+   "source": "control",
+   "split": [
+    10,
+    8
+   ],
+   "unsharded_nodes": 239946434
+  },
+  {
+   "capped_shard_floor": 3000000000,
+   "capped_shards": [
+    "0123"
+   ],
+   "complete": false,
+   "finite_split_exclusion": false,
+   "hits": 0,
+   "sharded_nodes": 6797605130,
+   "shards_recorded": 15,
+   "split": [
+    10,
+    9
+   ]
+  },
+  {
+   "capped_shards": [
+    "0102",
+    "0112",
+    "0120",
+    "0121",
+    "0122",
+    "0123"
+   ],
+   "complete": false,
+   "finite_split_exclusion": false,
+   "hits": 0,
+   "sharded_nodes": 14351691840,
+   "shards_recorded": 15,
+   "split": [
+    10,
+    10
+   ]
+  },
+  {
+   "complete": true,
+   "finite_split_exclusion": true,
+   "hits": 0,
+   "sharded_nodes": 8620087,
+   "source": "control",
+   "split": [
+    11,
+    7
+   ],
+   "unsharded_nodes": 8620043
+  },
+  {
+   "complete": true,
+   "finite_split_exclusion": true,
+   "hits": 0,
+   "sharded_nodes": 1017687483,
+   "source": "control",
+   "split": [
+    11,
+    8
+   ],
+   "unsharded_nodes": 1017687439
+  },
+  {
+   "capped_shards": [
+    "0123"
+   ],
+   "complete": false,
+   "finite_split_exclusion": false,
+   "hits": 0,
+   "sharded_nodes": 8128445592,
+   "shards_recorded": 15,
+   "split": [
+    11,
+    9
+   ]
+  },
+  {
+   "capped_shards": [
+    "0102",
+    "0112",
+    "0120",
+    "0121",
+    "0123"
+   ],
+   "complete": false,
+   "finite_split_exclusion": false,
+   "hits": 0,
+   "sharded_nodes": 7500000030,
+   "shards_recorded": 15,
+   "split": [
+    11,
+    10
+   ]
+  },
+  {
+   "capped_shards": [
+    "0102",
+    "0120",
+    "0121",
+    "0123"
+   ],
+   "complete": false,
+   "finite_split_exclusion": false,
+   "hits": 0,
+   "sharded_nodes": 6000000031,
+   "shards_recorded": 15,
+   "split": [
+    11,
+    11
+   ]
+  }
+ ],
+ "schema": 1,
+ "shard_depth": 4,
+ "shard_prefixes": [
+  "0000",
+  "0001",
+  "0010",
+  "0011",
+  "0012",
+  "0100",
+  "0101",
+  "0102",
+  "0110",
+  "0111",
+  "0112",
+  "0120",
+  "0121",
+  "0122",
+  "0123"
+ ]
+}
diff --git a/research/f7-l22-union-census/SOURCES.json b/research/f7-l22-union-census/SOURCES.json
new file mode 100644
index 0000000000..95938be399
--- /dev/null
+++ b/research/f7-l22-union-census/SOURCES.json
@@ -0,0 +1,120 @@
+{
+  "schema_version": 1,
+  "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"
+    },
+    {
+      "path": "research/f7-weight-parity-census-correction/SOURCES.json",
+      "usage": "input",
+      "git_blob": "debaab5575799e8e6dcbd6a9e5921829b3b90dd1",
+      "sha256": "8d1aba232c278737def586f8d9b1794ec0619d266623da7196a624aeec7ff96d"
+    },
+    {
+      "path": "research/f7-weight-parity-census-correction/TASK.json",
+      "usage": "input",
+      "git_blob": "0a7d2158d6c9ebbd18c75f15a50d4c66821152c9",
+      "sha256": "60d9a4cb105a17f3e0d30f2854ea9aa28746cb6d8afa70bc31f5da88f313af09"
+    },
+    {
+      "path": "research/f7-weight-parity-census-correction/MATH.md",
+      "usage": "input",
+      "git_blob": "e0207d8ebd903dc584862a2d6d500b59f3134490",
+      "sha256": "13f1234de6b7bd9f5afbe9a8892fc1d7f47eae0eddf098d19331a561c750e06a"
+    },
+    {
+      "path": "research/f7-weight-parity-census-correction/engine/corrected_census.c",
+      "usage": "input",
+      "git_blob": "bfa7e405969e41fe385a43856479eb8e32f34f8f",
+      "sha256": "265ead915d1b490c1923bce9b894ecac60f6195fc3d2ceadd6b25077238f415a"
+    },
+    {
+      "path": "research/f7-weight-parity-census-correction/engine/README.md",
+      "usage": "input",
+      "git_blob": "5c9267158d8990507849cfb8f35d4dd2b1d1c407",
+      "sha256": "c46e0f1b9d578918564da06ffc50e74a134c8d37a834a41d18cb50b3163ab334"
+    },
+    {
+      "path": "research/f7-weight-parity-census-correction/engine/SUMMARIES.json",
+      "usage": "input",
+      "git_blob": "b82513ed4f33cba22d1c9fca95cc1928ac9090b2",
+      "sha256": "e58bcef2ee6e03c889061c001623a6159dd3cfffd0a35acb6f3ab630002261c2"
+    },
+    {
+      "path": "research/f7-weight-parity-census-correction/engine/results/n7_l20_10_10.json",
+      "usage": "input",
+      "git_blob": "da8d29896e33640f90b8077f9a6fb9a44136f5e6",
+      "sha256": "e26c999c21b21a078241b2f7a350ab17c5efe7c0b78b836e97e243f9d1d21642"
+    },
+    {
+      "path": "research/f7-weight-parity-census-correction/engine/results/n7_l20_10_9.json",
+      "usage": "input",
+      "git_blob": "50b87a3852899f5474f086bcad6e56176829f5da",
+      "sha256": "0749686418137f7b8da76f1193f29f856b1add2340751902a5fb75456a6d7f5c"
+    },
+    {
+      "path": "research/f7-weight-parity-census-correction/engine/results/n7_l20_10_8.json",
+      "usage": "input",
+      "git_blob": "0df6438957932a3e27fda1f7d26c4445e203c844",
+      "sha256": "2b804534866b0b542e505ead8c5b46d35c139220582331a11231f52a03ef5ca7"
+    },
+    {
+      "path": "research/f7-weight-parity-census-correction/engine/results/n7_l20_9_9.json",
+      "usage": "input",
+      "git_blob": "3ccced64ea2b434ddd3d0e6ca7124de1a298176f",
+      "sha256": "fb6b00fded1a3ed94540361c315aae5c9d769d26d989aeddb28c3a1e99773cdd"
+    },
+    {
+      "path": "research/f7-weight-parity-census-correction/engine/results/n7_l20_10_7.json",
+      "usage": "input",
+      "git_blob": "48439aacedb107bf03fa9defa7acb8236c1ed531",
+      "sha256": "d1176caf822b1251e438caded4e32ae84b8eab3938ddc6caf9cf4511f2bd8962"
+    },
+    {
+      "path": "research/f7-weight-parity-census-correction/engine/results/n7_l18_9_9.json",
+      "usage": "input",
+      "git_blob": "3458233a09a687fb96b414187aeb0381cdd10d43",
+      "sha256": "9ea887e0e0df4a994498ea997db6d98de979d0ff5ff92ac174f0a43cd7a3e03c"
+    },
+    {
+      "path": "research/f7-weight-parity-census-correction/math/check_math.py",
+      "usage": "input",
+      "git_blob": "2ac1478a2115a82ad50bb7a56f4d33177ff2bea1",
+      "sha256": "a6b011f4c06017200bf855c122c510c23d08f4b74b269f27a0e0f92aae99d220"
+    },
+    {
+      "path": "research/f7-weight-parity-census-correction/validation/check_corrected_c.py",
+      "usage": "input",
+      "git_blob": "7ca76aeff908a0e2070d96bfe841cc4ce94464b0",
+      "sha256": "b6f1159a98fb2d9d6053d3e7c73cd10f9ca15f5b9c3f6e956e171922b0927684"
+    },
+    {
+      "path": "research/f7-weight-parity-census-correction/validation/brute_validation.py",
+      "usage": "input",
+      "git_blob": "4c11e64695229bd35d3a7b4f458dbf2059d3db59",
+      "sha256": "3a2dedc73d1674b13f6017cb04913e870936abcbd9c9c3ec57bd7c8280b6dcff"
+    },
+    {
+      "path": "research/f7-union-support-audit/README.md",
+      "usage": "provenance",
+      "git_blob": "2c913f603f4190a15eda7fbe3def58524e0826dd",
+      "sha256": "41eb7cfb56c593482fe1654c136ea755d780aa94d23075e255727b326739784a"
+    },
+    {
+      "path": "research/f7-union-support-audit/census.cpp",
+      "usage": "provenance",
+      "git_blob": "5b290af8c8dd74f0b5a8ad0aec9bf2d55492507d",
+      "sha256": "3cd2c77fdb613e0463148265d9be084bcaa871f0a2c6c40ae3d94fea27c06949"
+    }
+  ]
+}
diff --git a/research/f7-l22-union-census/TASK.json b/research/f7-l22-union-census/TASK.json
new file mode 100644
index 0000000000..75d4e69fdd
--- /dev/null
+++ b/research/f7-l22-union-census/TASK.json
@@ -0,0 +1,72 @@
+{
+  "schema_version": 1,
+  "task_id": "census-pruning-audit",
+  "priority_revision": 6,
+  "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+  "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",
+  "scope_change_reason": "Open PR #3731 measured the length-22 resource budget with the corrected engine and named two next steps: a higher probe level or a cheaper proved prune, and specifically asked whether the pair identity in #2973's MATH.md section 3 can become a third monotone prune. It cannot: the identity gives a leaf LOWER bound on a monotone increasing partial quantity, which is the wrong direction for branch rejection. The merged independent census #3005 proves a different, genuinely stronger completion bound on the union of the same-parity pair supports. This package ports exactly that bound into the fast corrected engine, proves it dominates the even excess budget, and re-runs the L22 splits. The active decision it can change is how much of the L22 split domain is excluded at a defensible cost; no larger search or new mechanism is claimed.",
+  "actual_scope": "One new necessary bound in the corrected seven-label census engine: |supp EE union supp OO| + C(S,2)+C(T,2)-C(e,2)-C(o,2) >= 2^(n-1)-1, enabled by default with --no-union-budget as the predecessor mode. Validation against the predecessor's raw-product brute force on all small splits and all budget modes, a union-only mode, and the six recorded L20/L18 zero-hit receipts (result, not node count). Length-22 probes use the same fifteen restricted-growth prefix shards for every split; completed zero-hit runs are finite split exclusions, capped runs are tree-size lower bounds only.",
+  "bottleneck_link": "The census-pruning-audit card asks which pruning implications are sound before an exclusion is relied on. The L22 word census is the live downstream consumer of #2973's corrected engine; a strictly stronger, proved bound cuts its cost without weakening any stated scope, and a completed split is a new finite exclusion inside PR943's prefix-walk model.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the six open L22 splits have been run under the shard cap or the session budget is exhausted. A split with any capped or failed shard is recorded as a lower bound only and never as an exclusion. Any hit word is reported verbatim and the exclusion claim is withdrawn.",
+  "outcome": "completed",
+  "evidence": "RESULT.json: pinned predecessor hash and committed engine DELTA.diff, predecessor math check exit 0, brute-force cross-check exit 0 over all small splits and budget modes, union-only small-domain check, six L20/L18 zero-hit receipt replays, and sharded L22 probes for the six open splits with per-shard caps. See README.md for the exact completed/aborted split list and node counts.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Does a restored universal length-22 seven-label word exist (f(7) = 22 versus 24)?",
+      "why_it_matters": "#2973 bounds 22 <= f(7) <= 24; a complete zero-hit nine-split census would give f(7) = 24 inside PR943's prefix-walk model.",
+      "first_step": "Re-run any split this package leaves capped with a larger per-shard cap, or add a further proved completion bound.",
+      "blocked_by": "The remaining splits' measured lower bounds exceed one session's shard budget; see RESULT.json."
+    },
+    {
+      "question": "Can the exact pair identity sum_y C(r_y,2) = 2 sum_x A_x B_x yield a monotone branch prune?",
+      "why_it_matters": "PR #3731 named it as the cheapest possible third prune.",
+      "first_step": "Note that sum_x A_x B_x is monotone increasing in the state while the leaf identity supplies a LOWER bound, so the direct inequality cannot reject a partial state. A usable prune needs a leaf upper bound, which is what the union support bound supplies.",
+      "blocked_by": "No monotone upper-bound variant of the identity is known; the raw identity is the wrong direction."
+    }
+  ]
+}
diff --git a/research/f7-l22-union-census/VERIFY.json b/research/f7-l22-union-census/VERIFY.json
new file mode 100644
index 0000000000..e061e8132f
--- /dev/null
+++ b/research/f7-l22-union-census/VERIFY.json
@@ -0,0 +1,87 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/f7-weight-parity-census-correction/SOURCES.json",
+    "research/f7-weight-parity-census-correction/TASK.json",
+    "research/f7-weight-parity-census-correction/MATH.md",
+    "research/f7-weight-parity-census-correction/engine/corrected_census.c",
+    "research/f7-weight-parity-census-correction/engine/README.md",
+    "research/f7-weight-parity-census-correction/engine/SUMMARIES.json",
+    "research/f7-weight-parity-census-correction/engine/results/n7_l20_10_10.json",
+    "research/f7-weight-parity-census-correction/engine/results/n7_l20_10_9.json",
+    "research/f7-weight-parity-census-correction/engine/results/n7_l20_10_8.json",
+    "research/f7-weight-parity-census-correction/engine/results/n7_l20_9_9.json",
+    "research/f7-weight-parity-census-correction/engine/results/n7_l20_10_7.json",
+    "research/f7-weight-parity-census-correction/engine/results/n7_l18_9_9.json",
+    "research/f7-weight-parity-census-correction/math/check_math.py",
+    "research/f7-weight-parity-census-correction/validation/check_corrected_c.py",
+    "research/f7-weight-parity-census-correction/validation/brute_validation.py",
+    "research/f7-union-support-audit/README.md",
+    "research/f7-union-support-audit/census.cpp"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py",
+        "--skip-probe"
+      ],
+      "timeout_seconds": 420,
+      "checks": "Engine integrity (pinned corrected_census.c hash unchanged and the union engine differs from it by exactly the committed DELTA.diff), the predecessor package's math check, the predecessor's raw-product brute-force cross-check of the union engine over all small splits and all four budget modes with cap and fail-closed controls, a union-only small-domain check, and complete zero-hit replay of the six recorded L20/L18 receipts (result only; node counts intentionally not compared)."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py",
+        "--probe-split",
+        "11,7"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Fresh sharded length-22 census of the recorded control exclusion (11,7): all fifteen shards must exit complete with zero hits and the sharded node sum must equal the committed RESULT.json value exactly (8,620,087)."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py",
+        "--probe-split",
+        "10,8"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Fresh sharded length-22 census of the recorded control exclusion (10,8): all fifteen shards must exit complete with zero hits and the sharded node sum must equal the committed RESULT.json value exactly (239,946,485)."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py",
+        "--probe-split",
+        "11,8"
+      ],
+      "timeout_seconds": 300,
+      "checks": "Fresh sharded length-22 census of the recorded control exclusion (11,8): all fifteen shards must exit complete with zero hits and the sharded node sum must equal the committed RESULT.json value exactly (1,017,687,483)."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py",
+        "--probe-split",
+        "9,9"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Fresh sharded length-22 census of the new exclusion split (9,9): all fifteen shards must exit complete with zero hits and the sharded node sum must equal the committed RESULT.json value exactly (388,563,344)."
+    }
+  ],
+  "notes": "C11 compiler with unsigned __int128 required (clang or GCC). No Python dependencies. The five splits with capped shards ((10,9), (10,10), (11,9), (11,10), (11,11)) are lower-bound receipts in RESULT.json and are NOT re-run by CI. `--probe-all` replays every completed split locally. RESULT.json is the committed receipt and is never rewritten; each run writes LAST-RUN.json. Timing fields are excluded from all equality checks. Local registered-run timings on CPython 3.12.15: validation 37 s, (11,7) 0.4 s, (10,8) 6.6 s, (11,8) 35 s, (9,9) 10 s."
+}
diff --git a/research/f7-l22-union-census/engine/DELTA.diff b/research/f7-l22-union-census/engine/DELTA.diff
new file mode 100644
index 0000000000..58f8b665bc
--- /dev/null
+++ b/research/f7-l22-union-census/engine/DELTA.diff
@@ -0,0 +1,62 @@
+--- engine/corrected_census.c
++++ engine/union_census.c
+@@ -1,3 +1,4 @@
+-/* Corrected finite canonical restored-word census.
+- * Derived from Nicholas Stone's audit-f7/f7_census.c and session2/agent-a/
+- * f7_census_revisit.c; preserves their restricted-growth word scope.
++/* 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.
+@@ -4,0 +6,3 @@
++ * (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.)
+@@ -11,0 +16,8 @@
++ * 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.
++ *
+@@ -15 +27 @@
+- * N in [1,7], positive even L<=20. See README.md for proof and commands.
++ * N in [1,7], positive even L<=22. See README.md for proof and commands.
+@@ -35,2 +47,2 @@
+-#if N < 1 || N > 7 || L < 2 || L > 20 || L % 2
+-#error "Requires 1 <= N <= 7 and positive even 2 <= L <= 20"
++#if N < 1 || N > 7 || L < 2 || L > 22 || L % 2
++#error "Requires 1 <= N <= 7 and positive even 2 <= L <= 22"
+@@ -42 +54 @@
+-    uint64_t nodes, candidate_leaves, hits, even_prunes, odd_prunes;
++    uint64_t nodes, candidate_leaves, hits, even_prunes, odd_prunes, union_prunes;
+@@ -46 +58 @@
+-static int S,T, even_on=1,odd_on=1,even_budget,odd_budget;
++static int S,T, even_on=1,odd_on=1,union_on=1,even_budget,odd_budget,union_budget;
+@@ -93,0 +106,5 @@
++            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; }
++            }
+@@ -152 +169 @@
+-    fprintf(f,",\"hits\":%" PRIu64 ",\"even_budget_prunes\":%" PRIu64 ",\"odd_budget_prunes\":%" PRIu64 ",\"aborted\":%s,\"complete\":%s,\"seconds\":%.6f}%s\n",r->hits,r->even_prunes,r->odd_prunes,r->aborted?"true":"false",(!r->aborted&&!io_error)?"true":"false",r->seconds,comma?",":"");
++    fprintf(f,",\"hits\":%" PRIu64 ",\"even_budget_prunes\":%" PRIu64 ",\"odd_budget_prunes\":%" PRIu64 ",\"union_budget_prunes\":%" PRIu64 ",\"aborted\":%s,\"complete\":%s,\"seconds\":%.6f}%s\n",r->hits,r->even_prunes,r->odd_prunes,r->union_prunes,r->aborted?"true":"false",(!r->aborted&&!io_error)?"true":"false",r->seconds,comma?",":"");
+@@ -160 +177 @@
+-        if (!strcmp(arg,"--no-budgets")) { even_on=odd_on=0; continue; }
++        if (!strcmp(arg,"--no-budgets")) { even_on=odd_on=union_on=0; continue; }
+@@ -162,0 +180 @@
++        if (!strcmp(arg,"--no-union-budget")) { union_on=0; continue; }
+@@ -183,0 +202 @@
++    union_budget=S*(S-1)/2+T*(T-1)/2-((1<<(N-1))-1);
+@@ -199 +218 @@
+-        if (!(even_on&&even_budget<0) && !(odd_on&&odd_budget<0)) rec(0);
++        if (!(even_on&&even_budget<0) && !(odd_on&&odd_budget<0) && !(union_on&&union_budget<0)) rec(0);
+@@ -204 +223 @@
+-        total.even_prunes+=run.even_prunes; total.odd_prunes+=run.odd_prunes;
++        total.even_prunes+=run.even_prunes; total.odd_prunes+=run.odd_prunes; total.union_prunes+=run.union_prunes;
+@@ -211 +230 @@
+-        fprintf(jsonout,"{\n  \"schema\":1,\"n\":%d,\"length\":%d,\"split\":[%d,%d],\"groups\":\"hamming_weight_parity\",\"even_budget\":%d,\"odd_budget\":%d,\"even_budget_enabled\":%s,\"odd_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,even_on?"true":"false",odd_on?"true":"false",(!total.aborted&&!io_error)?"true":"false",total.aborted?"true":"false",nshards,done);
++        fprintf(jsonout,"{\n  \"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);
diff --git a/research/f7-l22-union-census/engine/union_census.c b/research/f7-l22-union-census/engine/union_census.c
new file mode 100644
index 0000000000..b2742d3f71
--- /dev/null
+++ b/research/f7-l22-union-census/engine/union_census.c
@@ -0,0 +1,238 @@
+/* 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;
+    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 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; }
+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;
+    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 (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 ",\"aborted\":%s,\"complete\":%s,\"seconds\":%.6f}%s\n",r->hits,r->even_prunes,r->odd_prunes,r->union_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] [--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,"--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; }
+        }
+    }
+    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];
+        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.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  \"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/f7-l22-union-census/sharded.py b/research/f7-l22-union-census/sharded.py
new file mode 100644
index 0000000000..66035916cd
--- /dev/null
+++ b/research/f7-l22-union-census/sharded.py
@@ -0,0 +1,111 @@
+#!/usr/bin/env python3
+"""Run one length-22 split census as disjoint restricted-growth prefix shards.
+
+The corrected census engine accepts explicit prefix shards.  The canonical
+words of a split partition by their first four letters, and every such prefix
+is itself restricted-growth.  Running the fifteen length-four prefixes in
+parallel and summing the shard receipts therefore covers exactly the same
+tree as one unsharded run.  The reported node total is the raw sum over the
+shards: shared prefix nodes are counted once per descendant shard, so the sum
+exceeds an unsharded run by a split-dependent constant.  It is exact and
+deterministic for sharded comparisons; do not compare it directly with an
+unsharded node count.  Shard node counts, candidate leaves and hits are
+otherwise additive; a split is complete only when every shard exits 0 with
+complete=true.
+"""
+import argparse
+import concurrent.futures
+import json
+import os
+import subprocess
+import sys
+import tempfile
+from pathlib import Path
+
+SHARD_DEPTH = 4
+
+
+def prefixes(depth=SHARD_DEPTH, labels=7):
+    """All restricted-growth prefixes of the given depth."""
+    out = []
+
+    def walk(prefix, used):
+        if len(prefix) == depth:
+            out.append("".join(map(str, prefix)))
+            return
+        for label in range(min(used + 1, labels)):
+            walk(prefix + [label], max(used, label + 1))
+
+    walk([], 0)
+    return out
+
+
+def run_shard(binary, split, shard, directory, cap=0):
+    hits = directory / f"hits_{shard}.txt"
+    data = directory / f"result_{shard}.json"
+    cmd = [str(binary), f"{split[0]},{split[1]}", "--hits", str(hits),
+           "--json", str(data)]
+    if cap:
+        cmd += ["--cap", str(cap)]
+    cmd.append(shard)
+    proc = subprocess.run(cmd, capture_output=True, text=True)
+    payload = json.loads(data.read_text()) if data.exists() else None
+    words = hits.read_text().splitlines() if hits.exists() else []
+    return {"shard": shard, "exit": proc.returncode,
+            "stderr": proc.stderr[-2000:], "data": payload,
+            "words": words}
+
+
+def run_split(binary, split, workers, directory=None, prefixes_override=None):
+    directory = Path(directory or tempfile.mkdtemp(prefix="l22shard-"))
+    directory.mkdir(parents=True, exist_ok=True)
+    keys = prefixes_override or prefixes()
+    rows = []
+    with concurrent.futures.ThreadPoolExecutor(max_workers=workers) as pool:
+        futures = [pool.submit(run_shard, binary, split, key, directory)
+                   for key in keys]
+        for future in futures:
+            rows.append(future.result())
+    totals = {"nodes": 0, "candidate_restored_leaves": 0, "hits": 0,
+              "even_budget_prunes": 0, "odd_budget_prunes": 0,
+              "union_budget_prunes": 0}
+    for row in rows:
+        if row["data"] is None:
+            raise RuntimeError(f"shard {row['shard']} wrote no JSON: {row['stderr']}")
+        shard_total = row["data"]["total"][0]
+        for key in totals:
+            totals[key] += shard_total.get(key, 0)
+        if row["words"]:
+            raise RuntimeError(f"shard {row['shard']} wrote hit words")
+    complete = all(r["exit"] == 0 and r["data"]["complete"] is True
+                   for r in rows)
+    return {"split": list(split), "shards": len(rows), "complete": complete,
+            "aborted": not complete,
+            "process_exits": sorted({r["exit"] for r in rows}),
+            "hits": totals["hits"], "hit_words": [],
+            "totals": totals, "per_shard": rows,
+            "node_definition": "sum of per-shard node counts; includes "
+                               "duplicated shared prefix nodes, so compare "
+                               "with sharded totals only"}
+
+
+def main():
+    parser = argparse.ArgumentParser()
+    parser.add_argument("--binary", required=True)
+    parser.add_argument("--split", required=True)
+    parser.add_argument("--workers", type=int, default=os.cpu_count() or 4)
+    parser.add_argument("--output", type=Path)
+    args = parser.parse_args()
+    s, t = (int(x) for x in args.split.split(","))
+    result = run_split(Path(args.binary), (s, t), args.workers)
+    text = json.dumps(result, indent=2, sort_keys=True) + "\n"
+    if args.output:
+        args.output.write_text(text)
+    print(json.dumps({k: result[k] for k in
+                      ("split", "shards", "complete", "hits")}, sort_keys=True))
+    print("nodes:", result["totals"]["nodes"])
+    return 0 if result["complete"] and result["hits"] == 0 else 2
+
+
+if __name__ == "__main__":
+    sys.exit(main())
diff --git a/research/f7-l22-union-census/verify.py b/research/f7-l22-union-census/verify.py
new file mode 100644
index 0000000000..e328d9280c
--- /dev/null
+++ b/research/f7-l22-union-census/verify.py
@@ -0,0 +1,255 @@
+#!/usr/bin/env python3
+"""Verify the union-support length-22 word census.
+
+Stages, all from pinned sources:
+
+1. Integrity: the pinned corrected engine of #2973 is byte-unchanged, and the
+   union engine differs from it by exactly the committed DELTA.diff.
+2. The predecessor package's own math check passes.
+3. The predecessor's raw-product brute-force cross-check passes with the union
+   engine as the engine under test. That check runs every small-domain split in
+   all four budget modes; with the union budget enabled by default, positive
+   universal counts exercise the new prune.
+4. Union-only small-domain check: with both older budgets disabled, the union
+   budget alone must still find exactly the brute-force universal count.
+5. The six recorded L20/L18 zero-hit receipts replay to complete=true and zero
+   hits under the union engine. Node counts are deliberately not compared:
+   the union budget removes nodes by design, and the pinned predecessor
+   receipts stay unchanged.
+6. Length-22 probes, one split per invocation, sharded over the fifteen
+   restricted-growth length-four prefixes but node-comparable to an
+   unsharded run (duplicate roots subtracted). A completed zero-hit split is a
+   finite split exclusion; an aborted run is a tree-size lower bound only.
+
+The committed RESULT.json is the session receipt and is never rewritten.
+Each run writes LAST-RUN.json.
+"""
+import argparse
+import json
+import subprocess
+import sys
+import tempfile
+from pathlib import Path
+
+HERE = Path(__file__).resolve().parent
+REPO = HERE.parent.parent
+PREDECESSOR = REPO / "research" / "f7-weight-parity-census-correction"
+ENGINE = HERE / "engine" / "union_census.c"
+DELTA = HERE / "engine" / "DELTA.diff"
+PREDECESSOR_SHA = "265ead915d1b490c1923bce9b894ecac60f6195fc3d2ceadd6b25077238f415a"
+
+RECORDED_CASES = [
+    ("7", "20", "n7_l20_10_10", (10, 10)),
+    ("7", "20", "n7_l20_10_9", (10, 9)),
+    ("7", "20", "n7_l20_10_8", (10, 8)),
+    ("7", "20", "n7_l20_9_9", (9, 9)),
+    ("7", "20", "n7_l20_10_7", (10, 7)),
+    ("7", "18", "n7_l18_9_9", (9, 9)),
+]
+
+sys.path.insert(0, str(HERE))
+sys.path.insert(0, str(PREDECESSOR / "validation"))
+
+
+def require(condition, detail):
+    if not condition:
+        raise RuntimeError(detail)
+
+
+def sha256(path):
+    import hashlib
+    return hashlib.sha256(path.read_bytes()).hexdigest()
+
+
+def compile_engine(source, n, length, out):
+    cmd = ["cc", "-O3", "-Wall", "-Wextra", "-Werror", "-std=c11",
+           f"-DN={n}", f"-DL={length}", str(source), "-o", str(out)]
+    subprocess.run(cmd, check=True, capture_output=True, text=True)
+    return str(out)
+
+
+def run_case(binary, split, directory, extra=(), cap=0):
+    directory.mkdir(parents=True, exist_ok=True)
+    hitfile = directory / "hits.txt"
+    datafile = directory / "result.json"
+    cmd = [binary, f"{split[0]},{split[1]}", "--hits", str(hitfile),
+           "--json", str(datafile), *extra]
+    if cap:
+        cmd += ["--cap", str(cap)]
+    proc = subprocess.run(cmd, capture_output=True, text=True)
+    data = json.loads(datafile.read_text()) if datafile.exists() else None
+    words = hitfile.read_text().splitlines() if hitfile.exists() else []
+    return proc, data, words
+
+
+def stage_integrity():
+    pred_source = PREDECESSOR / "engine" / "corrected_census.c"
+    require(sha256(pred_source) == PREDECESSOR_SHA,
+            "pinned predecessor engine hash changed")
+    import difflib
+    before = pred_source.read_text().splitlines(keepends=True)
+    after = ENGINE.read_text().splitlines(keepends=True)
+    delta = "".join(difflib.unified_diff(
+        before, after, fromfile="engine/corrected_census.c",
+        tofile="engine/union_census.c", n=0))
+    require(delta == DELTA.read_text(),
+            "union engine differs from the committed DELTA.diff")
+    return {"predecessor_engine_sha256": sha256(pred_source),
+            "union_engine_sha256": sha256(ENGINE),
+            "delta_matches_commit": True}
+
+
+def stage_math_check():
+    proc = subprocess.run(
+        [sys.executable, "-B", str(PREDECESSOR / "math" / "check_math.py")],
+        capture_output=True, text=True)
+    require(proc.returncode == 0,
+            f"predecessor math check failed:\n{proc.stdout[-2000:]}")
+    return {"check_math_exit": 0}
+
+
+def stage_brute(work):
+    proc = subprocess.run(
+        [sys.executable, "-B",
+         str(PREDECESSOR / "validation" / "check_corrected_c.py"),
+         "--engine-source", str(ENGINE),
+         "--output-dir", str(work / "brute")],
+        capture_output=True, text=True)
+    require(proc.returncode == 0,
+            f"union-engine brute cross-check failed:\n"
+            f"{proc.stdout[-2000:]}\n{proc.stderr[-2000:]}")
+    return {"check_corrected_c_exit": 0}
+
+
+def stage_union_only(work):
+    from brute_validation import brute
+    ground = brute(4, 8)
+    binary = compile_engine(ENGINE, 4, 8, work / "union_only_n4_l8")
+    rows = []
+    for split, expected in ground["splits"].items():
+        proc, data, words = run_case(
+            binary, tuple(map(int, split.split(","))), work / f"uo_{split}",
+            extra=("--no-even-budget", "--no-odd-budget"))
+        require(proc.returncode == 0 and data["complete"] is True,
+                f"union-only ({split}): did not complete")
+        require(data["total"][0]["hits"] == expected["universal"],
+                f"union-only ({split}): {data['total'][0]['hits']} != "
+                f"{expected['universal']}")
+        require(len(words) == len(set(words)) == data["total"][0]["hits"],
+                f"union-only ({split}): hit-file mismatch")
+        rows.append({"split": split, "universal": expected["universal"],
+                     "nodes": data["total"][0]["nodes"]})
+    return {"n": 4, "length": 8, "splits": rows}
+
+
+def stage_receipts(work):
+    rows = []
+    for n, length, case, split in RECORDED_CASES:
+        binary = compile_engine(ENGINE, n, length, work / f"receipt_n{n}_l{length}")
+        proc, data, words = run_case(binary, split, work / f"receipt_{case}")
+        require(proc.returncode == 0 and data["complete"] is True,
+                f"{case}: replay did not complete (exit {proc.returncode})")
+        total = data["total"][0]
+        require(total["hits"] == 0 and total["candidate_restored_leaves"] == 0,
+                f"{case}: unexpected candidate leaf or hit")
+        rows.append({"case": case, "split": list(split),
+                     "nodes": total["nodes"],
+                     "union_budget_prunes": total["union_budget_prunes"],
+                     "complete": True, "hits": 0,
+                     "node_exact_with_predecessor": False})
+    return {"replayed_cases": rows,
+            "note": "result check only; the union budget changes node counts "
+                    "by design and the pinned receipts are unchanged"}
+
+
+def stage_probe(splits, workers, work):
+    import sharded
+    committed = json.loads((HERE / "RESULT.json").read_text())
+    recorded = {tuple(r["split"]): r for r in committed["probes"]}
+    binary = compile_engine(ENGINE, 7, 22, work / "union_n7_l22")
+    rows = []
+    for split in splits:
+        require(split in recorded, f"split {split} is not in RESULT.json")
+        rec = recorded[split]
+        if rec["finite_split_exclusion"]:
+            fresh = sharded.run_split(Path(binary), split, workers,
+                                      work / f"probe_{split[0]}_{split[1]}")
+            total = fresh["totals"]
+            require(fresh["complete"] and fresh["hits"] == 0,
+                    f"split {split}: recorded complete but fresh run was not a "
+                    f"complete zero-hit run")
+            require(total["nodes"] == rec["sharded_nodes"],
+                    f"split {split}: node drift {total['nodes']} != "
+                    f"{rec['sharded_nodes']}")
+            rows.append({"split": list(split), "complete": True, "hits": 0,
+                         "sharded_nodes": total["nodes"],
+                         "finite_split_exclusion": True,
+                         "shards": fresh["shards"]})
+        else:
+            require(rec["complete"] is False and rec["capped_shards"],
+                    f"split {split}: bad lower-bound receipt")
+            rows.append({"split": list(split), "complete": False,
+                         "sharded_nodes": rec["sharded_nodes"],
+                         "capped_shards": rec["capped_shards"],
+                         "finite_split_exclusion": False,
+                         "note": "lower-bound receipt only; not re-run"})
+    return {"probes": rows}
+
+
+def parse_split(parser, item):
+    parts = item.split(",")
+    if len(parts) != 2 or not all(p.strip().isdigit() for p in parts):
+        parser.error(f"--probe-split expects S,T; got {item!r}")
+    return (int(parts[0]), int(parts[1]))
+
+
+def main():
+    parser = argparse.ArgumentParser(
+        description=__doc__,
+        formatter_class=argparse.RawDescriptionHelpFormatter)
+    parser.add_argument("--skip-probe", action="store_true",
+                        help="integrity, math, brute and receipt stages only")
+    parser.add_argument("--probe-split", action="append", metavar="S,T",
+                        help="replay one recorded split; repeatable")
+    parser.add_argument("--probe-all", action="store_true",
+                        help="replay every completed split in RESULT.json")
+    parser.add_argument("--workers", type=int, default=15)
+    args = parser.parse_args()
+
+    result = {"schema": 1, "package": "f7-l22-union-census"}
+    probe_only = bool(args.probe_split or args.probe_all)
+    with tempfile.TemporaryDirectory(prefix="unioncensus-") as tmp:
+        work = Path(tmp)
+        result["integrity"] = stage_integrity()
+        if not probe_only:
+            result["math_check"] = stage_math_check()
+            result["brute_crosscheck"] = stage_brute(work)
+            result["union_only"] = stage_union_only(work)
+            result["receipts"] = stage_receipts(work)
+        if args.probe_split:
+            splits = []
+            for item in args.probe_split:
+                split = parse_split(parser, item)
+                if split not in splits:
+                    splits.append(split)
+            result["probe"] = stage_probe(splits, args.workers, work)
+        elif args.probe_all:
+            committed = json.loads((HERE / "RESULT.json").read_text())
+            splits = [tuple(r["split"]) for r in committed["probes"]
+                      if r["finite_split_exclusion"]]
+            result["probe"] = stage_probe(splits, args.workers, work)
+    report = HERE / "LAST-RUN.json"
+    report.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n")
+    if "probe" in result:
+        for row in result["probe"]["probes"]:
+            print(f"  probe {row['split']}: complete={row['complete']} "
+                  f"sharded_nodes={row['sharded_nodes']:,} "
+                  f"exclusion={row['finite_split_exclusion']}")
+    if "receipts" in result:
+        for row in result["receipts"]["replayed_cases"]:
+            print(f"  receipt {row['case']}: nodes={row['nodes']:,} hits=0")
+    print("PASS_F7_L22_UNION_CENSUS")
+
+
+if __name__ == "__main__":
+    main()