Prove the sharp global FFT setup constant (no new κ)

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.

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

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

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