diff --git a/research/f7-firing-threshold-all-n/README.md b/research/f7-firing-threshold-all-n/README.md
new file mode 100644
index 0000000000..162f1dbb76
--- /dev/null
+++ b/research/f7-firing-threshold-all-n/README.md
@@ -0,0 +1,142 @@
+# The first all-sound length of the fixed L/2 substitution, for every n ≥ 5
+
+**Claim type: a proof for every n ≥ 5, with finite checks and explicit
+witnesses. No new κ.** The selected conditional κ stays
+`0.001672660197076918`.
+
+## Object
+
+[PR #4322](https://github.com/CrocSwap/integer-mult-bounds/pull/4322)
+(unpaidmoon) studies the fixed `L/2` substitution on prefix walks of `F_2^n`.
+A nonzero mask fires on a universal simple restored word when
+
+```text
+base < excess <= base + d^2,     base(n, L) = (L/2)(L/2 - 1) - (2^(n-1) - 1).
+```
+
+It found that the firing set is empty from `L = 14` at `n = 4`, and it left
+three questions open:
+
+- the first all-sound length at `n = 5`;
+- whether larger `n` repeat the collapse;
+- whether "the firing set eventually becomes empty for every n" (it says
+  neither of its results shows this).
+
+[#4348](https://github.com/CrocSwap/integer-mult-bounds/pull/4348) answered
+the first by census: the answer is 26.
+
+## Theorem
+
+For every `n ≥ 5`, the first even length at which no mask fires on any
+universal canonical word is exactly
+
+```text
+L*(n) = 2^n - 2 floor(sqrt(2^(n-1) - 1)).
+```
+
+From `L*(n)` up to `2^n`, every functional is sound on **every** `L`-point
+subset of `F_2^n`. At `L*(n) − 2` a weight-one mask fires on an explicit
+word. Values:
+
+| n | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 12 | 16 | 20 |
+|---|---:|---:|---:|---:|---:|---:|---:|---:|---:|---:|
+| `L*` | 14* | 26 | 54 | 114 | 234 | 482 | 980 | 4006 | 65174 | 1047128 |
+
+`n = 4` (marked *) is #4322's theorem: there the closed form would give 12,
+but another split binds. `2^n − L*(n) ≈ 2^((n+1)/2)`. The answer at `n = 5`
+agrees with #4348's census.
+
+So the collapse recurs for every `n`, and only near-Hamiltonian lengths are
+safe for large `n`.
+
+## Proof
+
+**1. Min-sumset cap.** For `A ⊆ F_2^k` with `|A| > 2^(d−1)`,
+`|A + A| ≥ 2^d`.
+
+By Kneser's theorem, `|A+A| ≥ 2|A+H| − |H|`, where `H` is the stabilizer of
+`A+A`, of order `2^h`.
+
+- If `h ≥ d`, then `|A+A| ≥ |H| ≥ 2^d`.
+- Otherwise `A+H` has `a > 2^(d−1−h)` cosets, so
+  `|A+A| ≥ (2a−1)2^h ≥ 2^d + 2^h`.
+
+Equality holds for `A` inside a subgroup of order `2^d`.
+
+A level set of a nonzero functional is an affine flat, and differences in
+characteristic 2 are sums. So a `k`-point side has excess at most
+`e(k) = C(k,2) − 2^⌈log₂k⌉ + 1`, and a split `(s,t)` has excess at most
+`e(s) + e(t)`.
+
+**2. The binding split.** Write `s = 2^(n−1)` and `L = 2(s − j)`.
+
+For the split `(s, s − 2j)`, a full level set against the rest, with
+`s − 2j > 2^(n−2)`, direct expansion gives
+
+```text
+base(n, L) − (e(s) + e(s − 2j)) = (s − 1) − j².
+```
+
+Take `L ≥ L*(n)`, so `j ≤ ⌊√(s−1)⌋`. For `n ≥ 6`, every split `(s', L−s')`
+then has both parts in `(2^(n−2), 2^(n−1)]`. On that range `e` is
+`C(·,2)` minus a constant, which is convex, so the split cap is largest at
+the extreme split. Hence the cap is at most `base`, and nothing fires on any
+subset. `n = 5` is covered by the full scan.
+
+**3. Sharpness.** Take `j = ⌊√(s−1)⌋ + 1` and `t = s − 2j`. The walk is built
+in two halves, using bit 1 as `x_1`:
+
+- **The half `x_1 = 0`.** All of it is traversed along the reflected Gray
+  cycle of the other `n − 1` bits, cut at its closing edge.
+- **The half `x_1 = 1`.** A "ladder" path through exactly `t` points: the
+  first `t/2` rows of the lower Gray cycle, on both values of the top bit.
+- **The halves join** at the two ends of the cut edge.
+
+The result is a simple closed walk of length `L*(n) − 2`, and it is
+universal. For the mask `e_1`:
+
+- the full side has excess `e(s)` exactly;
+- the other side has `t > 2^(n−2)` points of one coset, so its sum set is
+  the whole subgroup and its excess is `e(t)` exactly;
+- the total exceeds `base` by `j² − (s−1) > 0` and is at most `base + j²`,
+  so `e_1` fires. The canonical relabeling carries this to a mask of the
+  canonical word.
+
+## Checks in `verify.py`
+
+| Check | Result |
+| --- | --- |
+| `|A+A| ≥ 2^⌈log₂|A|⌉` and the cap `e(k)` | exhaustive in `F_2^k`, `k ≤ 4` (all 65,536 subsets at `k = 4`); the cap is attained exactly |
+| Cap threshold by a full split scan | 6, 14, then exactly the closed form for every `5 ≤ n ≤ 22` |
+| `t > 2^(n−2)` at `L*` | every `6 ≤ n < 40` |
+| Explicit word at `L*(n) − 2`, `n = 5..11` | simple, closed, universal; `e_1` fires; the canonical word fires its relabeled mask |
+| Controls of length `L*(n)` | nothing fires: every mask for `n ≤ 8`, `e_1` for `n ≤ 11` |
+| #3733's `(4,12)` on main | still fires, so the `n = 4` threshold 14 is attained |
+
+## Not covered
+
+- Which masks fire below `L*(n) − 2`, and whether the firing set is
+  monotone below that.
+- `(7, 18)` and `(7, 20)`. Those are far below `L*(7) = 114`, so this theorem
+  says nothing there.
+- Any change to a retained exclusion.
+
+## Reproduce
+
+```sh
+python3.12 -B research/f7-firing-threshold-all-n/verify.py
+```
+
+It prints `PASS_F7_FIRING_THRESHOLD_ALL_N` in about 6 seconds, using only the
+standard library.
+
+## Open next questions
+
+None for the first all-sound length; it is decided for every `n ≥ 4`.
+
+## Credit
+
+The model and the `n = 4` theorem are unpaidmoon's (#4322), building on Nick
+Petalas's #3699 and #3733. Kneser's theorem is classical. Prepared by Ryanson
+Jonathan with substantial Claude Code (Claude Opus 5.5) assistance.
+Apache-2.0.
diff --git a/research/f7-firing-threshold-all-n/SOURCES.json b/research/f7-firing-threshold-all-n/SOURCES.json
new file mode 100644
index 0000000000..f8e0a7d3b3
--- /dev/null
+++ b/research/f7-firing-threshold-all-n/SOURCES.json
@@ -0,0 +1,24 @@
+{
+  "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"
+    },
+    {
+      "path": "research/f7-functional-independent-check/RESULT.json",
+      "usage": "input",
+      "git_blob": "d4f2bd8cc0bfb19ebc4d2c3212170472c690779b",
+      "sha256": "a94ad29fbaaf908ebb64b12d6270402cf8aef6f5f24b3babb1152ecabe44cb3f"
+    }
+  ]
+}
diff --git a/research/f7-firing-threshold-all-n/TASK.json b/research/f7-firing-threshold-all-n/TASK.json
new file mode 100644
index 0000000000..8611a16fee
--- /dev/null
+++ b/research/f7-firing-threshold-all-n/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 every n >= 5, the first even length at which the fixed L/2 substitution fires on no universal canonical word, answering #4322's open question 3 and its 'eventually empty for every n' remark.",
+  "scope_change_reason": "#4322 and #4348 settle n = 4 and n = 5 by census; a min-sumset cap and an explicit construction settle every n.",
+  "bottleneck_link": "Where the fixed substitution is sound decides which census exclusions it can shortcut at each dimension.",
+  "budget_minutes": 40,
+  "stop_rule": "Stop once the threshold is proved for every n and checked against the census values.",
+  "outcome": "completed",
+  "evidence": "verify.py: |A+A| >= 2^ceil(log2|A|) exhaustive in F_2^k, k <= 4, with the cap attained; full split scan gives 6, 14 and exactly L*(n) for 5 <= n <= 22; explicit universal words of length L*(n) - 2 fire mask e_1 for 5 <= n <= 11, also after canonical relabeling; length-L* controls fire nothing; #3733's (4,12) fires on main.",
+  "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.",
+  "open_questions": [],
+  "no_open_questions_reason": "The first all-sound length is decided for every n >= 4."
+}
diff --git a/research/f7-firing-threshold-all-n/VERIFY.json b/research/f7-firing-threshold-all-n/VERIFY.json
new file mode 100644
index 0000000000..7cf9642987
--- /dev/null
+++ b/research/f7-firing-threshold-all-n/VERIFY.json
@@ -0,0 +1,20 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/f7-functional-independent-check/RESULT.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Min-sumset lemma and cap exhaustive in F_2^k (k <= 4); cap threshold scan vs closed form (5 <= n <= 22); split-range condition; explicit firing walks at L*(n) - 2 (n = 5..11) simple, closed, universal and firing, with canonical relabeling; length-L* controls; #3733 (4,12) on main."
+    }
+  ]
+}
diff --git a/research/f7-firing-threshold-all-n/verify.py b/research/f7-firing-threshold-all-n/verify.py
new file mode 100644
index 0000000000..4dc14e1133
--- /dev/null
+++ b/research/f7-firing-threshold-all-n/verify.py
@@ -0,0 +1,174 @@
+#!/usr/bin/env python3
+"""The first all-sound length of the fixed L/2 substitution, for every n >= 5.
+
+Model of #4322: prefix walks on F_2^n; a nonzero mask fires on a universal simple restored word when
+base < excess <= base + d^2, base(n, L) = (L/2)(L/2 - 1) - (2^(n-1) - 1). The checks:
+  1. min-sumset cap: |A + A| >= 2^ceil(log2 |A|) in F_2^k (exhaustive for k <= 4), so a k-point subset
+     of an affine flat has excess at most e(k) = C(k,2) - 2^ceil(log2 k) + 1;
+  2. the cap is sound on every L-point subset exactly from L*(n) = 2^n - 2 floor(sqrt(2^(n-1) - 1)),
+     for 5 <= n <= 22 by a full split scan (and 14 at n = 4);
+  3. an explicit universal word of length L*(n) - 2 on which a weight-one mask fires, for 5 <= n <= 11,
+     also after canonical relabeling; a control of length L*(n) on which nothing fires.
+Standard library only; no code from #4322.
+Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0.
+"""
+from itertools import combinations
+import json
+from math import comb, isqrt
+from pathlib import Path
+import sys
+
+ROOT = Path(__file__).resolve().parents[2]
+
+
+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 cap(k):
+    return 0 if k < 2 else comb(k, 2) - (1 << (k - 1).bit_length()) + 1
+
+
+def l_star(n):
+    return (1 << n) - 2 * isqrt((1 << (n - 1)) - 1)
+
+
+def first_cap_sound(n):
+    half, last_bad = 1 << (n - 1), None
+    for L in range(2, (1 << n) + 1, 2):
+        if any(cap(s) + cap(L - s) > base(n, L) for s in range(max(0, L - half), min(half, L) + 1)):
+            last_bad = L
+    return last_bad + 2
+
+
+def excess(points):
+    k, seen = len(points), set()
+    for i in range(k):
+        for j in range(i + 1, k):
+            seen.add(points[i] ^ points[j])
+    return comb(k, 2) - len(seen)
+
+
+def fires(n, states, mask):
+    sides = ([], [])
+    for x in states:
+        sides[bin(x & mask).count("1") & 1].append(x)
+    e = excess(sides[0]) + excess(sides[1])
+    d = (len(sides[0]) - len(sides[1])) // 2
+    b = base(n, len(states))
+    return b < e <= b + d * d
+
+
+def gray_cycle(k):
+    """reflected Gray code of Q_k as a list of integers; consecutive (and last, first) differ in one bit"""
+    return [i ^ (i >> 1) for i in range(1 << k)]
+
+
+def firing_walk(n, t):
+    """prefix states of a closed simple walk on F_2^n: all of {x_1 = 0} plus t points of {x_1 = 1}
+
+    Bit 0 plays x_1. Inside x_1 = 0 use the reflected Gray cycle of the other n - 1 bits, cut at its
+    closing edge (0, 2^(n-2)) of the top bit. In x_1 = 1 use the 'ladder' cycle of length t on the
+    rows h_0..h_(t/2 - 1) of the Gray cycle of the lower n - 2 bits, also cut at the edge (0, top bit).
+    """
+    k = n - 1
+    top = 1 << (k - 1)
+    g = gray_cycle(k)
+    need(g[0] == 0 and g[-1] == top, "Gray cycle closes on the top bit")
+    h = gray_cycle(k - 1)
+    rows = t // 2
+    ladder = [h[i] for i in range(rows)] + [h[i] | top for i in reversed(range(rows))]   # from 0 to top
+    lift = lambda y: y << 1
+    path0 = [lift(y) for y in g]                        # 0 ... top, all of x_1 = 0
+    path1 = [lift(y) | 1 for y in reversed(ladder)]     # top+x_1 ... x_1, t points of x_1 = 1
+    return path0 + path1
+
+
+def word_of(states):
+    """labels of the steps, closing back to 0"""
+    out = []
+    for a, b in zip(states, states[1:] + states[:1]):
+        diff = a ^ b
+        need(diff and diff & (diff - 1) == 0, "consecutive states differ in one bit")
+        out.append(diff.bit_length() - 1)
+    return out
+
+
+def canonical(word, n):
+    names, out = {}, []
+    for lab in word:
+        names.setdefault(lab, len(names))
+        out.append(names[lab])
+    perm = names                                         # old label -> new label
+    return out, perm
+
+
+def check_walk(n, states):
+    L = len(states)
+    need(len(set(states)) == L and states[0] == 0, "simple walk from 0")
+    full = 1 << n
+    diff = {a ^ b for a in states for b in states}
+    need(len(diff) == full, "universal")
+    return L
+
+
+def main():
+    # 1. min-sumset lemma, exhaustive in F_2^k for k <= 4 (all 2^16 subsets at k = 4)
+    for k in range(1, 5):
+        N = 1 << k
+        best = {}
+        for s in range(1, 1 << N):
+            A = [x for x in range(N) if s >> x & 1]
+            size = len({a ^ b for a in A for b in A})
+            need(size >= 1 << (len(A) - 1).bit_length(), f"|A+A| >= 2^ceil(log2|A|) in F_2^{k}")
+            best[len(A)] = max(best.get(len(A), 0), excess(A))
+        need(all(best[j] == cap(j) for j in best), f"cap e(k) attained exactly in F_2^{k}")
+
+    # 2. the cap threshold: full split scan against the closed form
+    scan = {n: first_cap_sound(n) for n in range(3, 23)}
+    need(scan[3] == 6 and scan[4] == 14, "n = 3, 4 thresholds 6 and 14 (#4322's n = 4 theorem)")
+    need(all(scan[n] == l_star(n) for n in range(5, 23)), "L*(n) = 2^n - 2 floor(sqrt(2^(n-1) - 1)) for 5 <= n <= 22")
+    # the binding split for n >= 5: both parts above 2^(n-2) at every L >= L*(n)
+    need(all((1 << (n - 1)) - (1 << n) + l_star(n) > 1 << (n - 2) for n in range(6, 40)), "t > 2^(n-2) from n = 6")
+    # published n = 4 data on main: (4,12) still fires, so the n = 4 cap threshold is attained too
+    d3733 = {(r["n"], r["L"]): r for r in json.loads((ROOT / "research/f7-functional-independent-check/RESULT.json").read_text())["new_domains"]}
+    need(d3733[4, 12]["false_prunes"] > 0, "#3733: (4,12) fires")
+
+    # 3. explicit firing words one step below L*(n), and controls at L*(n)
+    built = {}
+    for n in range(5, 12):
+        s = 1 << (n - 1)
+        L = l_star(n) - 2
+        states = firing_walk(n, L - s)
+        need(check_walk(n, states) == L, f"n={n}: walk length L* - 2")
+        need(fires(n, states, 1), f"n={n}: mask e_1 fires at L* - 2")
+        word = word_of(states)
+        cword, perm = canonical(word, n)
+        cstates, x = [], 0
+        for lab in cword:
+            cstates.append(x)
+            x ^= 1 << lab
+        need(x == 0 and fires(n, cstates, 1 << perm[0]), f"n={n}: the canonical word fires its relabeled mask")
+        control = firing_walk(n, L + 2 - s)
+        if n <= 8:
+            need(not any(fires(n, control, m) for m in range(1, 1 << n)), f"n={n}: nothing fires on the length-L* control")
+        else:
+            need(not fires(n, control, 1), f"n={n}: e_1 does not fire on the length-L* control")
+        built[str(n)] = {"L_star": l_star(n), "firing_length": L}
+
+    print(json.dumps({
+        "status": "PASS_F7_FIRING_THRESHOLD_ALL_N",
+        "L_star_closed_form": "2^n - 2 floor(sqrt(2^(n-1) - 1)), n >= 5",
+        "scan": {str(n): v for n, v in scan.items() if n <= 12},
+        "firing_words_below_L_star": built,
+        "new_kappa_claimed": False,
+    }, indent=1))
+
+
+if __name__ == "__main__":
+    sys.exit(main())