Repository navigation
Prove and bind T74 cost in the actual selected width - #3599
Merged
Mister-Meeseeks merged 3 commits intoOct 20, 2026
Merged
Conversation
This was referenced Oct 20, 2026
Price one typed actual-width physical H and its toward-zero return
unpaidmoon/integer-mult-bounds#17
Draft
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.
In PR3477, I chose the physical T74 root's internal width from precision p, even when its caller selected fewer bits. I now use the actual selected width g and prove the resulting source-relative bound
I preserve the normalized H0 endpoint, pointwise spectators, borrowed input, full-depth row stock and one final truncation. The theorem requires actual complete coefficient records with
2^(b(log2 p)^2) <= randlog2 r <= Bp, for fixed b,B>0, plus the retained O(p) descriptor, source-native, hosting and physical-refinement premises. The constants may depend on b,B,q and the finite source.I bind PR3562's ordinary profile
c=1/577to the same physical cohort, change the stopping power from 1000 to 10^6, and retain the complete 2,394,506-child T74 invoice. The proof pays the deeper stop, reserved leaves and small-g fallback. I compare the copied transitions against their frozen predecessors and authenticate all 23 ordinary-backend files.I also prove a single-bit exposure identity for a complete global tensor, with final permutation support at most 2g. Its global cost remains conditional on the richer paid support-router contract and retains
polylog p. I supply finite algebra and a 16-record physical-root/reference-permutation composition. I do not supply an executable fast arbitrary-support router or a multiplication-exponent improvement.I started from canonical main
20ecf2891d80b5acf18d980b2164fb44ea7faa90, priority revision 6. I add one isolated package and leave the selected frontier unchanged. In the final overlap check at 07:18:53 UTC on 2026-10-18, I covered 314 open PRs and 2,436 Discussion records with complete pagination. I found no additional duplicate or objection beyond the credited work below. Canonical investigation.Validation at
72df81b8cee17ffd990fc18b2d54024f65971556:-I -O -Werror -B, and verified that the 25 regular files including the receipt remained byte-identical. Export SHA256:7eae80a477788a72899e0a7d1992f20cf82d58db1387e1b209911f32e77c090c.In the first CI run, I passed science and source contracts, then hit the plan suite's 240-second timeout on Ubuntu. I retained its four full-field cases, reused the p=5,g=2 result for the old/new comparison, and allowed 300 seconds within the 1200-second total budget. I measured 75 seconds locally and 185.615 seconds on the hosted runner for the revised plan check. I passed CI run39108314551 on the current head with CPython 3.12.15, including all six registered groups and the unchanged-committed-input check.
Reproduce with Python 3.12 and the standard library:
I retain Jose Manuel's PR3385/3477/3562, David Arias's PR2753 caller, Nick Petalas's PR2808/3493 wrappers, Adam Gall's PR2087 lifting, Marius-Paul Dumitrean/Dugongue and Jeremy Kothe's T74 word/profile, and Vlado Vojdanovski's PR1673 router/tensor arguments. The source exports preserve the remaining notices.
Hiroki Kumazaki's concurrent PR3576, head
1630afea0fc1083717b5b2799b8de7a819a6ea02, retunes the older root and stop. I credit that shared factory/rate step and adapt his binding-module namespace and constructor checks. Nick Petalas's PR3581, head282915e57cf71d7a6f0087fbb6ae03345a0b33d4, proves a Theta(Vg) barrier for a restricted materialized B1-only exposure adapter. I preserve that boundary and require the richer conditional router.I leave fast support-router implementation, missing-record placement, larger-group/outer error and packing integration, and independent scientific review open. Jose Manuel (
jmbarrancoml), with substantial OpenAI Codex assistance in proof, implementation, verification and source analysis. Apache-2.0.