diff --git a/research/pr4623-budget-check/README.md b/research/pr4623-budget-check/README.md
new file mode 100644
index 0000000000..5a10ea7d47
--- /dev/null
+++ b/research/pr4623-budget-check/README.md
@@ -0,0 +1,46 @@
+# Independent check of #4623's idle-mass bookkeeping and tangent bounds
+
+**Task:** independent-moment (independent check). **Base:** canonical main `f626db5c`. **No κ is claimed.**
+
+## The claim
+
+dillona's #4623 (head `fd5d3be1`) deletes the whole-idle stages and bounds what this can save. Its BUDGET.md says that:
+
+- the complex p16 main output mass falls from 177,408 to 35,840, with the idle mass cancelled exactly;
+- tangent bounds A(t) and B_J(t) are negative at C = .006 (complex) and C = .007 (BIT).
+
+Nothing is imported from #4623.
+
+## Results
+
+- **Masses.** From main's pinned `joint-helper-lattice/CONTROLLER.json`, the main target mass is **177,408** and the idle paid mass is **141,568**. Their difference, **35,840**, equals #4623's determinant formula M_p = 2v[p + b(p+2)] with v = 112, b = 8 and p = 16.
+- **Tangent bounds.** The engine is 40-digit Decimal, with h(t) = local helper moment − local paid moment:
+  - complex: PR4470's lists, v = 112, b = 8;
+  - BIT: 439 H8 helpers against the PR589 local paid list, v = 111, b = 7.
+
+  The results match #4623's printed values to every digit, and all are negative:
+
+| inventory | C | A(t) | B_J(t) |
+|---|---|---|---|
+| complex | .006 | −2.6366097978 | −132.6282065738 |
+| BIT | .007 | −3.5731057049 | −133.1717283853 |
+
+- **Monotone extension (separator premise).** The equal-rank signed terms of h are positive only above the separator (complex: ranks 7, 8 and 9 above 6; BIT: rank 8 above 7.5) and negative only below it. The Jensen base 1 + b + 2b/p lies above the separator and the rank-one thin queries lie below it. So J_p(t)/separator^t increases in t, and the exclusion extends to every larger saving, as #4623 states.
+
+## Verify
+
+```text
+python3 -B research/pr4623-budget-check/verify.py
+```
+
+The check takes under 1 s and uses the standard library only.
+
+## Limitations
+
+**Not checked:** the repeated-evaluation and decoder barriers, and the precision lemma.
+
+## Open next questions
+
+- **Decoder barrier.** Check #4623's copied-input decoder rank p − 1 independently. First step: rebuild the per-port query matrix for p = 2 and 3 exactly.
+
+Credit: dillona (Dillon) for #4623; Cinna Davis and the #4440/#4470/BIT lineage. Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance.
diff --git a/research/pr4623-budget-check/SOURCES.json b/research/pr4623-budget-check/SOURCES.json
new file mode 100644
index 0000000000..ee9a881cd5
--- /dev/null
+++ b/research/pr4623-budget-check/SOURCES.json
@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40",
+      "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+      "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+    },
+    {
+      "path": "research/joint-helper-lattice/CONTROLLER.json",
+      "usage": "input",
+      "git_blob": "49a2f0675819f9deeea27ed77be2c2b6ff2e87e5",
+      "sha256": "1f5d6aa267e4e66048818714b5d3b5eae17a58abe91d15deeaa34574f7391a5f"
+    }
+  ]
+}
diff --git a/research/pr4623-budget-check/TASK.json b/research/pr4623-budget-check/TASK.json
new file mode 100644
index 0000000000..174e65311b
--- /dev/null
+++ b/research/pr4623-budget-check/TASK.json
@@ -0,0 +1,100 @@
+{
+  "schema_version": 1,
+  "task_id": "independent-moment",
+  "priority_revision": 7,
+  "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1",
+  "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": "unchanged",
+  "actual_scope": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?",
+  "scope_change_reason": null,
+  "bottleneck_link": "Independent coverage of #4623's controller-level idle-deletion budget.",
+  "budget_minutes": 20,
+  "stop_rule": "Stop at masses and tangent bounds.",
+  "outcome": "completed",
+  "evidence": "Main mass 177,408 - idle 141,568 = 35,840 = M_p from pinned controller; Decimal tangent bounds match #4623 at C=.006/.007 and are negative.",
+  "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance",
+  "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance; no independent human review.",
+  "open_questions": [
+    {
+      "question": "Monotone separator extension.",
+      "why_it_matters": "Extends the exclusion to all larger savings.",
+      "first_step": "Compare equal-rank signed terms of h with the separator.",
+      "blocked_by": "None."
+    }
+  ]
+}
diff --git a/research/pr4623-budget-check/VERIFY.json b/research/pr4623-budget-check/VERIFY.json
new file mode 100644
index 0000000000..baa7cee89f
--- /dev/null
+++ b/research/pr4623-budget-check/VERIFY.json
@@ -0,0 +1,22 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "certificates/selected-result.json",
+    "docs/research/agent-task-catalog.json",
+    "research/joint-helper-lattice/CONTROLLER.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Mass bookkeeping from pinned controller; Decimal tangent bounds vs #4623 printed values."
+    }
+  ]
+}
diff --git a/research/pr4623-budget-check/verify.py b/research/pr4623-budget-check/verify.py
new file mode 100644
index 0000000000..38dcfd89b8
--- /dev/null
+++ b/research/pr4623-budget-check/verify.py
@@ -0,0 +1,61 @@
+#!/usr/bin/env python3
+"""Independent check of PR #4623's (dillona, head fd5d3be1) BUDGET.md mass bookkeeping and tangent bounds.
+
+Checks, with nothing imported from #4623: (1) from main's pinned joint-helper-lattice/CONTROLLER.json, the complex p16
+main target mass 177,408 minus the idle paid mass 141,568 equals the determinant formula M_p = 2v[p + b(p+2)] = 35,840
+(v = 112, b = 8, p = 16); (2) in 40-digit Decimal, the tangent bounds A(t) = h - v + 2v(1+b)^t and
+B_J(t) = 2h + v + 4vbt(1+b)^(t-1), h = local helper minus local paid moment, match #4623's printed values at
+C = .006 (complex, PR4470 lists) and C = .007 (BIT, 439 H8 helpers vs the PR589 local list) and are negative.
+(3) the separator premise of the monotone extension (signed equal-rank terms of h, Jensen base, thin query).
+Not checked: decoder and precision sections.
+Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0.
+"""
+from decimal import Decimal as D, getcontext
+import json
+from pathlib import Path
+import sys
+
+ROOT = Path(__file__).resolve().parents[2]
+getcontext().prec = 40
+
+
+def need(condition, message):
+    if not condition:
+        raise AssertionError(message)
+
+
+def moment(h, t):
+    return sum(D(n) * (D(r).ln() * t).exp() for r, n in h.items())
+
+
+def bounds(helpers, paid, v, b, c):
+    t = 1 - D(c)
+    h = moment(helpers, t) - moment(paid, t)
+    a = h - v + 2 * v * (D(1 + b).ln() * t).exp()
+    bj = 2 * h + v + 4 * v * b * t * (D(1 + b).ln() * (t - 1)).exp()
+    return a, bj
+
+
+def main():
+    row = json.loads((ROOT / "research/joint-helper-lattice/CONTROLLER.json").read_text(encoding="utf-8"))
+    main_mass = sum((1 + 8 * sum(term[1:])) * 112 for term in row["diagonal"])
+    idle = sum(8 * len(e[2]) * 224 for e in row["physical_events"] if e[0] == "IDLE")
+    need(main_mass == 177408 and idle == 141568 and main_mass - idle == 2 * 112 * (16 + 8 * 18) == 35840, "masses")
+    ca, cb = bounds({4: 28, 7: 7, 8: 47, 9: 326}, {1: 2237, 2: 388, 3: 494, 4: 147, 5: 36, 8: 8}, 112, 8, ".006")
+    ba, bb = bounds({8: 439}, {1: 1323, 2: 1342, 3: 79, 4: 44, 5: 102, 6: 11, 7: 19}, 111, 7, ".007")
+    for got, printed in ((ca, "-2.6366097977"), (cb, "-132.6282065737"), (ba, "-3.5731057048"), (bb, "-133.1717283852")):
+        need(abs(got - D(printed)) < D("1e-9") and got < 0, "tangent bound matches #4623 and is negative")
+    # monotone extension: equal-rank signed terms of h sit on the correct side of the separator, as do the Jensen main
+    # base 1 + b + 2b/p (> separator) and the rank-one thin queries (< separator); then J_p(t)/sep^t increases in t
+    for helpers, paid, b, sep in (({4: 28, 7: 7, 8: 47, 9: 326}, {1: 2237, 2: 388, 3: 494, 4: 147, 5: 36, 8: 8}, 8, 6),
+                                  ({8: 439}, {1: 1323, 2: 1342, 3: 79, 4: 44, 5: 102, 6: 11, 7: 19}, 7, D("7.5"))):
+        signed = {r: helpers.get(r, 0) - paid.get(r, 0) for r in set(helpers) | set(paid)}
+        need(all((n > 0) == (r > sep) for r, n in signed.items() if n), "signed terms separated")
+        need(1 + b > sep and 1 < sep, "Jensen base above and thin query below the separator")
+    print(json.dumps({"status": "PASS_PR4623_BUDGET_CHECK", "monotone_separator": True, "main_mass": main_mass, "idle_mass": idle,
+                      "M_p": main_mass - idle, "complex_A_BJ": [str(ca)[:14], str(cb)[:16]],
+                      "BIT_A_BJ": [str(ba)[:14], str(bb)[:16]], "new_kappa_claimed": False}, indent=1))
+
+
+if __name__ == "__main__":
+    sys.exit(main())