Repository navigation
Use dimension-30 geometry for conditional kappa = 1.2649e-7 - #12
Mister-Meeseeks merged 2 commits into
Conversation
…ithmetic Three libraries in the same Lake project prove each PR's counts, eta, log bounds, exponent certificates or moments, slacks, margins and min g > kappa (310 theorems, standard axioms only). PRChecksB.PR5Analytic also proves CrocSwap#5's analytic inequalities and PRChecksC the CrocSwap#10 bulk-guard Taylor bound. Drift tests tie every Lean literal to each PR's own certificate. The PR files they read are vendored under formal/open-prs/data with their head commits and SHA-256 in MANIFEST.json, checked by tests/test_open_pr_lean.py. formal/open-prs/README.md records scope (CrocSwap#1-CrocSwap#12 as of 2026-10-08) and the findings: the CrocSwap#3/CrocSwap#8 ceiling, CrocSwap#3 docs line 102, CrocSwap#4's outdated notes, the CrocSwap#5/CrocSwap#6 g4 wording, CrocSwap#6's window size, and CrocSwap#5's Harvey-van der Hoeven wording. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015MYnETxrAa57d3wqw3v9HR
|
Integrated and retained on main in 377e2bd. Thank you @rohanarun for this contribution. The complete original source tree at Reviewed scope: Dimension-30 mixed-width composition: six complete native dimension screens and scoped prime-power exclusions; all seven matching enumerations; h30 full producer replay and 456 template dirty-state controls, exact moment, 29 assembly constraints and patch. Unchanged #10 dependencies remain inherited; not a new full theorem audit. The batch review and per-file dispositions cover every original changed path. Local focused checks passed; regenerated artifacts match the submitted sources. Attribution is also recorded in CONTRIBUTORS.md. This is integration of historical research and finite evidence, not a new selected κ or full formal verification of inherited tape/analytic interfaces. Linux replay jobs are tracked separately. |
This follow-up supports the unreviewed conditional witness kappa = 12649/100000000000 = 1.2649e-7, about 2.84% above PR #10's 1.2299998e-7, in
T(n) = O(n (log n)^(1-kappa)).The change uses the five-subset bit network at dimension 30, the selected star rules of #9, and the bank-matching extension of #11. That dimension was weaker under uniform recursion but is stronger under icekylinx's controlled batching model. The dimension-28 complex network, its 7e-7 saving, path-depth guard, and Gaussian correction remain unchanged. The exact bit saving becomes 253/10^9.
This branch is based on PR #10 at
62691e395a0458ce089a1c7b5d89e74291e95e29, with its contribution retained unchanged except for the additional follow-up entry points and documentation. Dependencies from #9 and #11 are included. The incremental mathematical argument, certificate and integration generator are inresearch/batched-followup/; the full independent manuscript patch ispatches/batched-dimension30.patch.Validation completed:
make verifynow also runs the new producer and follow-up checks.The integrated patch retains the h28 baseline proofs, adds the h30 bit lemma, updates the layer interface and its downstream consumers, and includes the new integer rounding comparison for epsilon. Bundled
upstream/is unchanged. PDF compilation of the newly materialized manuscript is a separate check and is not claimed by the source-integration checks above.The contribution remains conditional on the retained upstream framework and the written proofs in #7 and #10; finite checks are not formal verification of the full theorem. The scoped review found no blocking defect in the examined batching arguments. Original attribution and licenses remain intact, including Zhihao Chen's ternary construction and icekylinx's batching work. The dimension-30 continuation was prepared with substantial OpenAI Codex assistance at Rohan Arun's request. No worldwide priority or practical runtime improvement is claimed.