Sharpen the composite cyclotomic precision exponent (no κ)

research/composite-zero-mean-gap/PROOF.md

@@ -0,0 +1,144 @@
+# A zero-mean mixed-radix height bound
+
+This scoped written proof was produced by Nick Petalas. The new step combines
+the all-radix Fourier identity of Nick Petalas's #5930 with the mixed-radix
+unit-average estimate of Hanson Sun / bbMisk's #1428. Those results are cited
+premises. Their proofs, programs and finite censuses are not rechecked here.
+The averaged-height framework is Chafik Boukhalfa's #1025; the resultant and
+cofactor implication is Ali Romman's #621, as specialized in #1428.
+
+## Statement and hypotheses
+
+Let r >= 3 be any integer, n = r-1, D = phi(r), ell = ceil(log2 r),
+zeta = exp(2 pi i/r), and t = log r, where log is natural. For each unit k
+modulo r define
+
+    a_(k,j) = product_(s=j+1)^(r-1) (1-zeta^(ks)),  0 <= j <= n,
+    f_k(z) = sum_(j=0)^n a_(k,j) z^j,
+    P_k(z) = f_k(z)/r,
+    H_k = sum_(j=0)^n |a_(k,j)|.
+
+The empty product is one. The new unconditional averaged-height estimate is
+
+    sum_(k unit mod r) log H_k <= r t(1+t) + D t.             (1)
+
+For the circle-gap consequence, additionally assume that the resultant of
+f_1 and f_1*(z) = z^n conjugate(f_1(1/conjugate(z))) is nonzero. Put
+
+    B_new = n [3r ell^2/4 + (r+D)ell],
+    d_new = 1 + 2ell + min(nDr, ceil(B_new)).                 (2)
+
+Then for every primitive embedding k and every |z| = 1,
+
+    |P_k(z)| >= 2^(-d_new).                                 (3)
+
+The inherited cyclic-operator transfer of #1428 also gives, for every L >= 1,
+integer w and |tau| = 1, with U = tau Z_L^w,
+
+    ||P_k(U)^(-1)||_infinity <= 2^(2d_new+r+2).               (4)
+
+Here Z_L is the cyclic shift on L coordinates. The nonzero-resultant
+hypothesis is essential to the derivation of (3)-(4), and is not asserted
+for every integer r. Jason Willems's #666, specialized and credited in
+#1428, supplies it for r = 2p^a with p >= 5 prime and a >= 1. We cite that
+family without replaying its lifting argument.
+
+## Proof of the new averaged height
+
+Use #5930's function F on Z/r:
+
+    F(0) = -t,  F(s) = log|1-zeta^s| for s != 0,
+    Fhat(h) = (1/r) sum_s F(s) zeta^(-hs).
+
+Its all-integer-r identity says
+
+    Fhat(0) = 0,  Fhat(h) < 0 for h != 0,
+    sum_(h != 0) |Fhat(h)| = t.                            (5)
+
+The Fourier identity in that source is stated for every integer r >= 3;
+only its subsequent height application was restricted to prime powers.
+No singular zero-residue value occurs in any a_(k,j), because k is a unit
+and 1 <= s < r. Fourier inversion and the geometric-sum inequality imply
+
+    log|a_(k,j)|
+        <= sum_(h != 0) |Fhat(h)| 2/|1-zeta^(hk)|.
+
+The same nonnegative bound includes the empty suffix. Therefore it bounds
+M_k = max_j log|a_(k,j)|. The zero Fourier mean removes the old additive t
+term at this step.
+
+For each fixed h != 0, the mixed-radix estimate of #1428 gives
+
+    (1/D) sum_(k unit mod r) 2/|1-zeta^(hk)|
+        <= (r/D)(1+t).                                    (6)
+
+That source proves (6) by equal fibers from units modulo r to units modulo
+q = r/gcd(h,r), pairing reciprocal sines and using q/phi(q) <= r/D. It
+does not require a prime-power radix. Apply (6) separately to each
+nonnegative term in the bound on M_k, then (5), to obtain
+
+    sum_k M_k <= r t(1+t).
+
+There are r coefficients, so H_k <= r exp(M_k). Summing log H_k proves (1).
+The maximum is bounded before averaging; no maximum is interchanged with
+an average. This is the new mixed-radix estimate.
+
+## Conditional gap and integer exponent
+
+Under the nonzero-resultant hypothesis, #1428's retained norm/cofactor
+argument gives
+
+    |P_k(z)| >= 1 / [2rn product_(a unit mod r) H_a^n].      (7)
+
+It applies at every primitive embedding. Substituting (1) into (7) gives
+the stronger, non-dyadic statement
+
+    |P_k(z)| >= exp(-n [r t(1+t)+D t])/(2rn).              (8)
+
+Write c = log 2. Since t <= ell c and c < 3/4,
+
+    [r t(1+t)+D t]/c
+        <= r c ell^2 + (r+D)ell
+        < 3r ell^2/4 + (r+D)ell.
+
+The coarse alternative H_k <= 2^r-1 < 2^r gives nDr. Also
+2rn <= 2^(1+2ell). Taking the smaller sufficient exponent and rounding
+up proves (2)-(3). Equation (4) is precisely the cited gap-to-operator
+implication with this improved d; it introduces no new operator claim.
+
+## Comparison with the old mixed-radix exponent
+
+The old analytic branch in #1428 is
+
+    B_old = 3nr(ell+1)^2/2 + 2nD ell,
+    d_old = 1+2ell+min(nDr, B_old).
+
+B_old is an integer because nr is even. Direct subtraction gives
+
+    B_old - B_new
+        = n [3r ell^2/4 + 2r ell + 3r/2 + D ell] > 1.
+
+Consequently ceil(B_new) < B_old and d_new <= d_old for every r >= 3.
+The full exponent can remain equal when both bounds use the coarse branch.
+For the certified mixed radix r = 8978 = 2*67^2, the exact new exponent is
+13,531,624,611, compared with the cited formula's 28,312,479,536. The
+standalone checker computes these integers; they are sufficient analytic
+exponents, not measured or executed precision.
+
+## Verification and limitations
+
+The written proof supplies all-radix quantifiers, conditional on the cited
+identities and implication. The new verifier independently encloses actual
+coefficient-height sums at thirteen mixed radices using rational intervals,
+Machin's identity, Taylor remainders, integer square roots and an atanh
+logarithm series. It checks the new natural-to-binary inequality and exponent
+arithmetic, including a half-integer ceiling boundary. It imports and runs
+no predecessor code and makes no floating-point inference.
+
+These finite checks corroborate the new estimate. They are not a proof kernel
+and do not establish nonvanishing at other radices. No paid composite solver,
+coefficient-preparation or rounding schedule, restored dirty workspace, native
+word, physical tape/caller invoice, compiler closure, supplier admission,
+new kappa or complete multiplication theorem is supplied. All five selected
+framework assumptions remain. Independent human and formal proof-kernel
+review are unclaimed.

research/composite-zero-mean-gap/README.md

@@ -0,0 +1,125 @@
+# A smaller sufficient precision exponent for composite radices
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Claim type: scoped written analytic proof with exact finite corroboration.
+No new kappa or selected-frontier change is claimed.
+
+For every integer r >= 3, n = r-1, D = phi(r), ell = ceil(log2 r), the
+cyclotomic coefficient heights of #1025/#1428 satisfy the new estimate
+
+    sum_(k unit mod r) log H_k <= r log r (1+log r) + D log r.
+
+Under the same nonzero-resultant hypothesis as #1428, this gives
+
+    |P_k(z)| >= 2^(-d_new) for every primitive embedding k and |z|=1,
+    d_new = 1+2ell+min(nDr, ceil(n[3r ell^2/4+(r+D)ell])).
+
+It never increases #1428's sufficient exponent. At the certified mixed
+radix 8978 = 2*67^2, the exponent is **13,531,624,611**, compared with
+28,312,479,536 from that source's formula. These are sufficient analytic
+exponents; no inverse at either precision was executed. The inherited
+cyclic-operator implication gives the corresponding infinity-norm bound
+`2^(2d_new+r+2)`.
+
+The new step combines Hanson Sun / bbMisk's #1428 mixed-radix unit average
+with Nick Petalas's older #5930 zero-mean logarithm, whose Fourier identity
+already holds at every integer radix. The prime-power height application
+in #5930 does not give this mixed-radix conclusion. The zero Fourier mean
+removes an additive term, and its exact mass halves the leading old bound.
+[PROOF.md](PROOF.md) states every hypothesis and the comparison argument.
+The predecessor statements are cited premises, not audit deliverables.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/composite-zero-mean-gap/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/composite-zero-mean-gap/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/composite-zero-mean-gap
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/composite-zero-mean-gap --check-source-history
+```
+
+Substitute another CPython 3.12 path elsewhere. Direct output is a generated
+JSON receipt with `PASS_COMPOSITE_ZERO_MEAN_GAP` and SHA256 of all six files.
+The checker writes nothing and needs no Git, network, external solver or
+predecessor implementation. The metadata runner resolves provenance through
+Git separately. Both registered commands execute the full verifier.
+
+The new finite checks enclose actual height sums for all 100 primitive
+embeddings at thirteen mixed radices from 6 through 30. Rational intervals
+use Machin's identity, cosine Taylor remainders, integer square roots and
+an atanh logarithm series, with outward rounding after arithmetic. They
+also check 254 new natural-to-binary inequalities and 2,062 exponent cases,
+including 1,964 strict improvements over the cited old formula. Cases are
+counted executions and can repeat a radix. Eight invalid inputs reject;
+one additional half-integer case checks the necessary ceiling. Normal and
+optimized Python retain every explicit mathematical check.
+
+## Scope, provenance and limits
+
+Canonical base is e54523517d0f03e58352e647c403a5af3e525a57, priority revision 8,
+selected #7000. The current selected-baseline orientation command passed for
+source bindings only. The `uniform-transfer-audit` card changes scope to
+this analytic precision-interface result; no selected assumption is discharged.
+[TASK.json](TASK.json) records that change and [SOURCES.json](SOURCES.json)
+pins the predecessor statements as historical provenance. There are no
+external executable mathematical inputs.
+
+The advance [CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19539388)
+followed live open/account PR lists, recent handoffs, active Discussions,
+local reservations, all-main README and merged searches. A dedicated #1428
+source query found no account PR from the preceding seven days. Sparse
+cached local notes and unpublished work limit overlap coverage; absence of
+matches is not a novelty certificate.
+
+A concurrent [prime-power harmonic claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19539414)
+seeks a new unit-average envelope within prime powers. This result instead
+uses the existing mixed-radix envelope and changes its logarithmic Fourier
+input. No computations were added to check that separate proposed lemma.
+
+The universal assertion is the written proof with cited premises, rather
+than enumeration or proof-kernel acceptance. The height estimate is
+unconditional; circle-gap and operator consequences retain the nonzero
+resultant hypothesis. We cite #666/#1428's certified family `r=2p^a`,
+prime p >= 5, without rechecking it. Other radices do not become certified
+by exponent arithmetic. The coarse branch can prevent a strict improvement.
+
+No paid solver, coefficient-preparation or rounding policy, restored dirty
+workspace, physical word/caller, tape/stock cost, supplier admission or
+complete multiplication theorem is supplied. All five framework assumptions
+remain. Selected cold replay, native suites, Lean and Docker are unrun.
+Independent human and formal proof-kernel review are unclaimed.
+
+## Open next questions
+
+Can one certified composite inverse execute at reduced precision with all
+costs retained? Start with r=10 or r=134 and an explicit preparation and
+inverse error recurrence. Paid coefficient work, rounding propagation,
+scratch restoration and tape/caller costs remain blockers. The analytic
+exponent alone establishes no executed or recursive saving.
+
+## Credit and implementation constraints
+
+Credit Chafik Boukhalfa / #1025 for averaged coefficient heights and precision;
+Hanson Sun / bbMisk / #1428 for arbitrary-radix unit averaging and the conditional
+gap/operator framework; Nick Petalas / #5930 for the all-radix zero-mean identity;
+Ali Romman / #621 for the resultant/cofactor argument; and Jason Willems /
+at1as / #666 for the certified composite nonvanishing family. Rohan Guliani /
+#846, Charles Bethin / #764 and the retained exact-DFT/q-Pochhammer lineage
+keep their context credit. Fourier inversion, geometric sums, Machin's
+identity and interval Taylor/logarithm arithmetic are classical. The new
+mixed-radix estimate, exponent substitution and checker were produced by
+Nick Petalas. No predecessor files or credit lines are changed.
+
+The checker includes actual coefficient-height enclosures as well as exponent
+arithmetic. Functions stay below 60 lines and every loop has a finite domain.
+Radices in the reference exponent function are at most 2^32,
+factor trials at most 65,535, height instances at most 30, Taylor terms 24,
+and logarithm terms 40. File inputs are trusted package sources, each checked
+against a 256 KiB limit. Explicit exceptions remain enabled under optimization.
+There is no recursion, subprocess, network, dynamic code generation or mutable
+shared state. Python's bounded live Fraction/list/integer allocation is a rule-3
+managed-runtime deviation; no fixed-allocation runtime is claimed. Warning-strict
+normal/optimized execution and AST compilation provide local diagnostics.
+No external static analyzer or formal kernel was run.

research/composite-zero-mean-gap/SOURCES.json

@@ -0,0 +1,48 @@
+{
+  "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/zero-mean-cyclotomic-height/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "2f24cc7a91f64ebb226ef2a3e286aa6ebd6d4cae",
+      "sha256": "9ebc26d401a3a7be6bf862d5e2860fd4f937302504e2c01c3fdd8a5f2a06f1a0"
+    },
+    {
+      "path": "research/zero-mean-cyclotomic-height/README.md",
+      "usage": "provenance",
+      "git_blob": "e6d363ffa503d03dbd3d657c07a6c8e7507f6d5d",
+      "sha256": "7f35f192c772d0d18e19c8eeffa2fee1400fafd9c5f4d7a2c0d4ab3e1b6774ed"
+    },
+    {
+      "path": "research/composite-height-audit-seed67/README.md",
+      "usage": "provenance",
+      "git_blob": "ee83d116a7035ea880089965454aa882eb487aa5",
+      "sha256": "2f05204e88ceb33a58f2abf6bd8d9b131f7b617263cfd40cc417fe4d568470eb"
+    },
+    {
+      "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"
+    }
+  ]
+}