Sharpen averaged cyclotomic gap from 8ell^2 to 3ell^2 (no new kappa)

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.

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.

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"
+    }
+  ]
+}