diff --git a/research/fft-setup-global-maximum/README.md b/research/fft-setup-global-maximum/README.md new file mode 100644 index 0000000000..28b51f6620 --- /dev/null +++ b/research/fft-setup-global-maximum/README.md @@ -0,0 +1,146 @@ +# The sharp FFT setup constant holds at every width + +This contribution was produced by Nick Petalas. Apache-2.0. + +For every integer `n >= 3`, define + +```text +beta = ceil(log2 n), q = ceil(n/beta), +ell = ceil(log2(2q)), r = 2^ell, p0 = 2 beta + ell, +S = r(ell+1)p0^2 + r p0^3 + p0^3. +``` + +Then `S <= (1017/7) n beta^2`, with equality if and only if `n=7`. +Moreover, `S < 144 n beta^2` whenever `n >= 513`. + +This is a scoped all-width arithmetic proof with a finite exact component. +James Reed's [PR3819](https://github.com/CrocSwap/integer-mult-bounds/pull/3819) +introduced `1017/7` and checked it through `2^22`. +The new contribution is the universal tail argument, which makes that +constant the global optimum and closes the finite-range restriction. +The predecessor executable and its census are not replayed here. + +Jose Manuel's [PR3787](https://github.com/CrocSwap/integer-mult-bounds/pull/3787) +defines this geometry and the setup invoice. Reed's +[PR3813](https://github.com/CrocSwap/integer-mult-bounds/pull/3813) +records the separate constants. These three expressions are the quadratic +majorant of the source invoice, after replacing `p0^(8/5)` by `p0^2`. +The bound applies before unspecified implementation constants. It is not +an exact instruction count or a new time theorem. + +## Proof + +Write `b=beta`. If `n >= 513`, then `b >= 10` and +`2^(b-1) < n <= 2^b`. Since `b >= 4`, + +```text +q <= ceil(2^b/b) <= 2^(b-2), +ell <= b-1, p0 <= 3b-1 < 3b, +ell+1+p0 = 2b+2ell+1 <= 4b-1. +``` + +The second ceiling inequality holds because `2^(b-2)` is an integer +at least `2^b/b`. Minimality of the power of two `r >= 2q` also gives +`r < 4q < 4n/b+4`. Factoring the sum gives + +```text +S = r p0^2 (ell+1+p0) + p0^3 + < (4n/b+4) 9b^2 (4b-1) + 27b^3 + = n b^2 [144 - 36/b + (171b-36)/n]. (1) +``` + +For every integer `b >= 10`, + +```text +2^(b-1) >= 19b^2/4. (2) +``` + +At `b=10` this is `512 >= 475`. For the induction step, +`2b^2 >= (b+1)^2` for `b >= 3`, since `b^2-2b-1 > 0` there. +Doubling (2) therefore proves it at `b+1`. Consequently +`n > 19b^2/4` and + +```text +(171b-36)/n < 171b/n < 36/b. +``` + +Equation (1) is strictly below `144 n b^2`. This proves the entire +infinite tail, without extrapolating from sampled widths. + +There remain precisely the 510 integers `3 <= n <= 512`. +The standalone [verifier](verify.py) computes their geometry and checks +`7S <= 1017 n b^2` by integer arithmetic. A second construction uses +bounded doubling and quotient/remainder operations, instead of the +primary bit-length and ceiling formulas. It agrees at every prefix +width. The prefix maximum is `1017/7`, attained only at `n=7`, where +`(b,q,ell,r,p0)=(3,3,3,8,9)` and `S=9153`. +Since `144 < 1017/7`, the tail adds no equality cases. This proves +the global maximum and uniqueness. + +## Evidence and reproduction + +From the repository root, using CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/fft-setup-global-maximum +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -B research/fft-setup-global-maximum/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/fft-setup-global-maximum --check-source-history +``` + +The registered normal and optimized commands each check the 510-width +prefix, the induction base, 4,087 induction probes and 8,174 tail endpoint +widths through `beta=4096`. These finite tail probes corroborate the +written induction; they do not establish its universal quantifier. +Eight invalid widths, three formula mutations and the smaller constant +145 are rejected. Every run prints a generated receipt bound to SHA256 +hashes of all five package files and writes no files. + +Replay requires neither Git nor predecessor files. [SOURCES.json](SOURCES.json) +pins their exact historical bytes as provenance. Receipts are generated +on stdout rather than stored as mutable expected results. + +The executable enforces a 4,096-bit geometry limit. Every loop has an +explicit finite bound; there is no recursion, dynamic evaluation or +runtime import of predecessor code. Python necessarily allocates integer +objects during the computation. This managed-runtime deviation from +fixed allocation is confined to bounded arithmetic probes and five +receipt files of at most 1 MiB each. Future larger probes must retain +an explicit bit bound. Warning-strict normal and optimized registered +execution supplies runtime diagnostics. Formal proof-kernel checking +and a separate static type checker are unrun. + +## Limitations + +This result prices only the three stated algebraic setup expressions. +It does not execute the FFT multiplier, bind hidden instruction constants, +admit a physical caller, prove retained numerical/recovery premises, +or change kappa or the selected frontier. The source uses a separate +small-width implementation; equality at seven concerns the declared +setup expression, not a measured production call at that width. +Independent human and formal proof-kernel review are unclaimed. + +## Open next questions + +1. Is 144 the sharp asymptotic upper limit of `S/(n beta^2)`? The tail + proves only an upper bound. First choose widths just after a + power-of-two jump in `2 ceil(n/beta)` while keeping `beta` fixed. + No asymptotic sharpness claim is made here. +2. What explicit constant bounds the unrelaxed invoice with `p0^(8/5)`? + First enclose that real power at geometry breakpoints and prove an + analytic tail. Exact instruction constants and physical caller + admission remain separate obligations. + +## Credit and overlap + +James Reed retains credit for the finite `1017/7` maximum and separate +setup comparisons. Jose Manuel retains credit for the digit geometry, +FFT word construction and invoice. Their classical FFT/radix and +Karatsuba lineage, PR3709 numerical/recovery implementation, Mason Hale's +PR2313 interval reference, Dugongue's PR2790 scalar interface and retained +Gaussian reports keep their credit. No predecessor credit line is changed. + +Live overlap checks covered open PR bodies and Discussions, this account's +recent contributions, main-tree exact-constant/object searches and merged +PR searches. The exact-constant match was the finite PR3819. +No universal successor was found within that coverage. Arbitrary diffs, +unpublished work and a complete literature priority search are not covered. diff --git a/research/fft-setup-global-maximum/SOURCES.json b/research/fft-setup-global-maximum/SOURCES.json new file mode 100644 index 0000000000..5effc88dca --- /dev/null +++ b/research/fft-setup-global-maximum/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "81e9bd69e4a5b00ba9c713a1620e36d576d5522e", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/fft-setup-sum/README.md", + "usage": "provenance", + "git_blob": "06d195232d6e87a80eefb996bb368fccf378c2f9", + "sha256": "d9af33d7976c0e33e1954aa2d88d8a891f648740d65e0e0f15a44f42714eacd7" + }, + { + "path": "research/physical-fft-word/README.md", + "usage": "provenance", + "git_blob": "d149d6c20f47208f81f78c0f038e0201585c2ba3", + "sha256": "0a47858de0cbe7700792b52ee3dcd9ae66f3ad9eb1f99f450515e820ed099dc8" + }, + { + "path": "research/physical-fft-word/PROOF.md", + "usage": "provenance", + "git_blob": "b066548b77ae99d36d11df379c6c2332caccd0f1", + "sha256": "5d7e5c3e47c4936023f191ef91ff4015d4786cb4de303d8fd3bef0fcec7a77b0" + } + ] +} diff --git a/research/fft-setup-global-maximum/TASK.json b/research/fft-setup-global-maximum/TASK.json new file mode 100644 index 0000000000..59a2dde556 --- /dev/null +++ b/research/fft-setup-global-maximum/TASK.json @@ -0,0 +1,96 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "81e9bd69e4a5b00ba9c713a1620e36d576d5522e", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove the exact global maximum 1017/7 of the three FFT setup expressions divided by n beta^2 for every integer n >= 3, with unique equality at n=7 and strict tail below 144 for n >= 513.", + "scope_change_reason": "This is an original universal continuation of James Reed PR3819, not an audit of the proposed all-size supplier. The existing bound was explicitly finite through 2^22.", + "bottleneck_link": "The result makes the sharp setup majorant independent of any finite width cutoff. Hidden implementation constants and complete caller admission remain outside scope.", + "budget_minutes": 60, + "stop_rule": "Ship the first universal setup estimate; do not extend the search or run the predecessor multiplier.", + "outcome": "completed", + "evidence": "Written tail induction, exact 510-width finite prefix with unique equality at seven, 4087 induction probes and 8174 tail endpoints. Eight invalid widths, three formula mutations and a smaller constant are rejected.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Is 144 the sharp asymptotic upper limit of S/(n beta^2)?", + "why_it_matters": "Separates the finite global maximizer from eventual setup efficiency.", + "first_step": "Choose widths just after power-of-two jumps in 2 ceil(n/beta), retaining beta.", + "blocked_by": "Only an upper tail bound is proved here; an attaining sequence is absent." + }, + { + "question": "What explicit constant bounds the unrelaxed invoice with p0^(8/5)?", + "why_it_matters": "The quadratic majorant may overprice the actual algebraic setup expressions.", + "first_step": "Enclose the real power at geometry breakpoints and establish an analytic tail.", + "blocked_by": "Certified real-power comparisons and hidden instruction constants are not included." + } + ], + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19142745", + "upstream_commit": "81e9bd69e4a5b00ba9c713a1620e36d576d5522e", + "priority_revision": 7, + "overlap_snapshot_utc": "2026-10-23T09:29:45Z", + "open_pr_records": 322, + "discussion_records": 4238, + "local_coverage": "129 searched records; 6695 main note paths omitted by sparse checkout, supplemented by main-tree exact-constant/object searches. Arbitrary diffs and unpublished work excluded.", + "preserved_checkout": "Clean detached HEAD at 81e9bd69e4a5b00ba9c713a1620e36d576d5522e; no earlier branch name." + }, + "environment": { + "python": "CPython 3.12.15", + "interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12", + "playbook": "investigation", + "orientation": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY; no full selected replay." + } +} diff --git a/research/fft-setup-global-maximum/VERIFY.json b/research/fft-setup-global-maximum/VERIFY.json new file mode 100644 index 0000000000..057a796bd6 --- /dev/null +++ b/research/fft-setup-global-maximum/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact finite prefix, independent geometry, tail induction controls, endpoint probes, invalid inputs, formula mutations and generated source-hash receipt." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "The same mathematical checks with optimization and isolated imports; no reliance on assert statements." + } + ] +} diff --git a/research/fft-setup-global-maximum/verify.py b/research/fft-setup-global-maximum/verify.py new file mode 100644 index 0000000000..bb9ebb5e28 --- /dev/null +++ b/research/fft-setup-global-maximum/verify.py @@ -0,0 +1,154 @@ +#!/usr/bin/env python3 +"""Exact finite component and boundary checks for the all-width setup proof.""" + +import hashlib +import json +import platform +from fractions import Fraction +from pathlib import Path + +MAX_BITS = 4096 +PREFIX_STOP = 513 +PACKAGE_FILES = ("README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def geometry(width: int) -> tuple[int, int, int, int, int]: + """The executable oracle is bounded; the written theorem is all-width.""" + if type(width) is not int or not 3 <= width <= 1 << MAX_BITS: + raise ValueError("width must be an integer in [3, 2^4096]") + beta = (width - 1).bit_length() + quotient = (width + beta - 1) // beta + ell = (2 * quotient - 1).bit_length() + ring = 1 << ell + return beta, quotient, ell, ring, 2 * beta + ell + + +def setup_sum(ell: int, ring: int, precision: int) -> int: + return ring * (ell + 1) * precision**2 + (ring + 1) * precision**3 + + +def reference(width: int) -> tuple[int, int, int, int, int]: + """Independent bounded doubling and quotient/remainder construction.""" + if type(width) is not int or not 3 <= width <= 1 << MAX_BITS: + raise ValueError("reference width outside bounded domain") + power = 1 + beta = 0 + for exponent in range(MAX_BITS + 1): + if power >= width: + beta = exponent + break + power *= 2 + require(beta >= 2, "reference beta not found") + quotient, remainder = divmod(width, beta) + quotient += int(remainder != 0) + ring = 1 + ell = 0 + for exponent in range(MAX_BITS + 2): + if ring >= 2 * quotient: + ell = exponent + break + ring *= 2 + require(ring >= 2 * quotient, "reference ring not found") + return beta, quotient, ell, ring, 2 * beta + ell + + +def finite_prefix() -> dict[str, object]: + maximum = Fraction(0) + winners = [] + count = 0 + for width in range(3, PREFIX_STOP): + data = geometry(width) + require(data == reference(width), "independent prefix geometry differs") + beta, _, ell, ring, precision = data + total = setup_sum(ell, ring, precision) + require(total == ring * precision**2 * (ell + 1 + precision) + precision**3, + "factored sum differs") + ratio = Fraction(total, width * beta**2) + require(ratio <= Fraction(1017, 7), "finite-prefix inequality failed") + if ratio > maximum: + maximum, winners = ratio, [width] + elif ratio == maximum: + winners.append(width) + count += 1 + require(maximum == Fraction(1017, 7) and winners == [7], "sharpness failed") + require(count == 510, "finite-prefix coverage differs") + return {"widths": count, "maximum": str(maximum), "equality_widths": winners} + + +def tail_boundaries() -> dict[str, int]: + """Corroboration of the written induction and exact rational envelope.""" + require(4 * 2**9 >= 19 * 10**2, "tail induction base failed") + require(2 * 10**2 >= 11**2, "quadratic doubling base failed") + comparisons = 0 + for beta in range(10, MAX_BITS + 1): + require(4 * (1 << (beta - 1)) >= 19 * beta**2, "induction probe failed") + require(2 * beta**2 >= (beta + 1)**2, "inductive step probe failed") + for width in ((1 << (beta - 1)) + 1, 1 << beta): + actual_beta, quotient, ell, ring, precision = geometry(width) + require(actual_beta == beta, "beta boundary differs") + require(ell <= beta - 1, "ell bound failed") + require(ring < 4 * quotient, "power-of-two bound failed") + require(beta * quotient < width + beta, "ceiling bound failed") + total = setup_sum(ell, ring, precision) + envelope = ((144 * beta - 36) * width * beta + + (171 * beta - 36) * beta**2) + require(total < envelope < 144 * width * beta**2, "tail chain failed") + comparisons += 1 + return {"beta_probes": MAX_BITS - 9, "endpoint_widths": comparisons} + + +def reject_controls() -> dict[str, int]: + rejections = 0 + for bad in (True, False, 2, 0, -1, 3.0, "7", (1 << MAX_BITS) + 1): + try: + geometry(bad) + except ValueError: + rejections += 1 + else: + raise ValueError("invalid width accepted") + require(Fraction(1017, 7) > 145, "smaller constant control missed width 7") + beta, quotient, ell, ring, precision = geometry(7) + require((beta, quotient, ell, ring, precision) == (3, 3, 3, 8, 9), + "attaining geometry differs") + require(setup_sum(ell, ring, precision) == 9153, "attaining sum differs") + # Each mutant must disagree with the independent literal recipe somewhere. + caught = set() + for width in range(3, PREFIX_STOP): + beta, _, ell, ring, precision = reference(width) + expected = setup_sum(ell, ring, precision) + mutants = ( + ring * (ell + 1) * precision**2 + ring * precision**3, + setup_sum(ell, ring // 2, precision), + setup_sum(ell, ring, 2 * beta + ell - 1), + ) + for index, value in enumerate(mutants): + if value != expected: + caught.add(index) + require(caught == {0, 1, 2}, "a mathematical omission control escaped") + return {"invalid_widths_rejected": rejections, "formula_mutants_rejected": len(caught), + "smaller_constant_rejected": 1} + + +def main() -> None: + prefix = finite_prefix() + tail = tail_boundaries() + controls = reject_controls() + package = Path(__file__).resolve().parent + hashes = {} + for name in PACKAGE_FILES: + path = package / name + require(path.is_file() and not path.is_symlink(), "missing or linked package file") + require(path.stat().st_size <= 1 << 20, "package file exceeds receipt bound") + hashes[name] = hashlib.sha256(path.read_bytes()).hexdigest() + print(json.dumps({"status": "PASS_FFT_SETUP_GLOBAL_MAXIMUM", "claim_type": "scoped proof", + "python": platform.python_version(), "prefix": prefix, "tail": tail, + "controls": controls, "sha256": hashes}, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()