diff --git a/research/f7-firing-n5-length-census/README.md b/research/f7-firing-n5-length-census/README.md
new file mode 100644
index 0000000000..d44d8dfeb2
--- /dev/null
+++ b/research/f7-firing-n5-length-census/README.md
@@ -0,0 +1,111 @@
+# The fixed L/2 firing set at n = 5 beyond length 16
+
+**Claim type: a scoped proof for L ≥ 26, plus an independent census through
+L = 24. No new κ.** It answers #4322's open question 1: at `n = 5` the first
+length at which every functional is sound is **26**. The selected conditional
+κ stays `0.001672660197076918`.
+
+## Object
+
+[PR #4322](https://github.com/CrocSwap/integer-mult-bounds/pull/4322)
+(unpaidmoon) shows that the fixed `L/2` substitution's firing set is not
+monotone in length at `n = 4`: it is empty at `L = 14, 16` by a flat-excess
+cap. At `n = 5` it found the firing set still monotone through `L = 16`.
+
+Its open question 1 asks: **for n = 5, which even length first makes every
+functional sound?**
+
+The model is #4322's:
+
+- canonical first-occurrence words;
+- simple restored prefix walks on `F_2^n`, universal when the difference set
+  of the prefix states is all of `F_2^n`;
+- a nonzero mask fires when `base < excess ≤ base + d²`, with
+  `base = (L/2)(L/2−1) − (2^(n−1) − 1)`.
+
+## Results
+
+**1. Soundness from L = 26 (proof).** At `n = 5` a level set is an affine
+4-flat. By enumerating all `2^16` subsets of `F_2^4`, the maximum excess of a
+`k`-subset is:
+
+| k | 0–3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | 12 | 13 | 14 | 15 | 16 |
+|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
+| max excess | 0 | 3 | 3 | 8 | 14 | 21 | 21 | 30 | 40 | 51 | 63 | 76 | 90 | 105 |
+
+A split `(s, t)` therefore has excess at most `e(s) + e(t)`. This cap is at
+most `base(5, L)` for every split exactly from `L = 26`. So every functional
+is sound on **every** 26-, 28-, 30- or 32-point subset, not only on walks. At
+`L = 24` the cap leaves only the `(8, 16)` split. A firing word there must
+contain an entire level set of its mask.
+
+**2. Census through L = 24.**
+
+| L | closed | universal | false prunes | firing masks |
+|---:|---:|---:|---:|---|
+| 12 | 3,695 | 828 | 2,856 | 24 |
+| 14 | 33,922 | 24,787 | 56,686 | 25 (all of weight ≤ 3) |
+| 16 | 267,890 | 263,140 | 447,912 | 25 |
+| 18 | 1,737,048 | 1,737,048 | 1,812,996 | **28**: adds `27, 29, 30` (weight 4) |
+| 20 | 9,019,738 | 9,019,738 | 5,357,220 | **30**: adds `15, 23` |
+| 22 | 35,938,056 | 35,938,056 | 11,569,998 | **30**: every mask but `31` |
+| 24 | 103,944,140 | 103,944,140 | 14,151,156 | **28**: `15` and `23` fall silent again |
+
+- **Not monotone at n = 5 either.** The firing set stays nested through
+  `L = 22`. At `L = 24` the weight-4 masks `15` and `23`, which fired at 20
+  and 22, fall silent, and the all-ones mask `31` never fires. By the cap,
+  every word that fires at `L = 24` contains an entire level set of its mask.
+- **Answer.** Something still fires at `L = 24`, and the cap proves every
+  functional sound from `L = 26`. So the first all-sound length at `n = 5` is
+  **26**. This is two steps later than the length-14 collapse at `n = 4`.
+
+**Agreement with the predecessors.** The census reproduces the published
+per-mask rows exactly: #3699's `(4,8)`, `(4,10)` and `(5,12)`, #3733's
+`(4,12)` and `(5,14)`, both on main, and #4322's new `(5,16)` row. It also
+confirms #4322's `n = 4` silence at `L = 14, 16`.
+
+## Method and independence
+
+Nothing is imported from #4322.
+
+- **`verify.py`**, standard library, rebuilds the 16-point flat caps, and
+  reruns the census itself for every `n = 4` case and for `n = 5` at
+  `L = 12, 14, 16`. That includes #4322's full `(5,16)` row, in about 50
+  seconds.
+- **`census.c`** is a separate C enumerator for the lengths Python cannot
+  reach. Its recorded runs in `evidence/CENSUS-RUNS.txt` are bound to the
+  source by SHA256. They match every published row and the Python census at
+  `(5,16)`, and give the new lengths 18, 20, 22 and 24.
+- **The C runs are local evidence.** CI reads them and does not recompile.
+  `(5,22)` took about 17 minutes and `(5,24)` about 56 CPU-minutes.
+- **Vendored file.** #4322's `verify.py` is vendored byte-identically only
+  for its literal `EXPECTED_5_16` row, which is read with `ast.literal_eval`
+  and never run.
+
+## Not covered
+
+- `(7, 18)` and `(7, 20)`, and `n ≥ 6`.
+- Any change to a retained seven-label exclusion.
+
+## Reproduce
+
+```sh
+python3.12 -B research/f7-firing-n5-length-census/verify.py
+cc -O2 -o census research/f7-firing-n5-length-census/census.c && ./census 5 24
+```
+
+The first prints `PASS_F7_FIRING_N5_LENGTH_CENSUS` in about a minute.
+
+## Open next questions
+
+None for `n = 5`: open question 1 is decided. #4322's open question 3, whether
+a larger `n` repeats a collapse after its firing set fills, now has a second
+data point. At `n = 5` the set shrinks from 30 to 28 masks at `L = 24` and is
+empty from 26.
+
+## Credit
+
+The model, the `n = 4` theorem and the open question are unpaidmoon's (#4322),
+building on Nick Petalas's #3699 and #3733, Nicholas Stone's #2973 and the
+PR943 walk. Prepared by Ryanson Jonathan with substantial Claude Code (Claude
+Opus 5.5) assistance. Apache-2.0.
diff --git a/research/f7-firing-n5-length-census/SOURCES.json b/research/f7-firing-n5-length-census/SOURCES.json
new file mode 100644
index 0000000000..fcfba8aa31
--- /dev/null
+++ b/research/f7-firing-n5-length-census/SOURCES.json
@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+      "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+    }
+  ]
+}
diff --git a/research/f7-firing-n5-length-census/TASK.json b/research/f7-firing-n5-length-census/TASK.json
new file mode 100644
index 0000000000..7091f77fa0
--- /dev/null
+++ b/research/f7-firing-n5-length-census/TASK.json
@@ -0,0 +1,60 @@
+{
+  "schema_version": 1,
+  "task_id": "census-pruning-audit",
+  "priority_revision": 7,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "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": "Decide for n = 5 which even length first makes every fixed L/2 functional sound (#4322 open question 1): prove soundness from L = 26 by the 16-point flat cap and run an independent census through L = 24.",
+  "scope_change_reason": "The card's census-pruning question at n = 5 was left open by #4322 beyond L = 16.",
+  "bottleneck_link": "Where the fixed substitution falsely prunes decides which census exclusions it can safely shortcut.",
+  "budget_minutes": 45,
+  "stop_rule": "Stop once the first all-sound length at n = 5 is decided.",
+  "outcome": "completed",
+  "evidence": "verify.py: 16-point flat caps by full enumeration prove every subset sound at n = 5 exactly from L = 26; Python census reproduces #3699, #3733 and #4322 rows including (5,16); recorded census.c runs match them and give L = 18, 20, 22, 24 with 1,737,048 / 9,019,738 / 35,938,056 / 103,944,140 closed (all universal) and firing sets of 28, 30, 30, 28 masks; nested through 22, then masks 15 and 23 fall silent at 24; mask 31 never fires; so the first all-sound length is 26 and the n = 5 firing set is not monotone.",
+  "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance",
+  "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance in reading, verifier implementation and writing; no independent human or proof-kernel review.",
+  "no_open_questions_reason": "#4322's open question 1 is decided at n = 5: the first all-sound length is 26.",
+  "open_questions": []
+}
diff --git a/research/f7-firing-n5-length-census/VERIFY.json b/research/f7-firing-n5-length-census/VERIFY.json
new file mode 100644
index 0000000000..f4006b25bf
--- /dev/null
+++ b/research/f7-firing-n5-length-census/VERIFY.json
@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "16-point and 8-point flat caps by enumeration; cap soundness from L = 26; Python census for n = 4 (L = 8..16) and n = 5 (L = 12, 14, 16) against #3699/#3733 on main and #4322's vendored (5,16) row; recorded census.c runs bound by SHA256, matching all published rows; L = 18..24 firing sets of 28, 30, 30, 28, nested through 22, masks 15 and 23 silent at 24; first all-sound length 26."
+    }
+  ]
+}
diff --git a/research/f7-firing-n5-length-census/census.c b/research/f7-firing-n5-length-census/census.c
new file mode 100644
index 0000000000..88ef2dca5f
--- /dev/null
+++ b/research/f7-firing-n5-length-census/census.c
@@ -0,0 +1,66 @@
+/* Canonical simple restored walks on F_2^n and the fixed L/2 firing census.
+ * Usage: ./census n L   -> prints closed, universal, false prunes and per-mask counts.
+ * Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0.
+ */
+#include <stdint.h>
+#include <stdio.h>
+#include <stdlib.h>
+
+static int n, L, base;
+static int word[64], st[64];
+static uint64_t closed, universal, prunes, per_mask[64];
+
+static void classify(void) {
+    closed++;
+    int N = 1 << n;
+    uint64_t sum = 0;                      /* difference set, as a bit mask over F_2^n */
+    for (int i = 0; i < L; i++)
+        for (int j = 0; j < L; j++) sum |= 1ULL << (st[i] ^ st[j]);
+    if (sum != (N == 64 ? ~0ULL : ((1ULL << N) - 1))) return;
+    universal++;
+    for (int m = 1; m < N; m++) {
+        uint64_t seen[2] = {0, 0};
+        int size[2] = {0, 0};
+        for (int i = 0; i < L; i++) size[__builtin_popcount(st[i] & m) & 1]++;
+        for (int i = 0; i < L; i++) {
+            int si = __builtin_popcount(st[i] & m) & 1;
+            for (int j = i + 1; j < L; j++)
+                if ((__builtin_popcount(st[j] & m) & 1) == si) seen[si] |= 1ULL << (st[i] ^ st[j]);
+        }
+        long excess = 0;
+        for (int s = 0; s < 2; s++)
+            excess += (long)size[s] * (size[s] - 1) / 2 - __builtin_popcountll(seen[s]);
+        long d = (size[0] - size[1]) / 2;
+        if (base < excess && excess <= base + d * d) { prunes++; per_mask[m]++; }
+    }
+}
+
+static void walk(int depth, int state, uint64_t visited, int maxlab) {
+    if (depth == L) { if (state == 0) classify(); return; }
+    int top = maxlab + 1 < n - 1 ? maxlab + 1 : n - 1;
+    for (int lab = 0; lab <= top; lab++) {
+        int nxt = state ^ (1 << lab);
+        if (depth == L - 1) { if (nxt != 0) continue; }
+        else if ((visited >> nxt) & 1) continue;
+        word[depth] = lab;
+        st[depth + 1 < L ? depth + 1 : 0] = depth + 1 < L ? nxt : 0;
+        walk(depth + 1, nxt, visited | (1ULL << nxt), lab > maxlab ? lab : maxlab);
+    }
+}
+
+int main(int argc, char **argv) {
+    if (argc != 3) { fprintf(stderr, "usage: census n L\n"); return 2; }
+    n = atoi(argv[1]); L = atoi(argv[2]);
+    if (n < 1 || n > 6 || L < 2 || L % 2 || L > (1 << n)) { fprintf(stderr, "domain\n"); return 2; }
+    base = (L / 2) * (L / 2 - 1) - ((1 << (n - 1)) - 1);
+    st[0] = 0;
+    walk(0, 0, 1ULL, -1);
+    printf("n=%d L=%d closed=%llu universal=%llu prunes=%llu", n, L,
+           (unsigned long long)closed, (unsigned long long)universal, (unsigned long long)prunes);
+    int fired = 0;
+    for (int m = 1; m < (1 << n); m++) fired += per_mask[m] > 0;
+    printf(" firing_masks=%d\n", fired);
+    for (int m = 1; m < (1 << n); m++)
+        if (per_mask[m]) printf("mask %d %llu\n", m, (unsigned long long)per_mask[m]);
+    return 0;
+}
diff --git a/research/f7-firing-n5-length-census/evidence/CENSUS-RUNS.txt b/research/f7-firing-n5-length-census/evidence/CENSUS-RUNS.txt
new file mode 100644
index 0000000000..82f32df77b
--- /dev/null
+++ b/research/f7-firing-n5-length-census/evidence/CENSUS-RUNS.txt
@@ -0,0 +1,237 @@
+# Recorded runs of census.c (SHA256 b907a74467e23c370e0de2867138490d76b7ab0994133f7b6eb108a73ebfc137)
+# Apple clang 21.0.0, arm64, macOS 27.2; built with: cc -O2 -o census census.c; run: ./census n L
+# Local evidence: CI does not rerun these. Wall time (some runs shared the machine): (5,18) 29 s, (5,20) 193 s, (5,22) 998 s; (5,24) 3,344 CPU s (8,321 s wall, the machine slept during the run).
+n=4 L=8 closed=29 universal=22 prunes=44 firing_masks=9
+mask 1 6
+mask 2 6
+mask 3 5
+mask 4 4
+mask 5 1
+mask 6 5
+mask 8 8
+mask 9 4
+mask 12 5
+n=4 L=10 closed=110 universal=110 prunes=190 firing_masks=10
+mask 1 20
+mask 2 20
+mask 3 10
+mask 4 23
+mask 5 8
+mask 6 16
+mask 8 37
+mask 9 18
+mask 10 10
+mask 12 28
+n=4 L=12 closed=314 universal=314 prunes=150 firing_masks=13
+mask 1 16
+mask 2 16
+mask 3 9
+mask 4 18
+mask 5 10
+mask 6 11
+mask 8 22
+mask 9 11
+mask 10 10
+mask 11 4
+mask 12 15
+mask 13 4
+mask 14 4
+n=4 L=14 closed=392 universal=392 prunes=0 firing_masks=0
+n=4 L=16 closed=112 universal=112 prunes=0 firing_masks=0
+n=5 L=12 closed=3695 universal=828 prunes=2856 firing_masks=24
+mask 1 248
+mask 2 248
+mask 3 96
+mask 4 278
+mask 5 143
+mask 6 119
+mask 7 25
+mask 8 221
+mask 9 41
+mask 10 105
+mask 11 15
+mask 12 175
+mask 13 10
+mask 14 26
+mask 16 361
+mask 17 140
+mask 18 100
+mask 19 50
+mask 20 64
+mask 21 4
+mask 22 32
+mask 24 241
+mask 25 44
+mask 28 70
+n=5 L=14 closed=33922 universal=24787 prunes=56686 firing_masks=25
+mask 1 4112
+mask 2 4112
+mask 3 2385
+mask 4 4197
+mask 5 1568
+mask 6 2574
+mask 7 356
+mask 8 4434
+mask 9 1630
+mask 10 1552
+mask 11 492
+mask 12 3684
+mask 13 334
+mask 14 487
+mask 16 8093
+mask 17 3013
+mask 18 2085
+mask 19 904
+mask 20 1677
+mask 21 309
+mask 22 903
+mask 24 5326
+mask 25 917
+mask 26 170
+mask 28 1372
+n=5 L=16 closed=267890 universal=263140 prunes=447912 firing_masks=25
+mask 1 35036
+mask 2 35036
+mask 3 17298
+mask 4 34635
+mask 5 13022
+mask 6 18872
+mask 7 2206
+mask 8 38495
+mask 9 13005
+mask 10 12896
+mask 11 3325
+mask 12 25332
+mask 13 2270
+mask 14 2910
+mask 16 65350
+mask 17 23887
+mask 18 18146
+mask 19 5547
+mask 20 15733
+mask 21 2747
+mask 22 6120
+mask 24 40473
+mask 25 5741
+mask 26 1728
+mask 28 8102
+n=5 L=18 closed=1737048 universal=1737048 prunes=1812996 firing_masks=28
+mask 1 144688
+mask 2 144688
+mask 3 64602
+mask 4 146366
+mask 5 53936
+mask 6 72729
+mask 7 8124
+mask 8 166566
+mask 9 51727
+mask 10 51865
+mask 11 11028
+mask 12 96790
+mask 13 7990
+mask 14 10574
+mask 16 261092
+mask 17 95179
+mask 18 76248
+mask 19 20676
+mask 20 67672
+mask 21 11660
+mask 22 22936
+mask 24 160772
+mask 25 22754
+mask 26 8894
+mask 27 352
+mask 28 32384
+mask 29 352
+mask 30 352
+n=5 L=20 closed=9019738 universal=9019738 prunes=5357220 firing_masks=30
+mask 1 407776
+mask 2 407776
+mask 3 208105
+mask 4 416060
+mask 5 161481
+mask 6 224376
+mask 7 26750
+mask 8 468149
+mask 9 169769
+mask 10 159516
+mask 11 34588
+mask 12 291915
+mask 13 26134
+mask 14 35737
+mask 15 20
+mask 16 697719
+mask 17 282629
+mask 18 229987
+mask 19 73455
+mask 20 210528
+mask 21 40303
+mask 22 77528
+mask 23 266
+mask 24 470974
+mask 25 81022
+mask 26 34194
+mask 27 1090
+mask 28 117309
+mask 29 1032
+mask 30 1032
+n=5 L=22 closed=35938056 universal=35938056 prunes=11569998 firing_masks=30
+mask 1 843444
+mask 2 843444
+mask 3 474372
+mask 4 855275
+mask 5 383057
+mask 6 503436
+mask 7 81714
+mask 8 947301
+mask 9 390647
+mask 10 368335
+mask 11 91189
+mask 12 634562
+mask 13 74801
+mask 14 99836
+mask 15 40
+mask 16 1331066
+mask 17 595816
+mask 18 497749
+mask 19 196145
+mask 20 465869
+mask 21 108244
+mask 22 197804
+mask 23 380
+mask 24 965123
+mask 25 211783
+mask 26 97188
+mask 27 952
+mask 28 308586
+mask 29 920
+mask 30 920
+n=5 L=24 closed=103944140 universal=103944140 prunes=14151156 firing_masks=28
+mask 1 1004286
+mask 2 1004286
+mask 3 578724
+mask 4 1011532
+mask 5 474180
+mask 6 602794
+mask 7 123908
+mask 8 1124810
+mask 9 501051
+mask 10 464410
+mask 11 150698
+mask 12 737598
+mask 13 134182
+mask 14 156056
+mask 16 1555470
+mask 17 687481
+mask 18 595508
+mask 19 270140
+mask 20 578477
+mask 21 173625
+mask 22 281321
+mask 24 1061009
+mask 25 283885
+mask 26 154315
+mask 27 8564
+mask 28 415718
+mask 29 8564
+mask 30 8564
diff --git a/research/f7-firing-n5-length-census/vendor/NOTICE.md b/research/f7-firing-n5-length-census/vendor/NOTICE.md
new file mode 100644
index 0000000000..84293d270c
--- /dev/null
+++ b/research/f7-firing-n5-length-census/vendor/NOTICE.md
@@ -0,0 +1,12 @@
+# Vendored file
+
+`pr4322-verify.py` is a byte-identical copy of
+`research/f7-monotone-firing-classification/verify.py` from
+[PR #4322](https://github.com/CrocSwap/integer-mult-bounds/pull/4322) at head
+`22c60f6687ec49e7eb6082bb450173bbed5478ef` (Git blob
+`b2b9d49d04a223819e4c47d47770ca4723017a71`).
+
+It is copied, not pinned, because that PR head is not reachable from canonical main.
+This package never imports or runs it. `verify.py` checks its SHA256 and reads only the
+literal `EXPECTED_5_16` dictionary, #4322's frozen (5,16) per-mask row, with
+`ast.literal_eval`. It is unpaidmoon's work, Apache-2.0, as its SPDX header states.
diff --git a/research/f7-firing-n5-length-census/vendor/pr4322-verify.py b/research/f7-firing-n5-length-census/vendor/pr4322-verify.py
new file mode 100644
index 0000000000..b2b9d49d04
--- /dev/null
+++ b/research/f7-firing-n5-length-census/vendor/pr4322-verify.py
@@ -0,0 +1,317 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: Apache-2.0
+"""Firing-set monotonicity for the fixed L/2 word-budget substitution.
+
+The walk is the PR943 singleton prefix walk: q_0 = 0 and
+q_{i+1} = q_i XOR e_{w_i}. A word is simple when the L prefix states are
+distinct, restored when it closes at 0 with even label counts, and universal
+when those states sum to the whole space. The retained engines replace the
+exact collision budget base + d^2 by the fixed balanced budget
+
+    base(n, L) = (L/2) * (L/2 - 1) - (2^{n-1} - 1),
+
+where d = (s - t) / 2 and s, t are the two functional class sizes. A
+functional fires on a universal word when
+
+    base < excess <= base + d^2.
+
+Counts below are canonical first-occurrence words, the same normal form as
+#3699 and #3733. No predecessor package is imported.
+"""
+
+import sys
+from itertools import combinations
+
+# Published per-mask false-prune counts. (4,8), (4,10) and (5,12) are #3699.
+# (4,12) and (5,14) are #3733's committed RESULT.json.
+PUBLISHED = {
+    (4, 8): {1: 6, 2: 6, 3: 5, 4: 4, 5: 1, 6: 5, 8: 8, 9: 4, 12: 5},
+    (4, 10): {1: 20, 2: 20, 3: 10, 4: 23, 5: 8, 6: 16, 8: 37, 9: 18,
+              10: 10, 12: 28},
+    (4, 12): {1: 16, 2: 16, 3: 9, 4: 18, 5: 10, 6: 11, 8: 22, 9: 11,
+              10: 10, 11: 4, 12: 15, 13: 4, 14: 4},
+    (5, 12): {1: 248, 2: 248, 3: 96, 4: 278, 5: 143, 6: 119, 7: 25,
+              8: 221, 9: 41, 10: 105, 11: 15, 12: 175, 13: 10, 14: 26,
+              16: 361, 17: 140, 18: 100, 19: 50, 20: 64, 21: 4, 22: 32,
+              24: 241, 25: 44, 28: 70},
+    (5, 14): {1: 4112, 2: 4112, 3: 2385, 4: 4197, 5: 1568, 6: 2574, 7: 356,
+              8: 4434, 9: 1630, 10: 1552, 11: 492, 12: 3684, 13: 334, 14: 487,
+              16: 8093, 17: 3013, 18: 2085, 19: 904, 20: 1677, 21: 309,
+              22: 903, 24: 5326, 25: 917, 26: 170, 28: 1372},
+}
+
+# Frozen (5,16) receipt from this enumerator. The published rows above are the
+# check that the same code still reproduces #3699 and #3733 before this row is
+# trusted. Both excess routes must rebuild it.
+EXPECTED_5_16 = {
+    1: 35036, 2: 35036, 3: 17298, 4: 34635, 5: 13022, 6: 18872, 7: 2206,
+    8: 38495, 9: 13005, 10: 12896, 11: 3325, 12: 25332, 13: 2270, 14: 2910,
+    16: 65350, 17: 23887, 18: 18146, 19: 5547, 20: 15733, 21: 2747, 22: 6120,
+    24: 40473, 25: 5741, 26: 1728, 28: 8102,
+}
+
+WITNESS_4_12 = (0, 1, 0, 2, 0, 1, 0, 3, 1, 2, 1, 3)
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def base_budget(n, length):
+    require(length % 2 == 0 and n >= 1, "even positive domain")
+    half = length // 2
+    return half * (half - 1) - ((1 << (n - 1)) - 1)
+
+
+def flat_excess(points):
+    """Collision excess of one subset of the model flat F_2^3."""
+    points = list(points)
+    size = len(points)
+    if size < 2:
+        return 0
+    support = 0
+    for i in range(size):
+        left = points[i]
+        for j in range(i + 1, size):
+            support |= 1 << (left ^ points[j])
+    return size * (size - 1) // 2 - support.bit_count()
+
+
+def flat_maxima():
+    """Maximum excess of a k-subset of an affine 3-flat, for every k."""
+    maxima = {}
+    for size in range(9):
+        maxima[size] = max(
+            (flat_excess(subset) for subset in combinations(range(8), size)),
+            default=0,
+        )
+    return maxima
+
+
+def prefix_states(word):
+    state = 0
+    states = []
+    for label in word:
+        states.append(state)
+        state ^= 1 << label
+    return tuple(states), state
+
+
+def class_excesses(states, mask):
+    """Both excess routes, plus the even and odd class sizes."""
+    even = []
+    odd = []
+    for point in states:
+        (odd if (point & mask).bit_count() & 1 else even).append(point)
+    counter_excess = 0
+    set_excess = 0
+    for side in (even, odd):
+        size = len(side)
+        if size < 2:
+            continue
+        pairs = size * (size - 1) // 2
+        bits = 0
+        seen = set()
+        for i in range(size):
+            left = side[i]
+            for j in range(i + 1, size):
+                difference = left ^ side[j]
+                bits |= 1 << difference
+                seen.add(difference)
+        counter_excess += pairs - bits.bit_count()
+        set_excess += pairs - len(seen)
+    return counter_excess, set_excess, len(even), len(odd)
+
+
+def fires(n, length, states, mask):
+    counter_excess, set_excess, even, odd = class_excesses(states, mask)
+    require(counter_excess == set_excess, "excess routes disagree")
+    require((even - odd) % 2 == 0, "class sizes")
+    gap = (even - odd) // 2
+    base = base_budget(n, length)
+    return base < counter_excess <= base + gap * gap, counter_excess, even, odd, gap, base
+
+
+def enumerate_canonical(n, length):
+    words = []
+    stack = [(0, 1, -1, 0, ())]
+    while stack:
+        state, visited, max_label, depth, word = stack.pop()
+        if depth == length:
+            if state == 0:
+                words.append(word)
+            continue
+        top = min(max_label + 1, n - 1)
+        if depth == length - 1:
+            for label in range(top + 1):
+                if state ^ (1 << label) == 0:
+                    stack.append((0, visited, max(max_label, label), depth + 1, word + (label,)))
+        else:
+            for label in range(top + 1):
+                nxt = state ^ (1 << label)
+                if ((visited >> nxt) & 1) == 0:
+                    stack.append((nxt, visited | (1 << nxt), max(max_label, label),
+                                  depth + 1, word + (label,)))
+    return words
+
+
+def canonical_form(word):
+    names = {}
+    out = []
+    for label in word:
+        if label not in names:
+            names[label] = len(names)
+        out.append(names[label])
+    return tuple(out)
+
+
+def enumerate_unconstrained_forms(n, length):
+    forms = set()
+    stack = [(0, 1, 0, ())]
+    while stack:
+        state, visited, depth, word = stack.pop()
+        if depth == length:
+            if state == 0:
+                forms.add(canonical_form(word))
+            continue
+        closing = depth == length - 1
+        for label in range(n):
+            nxt = state ^ (1 << label)
+            if closing:
+                if nxt == 0:
+                    stack.append((0, visited, depth + 1, word + (label,)))
+            elif ((visited >> nxt) & 1) == 0:
+                stack.append((nxt, visited | (1 << nxt), depth + 1, word + (label,)))
+    return forms
+
+
+def is_universal(states, n):
+    reached = 0
+    full = (1 << (1 << n)) - 1
+    for left in states:
+        for right in states:
+            reached |= 1 << (left ^ right)
+    return reached == full
+
+
+def classify(n, length):
+    """Return closed count, universal count, and per-mask false-prune counts."""
+    counts = {}
+    closed = 0
+    universal = 0
+    masks = range(1, 1 << n)
+    for word in enumerate_canonical(n, length):
+        closed += 1
+        states, end = prefix_states(word)
+        require(end == 0, "canonical word did not close")
+        require(len(set(states)) == length, "canonical word is not simple")
+        if not is_universal(states, n):
+            continue
+        universal += 1
+        for mask in masks:
+            if fires(n, length, states, mask)[0]:
+                counts[mask] = counts.get(mask, 0) + 1
+    return closed, universal, counts
+
+
+def firing_set(counts):
+    return {mask for mask, hits in counts.items() if hits}
+
+
+def check_flat_bound():
+    maxima = flat_maxima()
+    require(maxima == {0: 0, 1: 0, 2: 0, 3: 0, 4: 3, 5: 3, 6: 8, 7: 14, 8: 21},
+            "flat excess maxima")
+    # A 14-point set omits two points of F_2^4. They lie in one level set or
+    # in both, so every functional splits the set as (8,6) or (7,7).
+    require(maxima[8] + maxima[6] == 29, "fourteen-point excess cap")
+    require(maxima[7] + maxima[7] == 28, "balanced fourteen-point excess cap")
+    require(29 < base_budget(4, 14) == 35, "(4,14) cap is below the substituted budget")
+    require(maxima[8] + maxima[8] == 42 < base_budget(4, 16) == 49,
+            "(4,16) cap is below the substituted budget")
+    return maxima
+
+
+def check_published_and_new():
+    found = {}
+    for n, length in ((4, 8), (4, 10), (4, 12), (4, 14), (4, 16), (5, 12), (5, 14), (5, 16)):
+        closed, universal, counts = classify(n, length)
+        found[(n, length)] = (closed, universal, counts)
+        if (n, length) in PUBLISHED:
+            require(counts == PUBLISHED[(n, length)],
+                    "per-mask counts disagree with the published receipt at %s" % ((n, length),))
+    require(found[(4, 8)][:2] == (29, 22), "(4,8) census")
+    require(found[(4, 10)][:2] == (110, 110), "(4,10) census")
+    require(found[(4, 12)][:2] == (314, 314), "(4,12) census")
+    require(sum(found[(4, 12)][2].values()) == 150, "(4,12) prune total")
+    require(found[(4, 14)] == (392, 392, {}), "(4,14) census is universal and silent")
+    require(found[(4, 16)] == (112, 112, {}), "(4,16) census is universal and silent")
+    require(found[(5, 12)][:2] == (3695, 828), "(5,12) census")
+    require(sum(found[(5, 12)][2].values()) == 2856, "(5,12) prune total")
+    require(found[(5, 14)][:2] == (33922, 24787), "(5,14) census")
+    require(sum(found[(5, 14)][2].values()) == 56686, "(5,14) prune total")
+    require(found[(5, 16)][0] == 267890, "(5,16) closed count")
+    require(found[(5, 16)][1] == 263140, "(5,16) universal count")
+    require(found[(5, 16)][2] == EXPECTED_5_16, "(5,16) per-mask counts")
+    require(sum(EXPECTED_5_16.values()) == 447912, "(5,16) prune total")
+    return found
+
+
+def check_monotonicity(found):
+    sets = {key: firing_set(counts) for key, (_, _, counts) in found.items()}
+    require(sets[(4, 8)] < sets[(4, 10)] < sets[(4, 12)],
+            "n=4 firing sets grow through length 12")
+    require(sets[(4, 14)] == set() and sets[(4, 16)] == set(),
+            "n=4 firing sets are empty at lengths 14 and 16")
+    require(not sets[(4, 12)] <= sets[(4, 14)],
+            "the length-12 firing set was expected to escape length 14")
+    weight_at_most_three = {mask for mask in range(1, 32) if mask.bit_count() <= 3}
+    require(sets[(5, 12)] < sets[(5, 14)] == sets[(5, 16)] == weight_at_most_three,
+            "n=5 firing set stabilises at weight at most 3")
+    require(26 not in sets[(5, 12)] and 26 in sets[(5, 14)],
+            "mask 11010 is the (5,12) exception and it fires at (5,14)")
+    return sets
+
+
+def check_witness_and_forms():
+    states, end = prefix_states(WITNESS_4_12)
+    require(end == 0 and states == (0, 1, 3, 2, 6, 7, 5, 4, 12, 14, 10, 8),
+            "witness prefix states")
+    require(is_universal(states, 4), "witness universality")
+    fired, excess, even, odd, gap, base = fires(4, 12, states, 1)
+    require(fired and (excess, even, odd, gap, base) == (24, 8, 4, 2, 23),
+            "witness mask-1 bill")
+    for n, length in ((4, 8), (4, 10), (4, 12), (4, 14), (4, 16)):
+        forms = enumerate_unconstrained_forms(n, length)
+        canonical = set(enumerate_canonical(n, length))
+        require(forms == canonical, "enumerators disagree at %s" % ((n, length),))
+
+
+def main():
+    maxima = check_flat_bound()
+    found = check_published_and_new()
+    sets = check_monotonicity(found)
+    check_witness_and_forms()
+    print(
+        "PASS_F7_MONOTONE_FIRING_CLASSIFICATION "
+        "flat_max=%s "
+        "n4_firing=%s "
+        "n5_firing=%s "
+        "witness=010201031213 "
+        "mask1_fires_at_4_12=%s "
+        "mask1_fires_at_4_14=%s "
+        "no_new_kappa=true"
+        % (
+            [maxima[k] for k in range(9)],
+            [len(sets[(4, length)]) for length in (8, 10, 12, 14, 16)],
+            [len(sets[(5, length)]) for length in (12, 14, 16)],
+            1 in sets[(4, 12)],
+            1 in sets[(4, 14)],
+        )
+    )
+    return 0
+
+
+if __name__ == "__main__":
+    sys.exit(main())
diff --git a/research/f7-firing-n5-length-census/verify.py b/research/f7-firing-n5-length-census/verify.py
new file mode 100644
index 0000000000..0dbbafe742
--- /dev/null
+++ b/research/f7-firing-n5-length-census/verify.py
@@ -0,0 +1,161 @@
+#!/usr/bin/env python3
+"""The fixed L/2 firing set at n = 5 beyond length 16: flat cap and census.
+
+Model of #4322: canonical first-occurrence words on F_2^n, simple restored prefix walks,
+universal when the difference set of the prefix states is all of F_2^n; a nonzero mask fires
+when base < excess <= base + d^2, base(n, L) = (L/2)(L/2 - 1) - (2^(n-1) - 1).
+This file proves soundness at n = 5 for L >= 26 by the 16-point flat cap, reruns the small
+census in Python, and checks the recorded runs of census.c (local evidence) against #3699,
+#3733 and #4322 on main or vendored, and for the new lengths. No code from #4322.
+Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0.
+"""
+import ast
+import hashlib
+import json
+from pathlib import Path
+import re
+import sys
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+VENDORED_SHA256 = "b4f7196a7dff95973ce1c5ea52628fda5c992dc2cd7bde58734d4fe886bf33e0"
+
+
+def need(condition, message):
+    if not condition:
+        raise AssertionError(message)
+
+
+def base(n, L):
+    return (L // 2) * (L // 2 - 1) - ((1 << (n - 1)) - 1)
+
+
+def excess(points):
+    diffs, k = set(), len(points)
+    for i in range(k):
+        for j in range(i + 1, k):
+            diffs.add(points[i] ^ points[j])
+    return k * (k - 1) // 2 - len(diffs)
+
+
+def flat_caps(dim):
+    """max excess of a k-subset of F_2^dim, every k, by full enumeration"""
+    caps = [0] * ((1 << dim) + 1)
+    for s in range(1 << (1 << dim)):
+        pts = [x for x in range(1 << dim) if s >> x & 1]
+        caps[len(pts)] = max(caps[len(pts)], excess(pts))
+    return caps
+
+
+def census(n, L):
+    """(closed, universal, prunes, per-mask counts) over canonical words"""
+    out = [0, 0, 0, {}]
+    full = (1 << (1 << n)) - 1
+    b = base(n, L)
+
+    def rec(depth, state, visited, top, states):
+        if depth == L:
+            if state:
+                return
+            out[0] += 1
+            diff = 0
+            for x in states:
+                for y in states:
+                    diff |= 1 << (x ^ y)
+            if diff != full:
+                return
+            out[1] += 1
+            for m in range(1, 1 << n):
+                sides = ([], [])
+                for x in states:
+                    sides[bin(x & m).count("1") & 1].append(x)
+                e = excess(sides[0]) + excess(sides[1])
+                d = (len(sides[0]) - len(sides[1])) // 2
+                if b < e <= b + d * d:
+                    out[2] += 1
+                    out[3][m] = out[3].get(m, 0) + 1
+            return
+        for lab in range(min(top + 1, n - 1) + 1):
+            nxt = state ^ (1 << lab)
+            if depth == L - 1:
+                if nxt == 0:
+                    rec(depth + 1, 0, visited, max(top, lab), states)
+            elif not visited >> nxt & 1:
+                rec(depth + 1, nxt, visited | 1 << nxt, max(top, lab), states + [nxt])
+    rec(0, 0, 1, -1, [0])
+    return out
+
+
+def main():
+    # 1. the flat cap: at n = 5 a level set is an affine 4-flat, so a split (s, t) has excess <= e(s) + e(t)
+    caps = flat_caps(4)
+    need(caps == [0, 0, 0, 0, 3, 3, 8, 14, 21, 21, 30, 40, 51, 63, 76, 90, 105], "16-point flat caps")
+    need(flat_caps(3) == [0, 0, 0, 0, 3, 3, 8, 14, 21], "8-point caps agree with #4322's table")
+    open_lengths = []
+    for L in range(12, 33, 2):
+        live = [s for s in range(max(0, L - 16), min(16, L) + 1) if caps[s] + caps[L - s] > base(5, L)]
+        if live:
+            open_lengths.append(L)
+    need(open_lengths == [12, 14, 16, 18, 20, 22, 24], "cap proves every subset sound at n = 5 exactly from L = 26")
+
+    # 2. small census in Python, against #3699 / #3733 on main
+    d3699 = {(r["n"], r["L"]): r for r in json.loads((ROOT / "research/f7-bit0-functional-classification/RESULT.json").read_text())["domains"]}
+    d3733 = {(r["n"], r["L"]): r for r in json.loads((ROOT / "research/f7-functional-independent-check/RESULT.json").read_text())["new_domains"]}
+    published = {k: {int(m): v["count"] for m, v in r["records"].items()} for k, r in d3699.items() if k[0] >= 4}
+    published.update({k: {int(m): c for m, c in r["per_mask_counts"].items()} for k, r in d3733.items() if k[0] >= 4})
+    raw = (HERE / "vendor/pr4322-verify.py").read_bytes()
+    need(hashlib.sha256(raw).hexdigest() == VENDORED_SHA256, "vendored #4322 verify.py")
+    expected_5_16 = ast.literal_eval(re.search(r"EXPECTED_5_16 = (\{.*?\})\n", raw.decode(), re.S).group(1))
+    published[5, 16] = expected_5_16
+    totals = {}
+    for key in [(4, 8), (4, 10), (4, 12), (4, 14), (4, 16), (5, 12), (5, 14), (5, 16)]:
+        closed, univ, prunes, per = census(*key)
+        totals[key] = (closed, univ, prunes)
+        if key in published:
+            need(per == published[key], f"Python census {key} matches the published per-mask row")
+        else:
+            need(prunes == 0, f"Python census {key}: nothing fires (#4322's theorem)")
+    need(totals[5, 16] == (267890, 263140, 447912), "Python census (5,16) totals match #4322")
+
+    # 3. recorded C runs: bound to census.c, matching every published row, then the new lengths
+    text = (HERE / "evidence/CENSUS-RUNS.txt").read_text()
+    need(f"census.c (SHA256 {hashlib.sha256((HERE / 'census.c').read_bytes()).hexdigest()})" in text, "runs recorded for this census.c")
+    runs, cur = {}, None
+    for line in text.splitlines():
+        if line.startswith("n="):
+            f = dict(kv.split("=") for kv in line.split())
+            cur = (int(f["n"]), int(f["L"]))
+            runs[cur] = {"closed": int(f["closed"]), "universal": int(f["universal"]),
+                         "prunes": int(f["prunes"]), "firing": int(f["firing_masks"]), "per": {}}
+        elif line.startswith("mask "):
+            _, m, c = line.split()
+            runs[cur]["per"][int(m)] = int(c)
+    for key, row in published.items():
+        if key in runs:
+            need(runs[key]["per"] == row, f"C census {key} matches the published row")
+    need(runs[5, 16]["per"] == expected_5_16 and (runs[5, 16]["closed"], runs[5, 16]["universal"], runs[5, 16]["prunes"]) == totals[5, 16], "C census (5,16) matches #4322 and the Python census")
+    new = {L: runs[5, L] for L in (18, 20, 22, 24)}
+    sets = {L: set(runs[5, L]["per"]) for L in (12, 14, 16, 18, 20, 22, 24)}
+    order = sorted(sets)
+    need([len(sets[L]) for L in order] == [24, 25, 25, 28, 30, 30, 28], "n = 5 firing-set sizes 24, 25, 25, 28, 30, 30, 28")
+    need(all(sets[a] <= sets[b] for a, b in zip(order[:-1], order[1:-1])), "n = 5 firing sets nested from 12 through 22")
+    need(sets[22] == set(range(1, 31)), "at L = 22 every mask but 31 fires")
+    need(sets[24] == sets[22] - {15, 23}, "at L = 24 masks 15 and 23 fall silent: the n = 5 firing set is not monotone")
+    need(all(r["closed"] == r["universal"] for L, r in new.items()), "from L = 18 every closed word is universal")
+    need(runs[5, 24]["prunes"] > 0, "something still fires at L = 24, so with the cap the first all-sound length is 26")
+    # at L = 24 the cap leaves only the (8, 16) split: every firing word there contains a whole level set of its mask
+    need([s for s in range(8, 17) if caps[s] + caps[24 - s] > base(5, 24)] == [8, 16], "L = 24: only the 8/16 split survives the cap")
+
+    print(json.dumps({
+        "status": "PASS_F7_FIRING_N5_LENGTH_CENSUS",
+        "cap_sound_from": 26,
+        "cap_open_lengths": open_lengths,
+        "n5": {str(L): {k: v for k, v in r.items() if k != "per"} for L, r in sorted(new.items())},
+        "first_all_sound_length_n5": 26,
+        "silent_at_24": sorted(set(range(1, 32)) - sets[24]),
+        "new_kappa_claimed": False,
+    }, indent=1))
+
+
+if __name__ == "__main__":
+    sys.exit(main())