diff --git a/research/zero-mean-cyclotomic-height/PROOF.md b/research/zero-mean-cyclotomic-height/PROOF.md
new file mode 100644
index 0000000000..2f24cc7a91
--- /dev/null
+++ b/research/zero-mean-cyclotomic-height/PROOF.md
@@ -0,0 +1,158 @@
+# A zero-mean cyclotomic logarithm
+
+This scoped written proof was produced by Nick Petalas. It supplies one new
+Fourier estimate and substitutes it into Chafik Boukhalfa's
+[PR #1025](https://github.com/CrocSwap/integer-mult-bounds/pull/1025).
+The predecessor's resultant, cofactor and primitive-unit estimates are cited
+premises. Their replay is not this contribution. Independent human and formal
+proof-kernel review are unclaimed.
+
+## The finite Fourier identity
+
+Let r>=3 be an integer, zeta=exp(2 pi i/r), and define a real function on Z/r by
+
+    F(0)=-log r,
+    F(s)=log|1-zeta^s| for 1<=s<r.
+
+All logarithms are natural. Normalize Fourier coefficients by
+
+    Fhat(h)=(1/r) sum_s F(s) zeta^(-hs).
+
+Then
+
+    Fhat(0)=0,
+    Fhat(h)<0 for 1<=h<r,
+    sum_h |Fhat(h)|=log r.                                  (1)
+
+The special value at zero is never used in a coefficient product. It is a
+choice in the Fourier argument. No claim that it minimizes Fourier mass over
+all choices of that value is needed or made.
+
+For 0<=rho<1 put Lrho(s)=log|1-rho zeta^s|. The absolutely convergent
+logarithm series and finite Fourier orthogonality give, for 1<=h<r,
+
+    Lrho_hat(h)=-1/2 sum_(q>=0) [rho^(qr+h)/(qr+h)
+                                    +rho^(qr+r-h)/(qr+r-h)],
+    Lrho_hat(0)=(1/r)log(1-rho^r).
+
+When h=r/2 the two congruence classes coincide and the displayed halves
+correctly combine to one full term. Subtracting the mean and integrating
+the geometric series gives
+
+    -(Lrho_hat(h)-Lrho_hat(0))
+       =1/2 integral_0^rho
+          [x^(h-1)+x^(r-h-1)-2x^(r-1)]/(1-x^r) dx.          (2)
+
+As rho tends to one, the left side tends to -Fhat(h). Indeed the s=0
+summand cancels in the difference, all other summands converge, and
+sum_(s=1)^(r-1) log|1-zeta^s|=log r, by evaluating
+(X^r-1)/(X-1) at X=1. The same product proves Fhat(0)=0.
+
+The numerator of the integrand in (2) is positive for 0<x<1. Its quotient
+by 1-x equals
+
+    N_h(x)=sum_(a=h-1)^(r-2) x^a
+                  +sum_(a=r-h-1)^(r-2) x^a.
+
+Thus its quotient by 1-x^r is N_h(x)/S_r(x), where
+S_r(x)=1+x+...+x^(r-1). This extends continuously to x=1 and is positive
+on the open interval. The integral is finite and strictly positive.
+Consequently Fhat(h)<0. Fourier inversion at zero now gives
+sum_(h!=0) Fhat(h)=F(0)=-log r, proving (1).
+
+A second exact mass identity is
+
+    sum_(h=1)^(r-1) N_h(x)=2 S_r'(x).
+
+It makes the sum of the integrals in (2) equal to
+integral_0^1 S_r'/S_r=log r. These are elementary finite identities;
+no asymptotic equidistribution or irrational-rotation theorem is used.
+
+## Averaged coefficient height
+
+Use exactly PR #1025's polynomial and height notation:
+
+    n=r-1, D=phi(r), ell=ceil(log2 r),
+    a_(k,j)=product_(s=j+1)^n (1-zeta^(ks)),
+    f_k(z)=sum_(j=0)^n a_(k,j) z^j=r P_k(z),
+    H_k=sum_j |a_(k,j)|,
+
+where k runs over the units modulo r. For this section r is a prime power.
+Every suffix has s!=0, and multiplication by k preserves that fact. Fourier
+inversion therefore represents log|a_(k,j)| using F without changing a
+coefficient. Since Fhat(0)=0, the geometric-sum bound gives, simultaneously
+for every suffix,
+
+    log|a_(k,j)| <= sum_(h=1)^(r-1)
+                          |Fhat(h)| 2/|1-zeta^(hk)|.
+
+The same nonnegative right side also bounds the empty suffix, whose logarithm
+is zero. Let M_k be the maximum of these logarithms. PR #1025 proves that,
+for each nonzero h, the unit average of 2/|1-zeta^(hk)| is at most
+2(1+log r). This uses prime-power unit reduction and d/phi(d)<=2 for
+d=r/gcd(h,r), and is retained unchanged. Apply (1) to obtain
+
+    average_k M_k <= 2 log r (1+log r).
+
+There are r coefficients, so H_k<=r exp(M_k), and hence
+
+    sum_k log H_k <= D [2(log r)^2+3 log r].                 (3)
+
+This improves the predecessor's D[4(log r)^2+8 log r+2]. It averages a
+pointwise bound on the maximum. It does not interchange a maximum and an
+average or assert (3) at one chosen embedding.
+
+## Uniform circle gap
+
+For prime-power r, Ali Romman's PR #621 establishes the nonzero resultant
+used in PR #1025. The latter's norm/cofactor cancellation implies
+
+    |P_k(z)| >= 1/[2rn product_(a unit mod r) H_a^n], |z|=1.
+
+This is the cited implication, including its normalization, and is not a
+new resultant claim. Substitution of (3) yields
+
+    |P_k(z)| >= exp(-n D [2(log r)^2+3 log r])/(2rn).        (4)
+
+Write c=log 2. Since ell>=2, log r<=ell c and c<3/4,
+
+    [2(log r)^2+3 log r]/c
+        <= 2c ell^2+3ell
+        < (3/2)ell^2+3ell
+        <= 3ell^2.
+
+The last difference is (3/2)ell(ell-2)>=0. Also 2rn<=2^(1+2ell).
+The inherited coarse exponent, obtained from H_a<=2^r, remains available.
+Taking the smaller valid exponent proves
+
+    |P_k(z)| >= 2^-d_new,
+    d_new=1+2ell+n D min(r,3ell^2).                         (5)
+
+The predecessor's corresponding minimum uses 8ell^2. At r=4096,
+ell=12 and D=2048, (5) is 3,622,993,945, versus the predecessor's
+9,661,317,145. These are sufficient analytic gap exponents, not actual
+word lengths, norm measurements or timing results.
+
+## Exact finite corroboration and limits
+
+The verifier checks the N_h polynomial identities at every r=2..96 and
+1<=h<r. Its finite positive Abel sums also satisfy, exactly,
+
+    1/2 sum_(h=1)^(r-1) sum_(q=0)^(m-1)
+       [1/(qr+h)+1/(qr+r-h)-2/(qr+r)] = H_(mr)-H_m.
+
+Here H_j is a harmonic number, unrelated to the coefficient height H_k.
+The sum tends to log r. The script checks it at r=2..40, m=8,32 and
+encloses log r by an exact rational atanh series. The truncation tail is
+bounded geometrically, without binary floating point. Formal log(2),log(3)
+DFTs at r=3,4,6 independently check the chosen diagonal, zero mean and signs.
+Large dyadic budget cases test only integer exponent arithmetic.
+
+The universal analytic result is the written argument above. The finite
+checks do not prove it for every r. The primitive-unit estimate and the
+nonzero resultant remain cited predecessor premises. Composite radices,
+actual reduced-precision inverse execution, rounded preparation, common-label
+compilation, dirty restoration, physical tapes/hosting, full transforms and
+the multiplication theorem are outside this result. No new kappa or selected
+frontier change is claimed. The proof does not claim that 3 is an optimal
+dyadic coefficient or that this diagonal choice is optimal.
diff --git a/research/zero-mean-cyclotomic-height/README.md b/research/zero-mean-cyclotomic-height/README.md
new file mode 100644
index 0000000000..e6d363ffa5
--- /dev/null
+++ b/research/zero-mean-cyclotomic-height/README.md
@@ -0,0 +1,98 @@
+# A smaller averaged cyclotomic-height exponent
+
+This scoped written proof was produced by Nick Petalas. For every prime-power
+radix r>=3, put n=r-1, D=phi(r) and ell=ceil(log2 r). The coefficient heights
+of Chafik Boukhalfa's PR #1025 obey
+
+    sum_(k unit mod r) log H_k <= D [2(log r)^2+3 log r].
+
+The predecessor's bound is D[4(log r)^2+8 log r+2]. The new step sets the
+unused zero-residue value of log|1-zeta^s| to -log r. Its normalized Fourier
+transform has mean zero, every other coefficient is negative, and its exact
+absolute mass is log r. [PROOF.md](PROOF.md) derives the identity and substitution.
+
+The cited nonzero-resultant/cofactor argument then gives, uniformly in the
+primitive embedding and |z|=1,
+
+    |P_k(z)| >= 2^-d,
+    d=1+2ell+n D min(r,3ell^2).
+
+The predecessor uses 8ell^2. At r=4096 the sufficient gap exponent decreases
+from 9,661,317,145 to 3,622,993,945. These are analytic upper bounds on a
+sufficient exponent. No inverse at that precision was executed. No new kappa,
+physical supplier or selected-frontier change is claimed.
+
+## Reproduce
+
+From the repository root, using the local CPython 3.12 interpreter:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/zero-mean-cyclotomic-height
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/zero-mean-cyclotomic-height/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/zero-mean-cyclotomic-height --check-source-history
+```
+
+Other machines may substitute their CPython 3.12 path. Only the standard
+library is required. The standalone verifier also works in a Git-free export
+of these six files. It writes no files; stdout is a generated receipt bound
+to all six package-file hashes. Registered replay runs warning-strict normal
+and optimized modes. Explicit runtime checks remain active under optimization.
+
+The exact checks cover all kernel identities at r=2..96, harmonic telescoping
+at r=2..40 with two truncations, formal logarithmic DFTs at r=3,4,6, and
+integer prime-power/dyadic budgets. Controls reject altered kernels, a false
+zero mean and out-of-domain inputs. The proof supplies the universal result;
+finite arithmetic is corroboration, not a proof-kernel certificate.
+
+## Credit, overlap and limits
+
+Credit Chafik Boukhalfa / [#1025](https://github.com/CrocSwap/integer-mult-bounds/pull/1025)
+for averaged heights, the primitive-unit estimate and precision framework;
+Ali Romman / [#621](https://github.com/CrocSwap/integer-mult-bounds/pull/621)
+for the nonzero resultant and cofactor argument; Rohan Guliani / #846 and
+Charles Bethin / #764 for the retained solver and suffix lineage. Classical
+ingredients are the logarithm series, finite Fourier orthogonality and
+cyclotomic product. No historical priority is claimed for those tools.
+
+Hanson Sun / #1428 extends the earlier estimate to a different composite-radix
+domain. That extension is not pursued here. Nick Petalas / #5080 improves an
+independent inverse-envelope factor with a given circle gap; it does not prove
+this averaged-height estimate, and its follow-ups are not this target.
+Live PR bodies, the handoff discussion and merged/main searches were checked.
+Sparse local overlap coverage and unpublished work remain limits.
+
+No predecessor verifier is imported or replayed. Its analytic implications
+are cited premises, with exact proof/notice provenance in SOURCES.json.
+Actual reduced-precision inverse execution, preparation, common-label compiler,
+dirty restoration, physical tapes/hosting, full transform and multiplication
+obligations remain. No selected cold replay, native suite or Lean build was run.
+Independent human and formal proof-kernel review are unclaimed. Apache-2.0.
+
+## Open next questions
+
+Structured first steps and blockers are in [TASK.json](TASK.json).
+
+- Can another value at residue zero improve the complete interval bound,
+  including the resulting nonzero mean? Begin with its exact piecewise-linear
+  Fourier mass. Minimizing mass alone does not price the mean term.
+- Can the new height estimate be used in an actual reduced-precision inverse
+  execution with all preparation and rounding errors retained? Begin with one
+  fixed small prime-power instance of the cited arbitrary-stride solver.
+
+## Verifier constraints
+
+Functions are below 60 lines and loops have explicit fixed bounds. The only
+indirect calls are rejection controls with five locally named possible targets.
+There is no recursion, subprocess, network, dynamic code execution or output
+file creation. All mathematical comparisons use integers or Fraction.
+
+Power-of-ten rule 3 deviation: CPython allocates managed integers, Fractions
+and containers during checking. This six-file, one-shot verifier uses fixed
+domains, arrays of at most 97 coefficients, at most 1,280 harmonic terms and
+48 atanh terms. File reads are bounded by one MiB per file. No unbounded input
+is accepted. Inspection and the normal/optimized commands exercise these bounds.
+An embedded fixed-allocation implementation would require a separate runtime.
+Rule 9 deviation: the rejection helper calls only the five named local contract
+functions; every call has a fixed finite fixture and propagates unexpected
+exceptions. The eleven controls exercise the allowed targets. Python has no
+compiler warning mode; both registered checks use -W error and explicit guards.
diff --git a/research/zero-mean-cyclotomic-height/SOURCES.json b/research/zero-mean-cyclotomic-height/SOURCES.json
new file mode 100644
index 0000000000..f362dec0f9
--- /dev/null
+++ b/research/zero-mean-cyclotomic-height/SOURCES.json
@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/averaged-cyclotomic-height/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "3215a58a408a8c65796260d747eda23c4cd046af",
+      "sha256": "5f8ec1431faecb7a2503f8c2dd7e398e5a749176d36cd54ae57763b4a4f0d4c4"
+    },
+    {
+      "path": "research/averaged-cyclotomic-height/NOTICE.md",
+      "usage": "provenance",
+      "git_blob": "8ded624012439920c69bf66e9c176daa0b06305c",
+      "sha256": "4a0c8a8c8568ccea7dc4b0d9b455408b806da42d18521732ccc923a8275be2ce"
+    },
+    {
+      "path": "research/averaged-cyclotomic-height/vendor/pr621/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "0c757c37c70fdeb261d73f111ceedd3b233287bf",
+      "sha256": "2b8056c88e66f692f407450fff0414d41bcd09db8597be22e274a6c3dc20eb9e"
+    },
+    {
+      "path": "research/composite-height-audit-seed67/README.md",
+      "usage": "provenance",
+      "git_blob": "ee83d116a7035ea880089965454aa882eb487aa5",
+      "sha256": "2f05204e88ceb33a58f2abf6bd8d9b131f7b617263cfd40cc417fe4d568470eb"
+    }
+  ]
+}
diff --git a/research/zero-mean-cyclotomic-height/TASK.json b/research/zero-mean-cyclotomic-height/TASK.json
new file mode 100644
index 0000000000..a3eac03d3f
--- /dev/null
+++ b/research/zero-mean-cyclotomic-height/TASK.json
@@ -0,0 +1,105 @@
+{
+  "schema_version": 1,
+  "task_id": "independent-moment",
+  "priority_revision": 8,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "original_card": {
+    "id": "independent-moment",
+    "question": "Does a changed construction's serialized target/paid invoice independently support its claimed improvement?",
+    "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",
+      "docs/research/recursive-invoice-preflight.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": "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_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": "Independently recount one changed emitted word and its complete caller, importing no constructor or pricing engine. Include target losses, owned lifetimes, native orientation and extra charges. Check existing #5633/#5708/#5717/#5719 coverage to avoid duplicate audits and preserve its exact head. Stop after the chosen missing implication; a correct root alone is not supplier admission.",
+    "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": [
+      "invoice",
+      "signed moment",
+      "productive target",
+      "independent recount"
+    ],
+    "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": "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 a zero-mean finite Fourier logarithm identity and sharpen the prime-power averaged coefficient-height and uniform circle-gap exponents.",
+  "scope_change_reason": "This is a new analytic precision side result, rather than an independent recount of a recursive invoice. It improves a cited predecessor estimate without auditing it.",
+  "bottleneck_link": "A smaller sufficient circle-gap exponent can reduce a future cyclic inverse precision bill; no current physical caller or selected exponent is improved.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first proved smaller averaged-height envelope and package it with bounded exact corroboration.",
+  "outcome": "completed",
+  "evidence": "PROOF.md proves Fourier mass log r and the new averaged-height and dyadic envelopes. verify.py checks polynomial kernels, harmonic sums, formal logarithmic DFTs, integer budgets and rejection controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can another zero-residue value improve the complete interval bound, including the mean?",
+      "why_it_matters": "It may further reduce sufficient analytic precision.",
+      "first_step": "Derive the exact piecewise-linear Fourier mass as the diagonal value varies and retain the mean contribution.",
+      "blocked_by": "Minimum Fourier mass alone does not control the complete suffix bound."
+    },
+    {
+      "question": "Can one actual inverse run use the new height estimate at reduced precision?",
+      "why_it_matters": "The analytic exponent is not itself a physical precision saving.",
+      "first_step": "Instantiate one fixed small prime-power arbitrary-stride inverse with explicit preparation and rounding errors.",
+      "blocked_by": "No reduced-precision execution or complete caller is supplied here."
+    }
+  ]
+}
diff --git a/research/zero-mean-cyclotomic-height/VERIFY.json b/research/zero-mean-cyclotomic-height/VERIFY.json
new file mode 100644
index 0000000000..c817ba6870
--- /dev/null
+++ b/research/zero-mean-cyclotomic-height/VERIFY.json
@@ -0,0 +1,32 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact polynomial, harmonic, formal Fourier and budget corroboration with rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "The same explicit contracts with assertions disabled."
+    }
+  ]
+}
diff --git a/research/zero-mean-cyclotomic-height/verify.py b/research/zero-mean-cyclotomic-height/verify.py
new file mode 100644
index 0000000000..d5be295e91
--- /dev/null
+++ b/research/zero-mean-cyclotomic-height/verify.py
@@ -0,0 +1,216 @@
+"""Exact finite corroboration; the universal analytic proof is in PROOF.md."""
+
+from fractions import Fraction as F
+import hashlib
+import json
+from pathlib import Path
+import sys
+
+
+def require(condition: bool, message: str) -> None:
+    if not condition:
+        raise ValueError(message)
+
+
+def numerator(r: int, h: int) -> list[int]:
+    require(2 <= r <= 96 and 1 <= h < r, "kernel domain")
+    result = [0] * r
+    for a in range(h - 1, r - 1):
+        result[a] += 1
+    for a in range(r - h - 1, r - 1):
+        result[a] += 1
+    return result
+
+
+def check_kernel(r: int, h: int, values: list[int]) -> None:
+    require(len(values) == r, "kernel length")
+    actual = [0] * (r + 1)
+    for a, value in enumerate(values):
+        actual[a] += value
+        actual[a + 1] -= value
+    expected = [0] * (r + 1)
+    expected[h - 1] += 1
+    expected[r - h - 1] += 1
+    expected[r - 1] -= 2
+    require(actual == expected, "divided kernel identity")
+    require(all(v >= 0 for v in values) and any(values), "positive kernel")
+
+
+def kernel_checks() -> int:
+    count = 0
+    for r in range(2, 97):
+        total = [0] * r
+        for h in range(1, r):
+            values = numerator(r, h)
+            check_kernel(r, h, values)
+            require(values == numerator(r, r - h), "reflection")
+            total = [a + b for a, b in zip(total, values, strict=True)]
+            count += 1
+        require(total == [2 * (a + 1) for a in range(r - 1)] + [0],
+                "sum of kernels equals twice S derivative")
+    return count
+
+
+def log_unit(value: F) -> tuple[F, F]:
+    require(1 <= value <= 2, "log interval domain")
+    z = (value - 1) / (value + 1)
+    total, power = F(0), z
+    for j in range(48):
+        total += 2 * power / (2 * j + 1)
+        power *= z * z
+    tail = 2 * power / (97 * (1 - z * z))
+    return total, total + tail
+
+
+def log_integer(r: int) -> tuple[F, F]:
+    require(2 <= r <= 4096, "integer log domain")
+    k = r.bit_length() - 1
+    a, b = log_unit(F(r, 1 << k))
+    c, d = log_unit(F(2))
+    return a + k * c, b + k * d
+
+
+def series_checks() -> int:
+    count = 0
+    for r in range(2, 41):
+        lo, hi = log_integer(r)
+        for m in (8, 32):
+            total = F(0)
+            for h in range(1, r):
+                for q in range(m):
+                    term = (F(1, q * r + h) + F(1, q * r + r - h)
+                            - F(2, q * r + r)) / 2
+                    require(term > 0, "positive Abel series term")
+                    total += term
+            harmonic = sum((F(1, j) for j in range(m + 1, m * r + 1)), F(0))
+            require(total == harmonic, "harmonic telescoping")
+            require(total < lo <= hi < total + F(1, m), "log limit enclosure")
+            count += 1
+    return count
+
+
+def fourier_fixture(r: int, diagonal: tuple[F, F]) -> list[tuple[F, F]]:
+    """Formal log(2),log(3) coefficients; all cosines are rational here."""
+    require(r in (3, 4, 6), "fixture radix")
+    zero = (F(0), F(0))
+    logs = {
+        3: [zero, (F(0), F(1, 2)), (F(0), F(1, 2))],
+        4: [zero, (F(1, 2), F(0)), (F(1), F(0)), (F(1, 2), F(0))],
+        6: [zero, zero, (F(0), F(1, 2)), (F(1), F(0)),
+            (F(0), F(1, 2)), zero],
+    }[r]
+    cosines = {
+        3: [F(1), F(-1, 2), F(-1, 2)],
+        4: [F(1), F(0), F(-1), F(0)],
+        6: [F(1), F(1, 2), F(-1, 2), F(-1), F(-1, 2), F(1, 2)],
+    }[r]
+    logs[0] = diagonal
+    result = []
+    for h in range(r):
+        row = tuple(sum((logs[s][a] * cosines[(h * s) % r]
+                         for s in range(r)), F(0)) / r for a in range(2))
+        result.append(row)
+    return result
+
+
+def check_fixture(r: int, diagonal: tuple[F, F]) -> None:
+    rows = fourier_fixture(r, diagonal)
+    require(rows[0] == (F(0), F(0)), "zero Fourier mean")
+    for a, b in rows[1:]:
+        require(a <= 0 and b <= 0 and (a < 0 or b < 0), "negative Fourier mode")
+    mass = tuple(-sum((row[a] for row in rows[1:]), F(0)) for a in range(2))
+    require(mass == tuple(-v for v in diagonal), "Fourier mass")
+
+
+def is_prime(n: int) -> bool:
+    require(2 <= n <= 512, "prime test domain")
+    return all(n % d for d in range(2, n))
+
+
+def budget(r: int, degree: int) -> tuple[int, int]:
+    require(r >= 3 and 1 <= degree < r, "budget domain")
+    ell = (r - 1).bit_length()
+    old = 1 + 2 * ell + (r - 1) * degree * min(r, 8 * ell * ell)
+    new = 1 + 2 * ell + (r - 1) * degree * min(r, 3 * ell * ell)
+    return old, new
+
+
+def budget_checks() -> tuple[int, int]:
+    c, d = log_unit(F(2))
+    require(F(2, 3) < c <= d < F(3, 4), "log two constants")
+    for ell in range(2, 1025):
+        require(2 * d * ell * ell + 3 * ell <= 3 * ell * ell,
+                "dyadic polynomial envelope")
+    cases = set()
+    for p in range(2, 513):
+        if is_prime(p):
+            r = p
+            for _ in range(9):
+                if r > 512:
+                    break
+                if r >= 3:
+                    cases.add((r, r - r // p))
+                r *= p
+    cases.update((1 << a, 1 << (a - 1)) for a in range(2, 129))
+    improved = 0
+    for r, degree in sorted(cases):
+        old, new = budget(r, degree)
+        require(new <= old, "budget monotonicity")
+        improved += new < old
+    require(budget(4096, 2048) == (9661317145, 3622993945), "4096 budget")
+    return len(cases), improved
+
+
+def expect_rejection(function, *args) -> None:
+    try:
+        function(*args)
+    except ValueError:
+        return
+    raise ValueError("control unexpectedly passed")
+
+
+def controls() -> int:
+    count = 0
+    for r, h in ((3, 1), (4, 2), (17, 7), (96, 95)):
+        wrong = numerator(r, h)
+        wrong[h - 1] += 1
+        expect_rejection(check_kernel, r, h, wrong)
+        count += 1
+    for r in (3, 4, 6):
+        expect_rejection(check_fixture, r, (F(0), F(0)))
+        count += 1
+    expect_rejection(numerator, 97, 1)
+    expect_rejection(numerator, 4, 0)
+    expect_rejection(log_unit, F(3))
+    expect_rejection(budget, 3, 3)
+    return count + 4
+
+
+def main() -> None:
+    require(len(sys.argv) == 1, "no command-line arguments are accepted")
+    kernels = kernel_checks()
+    series = series_checks()
+    for r, diagonal in ((3, (F(0), F(-1))), (4, (F(-2), F(0))),
+                        (6, (F(-1), F(-1)))):
+        check_fixture(r, diagonal)
+    cases, improved = budget_checks()
+    rejected = controls()
+    package = Path(__file__).resolve().parent
+    names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py")
+    hashes = {}
+    for name in names:
+        path = package / name
+        require(path.is_file() and path.stat().st_size <= 1_048_576, "package file bound")
+        hashes[name] = hashlib.sha256(path.read_bytes()).hexdigest()
+    print("PASS_ZERO_MEAN_CYCLOTOMIC_HEIGHT", json.dumps({
+        "kernel_identities": kernels, "harmonic_checks": series,
+        "exact_fourier_fixtures": 3, "budget_cases": cases,
+        "strict_budget_improvements": improved, "rejected_controls": rejected,
+        "radix4096_old_d": 9661317145, "radix4096_new_d": 3622993945,
+        "package_sha256": hashes,
+        "scope": "finite exact corroboration; universal proof is PROOF.md",
+    }, sort_keys=True))
+
+
+if __name__ == "__main__":
+    main()