Sharpen prime-power cyclotomic gap exponents (no κ)

research/prime-power-harmonic-gap/PROOF.md

@@ -0,0 +1,153 @@
+# Primitive-unit harmonic cancellation
+
+This scoped written proof was produced by Nick Petalas. The finite verifier
+corroborates the new inequalities; it is not a proof-kernel verification.
+Independent human and formal proof-kernel review are unclaimed.
+
+## New primitive-unit envelope
+
+Let q = p^a, where p is prime and a >= 1. Set N = floor(q/2),
+m = floor(N/p), and H_j = sum_{i=1}^j 1/i, with H_0 = 0.
+For every integer p >= 2, p <= 2^(p-1). The integral bounds
+H_N <= 1 + log N and H_m >= log(m+1) therefore give
+
+```text
+R_q = q/phi(q) sum_{1 <= j <= N, gcd(j,q)=1} 1/j
+    = (p H_N - H_m)/(p-1)
+   <= log N + p/(p-1) + log(N/(m+1))/(p-1)
+   <= log q - log 2 + 2 + log 2
+    = log q + 2.                                            (1)
+```
+
+The penultimate line uses N <= q/2, N < p(m+1),
+p/(p-1) <= 2 and log p/(p-1) <= log 2. This includes m = 0
+and q = 2. The subtracted term H_m must be retained.
+
+For 1 <= j <= q/2, the sine chord bound is
+sin(pi j/q) >= 2j/q. Pair j and q-j in the unit group. At q = 2,
+counting the single midpoint twice only enlarges the upper bound. Thus
+
+```text
+1/phi(q) sum_{j unit mod q} 1/sin(pi j/q) <= R_q <= log q + 2. (2)
+```
+
+Now let r be a prime power and 0 < h < r. Put q = r/gcd(h,r).
+Reduction of units modulo r onto units modulo q has uniform fibers,
+and multiplication by h/gcd(h,r) permutes those units. For any interval I
+of consecutive integers and zeta = exp(2 pi i/r), the geometric-sum bound
+and (2) imply
+
+```text
+average_{k unit mod r} 2/|1-zeta^(hk)| <= log q + 2 <= log r + 2,
+|sum_{s in I} zeta^(hks)| <= 2/|1-zeta^(hk)|.                (3)
+```
+
+The right side is independent of I. This replaces the bound
+2(1+log r) used in Chafik Boukhalfa's #1025. The new step is the
+primitive harmonic cancellation in (1), rather than a new unit-group
+surjectivity theorem or sine inequality. These elementary tools are classical.
+
+## Substitution into the credited height argument
+
+Use #1025's polynomial, normalization and embedding-specific heights:
+
+```text
+n = r-1, D = phi(r), ell = ceil(log2 r), t = log r,
+a_(k,j) = product_{s=j+1}^{r-1} (1-zeta^(ks)),
+f_k(z) = sum_{j=0}^{r-1} a_(k,j) z^j = r P_k(z),
+H_k = sum_{j=0}^{r-1} |a_(k,j)|.
+```
+
+Here r >= 3 is a prime power, k is a unit modulo r, and log is natural.
+The empty suffix has coefficient one. Nick Petalas's older #5930 proves
+the following Fourier identity for the auxiliary sampled logarithm F:
+
+```text
+F(0) = -log r, F(s) = log|1-zeta^s| for s != 0,
+Fhat(0) = 0, sum_{h != 0} |Fhat(h)| = log r.
+```
+
+This is a cited premise. Its proof and scientific verifier are not replayed
+here. The residue-zero value never enters a suffix product. Fourier inversion
+and (3) give a bound valid simultaneously for every suffix, including the
+empty suffix:
+
+```text
+M_k = max_j log|a_(k,j)|
+    <= sum_{h != 0} |Fhat(h)| 2/|1-zeta^(hk)|,
+average_k M_k <= t(t+2).
+```
+
+Since H_k <= r exp(M_k), the new averaged-height inequality is
+
+```text
+sum_{k unit mod r} log H_k <= D [t^2 + 3t].                 (4)
+```
+
+The older #5930 inequality is D[2t^2+3t]. This bounds an average
+of pointwise upper envelopes of maxima. It does not commute a maximum
+with an average and does not claim a bound on one chosen H_k.
+
+## Uniform circle gap and an integer exponent
+
+Ali Romman's #621 supplies prime-power resultant nonvanishing. The
+embedding-specific norm/cofactor implication in #1025 gives
+
+```text
+|P_k(z)| >= 1/[2rn product_{u unit mod r} H_u^n], |z| = 1.
+```
+
+Both are cited inputs, not new resultant or inverse theorems. Substitution
+of (4) gives the sufficient analytic gap
+
+```text
+|P_k(z)| >= exp(-nD[t^2+3t])/(2rn).                        (5)
+```
+
+Put B_ell = ceil(3ell^2/4 + 3ell). With c = log 2 < 3/4 and
+t <= ell c,
+
+```text
+(t^2+3t)/c <= c ell^2 + 3ell <= B_ell.
+```
+
+The inherited coarse height bound gives the alternative exponent nDr,
+and 2rn <= 2^(1+2ell). Hence, uniformly in the primitive embedding and
+circle point,
+
+```text
+|P_k(z)| >= 2^(-d_new),
+d_new = 1+2ell+nD min(r, B_ell).                           (6)
+```
+
+For ell >= 2, the difference between 3ell^2 and 3ell^2/4+3ell is
+3ell(3ell-4)/4 >= 3. Since 3ell^2 is an integer, B_ell <= 3ell^2.
+Thus (6) never worsens the cited #5930 exponent.
+At r = 4096, B_ell = 144, and the sufficient exponent decreases
+from 3,622,993,945 to 1,207,664,665. These are conservative analytic
+exponents, not executed precision, actual inverse norms or runtime measurements.
+
+## Finite evidence and limits
+
+The checker evaluates the exact R_q expression for prime powers through
+4096, comparing with rational lower enclosures of log q. It independently
+enumerates the coprime harmonic sum through 512. Through 128 it encloses
+the actual primitive cosecant average using rational Machin/alternating-series
+bounds, checks the sine chord and covers every primitive residue by pairing.
+The midpoint q = 2 is explicit. These checks exercise the new envelope,
+without replaying a predecessor result or computing the predecessor heights.
+
+Large dyadic and ternary exponent cases check only integer budget arithmetic.
+The generated stdout receipt enumerates the finite domains and binds all
+six package files by SHA256. Controls include deleting the divisible harmonic
+terms at q = 64 and replacing a needed exponent ceiling by a floor.
+
+This is a scoped analytic proof, not a complete multiplication theorem.
+It stays within prime-power radices. The concurrent #7195 mixed-radix extension
+of #1428 uses the existing general-radix envelope; no composite result is claimed
+here. Actual reduced-precision inverse execution, coefficient preparation,
+rounding, scratch restoration, physical tapes, common-label compilation,
+hosting, full cost, supplier admission and all five selected framework
+assumptions remain outside this result. No new kappa or selected-frontier
+change is claimed. No Lean, Docker, historical or selected scientific replay
+was run.

research/prime-power-harmonic-gap/README.md

@@ -0,0 +1,133 @@
+# A smaller prime-power cyclotomic gap exponent
+
+This scoped analytic proof was produced by Nick Petalas. A new primitive-unit
+harmonic estimate improves the averaged-height step of Chafik Boukhalfa's
+[#1025](https://github.com/CrocSwap/integer-mult-bounds/pull/1025).
+With the older zero-mean Fourier identity of
+[#5930](https://github.com/CrocSwap/integer-mult-bounds/pull/5930) as a cited
+premise, it gives, for every prime-power radix r >= 3,
+
+```text
+sum_{k unit mod r} log H_k <= phi(r) [(log r)^2 + 3 log r].
+```
+
+The cited previous bound is phi(r)[2(log r)^2+3 log r]. Here H_k is
+#1025's coefficient height at primitive embedding k, and log is natural.
+The improvement comes from retaining the p-divisible harmonic subtraction
+when averaging geometric sums over units of a prime power q. The new envelope
+is log q + 2, replacing 2(1+log r).
+
+Write ell = ceil(log2 r), n = r-1, D = phi(r), and
+B_ell = ceil(3ell^2/4 + 3ell). The cited norm/cofactor implication then gives
+
+```text
+|P_k(z)| >= 2^(-d_new) for every primitive k and |z| = 1,
+d_new = 1+2ell+nD min(r, B_ell).
+```
+
+At r = 4096 this sufficient gap exponent is **1,207,664,665**, compared
+with the cited #5930 exponent **3,622,993,945**. These are analytic bound
+values. No inverse at this precision was executed, and no kappa or selected
+frontier is changed. [PROOF.md](PROOF.md) gives the argument and its premises.
+
+## Evidence and reproduction
+
+The new finite checks pass with CPython 3.12.15 and its standard library:
+
+- 604 exact primitive harmonic bounds, covering every prime power from
+  2 through 4096, with 117 independently enumerated harmonic identities
+  through 512.
+- 44 rationally enclosed primitive cosecant averages through 128,
+  with 1,083 pairing classes covering 2,165 primitive residues. The midpoint
+  at q = 2 is handled separately.
+- 968 exact exponent cases, including all preceding prime powers r >= 3,
+  dyadic exponents 2 through 256 and ternary exponents 1 through 128.
+  There are 948 strict improvements over the cited formula.
+- 13 controls: eleven invalid-input rejections and two mathematical controls.
+  Dropping the divisible harmonic terms breaks the new estimate at q = 64;
+  a floor in place of the dyadic ceiling undercharges at ell = 3.
+
+The universal claim is the written proof, supported by these finite checks.
+No predecessor scientific executable is imported or replayed. Source proofs
+and the assignment context are bibliographic provenance in
+[SOURCES.json](SOURCES.json), rather than runtime inputs.
+
+Run from the worktree root:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/prime-power-harmonic-gap
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/prime-power-harmonic-gap/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/prime-power-harmonic-gap/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/prime-power-harmonic-gap --check-source-history
+```
+
+Other machines may substitute a CPython 3.12 path. The expected marker is
+`PASS_PRIME_POWER_HARMONIC_GAP`, followed by a generated JSON receipt binding
+all six package files by SHA256. The scripts write no files, need no Git or
+network, and use explicit checks that remain active under optimization.
+The registered commands run the normal and optimized verifier separately.
+
+## Scope and credit
+
+Base main is `e54523517d0f03e58352e647c403a5af3e525a57`, priority revision 8.
+The `formal-interface-lemma` card has changed scope to a mathematical
+precision lemma. This is a side result, with no formalization or actual
+selected-caller binding. The first source-binding orientation command passed;
+its selected #7000 result and all five assumptions are unchanged.
+
+The question source is #1025's prime-power averaging step. The older #5930
+Fourier identity is a premise, rather than a recheck or a question taken from
+its Open next questions. Concurrent
+[#7195](https://github.com/CrocSwap/integer-mult-bounds/pull/7195) substitutes
+that identity into an existing general-radix envelope. This package proves a
+new primitive-unit envelope within prime powers. Its main scientific step is
+different. Its displayed composite example is outside this package's domain;
+no additional calculation checked its numbers. Live searches and sparse local overlap coverage are recorded in
+[TASK.json](TASK.json); neither search absence nor an advisory claim proves
+novelty against unpublished work.
+
+Credit Chafik Boukhalfa / chafreaky #1025 for the averaged-height framework,
+normalization and embedding-specific norm estimate; Nick Petalas #5930 for
+the zero-mean Fourier identity; Ali Romman #621 for prime-power resultant
+nonvanishing and the cofactor argument; and Rohan Guliani #846, Chafik
+Boukhalfa #862/#977 and Charles Bethin #764 for the retained inverse and
+suffix lineage. Harmonic integral bounds, finite Fourier inversion, the sine
+chord, Machin's formula and alternating Taylor series are classical.
+No literature-priority claim is made for those methods. Existing predecessor
+files and notices are unchanged. New material is Apache-2.0.
+
+Prime-power nonvanishing, the Fourier identity and the norm implication remain
+cited premises. Composite radices, optimal constants, actual inverse execution,
+coefficient preparation, rounding, dirty restoration, physical tapes, hosting,
+complete paid costs and supplier admission are not established here. No Lean,
+Docker or selected scientific replay was run. Independent human and formal
+proof-kernel review are unclaimed.
+
+## Open next questions
+
+- Can log q + 2 be replaced by a smaller explicit primitive-unit envelope?
+  Start with the exact subtracted harmonic expression or a sharper sine bound
+  for one prime-power family. This may improve the sufficient exponent further;
+  no mathematical blocker is identified. It was not pursued after the first gain.
+- Can one actual small prime-power inverse use the improved gap with its full
+  error and cost recurrence? Start with a fixed instance of the cited
+  arbitrary-stride solver and charge coefficient preparation, rounding,
+  restoration and tape access. The missing physical implementation and full
+  error ledger block any executed-precision or supplier claim.
+
+Structured entries are in [TASK.json](TASK.json).
+
+## Verifier constraints
+
+All functions are below 60 physical lines. There is no recursion, subprocess,
+network access or dynamic code evaluation. The finite radix loop has 4,095
+iterations, harmonic storage has 2,049 entries, logarithm series use 32 terms,
+and factor-removal loops have at most 257 iterations. Mathematical comparisons
+use integers and Fractions. Package reads are limited to one MiB per file.
+Both registered modes enable warning errors and explicit invariant checks.
+
+Power-of-ten rule 3 deviation: CPython allocates managed integers, Fractions
+and bounded containers while checking. This one-shot checker has no fixed
+allocation runtime; the enforced finite domains bound live data. Rule 9
+deviation: the rejection table invokes only its named local functions on
+eleven fixed fixtures. There is no external callback or plugin dispatch.

research/prime-power-harmonic-gap/SOURCES.json

@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8",
+      "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1"
+    },
+    {
+      "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/zero-mean-cyclotomic-height/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "2f24cc7a91f64ebb226ef2a3e286aa6ebd6d4cae",
+      "sha256": "9ebc26d401a3a7be6bf862d5e2860fd4f937302504e2c01c3fdd8a5f2a06f1a0"
+    },
+    {
+      "path": "research/prime-power-cyclic-inverse/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "0c757c37c70fdeb261d73f111ceedd3b233287bf",
+      "sha256": "2b8056c88e66f692f407450fff0414d41bcd09db8597be22e274a6c3dc20eb9e"
+    }
+  ]
+}