Skip to content

Batch recursive networks for a conditional kappa > 2^-23 bound - #10

Merged
Mister-Meeseeks merged 1 commit into
CrocSwap:mainfrom
icekylinx:research/batched-23
Oct 8, 2026
Merged

Mister-Meeseeks merged 1 commit into
CrocSwap:mainfrom
icekylinx:research/batched-23

Conversation

@icekylinx

Copy link
Copy Markdown
Contributor

Change and mathematical scope

This change supports the conditional integer-multiplication bound

$$ T(n)=O!\left(n(\log n)^{1-\kappa}\right),\qquad \kappa=\frac{6149999}{50000000000000}>2^{-23}. $$

  • Batch contiguous rational projector blocks using a simultaneous controlled basis.
  • Apply whole complex residuals as recursive calls, with mixed-width row handling and a dependency-path precision guard.
  • Correct the retained Gaussian input error enclosure to F = 2^ceil(1.14α²), preserving P = 34p and the final exponent.
  • Include the proof PDF, exact certificates, combined manuscript patch, and reproduction instructions. Integrate the new checks into make verify.

The change includes the required dependencies from PRs #3, #5, and #7. PR #7 is pinned at 6725c6a17b17871a35353fd29157f4ed851bc114. Existing contributor attribution and Apache-2.0 notices are preserved; the new contribution and substantial AI assistance are recorded in NOTICE and SOURCES.json.

The result remains conditional on the pinned upstream multiplication framework and retained interfaces. Finite checks do not constitute formal verification of the full theorem.

Validation

  • Retained h28 producer, coefficient, and frame checks passed.
  • 166 unit tests passed, including exponent-boundary, Gaussian-precision, and manuscript-integration controls.
  • Exact certificate and combined-patch regeneration passed.
  • All 18 retained manuscript patch checks passed.
  • The proof note and complete patched manuscript compiled successfully.
  • Bundled upstream source and licenses remain unchanged.

princezuda pushed a commit to princezuda/integer-mult-bounds that referenced this pull request Oct 8, 2026
…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
@princezuda princezuda mentioned this pull request Oct 8, 2026
@Mister-Meeseeks
Mister-Meeseeks merged commit 62691e3 into CrocSwap:main Oct 8, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants