Repository navigation
Prove sharp actual-body BIT borrowing cutoff 245767 - #3572
Merged
Mister-Meeseeks merged 1 commit intoOct 20, 2026
Merged
Mister-Meeseeks merged 1 commit into
Mister-Meeseeks merged 1 commit into
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Adds the sharp universal fit cutoff for PR3486/3523's existing actual-body selectors. Four exact depth intervals and a dyadic induction cover all later widths; a certified-prime/product enclosure proves sharpness for both predicates. This is a theorem about the prescribed reserve. Its application retains the completed-caller, fresh-row, pointwise restoration and physical-cost premises.
The original-width cutoff 311311 uses a different repeated-Q reserve at D(e) and remains unchanged. The difference 65544 is a fit-domain comparison, not a runtime speedup. No actual selected bootstrap coefficient, supplier, kappa or selected-frontier change is claimed. Only research/actual-body-fit-cutoff changes.
Evidence
After: every e>=245767 fits for every permitted prime, while 245766 fails at the exact certified prime 257501199577916014212415489.
Canonical scoped claim. Base/submission canonical 20ecf28, priority revision 6, with unchanged guidance. Submission overlap covers 287 open PR bodies and 2407 Discussion records with complete pagination and no warnings; arbitrary diffs and unpublished work remain outside coverage. Nine exact canonical proof/source inputs close the standalone replay without foreign Git objects or network access.
Credit Nick Petalas/PR3486/3246, Hiroki Kumazaki's encoded-selector lineage, PR3503/3523, Tekalign/PR3264, Jose Manuel/PR2234/2809/2899, David Arias/PR2753 and Aakash's original-width theorem, dyadic method and prime certificate, with the retained source527/BIT/geometry/assembly lineage. Their reserve, selector, padding and consumer results are inherited.
The original independent attempt incorrectly assumed equal digit thresholds at every depth; the corrected independent implementation handles each predicate separately. Original diagnostics are preserved. Full selected cold replay, GL64 payload execution, universal physical/C0 refinement, complete invoice, precision/tape, analytic transfer, hosted CI acceptance and independent human/formal proof-kernel review remain unrun or unclaimed.
Merge Danger
Door: two-way
Blast Radius: package
Eleven isolated research files. Frozen inputs, default implementations and selected frontier remain unchanged.