From 54b76434dd07ecfdeeaa5958268693f176f37e65 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 11 Nov 2026 10:12:29 +0000 Subject: [PATCH] feat(research): sharpen prime-power cyclotomic gap exponent --- research/prime-power-harmonic-gap/PROOF.md | 153 ++++++++++++ research/prime-power-harmonic-gap/README.md | 133 +++++++++++ .../prime-power-harmonic-gap/SOURCES.json | 42 ++++ research/prime-power-harmonic-gap/TASK.json | 177 ++++++++++++++ research/prime-power-harmonic-gap/VERIFY.json | 34 +++ research/prime-power-harmonic-gap/verify.py | 218 ++++++++++++++++++ 6 files changed, 757 insertions(+) create mode 100644 research/prime-power-harmonic-gap/PROOF.md create mode 100644 research/prime-power-harmonic-gap/README.md create mode 100644 research/prime-power-harmonic-gap/SOURCES.json create mode 100644 research/prime-power-harmonic-gap/TASK.json create mode 100644 research/prime-power-harmonic-gap/VERIFY.json create mode 100644 research/prime-power-harmonic-gap/verify.py diff --git a/research/prime-power-harmonic-gap/PROOF.md b/research/prime-power-harmonic-gap/PROOF.md new file mode 100644 index 0000000000..bb7e455f04 --- /dev/null +++ b/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. diff --git a/research/prime-power-harmonic-gap/README.md b/research/prime-power-harmonic-gap/README.md new file mode 100644 index 0000000000..d6bef047bb --- /dev/null +++ b/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. diff --git a/research/prime-power-harmonic-gap/SOURCES.json b/research/prime-power-harmonic-gap/SOURCES.json new file mode 100644 index 0000000000..80fa6e28b4 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/prime-power-harmonic-gap/TASK.json b/research/prime-power-harmonic-gap/TASK.json new file mode 100644 index 0000000000..5af7136a34 --- /dev/null +++ b/research/prime-power-harmonic-gap/TASK.json @@ -0,0 +1,177 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "New prime-power primitive-unit harmonic envelope and its averaged-height/circle-gap consequence.", + "scope_change_reason": "This is a scoped analytic precision lemma extending #1025, rather than a proof-assistant or actual-caller binding. The first working source-binding command passed; no formal-interface acceptance is claimed.", + "bottleneck_link": "Side result: lowers a sufficient analytic circle-gap exponent used in inverse precision. It does not change native paid/productive profiles, discharge a selected assumption, or improve kappa.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved and exactly corroborated new envelope; retain further constants and physical execution as open questions.", + "outcome": "completed", + "evidence": "PROOF.md establishes the uniform prime-power estimate. verify.py corroborates 604 harmonic bounds, 117 direct identities, 44 cosecant averages, 968 exponent cases and 13 controls; it emits a six-file SHA256-bound receipt.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can the prime-power unit envelope log q + 2 be replaced by a smaller explicit function while preserving a simple uniform proof?", + "why_it_matters": "Would further lower the sufficient analytic gap exponent.", + "first_step": "Retain the exact primitive harmonic expression, or improve the sine chord inequality, for one prime-power family.", + "blocked_by": "No mathematical blocker identified; not pursued after the first improvement." + }, + { + "question": "Can one actual prime-power inverse use the smaller gap exponent with its entire rounded error and cost recurrence?", + "why_it_matters": "An analytic exponent reduction alone is not executed precision or a paid supplier improvement.", + "first_step": "Choose one fixed small instance of the cited arbitrary-stride solver and charge coefficient preparation, rounding, restoration and tape access.", + "blocked_by": "A complete physical inverse implementation and error/cost ledger are absent from this package." + } + ], + "claim_type": "scoped proof", + "source_question": { + "pr": 1025, + "author": "chafreaky", + "question": "Sharpen the primitive-unit geometric-sum average in the prime-power height argument." + }, + "credited_premises": [ + { + "pr": 1025, + "author": "Chafik Boukhalfa", + "scope": "Averaged-height/norm framework and normalization." + }, + { + "pr": 5930, + "author": "Nick Petalas", + "scope": "Older zero-mean Fourier identity and previous 3 ell^2 exponent." + }, + { + "pr": 621, + "author": "Ali Romman", + "scope": "Prime-power nonzero resultant and norm/cofactor implication." + } + ], + "environment": { + "python": "CPython 3.12.15", + "dependencies": "standard library only" + }, + "selected_context": { + "source_pr": 7000, + "kappa": "363005817/100000000000", + "reproduce": "make frontier7000-verify", + "scientific_replay_run": false + }, + "overlap": { + "checked_at": "2026-11-11T10:07:00Z", + "source_spread": "Source #1025/chafreaky is distinct from the concurrent #1428/bbMisk composite question. #5930 predates seven days and is a cited premise, not the question source.", + "coverage": "Live open and account PR metadata and relevant bodies, recent handoffs and active Discussions, local reservations, main README formula/object searches and merged PR searches. Cached task search reports 488 open PRs and 7157 discussion records, but sparse local coverage omits 9946 of 10178 HEAD notes. The first task search completed after CLAIM; its delayed output was not claimed as preclaim coverage. Unpublished branches and arbitrary diffs are not covered." + }, + "verification_details": { + "proof": "PROOF.md", + "verifier": "verify.py", + "expected_marker": "PASS_PRIME_POWER_HARMONIC_GAP", + "domains": { + "harmonic_prime_powers": [ + 2, + 4096 + ], + "direct_harmonic_prime_powers": [ + 2, + 512 + ], + "cosecant_prime_powers": [ + 2, + 128 + ], + "dyadic_exponents": [ + 2, + 256 + ], + "ternary_exponents": [ + 1, + 128 + ] + }, + "counts": { + "harmonic_radices": 604, + "direct_harmonic_identities": 117, + "cosecant_radices": 44, + "primitive_pairs": 1083, + "primitive_units": 2165, + "budget_cases": 968, + "strict_budget_improvements": 948, + "controls": 13 + }, + "receipt": "Generated on stdout, with SHA256 of all six package files; not an input." + } +} diff --git a/research/prime-power-harmonic-gap/VERIFY.json b/research/prime-power-harmonic-gap/VERIFY.json new file mode 100644 index 0000000000..cd8c942f89 --- /dev/null +++ b/research/prime-power-harmonic-gap/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact new primitive harmonic/cosecant inequalities, exponent arithmetic and failure controls; generated package-hash-bound receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same finite corroboration with optimization; explicit checks remain active." + } + ] +} diff --git a/research/prime-power-harmonic-gap/verify.py b/research/prime-power-harmonic-gap/verify.py new file mode 100644 index 0000000000..db3ef59af9 --- /dev/null +++ b/research/prime-power-harmonic-gap/verify.py @@ -0,0 +1,218 @@ +"""Exact finite corroboration of the new primitive-unit envelope.""" + +from fractions import Fraction as F +from hashlib import sha256 +from math import factorial, gcd, isqrt +from pathlib import Path +import json +import sys + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def prime(n): + return n >= 2 and all(n % d for d in range(2, isqrt(n) + 1)) + + +def prime_power(q): + require(2 <= q <= 4096, "radix outside finite domain") + p = next((d for d in range(2, isqrt(q) + 1) if q % d == 0), q) + remaining = q + for _ in range(q.bit_length()): + if remaining % p: + break + remaining //= p + require(remaining == 1 and prime(p), "radix is not a prime power") + return p + + +def logarithm_core(y): + require(F(1) <= y <= F(2), "logarithm argument outside [1,2]") + x = (y - 1) / (y + 1) + total = sum((2 * x ** (2 * k + 1) / (2 * k + 1) + for k in range(32)), F(0)) + tail = 2 * x ** 65 / (65 * (1 - x * x)) + return total, total + tail + + +def logarithm(n): + require(isinstance(n, int) and 1 <= n <= 4096, "invalid logarithm input") + e = n.bit_length() - 1 + lo2, hi2 = logarithm_core(F(2)) + lo, hi = logarithm_core(F(n, 2 ** e)) + return e * lo2 + lo, e * hi2 + hi + + +def arctangent(x, terms): + require(F(0) < x <= F(1, 5) and 1 <= terms <= 24, "invalid arctangent") + value = sum(((-1) ** k * x ** (2 * k + 1) / (2 * k + 1) + for k in range(terms)), F(0)) + following = (-1) ** terms * x ** (2 * terms + 1) / (2 * terms + 1) + return min(value, value + following), max(value, value + following) + + +def pi_interval(): + lo5, hi5 = arctangent(F(1, 5), 24) + lo239, hi239 = arctangent(F(1, 239), 8) + lower = F(3141592653589793238, 10 ** 18) + upper = lower + F(1, 10 ** 18) + require(lower < 16 * lo5 - 4 * hi239, "Machin lower bound") + require(16 * hi5 - 4 * lo239 < upper, "Machin upper bound") + return lower, upper + + +def sine_interval(lo, hi): + require(0 < lo <= hi <= F(8, 5), "sine argument outside finite domain") + lower = F(0) + upper = F(0) + for k in range(12): + degree = 2 * k + 1 + denominator = factorial(degree) + if k % 2: + lower -= hi ** degree / denominator + upper -= lo ** degree / denominator + else: + lower += lo ** degree / denominator + upper += hi ** degree / denominator + upper += hi ** 25 / factorial(25) + require(0 < lower <= upper, "invalid positive sine enclosure") + return lower, upper + + +def harmonic_checks(): + values = [F(0)] + for j in range(1, 2049): + values.append(values[-1] + F(1, j)) + rows = [] + direct_count = 0 + for q in range(2, 4097): + try: + p = prime_power(q) + except ValueError: + continue + n = q // 2 + m = n // p + envelope = (p * values[n] - values[m]) / (p - 1) + loglo, loghi = logarithm(q) + require(envelope <= loglo + 2, f"new harmonic bound at {q}") + require(n < p * (m + 1), "floor remainder contract") + require(p <= 2 ** (p - 1), "integer logarithm comparison") + if q <= 512: + direct = sum((F(1, j) for j in range(1, n + 1) if j % p), F(0)) + require(envelope == F(p, p - 1) * direct, "primitive harmonic identity") + direct_count += 1 + rows.append((q, p, envelope, loglo, loghi)) + require(2 * values[32] > logarithm(64)[1] + 2, + "dropping the divisible terms must break the bound") + return rows, direct_count + + +def trigonometric_checks(rows): + pi_lo, pi_hi = pi_interval() + radices = 0 + pairs = 0 + represented_units = 0 + for q, p, envelope, loglo, _ in rows: + if q > 128: + continue + phi = q // p * (p - 1) + average_hi = F(0) + counted = 0 + for j in range(1, q // 2 + 1): + if gcd(j, q) != 1: + continue + multiplicity = 1 if 2 * j == q else 2 + if 2 * j == q: + sin_lo = F(1) + else: + sin_lo, _ = sine_interval(pi_lo * j / q, pi_hi * j / q) + require(sin_lo >= F(2 * j, q), "sine chord bound") + average_hi += F(multiplicity, phi) / sin_lo + counted += multiplicity + pairs += 1 + require(counted == phi, "primitive pair coverage") + require(average_hi <= envelope, "cosecant versus harmonic envelope") + require(average_hi <= loglo + 2, "new primitive-unit envelope") + represented_units += counted + radices += 1 + return radices, pairs, represented_units + + +def gap(r, p): + require(3 <= r <= 2 ** 256 and 2 <= p <= 4096 and prime(p), + "invalid gap parameters") + remaining = r + for _ in range(257): + if remaining % p: + break + remaining //= p + require(remaining == 1, "gap radix is not a power of p") + ell = (r - 1).bit_length() + numerator = 3 * ell * ell + 12 * ell + b = (numerator + 3) // 4 + require(4 * (b - 1) < numerator <= 4 * b, "exact dyadic ceiling") + require(b <= 3 * ell * ell, "comparison with cited bound") + mass = (r - 1) * (r // p * (p - 1)) + return 1 + 2 * ell + mass * min(r, b), 1 + 2 * ell + mass * min(r, 3 * ell * ell) + + +def budget_checks(rows): + cases = {(q, p) for q, p, *_ in rows if q >= 3} + cases.update((2 ** e, 2) for e in range(2, 257)) + cases.update((3 ** e, 3) for e in range(1, 129)) + improvements = 0 + for q, p in sorted(cases): + new, old = gap(q, p) + require(new <= old, "budget worsened") + improvements += new < old + require(gap(4096, 2) == (1207664665, 3622993945), "4096 example") + return len(cases), improvements + + +def rejection_checks(): + controls = ( + (prime_power, (6,)), (prime_power, (1,)), (prime_power, (4097,)), + (logarithm, (0,)), (logarithm, (4097,)), + (logarithm_core, (F(3),)), (arctangent, (F(1), 8)), + (sine_interval, (F(2), F(3))), (gap, (6, 2)), (gap, (16, 4)), + (gap, (2, 2)), + ) + for function, arguments in controls: + try: + function(*arguments) + except ValueError: + continue + raise ValueError("invalid-input control accepted") + require(4 * ((3 * 3 ** 2 + 12 * 3) // 4) < 3 * 3 ** 2 + 12 * 3, + "floor mutant should undercharge the exponent") + return len(controls) + 2 + + +def main(): + rows, direct = harmonic_checks() + radices, pairs, units = trigonometric_checks(rows) + budgets, improvements = budget_checks(rows) + controls = rejection_checks() + 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.stat().st_size <= 1024 ** 2, "package file exceeds one MiB") + hashes[name] = sha256(path.read_bytes()).hexdigest() + print("PASS_PRIME_POWER_HARMONIC_GAP") + print(json.dumps({"schema": "prime-power-harmonic-gap/1", + "python": sys.version.split()[0], "package_sha256": hashes, + "harmonic_radices": len(rows), "direct_harmonic_identities": direct, + "cosecant_radices": radices, "primitive_pairs": pairs, + "primitive_units": units, "budget_cases": budgets, + "strict_budget_improvements": improvements, "controls": controls, + "example_4096": {"new": 1207664665, "cited": 3622993945}}, + sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()