diff --git a/docs/research/bottleneck-brief.md b/docs/research/bottleneck-brief.md index 693f30d679..e295ba990e 100644 --- a/docs/research/bottleneck-brief.md +++ b/docs/research/bottleneck-brief.md @@ -42,7 +42,10 @@ The [review through #2027](community-efficient1000-review.md) leaves the selecte against that witness before designing a full schedule. - **Selected proof obligation:** [#1990's stock audit](../../research/selected-bootstrap-stock-audit/README.md) leaves the actual selected reserve coefficient unknown. Derive one source-bound - stage envelope rather than recomputing the already checked headrooms. + stage envelope rather than recomputing the already checked headrooms. The + [bootstrap obligation map](selected-bootstrap-scope-map.md) separates newer + conditional BIT coefficient proposals, time and fresh-field implications, + and the remaining implementation premises. These are not supplier admission. The new fixed-word frame bounds (#1995/#2013), Eisenstein additive pairing bound (#2017), and bounded register census (#1974) narrow particular search diff --git a/docs/research/selected-bootstrap-scope-map.md b/docs/research/selected-bootstrap-scope-map.md new file mode 100644 index 0000000000..6430d935f9 --- /dev/null +++ b/docs/research/selected-bootstrap-scope-map.md @@ -0,0 +1,173 @@ +# Which selected bootstrap obligation does this result address? + +Use this map before repeating stock-headroom arithmetic or treating a local +row route as bootstrap admission. It covers the selected #1094 ordinary +bootstrap, not every proposed outer algorithm. The +[selected record](../../certificates/selected-result.json) remains authoritative; +its [review](community-batch1099-review.md) retains the all-size, realization, +hosting, precision/tape and analytic obligations. No new bound or proof +adoption follows from this map. + +Snapshot: **2026-10-14, priority revision 4**, canonical main +`0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`. The first three entries below are +retained research with the scopes recorded in the +[review through #2027](community-efficient1000-review.md). The four later +entries are **open proposals**, pinned below and locally replayed for this +map. Passing their finite checks does not promote their conditional proofs +into the selected theorem. + +## Follow the obligation, not the largest coefficient cap + +| Result and author | What it establishes | What it does not establish | +| --- | --- | --- | +| [#1956, Josie Elliston](../../research/bootstrap-cutoff-carry/README.md) | All fourteen selected cutoffs reproduce; twelve fail the lemma's carried-time-constant rule as written. A corrected finite chain passes under its stated fresh-constant allowance. | A refutation of the asymptotic saving, or acceptance of a different proof wording. The numerical κ calculation does not read the cutoffs. | +| [#1965, Josie Elliston](../../research/bootstrap-cutoff-time-space-split/README.md) | Under H1–H3, time constants can enter the new induction constant rather than the fit cutoff. The fourteen cutoffs have explicit sufficient stock headrooms. | H2's uniform implementation estimate or H3's actual selected stock coefficient. Its "valid exactly when" is a statement about its sufficient guard, not necessity for actual fit. | +| [#1990, ToikY](../../research/selected-bootstrap-stock-audit/README.md) | An independent headroom audit and factor-16 extension of the sufficient stock-fit cap under the same envelope hypothesis. | A selected reserve implementation. The historical `m=120` increment 57,604 and external allowance 252 cannot simply be used as selected internal reserve coefficients. | +| [#2084, Adam Gall](https://github.com/CrocSwap/integer-mult-bounds/blob/8001a23b003bec5dff5e61edec907b652c475932/research/selected-bit-parent-reserve/README.md) | Under explicit full-cover, fixed-width, fresh-field, restoration and internally completed-leaf interfaces, the selected **BIT** parent has `log_q S(e,w) <= 8194*w*(1+log2 e)`. The native first-stage fit guard passes. | A physical GL64 packet implementation, H2, or fourteen independently admitted stages. The coefficient implication is conditional on the named interfaces. | +| [#2120, Nick Petalas](https://github.com/CrocSwap/integer-mult-bounds/blob/378593574261e0b0915e7e8a83147aa640274fc8/research/selected-bit-ceiling-free-stock/README.md) | With the same interfaces, terminal slack yields `D(n) <= (28/17)*log2(max(1,n))`, hence coefficient 6748 and a passing native first-stage fit guard. | Changed production pricing or a smaller implemented reserve. The row coefficient remains 18,355, and other stages need their preceding completed ordinary contract. | +| [#2087, Adam Gall](https://github.com/CrocSwap/integer-mult-bounds/blob/b5ffc48e3dd5c92f591bdb4fabafa2c8e8b33970/research/selected-bootstrap-uniform-time/README.md) | An all-width **implication** for H2 from a uniform stopped recurrence and a complete wrapper bill, with first-stage `K = C*max(401501,2*sigma)` when its primitive coefficients are at most C. | A bound on C, a stock coefficient, or proof that actual primitives meet those uniform contracts. Complete-fiber descriptor amortization is another explicit premise. | +| [#2097, Adam Gall](https://github.com/CrocSwap/integer-mult-bounds/blob/1d3ee0926656d5260c6cb1c0b81964ffe9fe1377/research/selected-cover-fresh-fibers/README.md) | Complete invocation fibers and the retained per-edge bad-class average follow from ancestor-only invocation decisions, fresh-role permutations, restoration and execution of the entire once-padded range. | An emitted selected all-size dependency certificate. A large reserve and restored final row alone do not imply those read/write restrictions or intermediate fiber completeness. | + +These are different implications. #1990 enlarges a **permitted coefficient +cap**; #2084/#2120 derive **sufficient coefficients** under implementation +premises; #2087 bounds time in terms of still-unknown primitive constants; +#2097 explains the address conditions needed for the averaging contract. +None makes the other premises automatic. + +H1 is the completed previous ordinary algorithm at every required width. +H2 is the cutoff-independent time estimate whenever stock fits. H3 is the +uniform stock envelope. With those premises established, #1965's restated +lemma separates fit from time absorption. Maintainer adoption of that wording +is separate from checking these implications; the frozen original proof and +its carried-constant audit remain unchanged. + +## Bind the ordinary producer correctly + +The selected complex supplier has `m=73` and binds the shared saving, but the +ordinary stopped producer in these four proposals is **PR589 BIT `m=64`**. +Its maximum child rank is 42, with 28,416 live roles and **28,425 physical +roles**, including nine work roles. Complex rank-48 depth work is a different +producer. The fourteen selected arithmetic headrooms do not identify fourteen +implemented reserve envelopes. + +For a fixed eligible odd prime `q>2^80` and integer `w>=1`, the BIT stock +proof charges a complete level divisor + +```text +W_q(w) = 28425 * |GL_64(F_q)| * q^(4096*(w-1)), +log_q W_q(w) < 4097*w, +S(n,w) = W_q(w)^D(n). +``` + +Here `W_q(w)` is an actual row divisor, not the time moment's live-role +denominator. High-matrix fibers may cancel in normalized time but not in +stock. Siblings and the two ordinary-wrapper calls reuse a restored quotient; +they do not multiply it. The zero external leaf factor requires an internally +completed ordinary leaf, not a claim that the leaf has no internal workspace. +For borrowing, #2120 chooses stock from original width e **before** choosing +borrowed width k and the resulting body width. + +The numerical connections are cheap to check without a supplier replay: + +```sh +python3 -I -B - <<'PY' +from fractions import Fraction + +assert 2**17 * 42**28 < 64**28 +assert 4097 * Fraction(28, 17) == 6748 +assert Fraction(6748, 8194) == Fraction(14, 17) +for sigma, ell in ((8194, 17), (6748, 16)): + assert 2**(ell-1) < 8*sigma <= 2**ell +assert max(401501, 2*6748) == 401501 +print("PASS_SELECTED_BOOTSTRAP_MAP_ARITHMETIC") +PY +``` + +Thus substituting the conditional `sigma=6748` into #2087's displayed +first-stage formula leaves `K=401501*C`. This is arithmetic, **not** a +measurement of C or a composed implementation certificate. At the recorded +native first-stage cutoff `L=4785575287428`, both stock proposals check the +sufficient guard. Neither result lowers that cutoff or prices the selected +supplier again. + +## Replay the right evidence + +The retained packages are present on the snapshot main. From the repository +root, using standard-library Python 3.12: + +```sh +python3.12 scripts/research_package.py --package research/bootstrap-cutoff-carry +python3.12 scripts/research_package.py --package research/bootstrap-cutoff-time-space-split +python3.12 scripts/research_package.py --package research/selected-bootstrap-stock-audit +``` + +The open packages are **not present on that main**. Run the same launcher in +an isolated checkout of the corresponding pinned head, with the package path +below. Do not overlay them onto frozen predecessors or substitute a moving +PR head for the cited one. + +| PR | Exact replay head | Package under `research/` | +| --- | --- | --- | +| [2084](https://github.com/CrocSwap/integer-mult-bounds/pull/2084) | `8001a23b003bec5dff5e61edec907b652c475932` | `selected-bit-parent-reserve` | +| [2120](https://github.com/CrocSwap/integer-mult-bounds/pull/2120) | `378593574261e0b0915e7e8a83147aa640274fc8` | `selected-bit-ceiling-free-stock` | +| [2087](https://github.com/CrocSwap/integer-mult-bounds/pull/2087) | `b5ffc48e3dd5c92f591bdb4fabafa2c8e8b33970` | `selected-bootstrap-uniform-time` | +| [2097](https://github.com/CrocSwap/integer-mult-bounds/pull/2097) | `1d3ee0926656d5260c6cb1c0b81964ffe9fe1377` | `selected-cover-fresh-fibers` | + +For example, at the cited #2120 head: + +```sh +python3.12 -Werror -B scripts/research_package.py --package research/selected-bit-ceiling-free-stock +``` + +All seven registered replays passed locally on Linux x86_64 / CPython +3.12.15 for this map, including their declared rejection controls. The four +open-head replays used separate source-bound sparse worktrees, which remained +clean afterwards. The arithmetic above and local link checks also passed. +These are replays of the authors' finite evidence, not an independently +implemented mathematical checker or human proof review. No selected cold +replay, physical compiler, formal-kernel or hosted CI result is claimed here. + +## Open next questions + +- **Bind the implementation premises, rather than recomputing headroom.** + A feasible first step is a selected invocation whose guard, edge list and + weights read only ancestor fields, and whose routes fix unused descendant + stock. Check complete high fibers, restoration and paid routing together. + This matters because #2097's adaptive-current-field and pruned-dummy-row + counterexamples preserve final rows while breaking the averaging argument. + A scalar endpoint check alone is not the missing certificate. +- **Bind an ordinary leaf and the uniform tolls.** Trace its internal borrowing, + completed spectators, conversion/preparation sites and row return at all + admitted widths. This determines whether H1, the external-factor-one stock + induction and #2087's width-independent primitive constants actually apply. + Component work is coordinated in + [Discussion #2114](https://github.com/CrocSwap/integer-mult-bounds/discussions/2114) + and the [whole-invocation claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/2179). + Those provisional follow-ups are not composed or audited by this map. +- **Extend only after completion of the previous stage.** Each later native + or conservative stage needs its own preceding completed ordinary contract + and any remaining fit conditions. The fourteen headrooms are an arithmetic + starting point, not a substitute for that induction or maintainer adoption. + +## Scope and credit + +Task `scope-navigation`, consolidation; nonce +`9540ac7c50e97c48ffce51501dabc841`, scope key `fff26335d457e528d9c4`. +Scope refined to this dependency map and one onboarding link. The initial +P104 alternative was not pursued because Aaron Wang's +[scope-map PR #2133](https://github.com/CrocSwap/integer-mult-bounds/pull/2133) +already covers it. Entry overlap covered 428 open PRs and 862 Discussion +records at 22:30/22:31 UTC. The pre-submission refresh covered 428 open PRs +and 864 Discussion records at 22:35/22:36 UTC, with complete pagination. +Canonical main and all four cited open heads were unchanged. Metadata searches +do not cover every code diff or unpublished result. The +[canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/2114#discussioncomment-18935479) +records coordination and final freshness. + +All mathematical results remain credited to the authors above. The selected +PR589 word and its nine-stage lineage are DreamingOfClouds' work on eumemic's +base; PR185/PR387 completed-row contracts and selected PR1094 are Rohan Arun's +work, with Jeremy Kothe's PR1087 and the source527 cover/borrowing lineage +retained. Sricharan Vagvala's separate complex-depth audit informed #2120's +inverse-threshold cross-check, not a change of producer here. This document +adds navigation and checked replay routes only. Apache-2.0.