diff --git a/research/pr4416-moment-check/README.md b/research/pr4416-moment-check/README.md
new file mode 100644
index 000000000..685e6ca63
--- /dev/null
+++ b/research/pr4416-moment-check/README.md
@@ -0,0 +1,99 @@
+# Independent check of #4416's moment and paid-tail inequalities
+
+**Claim type: an independent certified finite check. No new κ.** This does
+not accept #4416. It checks none of its native audit, outer ledger or
+inherited premises.
+
+## Object
+
+[PR #4416](https://github.com/CrocSwap/integer-mult-bounds/pull/4416)
+(1337isnot1337, head `e9058860`) claims a conditional κ = 0.00268647, the
+highest open claim when this check ran. Its strictification (TENSOR.md §3–4)
+needs, at saving `C = 0.00268648` with `τ = 1 − C`:
+
+```text
+alpha = P_tau/T_tau < 1 - 1/10^8,
+gamma = P_1/(10^C T_tau) < 4991/5000,
+delta = 7688*11/(10^C T_tau) < 2/3,
+alpha^6240 + 2 gamma^6240 + 2 delta^6240 < 1.
+```
+
+Here `X_τ = Σ n_r r^τ`, over the raw p7 invoices `T` (7,688 targets) and `P`
+(55,998 paid calls). No outside check existed.
+
+## Results
+
+Every link holds, recomputed with exact rationals and enclosure widths below
+`10⁻³⁰`:
+
+| Link | Value | Required |
+| --- | --- | --- |
+| `alpha` | `0.999999984403908…`, so `1 − alpha = 1.56·10⁻⁸` | `< 1 − 10⁻⁸` |
+| `gamma` (`c = 10`) | `0.998191712473…` | `< 4991/5000` |
+| `delta` (`b = 11`) | `0.643824709152…` | `< 2/3` |
+| `(4991/5000)^390 < 1/2`, `(2/3)² < 1/2`, `6240 = 16·390` | exact | — |
+| Normalized bound `1/(1 + 6240/10⁸) + 4/2¹⁶` | `10240625039/10240638976` | `< 1` |
+| Gap | exactly `13937/10240638976 = 1.36095…·10⁻⁶` | as stated |
+
+**Binding.** The invoices in RESULT.json's strictification block equal its
+native-inventory block and the two lines in TENSOR.md:
+
+- the counts are 7,688 and 55,998;
+- the rank-one moments are 131,723 and 131,115, a surplus of 608;
+- the ambient is 121.
+
+All three enclosures overlap #4416's recorded intervals.
+
+**Headroom: the tested saving is at this invoice's ceiling.** As the tensor
+power grows, the construction works for every `C` with `alpha < 1`; `gamma`
+and `delta` stay below 1 there. The limit saving, where `alpha = 1`, is
+
+```text
+C* = 0.002686489049…,      C* − 0.00268648 = 9.05·10⁻⁹.
+```
+
+So #4416's κ = 0.00268647 uses essentially all the headroom of this native
+p7 invoice. A higher κ on this route needs a different invoice, not a larger
+tensor power.
+
+**Controls.**
+
+- Completing every target to the full ambient (`b = 121`) gives `delta > 1`.
+- The undamped rank-one tail `P_1/T_τ` exceeds 1.
+
+So both damping choices are needed, as TENSOR.md says.
+
+## Not covered
+
+- The native audit that produces `T` and `P`. These are taken from #4416's
+  inventory, not rebuilt from the word.
+- The tensor composition, completion and splitting proofs, which are written
+  arguments.
+- The compiler ranks, the nine outer cost rows and every inherited physical,
+  precision and analytic premise.
+
+## Reproduce
+
+```sh
+python3.12 -B research/pr4416-moment-check/verify.py
+```
+
+It prints `PASS_PR4416_MOMENT_CHECK` in about 90 seconds, using only the
+standard library. `vendor/` holds #4416's TENSOR.md and RESULT.json,
+byte-identical and SHA256-checked.
+
+## Open next questions
+
+1. **Rebuild `T` and `P` from #4416's native word.**
+   - *Why it matters:* the moment margin is only `5.6·10⁻⁹` above what
+     `alpha` needs. One extra paid call of rank 1 changes `alpha` by about
+     `1/131723`, far more than that margin.
+   - *First step:* census #4416's p7 native word with separate code.
+   - *Blocked by:* nothing.
+
+## Credit
+
+The construction and the invoices are #4416's (1337isnot1337, with OpenAI
+Codex assistance), building on zxv's #4359, #4405, #4412 and #4414, and Jacob
+Alan Sussman's Theorem 1G. Prepared by Ryanson Jonathan with substantial
+Claude Code (Claude Opus 5.5) assistance. Apache-2.0.
diff --git a/research/pr4416-moment-check/SOURCES.json b/research/pr4416-moment-check/SOURCES.json
new file mode 100644
index 000000000..fcfba8aa3
--- /dev/null
+++ b/research/pr4416-moment-check/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/pr4416-moment-check/TASK.json b/research/pr4416-moment-check/TASK.json
new file mode 100644
index 000000000..a6752fc6f
--- /dev/null
+++ b/research/pr4416-moment-check/TASK.json
@@ -0,0 +1,100 @@
+{
+  "schema_version": 1,
+  "task_id": "independent-moment",
+  "priority_revision": 7,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "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": "refined",
+  "actual_scope": "Independently certify #4416's strictification inequalities (alpha, gamma, delta at saving 0.00268648, the v = 6240 closing argument and the gap) from its recorded p7 invoice, and compute the invoice's limit saving.",
+  "scope_change_reason": "The card asks for independent coverage of a new paid-profile or moment claim; #4416 is the highest open conditional kappa and had no outside check.",
+  "bottleneck_link": "#4416 raises the conditional kappa to 0.00268647; its moment inequalities must hold before its native and outer premises are worth review.",
+  "budget_minutes": 30,
+  "stop_rule": "Stop once every stated inequality is certified or fails.",
+  "outcome": "completed",
+  "evidence": "verify.py: invoices bound across RESULT.json and TENSOR.md (7,688 / 55,998, rank-one 131,723 / 131,115); alpha = 0.9999999844 < 1 - 1e-8, gamma = 0.99819 < 4991/5000, delta = 0.64382 < 2/3 with enclosures below 1e-30 overlapping #4416's; integer comparisons and Bernoulli bound; normalized bound 10240625039/10240638976 and gap 13937/10240638976 exact; limit saving C* = 0.002686489049, 9.05e-9 above the tested saving; b = 121 and undamped-tail controls fail.",
+  "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": [
+    {
+      "question": "Rebuild #4416's T and P invoices from its native word with separate code.",
+      "why_it_matters": "alpha clears its 1e-8 requirement by only 5.6e-9; one extra rank-one paid call moves alpha by about 7.6e-6.",
+      "first_step": "Census #4416's p7 native word independently.",
+      "blocked_by": "None."
+    }
+  ]
+}
diff --git a/research/pr4416-moment-check/VERIFY.json b/research/pr4416-moment-check/VERIFY.json
new file mode 100644
index 000000000..ed22ca13a
--- /dev/null
+++ b/research/pr4416-moment-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": 600,
+      "checks": "Vendored TENSOR.md and RESULT.json hashes and phrases; invoice binding and aggregates; certified alpha, gamma, delta at 0.00268648; integer comparisons, Bernoulli step, exact normalized bound and gap; limit saving by bisection; completion-base and undamped-tail controls."
+    }
+  ]
+}
diff --git a/research/pr4416-moment-check/vendor/NOTICE.md b/research/pr4416-moment-check/vendor/NOTICE.md
new file mode 100644
index 000000000..9ddec5197
--- /dev/null
+++ b/research/pr4416-moment-check/vendor/NOTICE.md
@@ -0,0 +1,9 @@
+# Vendored files
+
+Byte-identical copies of `research/pr4359-p7-padding/TENSOR.md` (Git blob
+`8ecfd3e4d0bcb449ecb1e150c4f1f4fbb39ca656`) and `research/pr4359-p7-padding/RESULT.json`
+(Git blob `ebb30a9b3b94fb159a316350f7da57bde4a30c25`) from
+[PR #4416](https://github.com/CrocSwap/integer-mult-bounds/pull/4416) at head
+`e9058860b5c850760fdf970e796a96aefcdb1d98`. They are copied because that head is not reachable
+from canonical main; `verify.py` checks their SHA256 values. 1337isnot1337's work with OpenAI
+Codex assistance, building on zxv's #4359; Apache-2.0, as that package states.
diff --git a/research/pr4416-moment-check/vendor/RESULT.json b/research/pr4416-moment-check/vendor/RESULT.json
new file mode 100644
index 000000000..ebb30a9b3
--- /dev/null
+++ b/research/pr4416-moment-check/vendor/RESULT.json
@@ -0,0 +1,296 @@
+{
+  "endpoint": {
+    "compiler": {
+      "H0": 4307773805920,
+      "H1": 16201843136005340321,
+      "N_encoding": "2^16201843136005340321",
+      "delta": "1/1400000000",
+      "exit_coefficient_log2_upper": "26640",
+      "final_strict_power_gap": "1/1400000000",
+      "h": "1/26",
+      "materialized_tensor_rule_or_uniform_word": false,
+      "negative_log2_eta_upper": "147931769/1250000",
+      "paid_max_bound_encoding": "10^6240",
+      "rank_one_induction": "131723^n > 131115^n; target padding adds equal paid and target rank, and splitting preserves rank",
+      "t": "12466419/12500000",
+      "target_max_encoding": "121^6240",
+      "target_min_encoding": "11^6240",
+      "tensor_power": 6240,
+      "theta_upper": "25/26",
+      "z": "139623893/140000000",
+      "z0": "1396238929/1400000000"
+    },
+    "gain_over_PR4359": "38647/100000000",
+    "gain_over_PR4405": "19069/50000000",
+    "gain_over_PR4414": "33/5000000",
+    "gain_over_allfresh_p3": "5223/25000000",
+    "kappa": "268647/100000000",
+    "ledger_source_sha256": "d097e55f06c3f244f2074ffd7c1a0a5f3c4b4b6a6accf9619d1dde5c0ae85e15",
+    "minimum_outer_margin": "524529867/122500000000000000",
+    "negative_controls": {
+      "closed_epsilon": {
+        "actual_logarithmic_gamma_guard": "0",
+        "epsilon_below_one": "0",
+        "gaussian_above_main": "-1410399/122500000000000000",
+        "global_gamma_power_slack": "-1/7000000000",
+        "new_semantic_guard_with_C1_one": "0",
+        "source_axis_superpolynomial": "0"
+      },
+      "closed_uniform_gap": {
+        "new_complex_uniform_saving_above_b": "0"
+      },
+      "insufficient_BIT": {
+        "actual_bit_above_effective": "-270533/700000000"
+      },
+      "unfunded_outer_point": {
+        "boundary_algebraic_matrix_above_kappa": "-525470133/122500000000000000",
+        "fused_gaussian_above_kappa": "-526410399/122500000000000000",
+        "global_coordinate_router_above_kappa": "-3/700000000",
+        "group_bit_router_above_kappa": "-1405641599/490000000000000000",
+        "main_transform_above_kappa": "-700470133/122500000000000000"
+      }
+    },
+    "outer": {
+      "functional_checks": {
+        "fixed_halo_explicit_metadata_branch": "13475000001/175000000",
+        "new_BIT_row_stock_sublinear_in_active_group": "697899997009/700000000000",
+        "new_semantic_group_guard": "3/700000000"
+      },
+      "margins": {
+        "boundary_algebraic_matrix": "329093274529867/122500000000000000",
+        "fused_gaussian": "329093273589601/122500000000000000",
+        "global_coordinate_router": "1880533/700000000",
+        "group_bit_router": "1316373794358401/490000000000000000",
+        "group_scans": "349999999/350000000",
+        "main_transform": "329093099529867/122500000000000000",
+        "microbox_face_corrections": "13475000001/175000000",
+        "polynomial_products": "699999999/700000000",
+        "sparse_union_movement": "50094718274529867/122500000000000000"
+      },
+      "parameters": {
+        "a": "1880533/700000000",
+        "b": "940267/350000000",
+        "beta": "699999997/700000000",
+        "bit_saving": "27/10000",
+        "cap_xi": "111344718099529867/122500000000000000",
+        "complex_uniform_saving": "376107/140000000",
+        "d": "1/700000000",
+        "epsilon": "699999999/700000000",
+        "kappa": "268647/100000000",
+        "lambda_": "39892541/40000000",
+        "lambda_prime": "174529867/175000000",
+        "layout": "1/700000000",
+        "q": "470133/175000000",
+        "r0": "1/7000000000",
+        "stop": "1/700000000",
+        "tested_saving": "33581/12500000"
+      },
+      "strict_checks": {
+        "actual_bit_above_effective": "9467/700000000",
+        "actual_logarithmic_gamma_guard": "1/700000000",
+        "actual_logarithmic_group_guard": "11155282162970133/61250000000000000",
+        "alpha_logarithm_absorption": "1/7000000000",
+        "boundary_algebraic_matrix_above_kappa": "699529867/122500000000000000",
+        "cap_above_band": "50094718099529867/122500000000000000",
+        "cap_below_cell": "11155281725470133/122500000000000000",
+        "cap_below_phase_cell_power": "133655281900470133/122500000000000000",
+        "complex_above_effective": "1/700000000",
+        "complex_below_one_over_32": "9997233/350000000",
+        "complex_endpoint": "1/350000000",
+        "epsilon_below_one": "1/700000000",
+        "epsilon_positive": "699999999/700000000",
+        "fine_prime_halo_umbrella": "7/2",
+        "fused_gaussian_above_kappa": "698589601/122500000000000000",
+        "gaussian_above_main": "87029867/61250000000000000",
+        "global_coordinate_router_above_kappa": "1/175000000",
+        "global_gamma_power_slack": "9/7000000000",
+        "group_below_dimension": "1/350000000",
+        "group_bit_router_above_kappa": "3494358401/490000000000000000",
+        "group_gauge_power_slack": "11155282154220133/61250000000000000",
+        "group_key_fits_record": "1/350000000",
+        "group_positive": "699999997/700000000",
+        "group_scans_above_kappa": "698119469/700000000",
+        "halo_covers_generic_inverse_radius": "5",
+        "improvement_over_user_baseline": "477749790400418148631/500000000000000000000000",
+        "lambda_above_internal": "1/1400000000",
+        "lambda_above_sigma": "3/1400000000",
+        "lambda_above_tau": "1/1400000000",
+        "lambda_prime_above_lambda": "1/1400000000",
+        "lambda_prime_above_leaf": "699059733/245000000000000000",
+        "leaf_saving_above_effective": "349059733/245000000000000000",
+        "main_transform_above_kappa": "524529867/122500000000000000",
+        "membership_arithmetic_fits_record": "1/700000000",
+        "microbox_face_corrections_above_kappa": "2155924779/28000000",
+        "microbox_halo_volume": "55300000003/700000000",
+        "new_complex_uniform_saving_above_b": "1/700000000",
+        "new_semantic_guard_with_C1_one": "1/700000000",
+        "polynomial_products_above_kappa": "69811947/70000000",
+        "positive_layout_slack": "1/700000000",
+        "q_below_effective": "1/700000000",
+        "q_below_internal": "1/700000000",
+        "q_below_leaf": "699059733/245000000000000000",
+        "q_positive": "470133/175000000",
+        "short_record_fallback": "349059733/350000000",
+        "source_axis_superpolynomial": "1/700000000",
+        "sparse_union_movement_above_kappa": "49765625699529867/122500000000000000",
+        "stop_below_one": "699999999/700000000",
+        "stop_positive": "1/700000000",
+        "strassen_integer_power_gap": "1951441519231",
+        "support_router_span": "3/700000000",
+        "theta_positive_polynomial_power": "2",
+        "union_header_fits_record": "3/700000000",
+        "union_tag_work_per_visit_fits_record": "3/700000000"
+      }
+    },
+    "schema": "native-p7-padding-strictification-outer-endpoint/1",
+    "scope": "Source-bound native p7 geometry, a finite tensor recipe with target padding, exact moment and outer inequalities, and a specified finite uniform rank. Native tensor closure and the PR4359 inherited precision, storage, analytic, fixed-tape and recovery hypotheses are written premises, not a full formal theorem certificate.",
+    "status": "PASS_CONDITIONAL_P7_OUTER_POINT",
+    "strictification_source_sha256": "1f3c2a38b34d9dad7266be212ca5d0225827d8e05bda4831e6c25c5713f624f0",
+    "tested_saving": "33581/12500000"
+  },
+  "independent_interval_crosscheck": true,
+  "scope": "Conditional native construction and exact finite arithmetic. The finite word and inherited physical, precision, analytic and fixed-tape proofs are not formally verified or materialized by this checker.",
+  "source_files": 23,
+  "status": "PASS_SOURCE_BOUND_CONDITIONAL_P7_PAID_PADDING_IMPROVEMENT",
+  "strictification": {
+    "alpha_interval": {
+      "lower": "0.99999998440390797702869232902431332",
+      "upper": "0.99999998440390797702869232902431333"
+    },
+    "alpha_upper": "99999999/100000000",
+    "completion_decay_block_length": 2,
+    "controls": {
+      "one_decay_block_rejected": true,
+      "undamped_completion_rejected": true,
+      "unpadded_rank_one_tail_rejected": true
+    },
+    "cutoff_base": 10,
+    "cutoff_encoding": "10^6240",
+    "decay_block_count": 16,
+    "decay_block_length": 390,
+    "delta_interval": {
+      "lower": "0.64382470915163933966321257464784307",
+      "upper": "0.64382470915163933966321257464784308"
+    },
+    "delta_upper": "2/3",
+    "exponent": 6240,
+    "gamma_interval": {
+      "lower": "0.99819171247300624373216957625759087",
+      "upper": "0.99819171247300624373216957625759088"
+    },
+    "gamma_upper": "4991/5000",
+    "materialized_tensor_or_completed_word": false,
+    "native_inventory": {
+      "artifact_hash_encoding": "Uncompressed UTF-8 JSON, sort_keys=True, separators=(comma,colon)",
+      "artifact_sha256": "12784fff6a13e3752ea6e80018e0484c5766a8adf2e88a7e71c80cf2bb68f398",
+      "contacts": 6720,
+      "dimension": 121,
+      "factor_receipt_sha256": "6f96f6be5d8441f71cbe6ebb1657c69b543eb085b848b92b591b7ac01d6e6598",
+      "fresh_helper_fields": 6120,
+      "keep": 232127,
+      "limits": "Finite exact physical controller admission; inherited all-column local word, tensor strictification, new full-word precision/stock and outer transfer remain written proof obligations.",
+      "main_fields": 1568,
+      "native_scalar_allowance": 2490856,
+      "native_source_gate": "PASS_ACTUAL_ARBITRARY_HELPERS_AND_COMPLETE_PHASE_CORRECT_IDLE_JOBS",
+      "negative_controls": {
+        "omitted_endpoint_translation_rejected": 784,
+        "wrong_native_orientation_rejected": true
+      },
+      "p": 7,
+      "paid": {
+        "1": 37305,
+        "16": 448,
+        "2": 10695,
+        "3": 3360,
+        "32": 448,
+        "4": 1530,
+        "48": 448,
+        "5": 300,
+        "8": 1464
+      },
+      "paid_calls": 55998,
+      "productive_fields": 7688,
+      "rank_margin": 608,
+      "scalar_allowance": 2490856,
+      "schema": "source-bound-p7-all-fresh-complete-native-controller/1",
+      "source_sha256": {
+        "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/bit-compression/carrier-reuse/reference/joint_pair_dag.py": "8a0de761642d21919e969475c3f13e5d01a4bae7343c1e1f37c586d94b676a85",
+        "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/DATA-PHASES.json": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa",
+        "research/kappa-rebuild/bit/complex_controller_factor.py": "1de9aaf918e6a4f2f5448754c1f3c3da3b85e6257849ebd097af09859c4e5497",
+        "research/kappa-rebuild/bit/mixed_productive_bit.py": "b32291b0db7fc0d332ec444c70746ab0fb03351d2e50546f8bcb64060e3ff95e",
+        "research/kappa-rebuild/complex/fresh-certificates/THREE-base-HELPER-BOUNDARIES.json.gz": "f90517e395bde58c72cacd5d3481c4ea31d459fe4535384ac16547ac40460555",
+        "research/kappa-rebuild/complex/full-identity-certificates/RESULT.json": "943d5fad2fc529f470df05a35446e07ecaef7344abfce450d2c2eb2c9b3798f6",
+        "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-CANONICAL.json.gz": "6418ec3da24d548a57f5c3fe5b9062c26c9478e638504a61c387f5cfb5f4ed61",
+        "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz": "c54b0a3e129d28e6dbf74fa731fc3bb70fe3c6705f07256750fbecddcc842d39",
+        "research/kappa-rebuild/complex/full_identity_rebuild.py": "9af2ffbb0038c92e2a7d281081b0daaeadce75b11b566e5427845dc1af91e33d",
+        "research/kappa-rebuild/controller/P3-NATIVE-COVER.json.gz": "facfc6d6ecde151afb7e6a167776f3fdaac1c816e785a21a39f7f0bfd9140f3f",
+        "research/kappa-rebuild/controller/p3_native_cover.py": "fae71fcbbd20b9ee73b049cf6f43ea1d048217fb15feb6055a007e47da3363fe",
+        "research/kappa-rebuild/transfer-audit/p3_cover_audit.py": "a0fe9a26f77556e83b31b0c91fea909d6f3d8209d0f9f7ad4e5bc1375d33615e",
+        "research/kappa-rebuild/transfer-audit/p3_native_audit.py": "5504a55a50546418d10c522984438cdeedb44993f7c1dab7bd4aa1ae0515d902"
+      },
+      "status": "PASS_EXACT_LAURENT_ALL_MAIN_CONTACTS_ENDPOINTS_AND_FULL_IDLE_PHASES",
+      "targets": {
+        "121": 224,
+        "25": 448,
+        "41": 448,
+        "5": 420,
+        "57": 448,
+        "6": 270,
+        "7": 840,
+        "8": 1395,
+        "9": 3195
+      },
+      "whole_idle_profile": {
+        "16": 448,
+        "32": 448,
+        "48": 448,
+        "8": 1344
+      }
+    },
+    "new_max_target_encoding": "121^6240",
+    "new_min_target_encoding": "11^6240",
+    "normalized_moment_upper_rational": "10240625039/10240638976",
+    "paid": {
+      "1": 37305,
+      "16": 448,
+      "2": 10695,
+      "3": 3360,
+      "32": 448,
+      "4": 1530,
+      "48": 448,
+      "5": 300,
+      "8": 1464
+    },
+    "paid_rank_one_moment": 131115,
+    "productive_fields": 7688,
+    "rank_one_surplus_encoding": "131723^6240-131115^6240",
+    "schema": "p7-paid-target-completion-tensor-certificate/1",
+    "scope": "Exact moment bounds for the documented chronological native product, paid target completion and disjoint splitting. Native all-column, precision, storage, analytic and fixed-tape premises remain separate; no full multiplication theorem is formally verified.",
+    "source_sha256": {
+      "research/kappa-rebuild/architecture/mixed_target_probe.py": "011c3c9d0cf81103dc84d709a0e36793eb7c5ae3f23c85eac27650ef13afa04a"
+    },
+    "status": "PASS_EXACT_P7_TARGET_COMPLETION_STRICTIFICATION",
+    "strict_moment_verified": true,
+    "strictification_gap": {
+      "lower": "0.00000136095023295546357907266586564",
+      "upper": "0.00000136095023295546357907266586565"
+    },
+    "strictification_gap_rational": "13937/10240638976",
+    "target_floor_base": 11,
+    "target_floor_encoding": "11^6240",
+    "target_rank_one_moment": 131723,
+    "targets": {
+      "121": 224,
+      "25": 448,
+      "41": 448,
+      "5": 420,
+      "57": 448,
+      "6": 270,
+      "7": 840,
+      "8": 1395,
+      "9": 3195
+    },
+    "tested_saving": "33581/12500000",
+    "theta_upper": "25/26"
+  }
+}
diff --git a/research/pr4416-moment-check/vendor/TENSOR.md b/research/pr4416-moment-check/vendor/TENSOR.md
new file mode 100644
index 000000000..8ecfd3e4d
--- /dev/null
+++ b/research/pr4416-moment-check/vendor/TENSOR.md
@@ -0,0 +1,237 @@
+# Native tensor products with paid completion of small targets
+
+This construction applies to the all-fresh p7/keep232127 native word in
+`NATIVE.md`. It retains the source all-column arbitrary-input semantics,
+complete spectators, whole-job matchers, finite-program closure and integer
+uniform compiler. The local word and controller come from zxv's PR4359;
+the integer compiler is Jacob Alan Sussman's Theorem 1G. The tensor product
+construction follows PR4414. Apache-2.0; substantial OpenAI/Codex assistance.
+
+The new step is to complete small productive endpoints before choosing the
+paid-rank cutoff. The enormous finite program is specified algorithmically;
+it has not been materialized. Finite moment checks do not prove the inherited
+analytic, precision, storage, fixed-tape or recovery premises. The selected
+frontier is unchanged.
+
+## 1. Chronological native product
+
+Let U have productive ranks k_i and chronological paid ranks r_l, and V
+have productive ranks h_j and paid ranks s_a. Their ambient ranks equal
+their maximum productive ranks and contain every paid job. Work in the
+product ambient space, retaining every unused coordinate as an arbitrary
+spectator.
+
+For each role j of V, instantiate a separate U copy at column count h_j.
+Its independent arbitrary productive fields have labels (i,j). Give each
+copy its own initialized, erased and uncredited center banks. Run these
+copies in lockstep through their common scalar and paid-call list.
+
+At paid position l, pause all copies. Copy j requests a rank r_l*h_j job
+on its current physical owner. The owners are distinct across the copies;
+they may include centers and may contain correlated values. Invoke V at
+column count r_l on these j-indexed fields, using permitted role-specific
+whole-job matchers. Its endpoints provide the requested ranks h_j*r_l.
+Its owned centers have separate identities. Complete V and restore every
+matcher before resuming the suspended U copies. Never combine different
+paid positions of the same U copy.
+
+This is a finite acyclic chronological substitution. Arbitrary-input
+correctness allows correlated data in distinct slots; no input is copied
+to create productive credit. Its final targets have ranks k_i*h_j and its
+remaining paid jobs have ranks r_l*s_a. Thus both moments multiply.
+The same argument lifts at every further positive column multiplicity by
+substitution of the fixed coordinate, phase and scalar generators. It does
+not tensor a sum of matrix operators.
+
+For v copies of the p7 unit, write T_tau and P_tau for the raw target and
+paid moments and B for the number of raw productive fields. The product
+has B^v distinct productive fields, target moment T_tau^v, paid moment
+P_tau^v, and ambient m^v where m=121.
+
+## 2. Paid completion on the actual productive owners
+
+Choose integers 1<c<b<m and put L=b^v, J=c^v. For every product role of
+rank K<L, provide an additional paid positive transform on D=L-K disjoint
+axes of that same physical owner. Roles with K>=L receive no completion.
+
+For precision about coordinates, conjugate the complete existing product
+word by its permitted per-role whole-job normalizers: the inverse map is
+applied to each input and the corresponding map to its final output. This
+gives the canonical rank-K endpoint on that field. After the whole product
+has finished, apply the positive transform on axes K,...,L-1. The disjoint
+factors commute and give exactly the canonical rank-L endpoint. Restore
+the external matchers where the surrounding interface requires them.
+A map only on the output would not be a whole-job conjugation.
+
+Every field remains an arbitrary original productive input. There is no
+new productive credit and no new owned bank. Since L<m^v, the needed axes
+already fit in the complete ambient array. At larger column multiplicity,
+use the corresponding disjoint column blocks. Completion runs after the
+entire native product, so it cannot interfere with any suspended local
+request, scalar contact or center cleanup.
+
+The new targets have ranks max(K,L), hence moment at least T_tau^v.
+Their minimum is exactly L and their maximum is m^v. Adding D target
+rank and paying D rank preserves the original positive rank-one surplus.
+
+## 3. Split every paid job and bound both tails
+
+Write tau=1-C with 0<C<1. Replace each paid rank R>J by consecutive
+jobs on disjoint axes of ranks J,...,J,r where R=qJ+r and 0<=r<J.
+Omit a zero remainder. Keep the original whole-job normalizers around
+this complete replacement. The exact disjoint-axis identity preserves
+its endpoint and rank-one mass.
+
+For an original paid job R>J, its new charge satisfies
+
+```
+q*J^tau+r^tau <= R*J^(-C)+J^tau <= 2*R*J^(-C).
+```
+
+Retaining the original moment as an overcount for the lower paid jobs
+therefore bounds the original paid part by
+
+```
+P_tau^v + 2*P_1^v/J^C.
+```
+
+For each added completion D<L, the same partition gives the bound
+
+```
+charge(D) <= D*J^(-C)+J^tau < (L+J)*J^(-C) < 2*L/J^C.
+```
+
+This bound also covers D<J: then q=0 and D^tau<=J^tau. For D=0 there
+is no job. Summing over at most B^v productive roles bounds all additional
+completion calls by 2*B^v*L/J^C. Consequently the complete normalized
+moment, using the lower bound T_tau^v on the new target moment, is at most
+
+```
+alpha^v + 2*gamma^v + 2*delta^v,
+alpha = P_tau/T_tau,
+gamma = P_1/(c^C*T_tau),
+delta = B*b/(c^C*T_tau).
+```
+
+All three ratios must be below one. A favorable raw mixed moment alone
+does not imply this construction. Every final paid rank is at most c^v,
+strictly below every final target rank b^v. The complete target and paid
+inventories are generated by exact finite products, completion and integer
+division; no real-valued batching is used.
+
+## 4. Exact finite p7 instance
+
+The source-bound native audit supplies m=121 and the complete invoice
+
+```
+T = {5:420,6:270,7:840,8:1395,9:3195,25:448,41:448,57:448,121:224},
+P = {1:37305,2:10695,3:3360,4:1530,5:300,8:1464,16:448,32:448,48:448}.
+```
+
+There are 7,688 productive fields and 55,998 paid calls. Their rank-one
+moments are 131,723 and 131,115, with surplus 608. At the exact tested
+saving C=0.00268648 the rational interval checker proves
+
+```
+alpha < 1-1/10^8,
+gamma < 4991/5000       with c=10,
+delta < 2/3            with b=11.
+```
+
+Take v=6240. The exact integer comparison
+`(4991/5000)^390<1/2` gives gamma^v<2^-16. Also `(2/3)^2<1/2`,
+so delta^v<2^-3120<=2^-16.
+Bernoulli's inequality bounds alpha^v by 1/(1+v/10^8), so
+
+```
+alpha^v+2*gamma^v+2*delta^v
+  < 1/(1+6240/10^8)+4/2^16 < 1.
+```
+
+This proves an explicit finite power. The checker separately rejects an
+undamped completion tail and an insufficient single decay block. It also
+checks the raw rank-one cutoff-base-five tail at this point: that simpler
+tail condition fails, explaining why target completion is needed here.
+The exact sufficient gap is greater than 0.00000136095023295546.
+An earlier sufficient choice used v=30000, c=7 and b=8. The new parameters
+reduce the finite tensor power and the derived uniform rank at the same
+saving. No smallest tensor power or optimal native controller is claimed.
+
+## 5. Effective uniform rank
+
+The completed mixed unit has m_new=121^v, k_min=11^v and r_max<=10^v.
+The exact comparison 10^26<11^25 gives theta<25/26; put h=1/26.
+For ambient rank x>=m_new the inherited exit estimate gives
+
+```
+m_new*E(x)/x <= r_max*m_new^h*x^(-h)
+                < 2^((111/26)*v)*x^(-h),
+```
+
+using 10<16=2^4 and 121<128=2^7. For a desired uniform exponent
+z>t=1-C, put z0=(t+z)/2 and d=z0-t. The exact complement coefficient
+eta=z0*m_new^(z0-1), with z0>1/2, satisfies
+
+```
+-log2(eta) < 1+7*v*(1-z0).
+```
+
+Thus rational sufficient choices are
+
+```
+H0 = ceil((((111/26)*v)*d+1+7*v*(1-z0))/(h*d)),
+H1 = floor(H0*(1-z0)/(z-z0))+1,
+N = 2^H1.
+```
+
+Check H0>=7v to cover all base ranks. Below the threshold, positive
+rank-one surplus gives L(x)<=x. Above it, the source strong induction gives
+L(x)<=A*x^z0 with A=(2^H0)^(1-z0). The strict H1 inequality then gives
+L(N)<N^z. The endpoint script supplies exact H0 and H1 and replays all
+outer predicates. It uses the actual new eta, not a dimension-independent
+lower bound inherited from a small raw word.
+
+## 6. Full constants and conditional scope
+
+Expand the product, completion, splitting and uniform compiler. Let U_raw
+count actual raw p7 instances and allocate O=U_raw complete owned-center
+banks, retaining each until its owner erases it. This counts raw units,
+not product macros. Let W be final productive width, P final rank-one
+paid count, and R the complete count of non-scalar native records and
+normalizers, including all completion, product and compiler routes.
+
+With S=2490856, the authenticated raw scalar allowance in `NATIVE.md`, use
+G=S*U_raw+8R as a conservative coefficient envelope. Pay actual coordinate
+movement separately. Unit phases and coordinate permutations have zero
+coefficient height. Substitute the new full-word constants
+
+```
+Z=W+O,
+E=64*(Z+N+P+G+1)^3,
+B_constant=P+E,
+C0=32*N*B_constant^2.
+```
+
+The completed-child recurrence retains the form
+`A(e)<=A(floor(e/N))+P*floor(e/N)+E`, hence A(e)<=2*B_constant*e.
+Every allocated field, scalar record, phase, role route, parking stack
+and borrowed-stock reserve comes from the newly expanded word. No old
+small-word numerical reserve is substituted for these counts.
+
+All these constants are finite and fixed before the multiplication input
+varies. Their absorption still requires the stated inherited physical,
+analytic, fine-prime, fixed-tape and exact-recovery hypotheses.
+
+The related [PR4375 tensor-frame audit](https://github.com/CrocSwap/integer-mult-bounds/pull/4375),
+read at head `9712f7cfc09723a557b3230a0d5e9826eaedcd2e`, concerns the
+different PR4088/PR4100 profile. It distinguishes one rank-r*f child from
+f scalar rank-r copies and leaves native frame realization and monomial
+pricing open. The construction here requires the complete PR4359 all-column
+contract: a paid position at column count f is one rank-r*f job, with every
+whole-job route charged. Factorwise repetition is not a substitute for that
+contract. The finite p7 geometry and moment checks do not independently
+discharge this all-column native or tape-action premise.
+
+Open next questions include reducing the sufficient tensor power, varying
+the target completion and paid cutoff, and extending the native controller
+only with independently verified contacts, phases and helper ownership.
diff --git a/research/pr4416-moment-check/verify.py b/research/pr4416-moment-check/verify.py
new file mode 100644
index 000000000..eae84e274
--- /dev/null
+++ b/research/pr4416-moment-check/verify.py
@@ -0,0 +1,161 @@
+#!/usr/bin/env python3
+"""Independent certified check of #4416's moment and paid-tail inequalities (kappa = 0.00268647).
+
+#4416 (TENSOR.md section 3-4) needs, at saving C and tau = 1 - C, with raw target invoice T, paid invoice
+P, B productive fields and completion bases c < b:
+    alpha = P_tau / T_tau,  gamma = P_1 / (c^C T_tau),  delta = B b / (c^C T_tau),
+    alpha^v + 2 gamma^v + 2 delta^v < 1,
+where X_tau = sum_r n_r r^tau. This recomputes alpha, gamma and delta with exact rational enclosures
+(ln by atanh after reducing by powers of two, exp by Taylor with a remainder), the closing integer
+comparisons at v = 6240, the gap, and the limit saving C* where alpha = 1. TENSOR.md and RESULT.json
+are vendored byte-identically. No code from #4416.
+Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0.
+"""
+from fractions import Fraction as Q
+import hashlib
+import json
+from pathlib import Path
+import sys
+
+HERE = Path(__file__).resolve().parent
+VENDORED = {
+    "vendor/TENSOR.md": "b2eba86cb979b4dc2a045f2e74bbd29e4d9e5ec87d6a2bc23ba7b54f1f58e3e3",
+    "vendor/RESULT.json": "9b814be97e3b45fcc28eafa8a65694897a7387f71a14d44796c6aadf303d7fab",
+}
+PHRASES = [
+    "T = {5:420,6:270,7:840,8:1395,9:3195,25:448,41:448,57:448,121:224},",
+    "P = {1:37305,2:10695,3:3360,4:1530,5:300,8:1464,16:448,32:448,48:448}.",
+    "alpha^v + 2*gamma^v + 2*delta^v,",
+    "alpha < 1-1/10^8,",
+    "gamma < 4991/5000       with c=10,",
+    "delta < 2/3            with b=11.",
+    "Take v=6240. The exact integer comparison",
+    "`(4991/5000)^390<1/2` gives gamma^v<2^-16. Also `(2/3)^2<1/2`,",
+    "Bernoulli's inequality bounds alpha^v by 1/(1+v/10^8), so",
+    "The exact sufficient gap is greater than 0.00000136095023295546.",
+]
+
+
+def need(condition, message):
+    if not condition:
+        raise AssertionError(message)
+
+
+def atanh_ln(x, terms=60):
+    z = (x - 1) / (x + 1)
+    s = 2 * sum(z ** (2 * k + 1) / (2 * k + 1) for k in range(terms + 1))
+    return s, s + 2 * z ** (2 * terms + 3) / ((2 * terms + 3) * (1 - z * z))
+
+
+LN2 = atanh_ln(Q(2))
+
+
+def ln_bounds(x):
+    """x >= 1 rational"""
+    k = (x.numerator // x.denominator).bit_length() - 1
+    c, d = atanh_ln(x / 2 ** k)
+    return k * LN2[0] + c, k * LN2[1] + d
+
+
+def exp_bounds(y, terms=40):
+    """0 <= y <= 1"""
+    s, term = Q(0), Q(1)
+    for k in range(terms + 1):
+        s += term
+        term = term * y / (k + 1)
+    return s, s + 3 * term
+
+
+def power_moment(inv, C):
+    """sum n r^(1-C) = sum n r exp(-C ln r), enclosed"""
+    lo = hi = Q(0)
+    for r, n in inv.items():
+        if r == 1:
+            lo, hi = lo + n, hi + n
+            continue
+        l_lo, l_hi = ln_bounds(Q(r))
+        lo += n * r / exp_bounds(C * l_hi)[1]
+        hi += n * r / exp_bounds(C * l_lo)[0]
+    return lo, hi
+
+
+def ratios(T, P, C, B, b, c):
+    t_lo, t_hi = power_moment(T, C)
+    p_lo, p_hi = power_moment(P, C)
+    l_lo, l_hi = ln_bounds(Q(c))
+    cc_lo, cc_hi = exp_bounds(C * l_lo)[0], exp_bounds(C * l_hi)[1]
+    P1 = sum(r * n for r, n in P.items())
+    return {"alpha": (p_lo / t_hi, p_hi / t_lo),
+            "gamma": (P1 / (cc_hi * t_hi), P1 / (cc_lo * t_lo)),
+            "delta": (B * b / (cc_hi * t_hi), B * b / (cc_lo * t_lo))}
+
+
+def main():
+    for rel, digest in VENDORED.items():
+        need(hashlib.sha256((HERE / rel).read_bytes()).hexdigest() == digest, f"vendored {rel}")
+    text = (HERE / "vendor/TENSOR.md").read_text()
+    for p in PHRASES:
+        need(p in text, f"TENSOR.md: {p[:40]}")
+    res = json.loads((HERE / "vendor/RESULT.json").read_text())["strictification"]
+    T = {int(k): v for k, v in res["targets"].items()}
+    P = {int(k): v for k, v in res["paid"].items()}
+    ni = res["native_inventory"]
+    need({int(k): v for k, v in ni["targets"].items()} == T and {int(k): v for k, v in ni["paid"].items()} == P,
+         "the strictification invoice is the native inventory's")
+    need(T == {5: 420, 6: 270, 7: 840, 8: 1395, 9: 3195, 25: 448, 41: 448, 57: 448, 121: 224}
+         and P == {1: 37305, 2: 10695, 3: 3360, 4: 1530, 5: 300, 8: 1464, 16: 448, 32: 448, 48: 448}, "the TENSOR.md invoice")
+    B = sum(T.values())
+    need(B == 7688 == ni["productive_fields"] and sum(P.values()) == 55998 == ni["paid_calls"], "counts")
+    T1, P1 = sum(r * n for r, n in T.items()), sum(r * n for r, n in P.items())
+    need((T1, P1) == (131723, 131115) and T1 - P1 == ni["rank_margin"] == 608, "rank-one moments and surplus")
+    need(max(T) == 121 == ni["dimension"], "ambient 121")
+
+    # the three ratios at the tested saving
+    C = Q(res["tested_saving"])
+    need(C == Q(33581, 12500000) and str(C.numerator * 10**8 // C.denominator) == "268648", "tested saving 0.00268648")
+    R = ratios(T, P, C, B, 11, 10)
+    need(R["alpha"][1] < 1 - Q(1, 10**8), "alpha < 1 - 1e-8")
+    need(R["gamma"][1] < Q(4991, 5000), "gamma < 4991/5000 (c = 10)")
+    need(R["delta"][1] < Q(2, 3), "delta < 2/3 (b = 11)")
+    for k in ("alpha", "gamma", "delta"):
+        lo, hi = R[k]
+        claimed = (Q(res[f"{k}_interval"]["lower"]), Q(res[f"{k}_interval"]["upper"]))
+        need(hi - lo < Q(1, 10**30) and not (hi < claimed[0] or lo > claimed[1]), f"{k} enclosure overlaps #4416's")
+
+    # the closing argument at v = 6240
+    v = 6240
+    need(v == 16 * 390 and Q(4991, 5000) ** 390 < Q(1, 2) and Q(2, 3) ** 2 < Q(1, 2), "integer comparisons")
+    need((1 - Q(1, 10**8)) ** 16 * (1 + 16 * Q(1, 10**8)) <= 1, "Bernoulli step, checked on a small power")
+    bound = 1 / (1 + v * Q(1, 10**8)) + 4 * Q(1, 2**16)
+    need(bound == Q(res["normalized_moment_upper_rational"]) and 1 - bound == Q(res["strictification_gap_rational"]), "normalized bound and gap")
+    need(1 - bound > Q("0.00000136095023295546"), "gap as stated")
+
+    # headroom: the limit saving C* with alpha = 1 (gamma, delta stay below 1 there)
+    lo, hi = C, Q(3, 1000)
+    need(ratios(T, P, hi, B, 11, 10)["alpha"][0] > 1, "alpha > 1 at 0.003")
+    for _ in range(30):
+        mid = (lo + hi) / 2
+        if ratios(T, P, mid, B, 11, 10)["alpha"][1] < 1:
+            lo = mid
+        else:
+            hi = mid
+    Rs = ratios(T, P, hi, B, 11, 10)
+    need(Rs["gamma"][1] < 1 and Rs["delta"][1] < 1, "gamma, delta < 1 at C*")
+
+    # control: completing every target to the full ambient (b = 121) breaks the completion tail
+    need(ratios(T, P, C, B, 121, 10)["delta"][0] > 1, "control: b = 121 gives delta > 1")
+    need(Q(P1, 1) / power_moment(T, C)[1] > 1, "control: an undamped rank-one tail P_1/T_tau exceeds one")
+
+    print(json.dumps({
+        "status": "PASS_PR4416_MOMENT_CHECK",
+        "alpha": f"{float(R['alpha'][1]):.15f}", "one_minus_alpha": f"{float(1 - R['alpha'][1]):.4e}",
+        "gamma": f"{float(R['gamma'][1]):.12f}", "delta": f"{float(R['delta'][1]):.12f}",
+        "gap": str(1 - bound),
+        "limit_saving_C_star": [f"{float(lo):.12f}", f"{float(hi):.12f}"],
+        "headroom_over_tested": f"{float(lo - C):.4e}",
+        "new_kappa_claimed": False,
+    }, indent=1))
+
+
+if __name__ == "__main__":
+    sys.exit(main())