From f9e68f40b0da7236a7fad415f7172218c0666d27 Mon Sep 17 00:00:00 2001
From: Nick Petalas <webmasternikos@gmail.com>
Date: Mon, 2 Nov 2026 19:38:12 +0000
Subject: [PATCH] feat(research): prove sharp direct higher-moment split charge

---
 research/direct-higher-moment-split/PROOF.md  | 142 ++++++++++++++
 research/direct-higher-moment-split/README.md | 141 ++++++++++++++
 .../direct-higher-moment-split/SOURCES.json   |  30 +++
 research/direct-higher-moment-split/TASK.json |  89 +++++++++
 .../direct-higher-moment-split/VERIFY.json    |  37 ++++
 research/direct-higher-moment-split/verify.py | 184 ++++++++++++++++++
 6 files changed, 623 insertions(+)
 create mode 100644 research/direct-higher-moment-split/PROOF.md
 create mode 100644 research/direct-higher-moment-split/README.md
 create mode 100644 research/direct-higher-moment-split/SOURCES.json
 create mode 100644 research/direct-higher-moment-split/TASK.json
 create mode 100644 research/direct-higher-moment-split/VERIFY.json
 create mode 100644 research/direct-higher-moment-split/verify.py

diff --git a/research/direct-higher-moment-split/PROOF.md b/research/direct-higher-moment-split/PROOF.md
new file mode 100644
index 0000000000..32a27958b2
--- /dev/null
+++ b/research/direct-higher-moment-split/PROOF.md
@@ -0,0 +1,142 @@
+# The sharp direct higher-moment split coefficient
+
+This proof was produced by Nick Petalas. Apache-2.0.
+
+## Theorem
+
+Fix real numbers `0<t<1` and `sigma>1`. For positive integers `R>J`, write
+`R=qJ+r`, where `q>=1` and `0<=r<J`, and set
+
+```
+split_t(R,J) = q J^t + r^t.
+```
+
+There is exactly one `s=s_(t,sigma)` in `(0,1)` satisfying
+
+```
+t s^(t-1) + (t-sigma)s^t - sigma = 0.
+```
+
+The least coefficient valid for every such integer split is
+
+```
+K(t,sigma) = (1+s^t)/(1+s)^sigma
+           = (t/sigma) s^(t-1) (1+s)^(1-sigma).
+
+split_t(R,J) <= K(t,sigma) R^sigma J^(t-sigma).
+```
+
+It satisfies `1<K(t,sigma)<K(t,1)<2`, where `K(t,1)` is the coefficient
+of PR4832. Equality at finite integers occurs exactly when `q=1` and
+`r/J=s_(t,sigma)`. The supremum is sharp even when that remainder is irrational.
+
+## Proof
+
+Divide the split charge by `R^sigma J^(t-sigma)` and put `s=r/J`. The ratio is
+
+```
+F_q(s) = (q+s^t)/(q+s)^sigma.
+```
+
+For a fixed `s` in `[0,1)`, extend `q` temporarily to a real variable `q>=1`.
+Its derivative has the sign of
+
+```
+(1-sigma)q + s - sigma s^t < 0.
+```
+
+Indeed `s<=s^t` and `sigma>1`. Thus every integer `q>1` is strictly worse
+than `q=1`. This step retains the denominator's full higher moment, unlike
+the linear-rank estimate followed by a separate moment comparison in PR4832.
+
+For `F_1`, the derivative on `(0,1)` has the sign of
+
+```
+h(s) = t s^(t-1) + (t-sigma)s^t - sigma,
+h'(s) = t(t-1)s^(t-2) + t(t-sigma)s^(t-1) < 0.
+```
+
+The function `h` tends to positive infinity at zero and has
+`h(1)=2(t-sigma)<0`. It has one zero, and this is the unique maximum of
+`F_1` on `[0,1]`. Its stationary equation gives the second expression for K.
+Since `F_1(0)=1` and the derivative is positive before that maximum, `K>1`.
+At its positive maximizer, division by `(1+s)^(sigma-1)>1` gives
+`K(t,sigma)<(1+s^t)/(1+s)<=K(t,1)`. PR4832 supplies `K(t,1)<2`.
+
+For sharpness over integers, let `J` tend to infinity and choose
+`r=floor(s_(t,sigma) J)`, `R=J+r`. Eventually `0<r<J`, and continuity makes
+the ratio tend to K. Every coefficient smaller than K therefore fails for
+some integer split. Strict quotient monotonicity and the unique maximum
+also give the stated equality characterization. This proves the theorem.
+
+## An exactly attaining rational-power example
+
+Take `t=1/2`, `sigma=17/10`. Substitution gives `h(1/16)=0`, so
+
+```
+s = 1/16,
+K = (5/4) (16/17)^(17/10),
+K^10 = (5/4)^10 (16/17)^17.
+```
+
+Every `J=16n`, `R=17n`, for positive integer n, attains the coefficient.
+Exact integer comparisons show `9/8<K<8/7<6/5`. In contrast,
+PR4832's cited coefficient `K(1/2,1)=(1+sqrt(2))/2` is greater than `6/5`.
+This is a strict improvement of the direct higher-moment coefficient.
+It does not by itself specify a realizable productive/paid profile.
+
+## Consequence for retained strictification
+
+Retain every chronological product, native, completion, splitting and compiler
+hypothesis of zxv's PR4433, section 2. Let `C=1-t`, `u>C`, `sigma=t+u>1`,
+`J=c^v` and `L=b^v`, with `1<c<b<m` and positive integer v. Write `P_x,T_x`
+for the raw paid and productive rank moments and B for its productive count.
+For every original paid rank R exceeding J, the theorem gives
+
+```
+split_t(R,J) <= K(t,t+u) R^(t+u) J^(-u).
+```
+
+The predecessor's moment multiplication and its unchanged unsplit overcount
+therefore bound the original-paid charge by
+
+```
+P_t^v + K(t,t+u) P_(t+u)^v / J^u.
+```
+
+Keep its full separate completion bound `2 B^v L J^(-C)` and the lower bound
+`T_t^v` on the completed productive moment. The complete sufficient charge is
+
+```
+alpha^v + K(t,t+u) gamma_u^v + 2 delta^v,
+alpha=P_t/T_t,
+gamma_u=P_(t+u)/(c^u T_t),
+delta=B b/(c^C T_t).
+```
+
+This strictly lowers the coefficient `K(t,1)` in PR4832 whenever `u>C`.
+The completion coefficient, unsplit overcount and all realization premises
+are retained. No particular inventory, tensor power or admitted supplier is
+certified here. The direct compiler of zxv's PR4483 can avoid strictification
+for profiles satisfying its own gates; this result makes no comparison to
+that compiler's sufficient sizes.
+
+## Exact finite certificate
+
+For rational `t=a/b`, `sigma=c/d`, put `y=s^(1/b)`. The critical equation
+becomes the strictly decreasing polynomial
+
+```
+ad + (ad-bc)y^b - bc y^(b-a) = 0.
+```
+
+The verifier bisects this polynomial using rational arithmetic. At any rational
+y, the normalized ratio's d-th power is exactly
+
+```
+F_q(y^b)^d = (q+y^a)^d / (q+y^b)^c.
+```
+
+Thus its root enclosures, finite split checks and attaining example require
+neither floating-point tolerances nor algebraic-number libraries. These checks
+corroborate the proof; they are not a universal census or proof-kernel acceptance.
diff --git a/research/direct-higher-moment-split/README.md b/research/direct-higher-moment-split/README.md
new file mode 100644
index 0000000000..ddfb5f4cab
--- /dev/null
+++ b/research/direct-higher-moment-split/README.md
@@ -0,0 +1,141 @@
+# Sharp direct higher-moment split charge
+
+For every real `0<t<1` and `sigma>1`, the least coefficient in
+
+```
+split_t(R,J) <= K(t,sigma) R^sigma J^(t-sigma),
+R=qJ+r>J,  0<=r<J,
+split_t(R,J)=q J^t+r^t,
+```
+
+is
+
+```
+K(t,sigma) = (1+s^t)/(1+s)^sigma,
+t s^(t-1)+(t-sigma)s^t-sigma=0,  0<s<1.
+```
+
+The defining equation has one solution, and the coefficient is sharp over
+integer jobs. This answers Open next question 2 of
+[PR4832](https://github.com/CrocSwap/integer-mult-bounds/pull/4832).
+The claim type is a scoped written proof with exact finite corroboration.
+
+The coefficient is strictly smaller than the linear-rank coefficient
+`K(t,1)` transferred to the higher moment. At `t=1/2, sigma=17/10`,
+
+```
+K = (5/4)(16/17)^(17/10),
+9/8 < K < 8/7 < 6/5 < K(1/2,1).
+```
+
+Every `J=16n, R=17n`, with positive integer n, attains this new coefficient.
+[PROOF.md](PROOF.md) proves the universal optimization, integer sharpness and
+its exact strictification consequence. No new kappa or selected-frontier change
+is claimed.
+
+## What changes in the retained compiler estimate
+
+Retain all hypotheses of zxv's
+[PR4433 higher-moment construction](https://github.com/CrocSwap/integer-mult-bounds/pull/4433).
+With `C=1-t` and `u>C`, its complete sufficient charge improves as follows.
+
+```diff
+-alpha^v + K(t,1)   gamma_u^v + 2 delta^v
++alpha^v + K(t,t+u) gamma_u^v + 2 delta^v
+```
+
+The full completion charge and unsplit overcount remain. The proof derives
+this consequence from the credited moment-product premise, without replaying
+predecessor programs or numbers. This is a sharp coefficient for the full
+split charge, not a net-tax optimum, a smaller demonstrated tensor power or
+a newly admitted supplier. PR4483's different direct compiler can avoid
+strictification under its own gates.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/direct-higher-moment-split/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/direct-higher-moment-split/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/direct-higher-moment-split
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/direct-higher-moment-split --check-source-history
+```
+
+Other hosts may substitute their CPython 3.12 path. The last check requires
+committed publication bytes. The scientific command prints a JSON receipt with
+`PASS_DIRECT_HIGHER_MOMENT_SPLIT`; the runner prints
+`PASS_REGISTERED_RESEARCH_PACKAGE`. To save a generated receipt, append
+`--receipt /absolute/path/outside/the/checkout.json` to a direct command.
+Normal replay writes no files. Receipts bind all six package files and both
+source documents by SHA256; no receipt is hand-written or treated as an oracle.
+
+The finite verifier checks 30 rational parameter pairs, 7,650 exact integer
+splits, 6,720 strict quotient comparisons and 30 near-maximizing integer
+witnesses. It also checks the exactly attaining family representative and
+13 rejecting controls. Rational polynomial bisection encloses each maximizing
+remainder; comparisons use powers of positive rational numbers. No floating
+point or predecessor executable is used. The written proof covers arbitrary
+real parameters; finite examples do not supply that universal quantification.
+Checks remain enabled under Python optimization.
+
+## Scope and overlap
+
+The `uniform-transfer-audit` card is changed from assumption audit to a new
+compiler coefficient theorem. This side result tightens one sufficient
+accounting bound; it does not discharge any of the five framework assumptions.
+The documented first source-binding control passes against selected PR6030.
+Source provenance is canonical main
+`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8.
+
+[The advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19358948)
+records the exact question. Entry checks inspected live open PRs, recent handoff
+claims, merged titles/bodies and distinctive formulas in all tracked main
+package READMEs. The question source predates the recent contribution series.
+Search coverage does not certify novelty; sparse notes, arbitrary historical
+diffs and unpublished work remain limits.
+
+Native semantics, dirty restoration, paid placement, chronological compiler
+closure, precision, stock, tape access and exact recovery remain inherited
+obligations. No physical caller, selected cold replay, native suite, Lean or
+Docker run is supplied. No independent human or proof-kernel acceptance is
+claimed.
+
+## Verification design
+
+The verifier has no recursion, subprocesses, callbacks or imported predecessor
+code. All scientific loops have explicit finite bounds. Its census uses six
+exponents, five higher moments, 32 remainder parameters and eight quotients;
+root isolation takes 72 steps. Rational parameters have denominators at most
+16, `0<t<1` and `1<sigma<=4`. Functions stay below 60 physical lines. Input
+source documents must match the declared hashes.
+
+Power of Ten deviation, rule 3: Python's integers, fractions and JSON serializer
+allocate dynamically. The fixed census, root precision, parameter limits and
+2 MB per-file check bound this verifier's mathematical workload. The reviewed
+local metadata files and synchronous standard-library reads are trusted inputs;
+this is not an allocation-free or hostile-filesystem parser. A fixed-memory
+port would be needed if that execution contract becomes a requirement.
+
+## Open next questions
+
+- Apply the coefficient to one fully charged supplier that still uses
+  strictification. First reuse its exact moment enclosures and replace only
+  this coefficient. A smaller sufficient tensor power must retain all native,
+  completion, compiler and outer premises.
+- Determine the least direct coefficient for the net splitting tax. Start with
+  `(q+s^t-(q+s)^t)/(q+s)^sigma`, and inspect PR4480's net-tax bounds. The quotient
+  monotonicity here concerns a different objective and cannot be transferred.
+
+## Credit
+
+This contribution was produced by Nick Petalas. Independent human and formal
+proof-kernel review are unclaimed. Apache-2.0.
+
+PR4832 supplies the question and linear-rank predecessor. zxv's PR4433 supplies
+the higher-moment splitting/completion framework; PR4480 and PR4483 retain their
+net-tax and direct-compiler results. Cinna Davis's PR4412/4414/4416 supplies the
+chronological tensor product and padding construction. Jacob Alan Sussman
+supplies the integer compiler. Their native, helper, controller and outer
+predecessors retain their existing credit. Elementary one-variable calculus
+is classical; no literature-priority claim is made.
diff --git a/research/direct-higher-moment-split/SOURCES.json b/research/direct-higher-moment-split/SOURCES.json
new file mode 100644
index 0000000000..de86a7c7f3
--- /dev/null
+++ b/research/direct-higher-moment-split/SOURCES.json
@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/higher-moment-strictification/README.md",
+      "usage": "input",
+      "git_blob": "0a736ca89e1eafb73a30e1f2589cc45e6b5f76c3",
+      "sha256": "ebe80b68ff026ce90f71f274c31744f4c0b36132d15ebb7e39cf2d5df4df270d"
+    },
+    {
+      "path": "research/sharp-integer-split-charge/README.md",
+      "usage": "input",
+      "git_blob": "224381ce045536f526282437cd2d4faffbbf01d3",
+      "sha256": "522439b2265b6a497a0d432e0911eb3e52e360650583c5469bc948da0cf6572d"
+    }
+  ]
+}
diff --git a/research/direct-higher-moment-split/TASK.json b/research/direct-higher-moment-split/TASK.json
new file mode 100644
index 0000000000..10a98282c9
--- /dev/null
+++ b/research/direct-higher-moment-split/TASK.json
@@ -0,0 +1,89 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "native_all_columns",
+      "owned_erasure",
+      "compiler",
+      "precision_tape",
+      "analytic_recovery"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Prove the least direct higher-moment coefficient for exact integer job splitting, answering PR4832 Open next question 2.",
+  "scope_change_reason": "Changed from auditing a selected assumption to a new sharp compiler inequality. This does not discharge the compiler assumption or supply a caller.",
+  "bottleneck_link": "Tightens the oversized paid-job term in the fully charged strictification construction. It is a compiler accounting side result, with no new native word or admitted saving.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first sharp coefficient theorem and exact attaining example; leave supplier-specific applications open.",
+  "outcome": "completed",
+  "evidence": "PROOF.md and verify.py: 30 rational parameter pairs, 7650 integer splits, 6720 quotient comparisons, 30 near-maximizing integer splits, one exact attaining family, and 13 rejecting controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Does the direct coefficient reduce a sufficient tensor power for one source-bound supplier that still uses strictification?",
+      "why_it_matters": "Turns the sharper universal accounting coefficient into a concrete construction-size gain.",
+      "first_step": "Substitute the new coefficient enclosure into an existing fully charged alpha/gamma/delta certificate.",
+      "blocked_by": "Requires an exact inventory and all unchanged native, completion, compiler and outer premises."
+    },
+    {
+      "question": "What is the sharp direct coefficient for the net splitting tax rather than the full split charge?",
+      "why_it_matters": "The retained unsplit overcount can dominate this sufficient bound.",
+      "first_step": "Optimize (q+s^t-(q+s)^t)/(q+s)^sigma while accounting for every integer quotient.",
+      "blocked_by": "The quotient reduction proved here does not apply to that different objective; check PR4480 net-tax bounds before proceeding."
+    }
+  ]
+}
diff --git a/research/direct-higher-moment-split/VERIFY.json b/research/direct-higher-moment-split/VERIFY.json
new file mode 100644
index 0000000000..568b7d64f2
--- /dev/null
+++ b/research/direct-higher-moment-split/VERIFY.json
@@ -0,0 +1,37 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/higher-moment-strictification/README.md",
+    "research/sharp-integer-split-charge/README.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact rational critical-root enclosures, finite integer split census, quotient monotonicity, sharp attaining fixture, source hashes and 13 rejecting controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "The same exact checks with optimization enabled; checks use explicit exceptions."
+    }
+  ]
+}
diff --git a/research/direct-higher-moment-split/verify.py b/research/direct-higher-moment-split/verify.py
new file mode 100644
index 0000000000..51d68adb38
--- /dev/null
+++ b/research/direct-higher-moment-split/verify.py
@@ -0,0 +1,184 @@
+#!/usr/bin/env python3
+"""Exact finite corroboration of the direct higher-moment split theorem.
+
+Produced by Nick Petalas. Apache-2.0.
+The universal statement is proved in PROOF.md; this census is bounded.
+"""
+
+import argparse
+import hashlib
+import json
+from fractions import Fraction as Q
+from pathlib import Path
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def parameters(t, sigma):
+    require(isinstance(t, Q) and isinstance(sigma, Q), "rational parameters required")
+    require(0 < t < 1 and 1 < sigma <= 4, "parameter range")
+    require(t.denominator <= 16 and sigma.denominator <= 16, "denominator budget")
+    return t.numerator, t.denominator, sigma.numerator, sigma.denominator
+
+
+def critical_polynomial(y, t, sigma):
+    a, b, c, d = parameters(t, sigma)
+    return a * d + (a * d - b * c) * y**b - b * c * y ** (b - a)
+
+
+def normalized_power(q, y, t, sigma):
+    a, b, c, d = parameters(t, sigma)
+    require(isinstance(q, int) and 1 <= q <= 8, "quotient budget")
+    require(isinstance(y, Q) and 0 <= y < 1, "remainder parameter")
+    return (q + y**a) ** d / (q + y**b) ** c
+
+
+def literal_split_power(q, y, t, sigma):
+    a, b, c, d = parameters(t, sigma)
+    numerator, denominator = y.numerator, y.denominator
+    cutoff = denominator**b
+    remainder = numerator**b
+    rank = q * cutoff + remainder
+    charge = q * denominator**a + numerator**a
+    return Q(charge**d * denominator ** (b * c - a * d), rank**c)
+
+
+def coefficient_enclosure(t, sigma):
+    a, b, c, d = parameters(t, sigma)
+    low, high = Q(0), Q(1)
+    for _ in range(72):
+        middle = (low + high) / 2
+        if critical_polynomial(middle, t, sigma) >= 0:
+            low = middle
+        else:
+            high = middle
+    require(critical_polynomial(low, t, sigma) >= 0, "lower root bracket")
+    require(critical_polynomial(high, t, sigma) < 0, "upper root bracket")
+    lower = normalized_power(1, low, t, sigma)
+    upper = (1 + high**a) ** d / (1 + low**b) ** c
+    require(1 < lower <= upper and upper - lower < Q(1, 2**52), "coefficient bracket")
+    return low, high, lower, upper
+
+
+def census():
+    exponents = (Q(1, 4), Q(1, 3), Q(1, 2), Q(2, 3), Q(3, 4), Q(7, 8))
+    moments = (Q(5, 4), Q(3, 2), Q(17, 10), Q(2), Q(3))
+    rows, cases, quotient_checks, witnesses = [], 0, 0, 0
+    for t in exponents:
+        for sigma in moments:
+            low, high, lower, upper = coefficient_enclosure(t, sigma)
+            for k in range(32):
+                y = Q(k, 32)
+                previous = normalized_power(1, y, t, sigma)
+                for q in range(1, 9):
+                    value = normalized_power(q, y, t, sigma)
+                    require(value == literal_split_power(q, y, t, sigma), "literal integer split")
+                    require(value <= upper, "split exceeds certified maximum")
+                    if q > 1:
+                        require(value < previous, "quotient monotonicity")
+                        quotient_checks += 1
+                    previous = value
+                    if k or q > 1:
+                        cases += 1
+            a, b, c, d = parameters(t, sigma)
+            cutoff, remainder = low.denominator**b, low.numerator**b
+            require(0 < remainder < cutoff, "integer sharpness witness")
+            require(Q(remainder, cutoff) == low**b, "integer normalization")
+            require(normalized_power(1, low, t, sigma) == lower, "witness value")
+            require(literal_split_power(1, low, t, sigma) == lower, "literal witness charge")
+            witnesses += 1
+            rows.append({"t": str(t), "sigma": str(sigma), "root_y": [str(low), str(high)],
+                         "K_power": d, "K_power_interval": [str(lower), str(upper)],
+                         "witness_cutoff_bits": cutoff.bit_length()})
+    require((cases, quotient_checks, witnesses) == (7650, 6720, 30), "census domain")
+    return rows, cases, quotient_checks, witnesses
+
+
+def sharp_fixture():
+    t, sigma, y = Q(1, 2), Q(17, 10), Q(1, 4)
+    require(critical_polynomial(y, t, sigma) == 0, "exact maximizing remainder")
+    power = Q(5, 4) ** 10 * Q(16, 17) ** 17
+    require(normalized_power(1, y, t, sigma) == power, "attaining J=16 R=17")
+    require(literal_split_power(1, y, t, sigma) == power, "literal attaining charge")
+    require(Q(9, 8) ** 10 < power < Q(8, 7) ** 10, "strict rational separation")
+    # PR4832's cited half-power coefficient is (1+sqrt(2))/2 > 6/5.
+    require(Q(2) > Q(7, 5) ** 2, "old coefficient exceeds 6/5")
+    require(power < Q(6, 5) ** 10, "strict improvement over linear-rank transfer")
+    return {"t": str(t), "sigma": str(sigma), "J": 16, "R": 17,
+            "maximizing_remainder": "1/16", "K_to_10": str(power),
+            "K_strict_interval": ["9/8", "8/7"]}
+
+
+def controls(fixture):
+    rejected = 0
+    invalid = ((Q(0), Q(2)), (Q(1), Q(2)), (Q(-1), Q(2)),
+               (Q(1, 2), Q(1)), (Q(1, 2), Q(0)), (Q(1, 2), Q(5)),
+               (Q(1, 17), Q(2)), (Q(1, 2), Q(33, 17)))
+    for t, sigma in invalid:
+        try:
+            parameters(t, sigma)
+        except ValueError:
+            rejected += 1
+        else:
+            raise ValueError("invalid parameters accepted")
+    for q, y in ((0, Q(1, 2)), (1, Q(-1, 2)), (1, Q(1))):
+        try:
+            normalized_power(q, y, Q(1, 2), Q(17, 10))
+        except ValueError:
+            rejected += 1
+        else:
+            raise ValueError("invalid split accepted")
+    for underclaim in (Q(1), Q(9, 8)):
+        require(underclaim**10 < Q(fixture["K_to_10"]), "false coefficient not rejected")
+        rejected += 1
+    require(rejected == 13, "control count")
+    return rejected
+
+
+def source_hashes():
+    package = Path(__file__).resolve().parent
+    root = package.parent.parent
+    names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py")
+    hashes = {}
+    for name in names:
+        data = (package / name).read_bytes()
+        require(len(data) <= 2_000_000, "package file budget")
+        hashes[f"research/direct-higher-moment-split/{name}"] = hashlib.sha256(data).hexdigest()
+    manifest = json.loads((package / "SOURCES.json").read_text())
+    inputs = [row for row in manifest["files"] if row["usage"] == "input"]
+    require(len(inputs) == 2, "source input count")
+    for row in inputs:
+        data = (root / row["path"]).read_bytes()
+        require(len(data) <= 2_000_000, "source file budget")
+        digest = hashlib.sha256(data).hexdigest()
+        require(digest == row["sha256"], "source pin mismatch")
+        hashes[row["path"]] = digest
+    return hashes
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--receipt", type=Path)
+    args = parser.parse_args()
+    rows, cases, quotient_checks, witnesses = census()
+    fixture = sharp_fixture()
+    rejected = controls(fixture)
+    result = {"status": "PASS_DIRECT_HIGHER_MOMENT_SPLIT", "claim_type": "scoped proof with finite corroboration",
+              "split_cases": cases, "quotient_comparisons": quotient_checks,
+              "integer_near_maximizers": witnesses, "rejected_controls": rejected,
+              "coefficient_enclosures": rows, "sharp_fixture": fixture, "sha256": source_hashes()}
+    payload = json.dumps(result, indent=2, sort_keys=True) + "\n"
+    if args.receipt is not None:
+        target = args.receipt.resolve()
+        require(not target.is_relative_to(Path(__file__).resolve().parent.parent.parent),
+                "keep generated receipts outside the checkout")
+        written = target.write_text(payload)
+        require(written == len(payload) and target.read_text() == payload, "receipt write")
+    print(payload, end="")
+
+
+if __name__ == "__main__":
+    main()