diff --git a/research/projection-recursion-check/README.md b/research/projection-recursion-check/README.md
new file mode 100644
index 0000000000..1d8c9f7b1b
--- /dev/null
+++ b/research/projection-recursion-check/README.md
@@ -0,0 +1,191 @@
+# Independent check of #4628's block-5 and block-6 bounds (2.99172, 2.97290, 2.9447)
+
+No new κ. Nothing here is about integer multiplication. This is an independent check of one hand-argued claim of
+open PR #4628 (Jacob Alan Sussman, head `ee4fd87f064017c23e5a86fc1dcfe0a5237caed3`):
+
+> m ≥ 4: at least 2.9447 calls per array (2.99172 at m = 5, 2.97290 at m = 6), engine game, argued by hand
+> (two AI reviewers reproduced the numbers).
+
+PROOF.md §7 of #4628 says only "The block-4 hook is carried upward through projections between the frame graphs of
+the engine, controlled by a coupling argument", and refers to the author's repository for the argument.
+
+## Result
+
+| Item | Verdict | How |
+|---|---|---|
+| Projection counts N_r(s) | **correct** | own derivation (section 3); brute force over **all** 15, 135 and 2,295 Lagrangians at m = 2, 3, 4 and every nonzero p, plus 60 sampled Lagrangians at m = 5 |
+| T_5 = 834241/278850 = 2.991720, T_6 = 1188222/399685 = 2.972896 | **reproduced exactly** | own recursion in exact fractions |
+| ≥ 2.9447 for every m ≥ 4 | **reproduced** | exact for m = 4..60 (minimum 2.944709234, decreasing in m); for m ≥ 60 by a monotone coupling whose transition inequalities I prove for every k (section 4; the author's `tail.py` checks them for k ≤ 80 only), c* = 2.944709234 |
+| Soundness of the recursion | **a sound route exists** (my reconstruction, argued by hand, section 2) | induced representations over the nonzero Paulis plus Bruhat transitivity for the engine's frame group |
+| Inputs | **the numbers rest on two block-4 values that nobody re-checked**: a_3 ≥ 68,320 (enters T_5) and a_2 ≥ 48,576 (enters T_6) | section 5 |
+
+Gaps found, none of which refutes the claim:
+
+1. **The written argument is not public.** #4628 says "The programs and the written argument are in my repository".
+   At commit `86e575e2` of jacobalansussman/wht-power-saving-lean only the programs and their outputs are public
+   (`research/block-bounds-and-new-rules/programs/engine-bounds-blocks-5-and-6/`). The proof they cite ("PROOF.md,
+   Theorem 3", "Lemma 1(c)", "Lemma 2", "Theorems 4 and 5") is in the folder `proofs/induction/` of a private archive
+   (that repository's `block-bounds-and-new-rules/README.md`, Sources). So the hand argument cannot be read by
+   reviewers. Section 2 gives an independent route.
+2. **Two inputs come from one program.** T_5 = (N_5(4)·a_4 + N_5(3)·a_3)/(N_5,1(1)·a_1) uses the block-4 hook values
+   a_1 = 27,456 (cap, proved in Lean), a_4 ≥ 86,592 (demand, determinant certificate, C author evidence) and
+   **a_3 ≥ 68,320**; T_6 also uses **a_2 ≥ 48,576**. The last two are mod-p rank lower bounds printed by the author's
+   `hookG.py` (`data/block4-hook/out_rank2_blocks.txt`). Mod-p rank is the safe direction, but no certificate is
+   stored, and #4628's `verify.py` does not check them. The author's README calls the three-move value "computed
+   modulo a prime but not certified" (that remark is about using it as an upper bound; here it is used as a lower
+   bound). With only the triangle bounds a_2 ≥ a_4 − 2a_1 = 31,680 and a_3 ≥ a_4 − a_1 = 59,136 the route gives
+   T_5 ≥ 2.83219, T_6 ≥ 2.77245, T_60 ≥ 2.70821.
+3. **The tail was checked numerically only up to k = 80.** The coupling needs two inequalities at every block k.
+   They hold for all k (section 4), so this gap is closed here.
+4. **Status of the soundness step.** My reconstruction in section 2 is argued by hand, like the original. It is
+   independent: I did not see the author's proof.
+
+Bearing on the open shapes: with T_5 and T_6 and the bound W + m (not checked here), the smallest shapes left open are
+2 in 7 and 3 in 9 at block 5, and 2 in 8 and 3 in 9 at block 6. These match #4628's table. 3 in 9 needs more than
+3 calls per array. This route cannot give that: its limit is 2.94471, and it falls with m. Excluded by T_m alone:
+3 in 8 and 4 in 11 at blocks 5 and 6, 5 in 14 at block 6, and W in 3W − 1 for W ≤ 120 (block 5) and W ≤ 36 (block 6).
+All of these match #4628.
+
+## 1. The claim, in the form checked
+
+Frames are Lagrangian subspaces of F_2^(2m), the symplectic space of the m-qubit Paulis. The engine's free letters
+are shifts (X Paulis), invertible XOR-linear address maps, and phases i^(z·x + c). Conjugating S-phases by address
+maps gives CZ. Together these generate every Pauli and every Clifford that fixes the Z-frame L_0. Their image in
+Sp(2m, 2) is the whole Siegel parabolic P = {[[A, B], [0, A^(-T)]]}. A call C_v = (1+i)/2·I + (1−i)/2·X_v is √X_v,
+a Clifford at frame distance 1 from L_0, and the target C^(⊗m) is at distance m.
+For a subspace N kept by every free letter, raise(f g f′) = raise(g) for free f, f′. So the double cosets P\Sp/P,
+which are the distances d = m − dim(L_0 ∩ gL_0), make raise a function a_d of the distance alone (with a_0 = 0).
+The brute-force count confirms that every Lagrangian at the same distance gives the same projection counts.
+
+The recursion (author's `induct.py`, re-implemented here) is a^(m)_r = Σ_s N^(m)_r(s)·a^(m−1)_s. Here N^(m)_r(s)
+is the number of nonzero p ∈ F_2^(2m) for which the reductions π_p L = (L ∩ p^⊥) + ⟨p⟩ of a distance-r pair have
+distance s in p^⊥/⟨p⟩. The bound at block m is T_m = a^(m)_m / a^(m)_1, by Theorem R (#4628 PROOF.md §1).
+
+## 2. Why the recursion is a valid lower bound (independent reconstruction; argued by hand)
+
+Let N′ be a block-(m−1) certificate kept by the block-(m−1) frame group, with profile a′. The steps:
+
+- **Copies of N′ for each p.** For each nonzero p, pick a Clifford h_p with h_p p = z_1 and h_p(π_p L_0) = L_0.
+  This is possible because the stabiliser of z_1 acts transitively on the Lagrangians containing z_1. Let U_p be
+  the sum of the two eigenspaces of P taken in all f columns at once (V_+(P)^(⊗f) ⊕ V_−(P)^(⊗f)). Put the copy
+  N_p = h_p^(−1)(N′ ⊗ both Z_1-eigenspaces) inside U_p; the X_1 Pauli identifies the two eigenspaces.
+- **The new space.** Set U = ⊕_p U_p. A Clifford g maps U_p to U_(gp), and the eigenvalue signs cancel because all
+  f columns carry the same sign. U is a representation of the finite group G generated by the letters.
+- **The program identity holds on U.** A program right at every width f ≥ 1 is an identity in C[G]. Burnside–Brauer
+  (faithful V, the Vandermonde argument run with exponents n ≥ 1) puts every irreducible of G into some V^(⊗f) with
+  f ≥ 1. So Theorem R applies on U, with any linear (complex) mixing.
+- **Free letters keep N = ⊕_p N_p.** For a free b, the map h_(bp)·b·h_p^(−1) fixes z_1 and L_0. Its reduction is
+  therefore a block-(m−1) free element, which keeps N′.
+- **Raise splits over p.** raise_U(g) = Σ_q raise_(N′)(h_q g h_(g⁻¹q)^(−1)). The reduced map sends the standard
+  frame to h_q(π_q gL_0). Its distance from the standard frame h_q(π_q L_0) is d(π_q L_0, π_q gL_0). So raise_U(g)
+  = Σ_q a′_(d(π_q L_0, π_q gL_0)), which is the recursion, up to a uniform factor 2 that cancels in T_m.
+
+In which direction each input is needed: the cap at block m is N_1(1)·a′_1 and needs a′_1 as an upper bound, with
+a′_0 = 0. The demands need a′_(m−1) and a′_(m−2) as lower bounds. The optional triangle step a_r ≥ a_m − (m−r)·a_1
+is valid (raise is subadditive) and changes nothing here. The checks agree: with and without it the tops are
+identical.
+
+This route uses the frame group of the engine (Lagrangians, the Siegel parabolic). As #4628 says, it does not carry
+over to the widened game (Toffoli is not Clifford).
+
+## 3. The projection counts (own derivation)
+
+Let L, M be at distance r, so I = L ∩ M has dim m − r and L + M = I^⊥. The cases for p:
+
+| p | number of such p | reduced distance s |
+|---|---|---|
+| in I | 2^(m−r) − 1 | r |
+| outside L + M | 4^m − 2^(m+r) | r (π_pL ∩ π_pM = (I ∩ p^⊥) + p) |
+| in exactly one of L, M | 2(2^m − 2^(m−r)) | r − 1 (the intersection is I + p) |
+| p = l + m′ (l ∈ L∖I, m′ ∈ M∖I), ω(l, m′) = 1 | (2^r − 1)·2^(r−1)·2^(m−r) | r − 1 |
+| same, ω(l, m′) = 0 | (2^r − 1)(2^(r−1) − 1)·2^(m−r) | r − 2 (l also lies in the intersection) |
+
+ω(l, m′) is well defined modulo I. The pairing L/I × M/I → F_2 is nondegenerate, which gives the split
+(2^r − 1)·2^(r−1) against (2^r − 1)(2^(r−1) − 1). This is the author's closed form. `verify.py` confirms it against
+brute force.
+
+## 4. The tail for m > 60 (independent proof of the coupling inequalities)
+
+Write j = k − r for the deficit. A random p moves block k to block k − 1, and the deficit
+- goes up with probability p_up = N_r(r−2)/(4^k − 1) = (2^r − 1)(2^(r−1) − 1)·2^j/(4^k − 1);
+- goes down with probability p_down = N_r(r)/(4^k − 1) = (2^j − 1 + 4^k − 2^(2k−j))/(4^k − 1).
+
+R^(k)_r = a^(k)_r/a^(k)_1 = (1/q_k)·E[R^(k−1)_s] with q_k = N_1(1)/(4^k − 1) ≤ 1. Hence
+T_m ≥ E[R^(60)_(60 − J)], where J is the deficit at block 60.
+
+- **Up-probability.** The numerator equals 2^(2k−j−1) − 3·2^(k−1) + 2^j ≤ 2^(2k−j−1) − 2^k. This is less than
+  2^(−(j+1))·(4^k − 1), so p_up ≤ 2^(−(j+1)).
+- **Down-probability.** p_down ≥ 1 − 2^(−j) is equivalent to 2^j ≥ 2^(−j). Once r = 0 the chain only goes down.
+- **The dominating chain.** It moves up with probability 2^(−(j+1)) and down with probability 1 − 2^(−j). It is
+  monotone, since Q_up(j) + Q_down(j+1) = 1, and its stationary law is π*(j) ∝ Π_(i≤j) 1/(2^i − 1).
+- **Comparison.** Started at deficit 0, J ≤_st π*. The block-60 profile is nondecreasing in r (checked), so T_m ≥
+  Σ_j π*(j)·R^(60)_(60−j). The tail of the normaliser is bounded by 2w_J with J = 80 (w_(j+1)/w_j ≤ 1/3). This gives
+  c* = 2.944709234 > 2.9447, the same constant as the author's.
+
+## 5. Inputs, and what each number rests on
+
+| input (block-4 hook, k = 8, f = 9) | used in | status |
+|---|---|---|
+| a_1 = 27,456 (cap) | all | proved in Lean (`hook_cap`), as an upper bound |
+| a_4 ≥ 86,592 (demand) | all | 5,412 × 5,412 minor, C checker (author evidence in #4628; about an hour) |
+| a_3 ≥ 68,320 | T_5 and later | mod-p rank in the author's `hookG.py`; no stored certificate; not re-checked by #4628 |
+| a_2 ≥ 48,576 | T_6 and later | as above. The README of #4628 also cites 48,576 as a certified **upper** bound (two calls in a row); the induction needs it as a **lower** bound, which is again only the mod-p rank |
+
+## Reproduce
+
+```sh
+python3.12 -B research/projection-recursion-check/verify.py       # PASS_PROJECTION_RECURSION_CHECK, about 35 s, stdlib
+python3 scripts/research_package.py --package research/projection-recursion-check --check-only
+python3.12 scripts/research_package.py --package research/projection-recursion-check
+```
+
+`verify.py` imports nothing from #4628 or from the author's repository. Ten controls must be rejected, and are:
+
+- a closed form with one count moved;
+- T_5 and T_6 off by one in the denominator;
+- a_3 + 1 reproducing T_5;
+- two weakened dominating chains;
+- 3 in 9 at block 6 claimed excluded;
+- 3 in 8 at block 5 claimed allowed;
+- 2.99172 claimed from the triangle inputs alone;
+- a nonmonotone profile.
+
+## NOT covered
+
+- The block-4 hook values themselves. I did not recompute a_2, a_3 or a_4 (dimension 102,960), or the Lean proofs
+  of the cap.
+- The author's private written proof. Section 2 is my own reconstruction; it is argued by hand, and no person has
+  checked it.
+- The other claims of #4628: W + m and 2W, one array, no-phase block 3, the widened-game keptness, and section 7.
+  The shapes above use W + m as stated in #4628.
+- Whether #288's or Harvey's models lie inside the engine game.
+
+## Open next questions
+
+See `open_questions` in [TASK.json](TASK.json):
+
+1. Certify a_3 ≥ 68,320 and a_2 ≥ 48,576 with a stored minor and a separate checker.
+2. Write section 2 as a full proof, or in Lean.
+3. Exclude 3 in 9 at block 5 or 6. That needs a certificate above 3 calls per array, which this route cannot give.
+
+## Sources (pins in SOURCES.json; external files by sha256)
+
+- #4628 at head `ee4fd87f064017c23e5a86fc1dcfe0a5237caed3`: `research/complex-small-m-lower-bounds/README.md`
+  (table of section 1, section 6) and `PROOF.md` §7.
+- jacobalansussman/wht-power-saving-lean at `86e575e28ed94890872dcff1bb2621d7ff559cbd`, read only to locate the
+  claim and its inputs; no code reused. Files under `research/block-bounds-and-new-rules/`:
+  - `README.md`, sha256 `47c99107…54f50a`;
+  - `data/engine-bounds-blocks-5-and-6/out_induct.txt`, `e4cf4402…bb4072`;
+  - `data/engine-bounds-blocks-5-and-6/out_tail.txt`, `9861aa2c…778c2b`;
+  - `programs/engine-bounds-blocks-5-and-6/induct.py`, `dabe7190…2c428c`;
+  - `programs/engine-bounds-blocks-5-and-6/nrs_closed.py`, `54ba1ab4…71eeb`;
+  - `programs/engine-bounds-blocks-5-and-6/tail.py`, `2ac28e4c…12e717d5d4`;
+  - `data/block4-hook/out_rank2_blocks.txt` (the a_2, a_3 values).
+
+## Credit
+
+The claim, the projection recursion, the block-4 hook and its numbers are Jacob Alan Sussman's (#4628 and his
+repository, written with AI agents). The certificate method (Theorem R / the FO lemma) is eumemic's (#288), with
+Swapnil Jain's P1/P2 as cited there. The engine and cost model are OpenAI's.
+
+Prepared by lm1909 with Claude Code (Claude Opus 5.5) assistance. Apache-2.0.
diff --git a/research/projection-recursion-check/SOURCES.json b/research/projection-recursion-check/SOURCES.json
new file mode 100644
index 0000000000..dfc2710efc
--- /dev/null
+++ b/research/projection-recursion-check/SOURCES.json
@@ -0,0 +1,32 @@
+{
+  "schema_version": 1,
+  "base_commit": "fbc9ea0249746acca4f504d4fda2b84e0e36cf0d",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/complex-small-m-lower-bounds/README.md",
+      "usage": "provenance",
+      "pin": "head:ee4fd87f064017c23e5a86fc1dcfe0a5237caed3:research/complex-small-m-lower-bounds/README.md",
+      "git_blob": "764fe1ea7b6d31e39f802233fdaeb5514f4b4ab4",
+      "sha256": "565b38d373a333dec701839b71c485d27ec5c1383816a2e816f93f2883763069"
+    },
+    {
+      "path": "research/complex-small-m-lower-bounds/PROOF.md",
+      "usage": "provenance",
+      "pin": "head:ee4fd87f064017c23e5a86fc1dcfe0a5237caed3:research/complex-small-m-lower-bounds/PROOF.md",
+      "git_blob": "46bccf74885682ca3e4bf97aea78d12770eec59c",
+      "sha256": "4a67f8ccb6284bf17389086bd00ff38c3d256fab4e69a184aade1a6ca33eb7fe"
+    }
+  ]
+}
diff --git a/research/projection-recursion-check/TASK.json b/research/projection-recursion-check/TASK.json
new file mode 100644
index 0000000000..fec3de5c69
--- /dev/null
+++ b/research/projection-recursion-check/TASK.json
@@ -0,0 +1,112 @@
+{
+  "schema_version": 1,
+  "task_id": "independent-moment",
+  "priority_revision": 7,
+  "base_commit": "fbc9ea0249746acca4f504d4fda2b84e0e36cf0d",
+  "original_card": {
+    "id": "independent-moment",
+    "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/staged544-mixed-fourth-entry/README.md",
+      "research/staged-fourth-mixture-ceiling/README.md",
+      "research/r437-two-window-carrier/README.md"
+    ],
+    "methods": [
+      "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.",
+      "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls."
+    ],
+    "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.",
+    "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.",
+    "allowed_variations": [
+      "Reconstruct either a source ledger or a numeric enclosure with a different method."
+    ],
+    "scope_change_triggers": [
+      "Importing the primary function and calling its output independent verification.",
+      "Calling an aggregate histogram or source archive an independently accepted physical supplier."
+    ],
+    "overlap_terms": [
+      "independent moment",
+      "rank histogram",
+      "exact enclosure",
+      "2979",
+      "rank7 joint endframes",
+      "paired extraction",
+      "joint lowering",
+      "4088",
+      "4091",
+      "4067",
+      "staged544-mixed-fourth-entry",
+      "staged-fourth-mixture-ceiling",
+      "r437-two-window-carrier"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.",
+        "evidence": "research/staged544-mixed-fourth-entry/README.md",
+        "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.",
+        "status": "author-checked",
+        "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.",
+        "evidence": "research/staged-fourth-mixture-ceiling/README.md",
+        "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.",
+        "status": "author-checked",
+        "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.",
+        "evidence": "research/r437-two-window-carrier/README.md",
+        "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.",
+        "status": "author-checked",
+        "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Independent check of one hand-argued claim of open PR #4628 (head ee4fd87f): the engine-game bound of at least 2.9447 calls per array from block 4 on (2.99172 at block 5, 2.97290 at block 6), obtained by projecting the block-4 hook profile through symplectic reductions. Re-derives the projection counts, recomputes the recursion and the all-m tail with own exact code, reconstructs a soundness argument, and isolates which block-4 inputs the numbers rest on.",
+  "scope_change_reason": "The card's examples (#4088, #4091, #4067) concern the bit-side paid ledgers; this package applies the card's method (independent reconstruction of a paid profile with source binding, positive cases and semantic failure controls) to the paid-call profile of the complex small-block lower bounds in #4628, which nobody had checked independently.",
+  "bottleneck_link": "Side result for the complex small-block line: it decides how much weight the open-case table of #4628 (2 in 7 and 3 in 9 at blocks 5 and 6) can carry. No new kappa and no claim about integer multiplication.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the projection-recursion claim is reconstructed, recomputed and its inputs isolated; do not recompute block-4 hook ranks.",
+  "outcome": "completed",
+  "evidence": "verify.py: brute-force projection counts over all 15/135/2295 Lagrangians at m = 2, 3, 4 (sample at m = 5); exact T_5 = 834241/278850, T_6 = 1188222/399685, min over m = 5..60 = 2.944709234; dominating-chain inequalities for k <= 300 (proved for all k in README) and c* = 2.944709234 > 2.9447; sensitivity to the block-4 inputs; 10 failure controls rejected.",
+  "author": "lm1909",
+  "ai_assistance": "Prepared by lm1909 with Claude Code (Claude Opus 5.5) assistance; code, derivation and text written by the AI under lm1909's direction.",
+  "open_questions": [
+    {
+      "question": "Are the block-4 hook values a_3 >= 68,320 (enters T_5) and a_2 >= 48,576 (enters T_6) correct as lower bounds on the raise of a rank-3 and rank-2 Clifford?",
+      "why_it_matters": "They are the only inputs of 2.99172 and 2.97290 that rest on a single author program (mod-p ranks, no stored certificate, not re-checked by #4628's verify.py); with the triangle bounds alone the numbers drop to 2.832 and 2.772.",
+      "first_step": "Store an explicit nonzero minor (or a rank certificate over one character block) for C_e0 C_e1 C_e2 on the k = 8, f = 9 hook and check it with a separate checker, as was done for the demand 86,592.",
+      "blocked_by": "Size: the hook has dimension 102,960; a character-block split as in hookG is needed."
+    },
+    {
+      "question": "Can the induced-representation argument of README section 2 be written as a full proof (or in Lean) on the engine's own definitions?",
+      "why_it_matters": "The author's written proof (PROOF.md Theorem 3 of the pf-induction track) is in a private archive; this package gives an independent sketch, not a checked proof.",
+      "first_step": "Formalise the step 'program right at every width => identity in C[G]' (Burnside-Brauer for the finite Clifford group) and the decomposition raise_U(g) = sum_q raise(reduced g).",
+      "blocked_by": "Nothing; it is writing work."
+    },
+    {
+      "question": "Does any certificate exclude 3 in 9 at block 5 or 6 (needs more than 3 calls per array)?",
+      "why_it_matters": "It is the smallest engine-game shape at blocks 5 and 6 that no stated bound excludes; this projection route stays below 3 at both blocks (2.99172, 2.97290) and its limit is 2.94471.",
+      "first_step": "Run the same recursion from a block-5 base profile with top ratio above 3 (for example a block-5 hook at larger width), if one can be computed.",
+      "blocked_by": "#4628's own ceiling notes say projection gains at most a factor 1.1 and hook-type certificates stay below 4."
+    }
+  ]
+}
diff --git a/research/projection-recursion-check/VERIFY.json b/research/projection-recursion-check/VERIFY.json
new file mode 100644
index 0000000000..05960abe51
--- /dev/null
+++ b/research/projection-recursion-check/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": 120,
+      "checks": "Brute-force projection counts (m = 2, 3, 4 complete; m = 5 sample) against the closed form; exact recursion T_5 = 834241/278850, T_6 = 1188222/399685, min over 5..60; all-m tail by dominating chain and c*; input sensitivity; shapes; 10 failure controls must be rejected. Prints PASS_PROJECTION_RECURSION_CHECK."
+    }
+  ]
+}
diff --git a/research/projection-recursion-check/verify.py b/research/projection-recursion-check/verify.py
new file mode 100644
index 0000000000..3715ffa462
--- /dev/null
+++ b/research/projection-recursion-check/verify.py
@@ -0,0 +1,348 @@
+#!/usr/bin/env python3
+"""Independent check of the m >= 4 engine-game bound of PR #4628 (2.9447 / 2.99172 / 2.97290).
+
+Prepared by lm1909 with Claude Code (Claude Opus 5.5) assistance. Apache-2.0.
+Standard library only; nothing is imported from PR #4628 or from the author's repository.
+
+Parts:
+  counts   brute-force N_r(s): over ALL Lagrangians M of F_2^(2m) (m = 2, 3, 4) and every nonzero p,
+           the reduced distance d(pi_p L0, pi_p M); compared with the closed form derived in README section 3.
+           m = 5 on a deterministic random sample of Lagrangians.
+  recur    the projection recursion from the block-4 hook profile (27456, 48576, 68320, 86592), exact
+           fractions: T_5 = 834241/278850, T_6 = 1188222/399685, min over m = 5..60; profile monotonicity.
+  tail     the all-m tail by a monotone coupling with an explicit dominating chain: the transition
+           inequalities checked exactly for k <= 300 (proved for all k in README section 4) and the
+           certified constant c* from the block-60 profile.
+  sens     sensitivity: which block-4 inputs the numbers use, and what is left with weaker inputs.
+  shapes   exclusions and smallest open shapes at m = 5, 6 implied by T_m and W + m.
+  controls each corrupted claim below must be rejected.
+"""
+import random
+import sys
+from fractions import Fraction as F
+from math import ceil
+
+FAIL = []
+QUIET = [False]
+
+
+def check(cond, msg):
+    if not cond:
+        FAIL.append(msg)
+        if not QUIET[0]:
+            print("FAIL:", msg)
+    return cond
+
+
+# ---------------------------------------------------------------- symplectic geometry over F_2
+def pc(x):
+    return bin(x).count("1")
+
+
+def form(m, a, b):
+    """standard symplectic form on F_2^(2m); low m bits = x part, high m bits = z part."""
+    M = (1 << m) - 1
+    return (pc((a & M) & (b >> m)) + pc((a >> m) & (b & M))) & 1
+
+
+def span(gens):
+    out = {0}
+    for g in gens:
+        if g not in out:
+            out |= {x ^ g for x in out}
+    return frozenset(out)
+
+
+def z_frame(m):
+    return span([1 << (m + i) for i in range(m)])
+
+
+def all_lagrangians(m):
+    """orbit of the Z-frame under all symplectic transvections (they generate Sp(2m, 2))."""
+    start = z_frame(m)
+    seen = {start}
+    todo = [start]
+    vs = range(1, 1 << (2 * m))
+    while todo:
+        A = todo.pop()
+        for v in vs:
+            B = frozenset(x ^ v if form(m, x, v) else x for x in A)
+            if B not in seen:
+                seen.add(B)
+                todo.append(B)
+    return seen
+
+
+def log2size(S):
+    return len(S).bit_length() - 1
+
+
+def dist(m, A, B):
+    return m - log2size(A & B)
+
+
+def proj(m, A, p):
+    """pi_p A = (A cap p-perp) + <p>, as a subset of p-perp (a Lagrangian of p-perp/<p> plus p)."""
+    S = [a for a in A if form(m, a, p) == 0]
+    return frozenset(S) | frozenset(s ^ p for s in S)
+
+
+def reduced_dist(m, A, B, p):
+    # both projections contain p; in p-perp/<p> (dimension 2(m-1)) the distance is
+    # (m-1) - (dim(piA cap piB) - 1) = m - dim(piA cap piB)
+    return m - log2size(proj(m, A, p) & proj(m, B, p))
+
+
+def N_closed(m, r):
+    """closed form derived in README section 3 (own derivation)."""
+    out = {}
+
+    def add(s, c):
+        if c:
+            out[s] = out.get(s, 0) + c
+    add(r, (2 ** (m - r) - 1) + (4 ** m - 2 ** (m + r)))            # p in L cap M, or p outside L + M
+    add(r - 1, 2 * (2 ** m - 2 ** (m - r)))                           # p in exactly one of L, M
+    add(r - 1, (2 ** r - 1) * 2 ** (r - 1) * 2 ** (m - r))            # p = l + m', omega(l, m') = 1
+    add(r - 2, (2 ** r - 1) * (2 ** (r - 1) - 1) * 2 ** (m - r))      # p = l + m', omega(l, m') = 0
+    assert sum(out.values()) == 4 ** m - 1
+    return out
+
+
+def brute_counts(m, Ms, L0):
+    """for each M: dict s -> #p; returns {r: set of frozen dicts}."""
+    res = {}
+    for M in Ms:
+        r = dist(m, L0, M)
+        if r == 0:
+            continue
+        cnt = {}
+        for p in range(1, 1 << (2 * m)):
+            s = reduced_dist(m, L0, M, p)
+            cnt[s] = cnt.get(s, 0) + 1
+        res.setdefault(r, set()).add(frozenset(cnt.items()))
+    return res
+
+
+def part_counts(closed=N_closed, quiet=False, ms=(2, 3, 4), sample=True):
+    ok = True
+    for m in ms:
+        Ls = all_lagrangians(m)
+        expect = 1
+        for i in range(1, m + 1):
+            expect *= 2 ** i + 1
+        ok &= check(len(Ls) == expect, f"m={m}: {len(Ls)} Lagrangians, expected {expect}")
+        L0 = z_frame(m)
+        res = brute_counts(m, Ls, L0)
+        for r in range(1, m + 1):
+            got = res.get(r, set())
+            ok &= check(len(got) == 1, f"m={m} r={r}: counts not constant over the {r}-distance class")
+            ok &= check(got == {frozenset(closed(m, r).items())}, f"m={m} r={r}: brute {got} != closed {closed(m, r)}")
+        if not quiet:
+            print(f"counts m={m}: {len(Ls)} Lagrangians, all M at each distance r=1..{m} agree with the closed form")
+    if not sample:
+        return ok
+    # m = 5: deterministic random sample of Lagrangians, generated by random transvection words
+    m = 5
+    rng = random.Random(4628)
+    L0 = z_frame(m)
+    sample = []
+    for _ in range(60):
+        A = L0
+        for _ in range(rng.randrange(1, 12)):
+            v = rng.randrange(1, 1 << (2 * m))
+            A = frozenset(x ^ v if form(m, x, v) else x for x in A)
+        sample.append(A)
+    res = brute_counts(m, sample, L0)
+    for r, got in res.items():
+        ok &= check(got == {frozenset(closed(m, r).items())}, f"m=5 r={r}: sampled counts disagree")
+    if not quiet:
+        print(f"counts m=5: {len(sample)} sampled Lagrangians, distances {sorted(res)}, all agree")
+    return ok
+
+
+# ---------------------------------------------------------------- the recursion
+BASE4 = (27456, 48576, 68320, 86592)   # block-4 hook k=8, f=9: cap (exact), and lower bounds for r = 2, 3, 4
+
+
+def step(a, m, improve=False):
+    """a[0..m-1] profile at block m-1 (a[0] = 0) -> profile at block m."""
+    b = [0] * (m + 1)
+    for r in range(1, m + 1):
+        b[r] = sum(c * a[s] for s, c in N_closed(m, r).items() if 1 <= s <= m - 1)
+    if improve:   # raise is subadditive: a_m <= a_r + (m - r) a_1, so a_r >= a_m - (m - r) a_1
+        for r in range(2, m):
+            b[r] = max(b[r], b[m] - (m - r) * b[1])
+    return b
+
+
+def run(base, M, improve=False):
+    a = [0] + list(base)
+    tops = {len(base): F(a[-1], a[1])}
+    profs = {}
+    for m in range(len(base) + 1, M + 1):
+        a = step(a, m, improve)
+        tops[m] = F(a[m], a[1])
+        profs[m] = a
+    return tops, profs
+
+
+def part_recur(base=BASE4, quiet=False):
+    tops, profs = run(base, 60)
+    tops_i, _ = run(base, 60, improve=True)
+    ok = check(tops[4] == F(41, 13), "T_4 != 41/13")
+    ok &= check(tops[5] == F(834241, 278850), f"T_5 = {tops[5]}")
+    ok &= check(tops[6] == F(1188222, 399685), f"T_6 = {tops[6]}")
+    ok &= check(tops == tops_i, "triangle improvement changes the tops")
+    mn = min(tops[m] for m in range(5, 61))
+    ok &= check(mn > F(29447, 10000), f"min T_m (5..60) = {float(mn)}")
+    ok &= check(all(tops[m + 1] < tops[m] for m in range(4, 60)), "tops not decreasing")
+    a = profs[60]
+    ok &= check(all(a[r] <= a[r + 1] for r in range(1, 60)), "block-60 profile not nondecreasing")
+    if not quiet:
+        print(f"recur: T_4 = {tops[4]}, T_5 = {tops[5]} = {float(tops[5]):.6f}, T_6 = {tops[6]} = {float(tops[6]):.6f}, "
+              f"T_7 = {tops[7]}, T_60 = {float(tops[60]):.12f}; min(5..60) = {float(mn):.9f}")
+    return ok, tops, profs
+
+
+# ---------------------------------------------------------------- tail
+def p_up(k, j):
+    r = k - j
+    return F(N_closed(k, r).get(r - 2, 0), 4 ** k - 1) if r >= 1 else F(0)
+
+
+def p_down(k, j):
+    r = k - j
+    return F(N_closed(k, r).get(r, 0), 4 ** k - 1) if r >= 1 else F(1)
+
+
+def dominating_ok(K, qup, qdown):
+    for k in range(1, K + 1):
+        for j in range(0, k + 1):
+            if p_up(k, j) > qup(j):
+                return False, (k, j, "up")
+            if j >= 1 and p_down(k, j) < qdown(j):
+                return False, (k, j, "down")
+    # Q is a probability kernel and is monotone (Q_up(j) + Q_down(j+1) <= 1)
+    for j in range(0, 400):
+        if qup(j) + (qdown(j) if j >= 1 else 0) > 1 or qup(j) + qdown(j + 1) > 1:
+            return False, (None, j, "Q")
+    return True, None
+
+
+QUP = lambda j: F(1, 2 ** (j + 1))
+QDOWN = lambda j: 1 - F(1, 2 ** j)
+
+
+def cstar(prof, M0, J=80):
+    w = [F(1)]
+    for j in range(1, J + 1):
+        w.append(w[-1] / (2 ** j - 1))
+    Zup = sum(w) + 2 * w[J]           # w_(j+1)/w_j <= 1/3 for j >= 1
+    R = lambda r: F(prof[r], prof[1]) if r >= 1 else F(0)
+    return sum(w[j] * R(M0 - j) for j in range(0, min(J, M0) + 1)) / Zup
+
+
+def part_tail(profs, quiet=False):
+    ok, where = dominating_ok(300, QUP, QDOWN)
+    check(ok, f"dominating chain inequality fails at {where}")
+    c = cstar(profs[60], 60)
+    ok &= check(c > F(29447, 10000), f"c* = {float(c)}")
+    if not quiet:
+        print(f"tail: transition inequalities hold for every k <= 300 and 0 <= j <= k; c*(block 60) = {float(c):.12f} > 2.9447")
+    return ok
+
+
+# ---------------------------------------------------------------- sensitivity
+def part_sens(quiet=False):
+    a1, a2, a3, a4 = BASE4
+    weak = (a1, a4 - 2 * a1, a4 - a1, a4)       # triangle lower bounds only: a2 >= a4 - 2 a1, a3 >= a4 - a1
+    t_full, _ = run(BASE4, 6)
+    t_weak, _ = run(weak, 6)
+    # which inputs does T_5 use?  T_5 = (N_5(4) a4 + N_5(3) a3) / (N_1(1) a1): a2 does not enter
+    t_a2, _ = run((a1, 0, a3, a4), 6)
+    ok = check(t_a2[5] == t_full[5], "T_5 depends on a2")
+    ok &= check(t_a2[6] != t_full[6], "T_6 does not depend on a2")
+    tw, pw = run(weak, 60)
+    if not quiet:
+        print(f"sens: T_5 uses a1, a3, a4 only; T_6 also a2.  With triangle-only a2 = {weak[1]}, a3 = {weak[2]}: "
+              f"T_5 = {float(t_weak[5]):.5f}, T_6 = {float(t_weak[6]):.5f}, T_60 = {float(tw[60]):.5f}")
+    return ok, tw
+
+
+# ---------------------------------------------------------------- shapes
+def smallest_open(T, m, W):
+    s = max(ceil(T * W), W + m if W >= 2 else m, 2 * W)
+    return s if s < m * W else None
+
+
+def part_shapes(tops, quiet=False):
+    ok = True
+    T5, T6 = tops[5], tops[6]
+    ok &= check(T5 * 3 > 8 and T6 * 3 > 8, "3 in 8 not excluded")
+    ok &= check(T5 * 4 > 11 and T6 * 4 > 11, "4 in 11 not excluded")
+    ok &= check(T6 * 5 > 14, "5 in 14 at m=6 not excluded")
+    ok &= check(T5 * 3 <= 9 and T6 * 3 <= 9, "3 in 9 excluded?")
+    ok &= check(smallest_open(T5, 5, 2) == 7 and smallest_open(T5, 5, 3) == 9, "m=5 smallest open shapes")
+    ok &= check(smallest_open(T6, 6, 2) == 8 and smallest_open(T6, 6, 3) == 9, "m=6 smallest open shapes")
+    w5 = max(W for W in range(1, 1000) if T5 * W > 3 * W - 1)
+    w6 = max(W for W in range(1, 1000) if T6 * W > 3 * W - 1)
+    ok &= check((w5, w6) == (120, 36), f"3W-1 exclusion range {w5}, {w6}")
+    if not quiet:
+        print("shapes: " + "; ".join(f"m={m} W={W}: smallest open s={smallest_open(tops[m], m, W)}"
+                                     for m in (5, 6) for W in (2, 3, 4, 5)) + f"; 3W-1 excluded for W <= {w5} (m=5), {w6} (m=6)")
+    return ok
+
+
+# ---------------------------------------------------------------- controls
+def part_controls():
+    rej = []
+
+    def bad_closed(m, r):            # move one p from s = r-1 to s = r-2
+        d = dict(N_closed(m, r))
+        if r >= 2 and d.get(r - 1):
+            d[r - 1] -= 1
+            d[r - 2] = d.get(r - 2, 0) + 1
+        return d
+    saved = FAIL[:]
+    QUIET[0] = True
+    rej.append(("perturbed closed form (m = 3)", not part_counts(bad_closed, quiet=True, ms=(3,), sample=False)))
+    _, tops, profs = part_recur(quiet=True)
+    rej.append(("T_5 claimed 834241/278849", tops[5] != F(834241, 278849)))
+    rej.append(("T_6 claimed 1188222/399684", tops[6] != F(1188222, 399684)))
+    t_bad, _ = run((27456, 48576, 68321, 86592), 6)
+    rej.append(("a3 = 68321 reproduces T_5", t_bad[5] != tops[5]))
+    okq, _ = dominating_ok(60, lambda j: F(1, 2 ** (j + 2)), QDOWN)
+    rej.append(("dominating chain with up-probability 2^-(j+2)", not okq))
+    okq2, _ = dominating_ok(60, QUP, lambda j: 1 - F(1, 2 ** (j + 1)))
+    rej.append(("dominating chain with down-probability 1 - 2^-(j+1)", not okq2))
+    rej.append(("3 in 9 at m=6 claimed excluded", not (tops[6] * 3 > 9)))
+    rej.append(("3 in 8 at m=5 claimed allowed", not (tops[5] * 3 <= 8)))
+    tw, _ = run((27456, 86592 - 2 * 27456, 86592 - 27456, 86592), 6)
+    rej.append(("2.99172 claimed from triangle-only inputs", tw[5] < F(299172, 100000)))
+    fake = [0, 1, 3, 2, 4]
+    rej.append(("nonmonotone profile accepted", not all(fake[r] <= fake[r + 1] for r in range(1, 4))))
+    QUIET[0] = False
+    del FAIL[:]
+    FAIL.extend(saved)
+    for name, r in rej:
+        check(r, f"control not rejected: {name}")
+        print(f"control {'REJECTED' if r else 'ACCEPTED (bad)'}: {name}")
+    return all(r for _, r in rej)
+
+
+def main():
+    part_counts()
+    _, tops, profs = part_recur()
+    part_tail(profs)
+    part_sens()
+    part_shapes(tops)
+    part_controls()
+    if FAIL:
+        print(f"FAIL ({len(FAIL)} checks)")
+        return 1
+    print("PASS_PROJECTION_RECURSION_CHECK")
+    return 0
+
+
+if __name__ == "__main__":
+    sys.exit(main())