diff --git a/research/centered-gaussian-residue/PROOF.md b/research/centered-gaussian-residue/PROOF.md new file mode 100644 index 0000000000..fb48a42212 --- /dev/null +++ b/research/centered-gaussian-residue/PROOF.md @@ -0,0 +1,166 @@ +# A centered child for the paid Gaussian residue lane + +This proof was produced by Nick Petalas. Apache-2.0. +Claim type: scoped constructive written proof with finite exact corroboration. + +The question is PR3926 Open next question 2. ToikY supplies the attained +unsigned child-size theorem. David Ganz / Dugongue's PR3881 supplies the paid +residue-assisted Gaussian lane and its numerical recovery theorem, building +on Mason Hale's Gaussian backend, normalization, CRT ordering and carry scan. +Those results are cited premises. The new step replaces only the exact lane's +packing and extraction. Signed Kronecker substitution is classical. + +## Signed coefficient separation + +Let two nonempty arrays have lengths A and B, and let k>=1. Put + +```text +q = 2^k, a = q/2, m = min(A,B), h = ceil(log2 m), +w = 2k-1+h, beta = 2^w. +``` + +Replace every original nonnegative digit x by its unique congruent value +`c(x)` in `[-a,a-1]`. Pack the centered arrays as the signed integers + +```text +U = sum_i c(x_i) beta^i, V = sum_j c(y_j) beta^j. +``` + +One multiplication of the nonnegative magnitudes |U| and |V|, followed by +the known product sign, supplies UV. Sign handling, packing and extraction +are additional work, not free operations or extra recursive products. + +For output coefficient j let nu_j be its number of summands. Each summand +lies in `[-a(a-1),a^2]`, so its exact signed convolution coefficient C_j is +in the integer interval + +```text +l_j = -nu_j a(a-1) <= C_j <= u_j = nu_j a^2. +``` + +This interval has diameter + +```text +u_j-l_j = nu_j(2a^2-a) < 2m a^2 <= 2^(2k-1+h) = beta. +``` + +Consequently at most one integer in this interval represents a given residue +modulo beta. Starting with P=UV, recover successive coefficients by + +```text +C_j = l_j + ((P-l_j) mod beta), +P = (P-C_j)/beta. +``` + +The first congruence identifies the genuine C_j because every higher term +is divisible by beta. After subtraction and division the same argument +applies to the next coefficient. Induction recovers every coefficient and +leaves P=0. This argument works with negative packed values and floor +division because the numerator is exactly divisible. Reducing C_j modulo +q gives the original unsigned convolution coefficient modulo q. + +The asymmetry is necessary at this width. For k=2 and two entries per +array, the arrays (-2,-2) have convolution (4,8,4), with middle coefficient +exactly beta/2=8. A symmetric half-open decoder would choose -8. Using +ordinary unsigned extraction on a negative packed product can also introduce +spurious higher coefficients. The interval algorithm addresses both cases. + +The retained unsigned lane uses w_old=2k+h. The construction therefore saves +exactly one bit per slot at every k and positive overlap. This is a sufficient +new slot rule, not a claim of minimum width over every possible packing. + +## Attained magnitude bit length + +Now both arrays come from a declared n-bit integer in base 2^b, with +1<=k<=b. Let + +```text +L = ceil(n/b), t = n-b(L-1), h = ceil(log2 L), w = 2k-1+h. +``` + +The exact largest bit length of the packed magnitude, with bit_length(0)=0, +is + +```text +D_center(n,b,k) = min(k,t) + (L-1)(2k-1+h). +``` + +For L=1, reduction and centering give a maximum magnitude-bit length k if +t>=k, attained by the digit a. If t=2. If t>=k, every centered digit has magnitude at most a, so + +```text +|U| <= a sum_(i=0)^(L-1) beta^i < 2a beta^(L-1). +``` + +Thus its magnitude-bit length is at most k+(L-1)w. A top digit a and all +lower digits zero give U=-a beta^(L-1), attaining this bit length. + +If ta+1, +because L>=2 implies h>=1 and beta>=2^(2k). The lower part has magnitude + +```text +a sum_(i=0)^(L-2) beta^i < beta^(L-1). +``` + +The complete magnitude is therefore strictly below 2^t beta^(L-1). +A top digit 2^(t-1) and all lower digits zero attain bit length +t+(L-1)w. These input digits are legal in the declared n-bit domain. +This proves the formula and its attainment, including partial top digits. + +Subtracting it from ToikY's cited unsigned formula gives exactly L-1 saved +operand bits. Both recursive child operands use nonnegative magnitudes. +The product may have twice their bit length; no output-size or total-cost +reduction is inferred from the input bound alone. + +## The new uniform tail in the retained box + +Retain b=64 and the PR3881 source box of size 455, which permits +L<=228 because 2L-1<=455. At k=28 the new width is w=55+h<=63. +For L>=2, + +```text +D_center <= t+63(L-1) < t+64(L-1) = n. +``` + +For L=1 and n>=29, D_center<=28=29 also fails there. Hence +28 is the largest fixed k in this new slot scheme with strict shrinkage +throughout its supported tail k+1..14592. This is not a bound on other +packing algorithms or Gaussian certificates. + +PR3926's cited fixed numerical certificate has least p=208-k. Its +Gaussian proof depends on the residue value modulo 2^k, not on this lane's +choice of representatives. The new lane supplies exactly the same residues, +so its recovery implication applies at k=28,p=180 for the entire new uniform +tail. The previous k=27 uniform tail used p=181. This is one fewer rounded +payload bit under that sufficient certificate; Q=448 is unchanged. + +The universal recovery statement remains conditional on the credited backend +and numerical proof premises. The new boundary replay replaces the lane in +the unchanged source caller and executes p=180 at n=8193 and n=14592, +including an attaining packed magnitude and negative packed operands. +Reference products and schoolbook coefficients are used only after recovery. + +## Remaining obligations + +This settles a changed-packing/strict-child interface question. It does not +price the complete numerical transforms, pointwise products, sign handling, +packing, signed extraction, lifting, carry, preparation, physical movement, +storage or restoration. In particular a smaller child need not reduce total +time. No all-size recursion/base-case policy, actual native supplier, selected +admission, new kappa or complete multiplication theorem follows. The five +selected framework assumptions remain open. Independent human and formal +proof-kernel review are unclaimed. diff --git a/research/centered-gaussian-residue/README.md b/research/centered-gaussian-residue/README.md new file mode 100644 index 0000000000..5137d8fef8 --- /dev/null +++ b/research/centered-gaussian-residue/README.md @@ -0,0 +1,152 @@ +# A uniformly shrinking 28-bit Gaussian residue child + +This contribution was produced by Nick Petalas. Apache-2.0. +Claim type: scoped constructive written proof with exact finite corroboration. +No new kappa or selected-frontier change is claimed. + +Centering the residues and decoding through an asymmetric signed interval +saves one bit in every Kronecker slot of the paid Gaussian residue lane: + +```diff +- unsigned slot: 2k + ceil(log2 L) ++ centered slot: 2k - 1 + ceil(log2 L) +``` + +For declared parent width n, digit width b, length L=ceil(n/b) and top digit +width t=n-b(L-1), the sharp maximum child magnitude-bit length is + +```text +D_center = min(k,t) + (L-1)(2k-1+ceil(log2 L)). +``` + +Both child operands are nonnegative magnitudes. Exactly one paid exact +multiplication supplies their product; sign handling and extraction remain +additional work. The new bound saves exactly L-1 operand bits relative to +the cited unsigned formula. + +In the retained 455-point Gaussian box with 64-bit digits: + +| Quantity | Result for the new layout | +|---|---| +| Largest fixed residue width shrinking throughout its supported tail | k=28, at every n=29..14592 | +| Prior unsigned uniform choice | k=27 | +| Full-width k28 child at n=14592 | 14329 bits, saving 227 bits | +| New k28 boundary at n=8193 | 8065 bits | +| k29 obstruction for this new layout at n=8193 | 8321 bits | + +The credited fixed numerical certificate permits p=208-k. The new uniform +tail therefore permits rounded payload precision p=180 rather than p=181. +Working enclosure precision Q=448 is unchanged. This is a precision and +child-size improvement, without a total-runtime or physical-cost claim. +[PROOF.md](PROOF.md) gives the all-length construction, attained size theorem, +uniform-tail proof and exact limits. The executable reference bounds arrays +to 228 entries and digits/residue widths to 64 bits. + +## Evidence and reproduction + +The standalone exact checker enumerates 13,140 array pairs and 50,628 +convolution coefficients. The domains include unequal lengths, zeros, +negative packed values and both signed endpoints. It checks 100 exact +small size maxima across 20,460 original inputs, five large attaining +inputs, all 933,888 supported width/residue pairs and every one of the +14,564 new k28 tail widths. The new layout admits 417,584 pairs versus +410,725 under the cited unsigned formula, adding 6,859 pairs. Fourteen +invalid-input/decoder cases reject. Four semantic controls include the +positive half-base endpoint, an undersized-slot collision and a failure +of unsigned extraction on a negative packed product. + +The changed-caller replay authenticates eight existing input files, loads +the retained PR3881 caller, and substitutes only its exact lane dependency +inside that private process. A finally block restores the dependency. +It executes complete p180 Gaussian products at n=8193 and n=14592, +checks all 455 recovered coefficients in each execution, and reaches the +new sharp child bounds in both. Each execution performs 573 Gaussian line +calls. The numerical backend, preparation, transforms, CRT order, lifting +and carry are inherited inputs, not results re-audited by this package. +Reference products and schoolbook coefficients are used only as postchecks. + +From the repository root, with the standard-library CPython 3.12 interpreter: + +```sh +PY=/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 +"$PY" -W error -X dev -I -B research/centered-gaussian-residue/verify.py +"$PY" -W error -X dev -I -B research/centered-gaussian-residue/boundary.py +"$PY" -B scripts/research_package.py --package research/centered-gaussian-residue +"$PY" -B scripts/check_research_commit.py --package research/centered-gaussian-residue --check-source-history +``` + +Substitute another CPython 3.12 path on another machine. The last command +requires committed package bytes. The registered replay runs both direct +checks normally and with optimization enabled. Expected markers are +`PASS_CENTERED_GAUSSIAN_RESIDUE`, `PASS_CENTERED_GAUSSIAN_BOUNDARY`, +`PASS_REGISTERED_RESEARCH_PACKAGE` and `PASS_RESEARCH_COMMIT_BYTES`. +Each direct invocation generates a stdout receipt bound to SHA256 hashes +of the package files. No receipt is handwritten or frozen. Outputs belong +outside the checkout. The official package export includes the declared +inputs; the two direct scripts require no Git or network in that export. + +## Scope, credit and overlap + +ToikY's [PR3926](https://github.com/CrocSwap/integer-mult-bounds/pull/3926), +Open next question 2, asks for a changed packing or numerical certificate. +Credit its attained unsigned size law, strict-child window and inherited +fixed-certificate precision law. David Ganz / Dugongue's +[PR3881](https://github.com/CrocSwap/integer-mult-bounds/pull/3881), head +`75e098dc12a2567e73a2858137408e08d31dbf84`, supplies the paid residue lane +and its Gaussian recovery theorem. Mason Hale supplies the numerical backend, +normalization, FFT/CRT ordering and carry path. Their source-specific notices +retain the Harvey-van der Hoeven and earlier contributor lineage. Signed +Kronecker substitution and modular lifting are classical. No general +literature-priority claim is made. Predecessor bytes and credit are unchanged. + +[SOURCES.json](SOURCES.json) pins live runtime inputs and historical provenance +at main `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8. +[TASK.json](TASK.json) records the explicit change from invoice verification +to this new packing construction. The selected-binding first command passed; +it was orientation, not a selected scientific replay. +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19363350) +preceded construction and execution. Live PRs, recent account PRs, claims, +merged searches and distinctive all-main README/PROOF searches were checked. +The cached remote snapshot covered 430 open PRs and 6,401 Discussion records. +Only 113 of 8,917 local note paths were materialized for that scan; targeted +Git searches supplemented it. Unpublished work and arbitrary diffs remain +outside this bounded overlap check. + +No new Gaussian error theorem, minimal packing theorem, complete caller +invoice, all-size recursion/base-case policy, physical implementation, +stock/tape bound, supplier admission or multiplication theorem is supplied. +All five selected framework assumptions remain. Lean, Docker, a selected +cold replay and independent human or formal proof-kernel review are unrun. + +## Open next questions + +- Does the new lane reduce the complete cost of one physical caller? Price + the k27/p181 and centered k28/p180 programs, including signs, extraction, + numerical transforms, preparation, movement and restoration. The missing + physical composition and complete invoice block a total-cost conclusion. +- Can another packing admit k29 uniformly? Begin at n=8193 with a different + pack/extract contract and its attained magnitude-bit maximum. The 8321-bit + exclusion here concerns this constant-slot scheme only. No further search + or follow-up construction is included. + +## Verification constraints + +Build the Lever supplies the explicit lane and deterministic checker. +Prove It Works requires two complete executions through the actual retained +caller, with the new lane reached and every recovered coefficient checked. +New functions are below 60 physical lines. There is no recursion or process +launch. All new arithmetic loops have bounds from 228 entries, 64-bit digits, +the fixed finite domains above, at most 455 coefficients or eight source +files. Acceptance checks use explicit exceptions and survive optimization. +Warning-strict normal/optimized execution and in-memory syntax compilation +provide the available diagnostics; no separate static analyzer was run. + +Power of Ten rule 3 deviation: CPython and Fraction allocate dynamically. +The bounded command uses fixed small lists and bounded operand sizes, with +at most 228 digits and packed operands below 31,000 bits. Receipt reads +are bounded to eight package files of at most one MiB each. No fixed-memory +or allocator-internals claim is made. Rule 9 deviation: one authenticated +fixed-path module import and one named lane substitution bind the actual +caller; their targets are fixed and restoration runs on every exit. +Inherited backend code and its runtime are unchanged dependencies, with +their existing contracts, rather than newly certified Power of Ten code. diff --git a/research/centered-gaussian-residue/SOURCES.json b/research/centered-gaussian-residue/SOURCES.json new file mode 100644 index 0000000000..8466a7154b --- /dev/null +++ b/research/centered-gaussian-residue/SOURCES.json @@ -0,0 +1,84 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/gaussian-residue-shrink-window/PROOF.md", + "usage": "provenance", + "git_blob": "62e19e3c8a487a7a70d5533ad27fe51bf49188b2", + "sha256": "7b571536706df789bbe65df9e4da40426ea8fd5f61609f7db014f8c7f0c05203" + }, + { + "path": "research/gaussian-residue-shrink-window/README.md", + "usage": "provenance", + "git_blob": "40079b9a38831f0a6380a9d7c7c8f7847cbf6d6b", + "sha256": "6e6bbb4610c633cb99e4802f4df3d0346a8b3cd1527507579e6f300cdb7a83f3" + }, + { + "path": "research/modular-gaussian-recovery/INPUTS.json", + "usage": "input", + "git_blob": "bd71e58b58b3df7ad12533b9c4d8d37e19985423", + "sha256": "460151dd416a183c7e236cf07e6a989a897ec4f370e92444a2f005d69776cd59" + }, + { + "path": "research/modular-gaussian-recovery/PROOF.md", + "usage": "provenance", + "git_blob": "728c1d179f30f35d9d954c71c1437b22fbe1015a", + "sha256": "6242cb6b32de0c237612f8c3e025e874367fa4359fc63d5f5d1a595ebeeb769e" + }, + { + "path": "research/modular-gaussian-recovery/hybrid.py", + "usage": "input", + "git_blob": "4015d0195c1c5e381f0069cd073dff51089d930a", + "sha256": "cb716f1bec3e3fc0aa5a2b51219462ac813821ce9dc278a386c0a841c2ba18b6" + }, + { + "path": "research/modular-gaussian-recovery/vendor/NOTICE.md", + "usage": "input", + "git_blob": "5e3269b5afe5e11f044ffae45216c4731b42c7af", + "sha256": "10acae9e78402ca70c6afd0e8d6da8fefc0da519c646cf43d93f923aba85b86d" + }, + { + "path": "research/modular-gaussian-recovery/vendor/PR3878-PROOF.md", + "usage": "input", + "git_blob": "89642f4740c62460835380a3bfa00f63808009a8", + "sha256": "5452f3e2191824b4a8451c83fbdf58b3b2228f4e1966a6f22c3e60bd152e56b0" + }, + { + "path": "research/modular-gaussian-recovery/vendor/PROOF.md", + "usage": "input", + "git_blob": "9dace009004a4336d6ce57764c255190fbf87e64", + "sha256": "65480dd23fb1aae314365aeea4aacbc146e160e5c8a7a4ac4f602f22ae4581de" + }, + { + "path": "research/modular-gaussian-recovery/vendor/gaussian.py", + "usage": "input", + "git_blob": "ac444a242caba128754615227ad6057545822a34", + "sha256": "572c2a88b12dd6e9f8fe4387ba2f8fa58e9bc01c6a4e01d2945be4d4277c6d3e" + }, + { + "path": "research/modular-gaussian-recovery/vendor/intervals.py", + "usage": "input", + "git_blob": "91d458865aa026bdf0d59653a4ecbfe3a178ecbc", + "sha256": "159d2a7d32a8cc7c8f56632a8ef127308b984a0a6753c9d6bdccacc6e7d6d4df" + }, + { + "path": "research/modular-gaussian-recovery/vendor/pipeline.py", + "usage": "input", + "git_blob": "8b5fbc26b38fce5f917d214f987eda8a55d34bd1", + "sha256": "3cceae8665d06f72275258acf8e2bc17b816a0bde45d8f109aa7364a30861728" + } + ] +} diff --git a/research/centered-gaussian-residue/TASK.json b/research/centered-gaussian-residue/TASK.json new file mode 100644 index 0000000000..b5d3e0e0bd --- /dev/null +++ b/research/centered-gaussian-residue/TASK.json @@ -0,0 +1,127 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "independent-moment", + "question": "Does a changed construction's serialized target/paid invoice independently support its claimed improvement?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "docs/research/recursive-invoice-preflight.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Independently recount one changed emitted word and its complete caller, importing no constructor or pricing engine. Include target losses, owned lifetimes, native orientation and extra charges. Check existing #5633/#5708/#5717/#5719 coverage to avoid duplicate audits and preserve its exact head. Stop after the chosen missing implication; a correct root alone is not supplier admission.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "invoice", + "signed moment", + "productive target", + "independent recount" + ], + "existing_checks": [ + { + "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.", + "evidence": "research/staged-fourth-mixture-ceiling/README.md", + "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.", + "status": "author-checked", + "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.", + "evidence": "research/r437-two-window-carrier/README.md", + "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.", + "status": "author-checked", + "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Construct a centered signed residue lane, prove its attained child-size formula and the new k28 uniform tail, and execute the changed lane in the retained Gaussian caller.", + "scope_change_reason": "The assignment requires an original contribution. PR3926 Open next question 2 explicitly asks for a changed packing; predecessor mathematical results are cited, not audited.", + "bottleneck_link": "A residue-assisted numerical caller needs a genuinely smaller paid exact child. This packing admits one additional uniform residue bit under the fixed numerical certificate, without asserting a favorable complete invoice.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified one-bit-per-slot improvement, package its proof and new boundary executions, and leave further optimization under Open next questions.", + "outcome": "completed", + "evidence": "PROOF.md; packing.py; verify.py; boundary.py; generated hash-bound stdout receipts.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does the new signed lane reduce the complete cost of one named physical Gaussian caller?", + "why_it_matters": "Strict child shrinkage and one fewer rounded payload bit do not prove total time savings.", + "first_step": "Price both complete callers at k27/p181 and centered k28/p180, including signs, signed extraction, transforms, preparation and movement.", + "blocked_by": "No complete source-bound physical caller invoice is supplied." + }, + { + "question": "Can an exact variable-slot or alternate packing admit k29 uniformly in this box?", + "why_it_matters": "The k29 exclusion here concerns only the stated constant-slot construction.", + "first_step": "Specify another reversible pack/extract contract and prove its attained magnitude-bit maximum at n8193.", + "blocked_by": "A different packing and complete extraction bill are needed; more tests of this fixed layout cannot change its bound." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19363350", + "predecessors": [ + { + "pr": 3926, + "author": "ToikY", + "scope": "Attained unsigned size law, fixed-certificate precision law and explicit changed-packing question." + }, + { + "pr": 3881, + "author": "Dugongue", + "head": "75e098dc12a2567e73a2858137408e08d31dbf84", + "scope": "Paid exact residue lane and Gaussian recovery theorem; Mason Hale backend and retained lineage." + } + ], + "overlap_coverage": { + "open_prs": 430, + "discussion_records": 6401, + "remote_fetched_at": "2026-11-03T00:39:08Z", + "local_notes_searched": 113, + "local_head_notes": 8917, + "limits": "Sparse local notes; all-main targeted README/PROOF searches and merged PR searches supplement these. Unpublished work and arbitrary diffs are not covered." + } +} diff --git a/research/centered-gaussian-residue/VERIFY.json b/research/centered-gaussian-residue/VERIFY.json new file mode 100644 index 0000000000..b6f4ce0da2 --- /dev/null +++ b/research/centered-gaussian-residue/VERIFY.json @@ -0,0 +1,76 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/modular-gaussian-recovery/INPUTS.json", + "research/modular-gaussian-recovery/hybrid.py", + "research/modular-gaussian-recovery/vendor/NOTICE.md", + "research/modular-gaussian-recovery/vendor/PR3878-PROOF.md", + "research/modular-gaussian-recovery/vendor/PROOF.md", + "research/modular-gaussian-recovery/vendor/gaussian.py", + "research/modular-gaussian-recovery/vendor/intervals.py", + "research/modular-gaussian-recovery/vendor/pipeline.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-X", + "dev", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "New signed convolution, attained small and large magnitude widths, complete supported-width domain and rejection/semantic controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-X", + "dev", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "The same exact new packing checks with optimization enabled." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-X", + "dev", + "-I", + "-B", + "{package}/boundary.py" + ], + "timeout_seconds": 120, + "checks": "Authenticated source caller with only the new lane substituted; two complete p180 Gaussian products at new uniform-tail and full-width boundaries, every recovered coefficient and attaining child magnitude." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-X", + "dev", + "-I", + "-O", + "-B", + "{package}/boundary.py" + ], + "timeout_seconds": 120, + "checks": "The same changed-caller endpoint and residue-lane checks with optimization enabled." + } + ] +} diff --git a/research/centered-gaussian-residue/boundary.py b/research/centered-gaussian-residue/boundary.py new file mode 100644 index 0000000000..331d40ab83 --- /dev/null +++ b/research/centered-gaussian-residue/boundary.py @@ -0,0 +1,101 @@ +"""Execute the changed lane in the credited caller. Produced by Nick Petalas.""" +from fractions import Fraction +from hashlib import sha256 +import importlib.util +import json +from pathlib import Path +import sys + +ROOT = Path(__file__).resolve().parent +sys.path.insert(0, str(ROOT)) +from packing import child_bits, residue_lane + + +def check(condition, message): + if not condition: + raise AssertionError(message) + + +def authenticated_caller(): + repository = ROOT.parent.parent + sources = json.loads((ROOT / "SOURCES.json").read_text()) + check(len(sources["files"]) <= 32, "source inventory capacity") + check(sum(row["usage"] == "input" for row in sources["files"]) == 8, "input count") + for row in sources["files"]: + if row["usage"] == "input": + path = repository / row["path"] + with path.open("rb") as stream: + raw = stream.read(1024 * 1024 + 1) + check(len(raw) <= 1024 * 1024, "source capacity") + check(sha256(raw).hexdigest() == row["sha256"], "source hash " + row["path"]) + path = repository / "research/modular-gaussian-recovery/hybrid.py" + spec = importlib.util.spec_from_file_location("centered_residue_source_caller", path) + check(spec is not None and spec.loader is not None, "source loader") + caller = importlib.util.module_from_spec(spec) + spec.loader.exec_module(caller) + return caller + + +def schoolbook(left, right): + result = [0] * (len(left) + len(right) - 1) + for j, x in enumerate(left): + for i, y in enumerate(right): + result[i + j] += x * y + return result + + +def run_case(caller, lines, n): + length = (n + 63) // 64 + top = n - 64 * (length - 1) + # Leading coefficient attains the new sharp magnitude-bit bound. + left = 1 << (64 * (length - 1) + min(top, 28) - 1) + # Populate all lower signed slots, including negative representatives. + right = (1 << n) - 1 + answer, trace = caller.multiply(left, right, lines, 64, 28, input_bits=n) + check(answer == left * right, "changed complete Gaussian product") + radix = 1 << 64 + a = [(left >> (j * 64)) % radix for j in range(length)] + b = [(right >> (j * 64)) % radix for j in range(length)] + expected = schoolbook(a, b) + check(trace["coefficients"] == expected + [0] * (455 - len(expected)), "recovered coefficients") + lane = trace["exact_lane"] + check(lane["left_child_bits"] == child_bits(n, 64, 28), "new attained child bound") + check(lane["slot_bits"] == 55 + (length - 1).bit_length(), "new source adapter reached") + check(lane["exact_child_calls"] == 1 and lane["strictly_smaller_child_bound"], "paid strict child") + check(Fraction(*trace["uniform_radius"]) < 1 << 27, "inherited modular precision") + check(trace["precision"] == 180, "new uniform-tail precision") + return {"parent_bits": n, "sharp_child_bits": child_bits(n, 64, 28), + "actual_child_bits": [lane["left_child_bits"], lane["right_child_bits"]], + "slot_bits": lane["slot_bits"], "recovered_coefficients": len(trace["coefficients"]), + "gaussian_line_executions": trace["gaussian_line_executions"], + "precision": trace["precision"], "uniform_radius": trace["uniform_radius"]} + + +def main(): + caller = authenticated_caller() + seeds = caller.seed_lines() + lines = caller.precision_view(seeds, 180) + original_lane = caller.residue_lane + # The source module is private to this process. Its caller, certificates, + # transforms, CRT order and carry scan are unchanged. Restore the sole + # substituted dependency even if an endpoint check raises. + caller.residue_lane = residue_lane + try: + cases = [run_case(caller, lines, n) for n in (8193, 14592)] + finally: + caller.residue_lane = original_lane + check(caller.residue_lane is original_lane, "restored source dependency") + result = {"status": "PASS_CENTERED_GAUSSIAN_BOUNDARY", "cases": cases} + files = sorted(p for p in ROOT.iterdir() if p.is_file()) + check(len(files) == 8, "package file count") + result["sha256"] = {} + for path in files: + with path.open("rb") as stream: + raw = stream.read(1024 * 1024 + 1) + check(len(raw) <= 1024 * 1024, "receipt file capacity") + result["sha256"][path.name] = sha256(raw).hexdigest() + print(json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/centered-gaussian-residue/packing.py b/research/centered-gaussian-residue/packing.py new file mode 100644 index 0000000000..565823f9c9 --- /dev/null +++ b/research/centered-gaussian-residue/packing.py @@ -0,0 +1,81 @@ +"""Centered low-residue child. Produced by Nick Petalas. Apache-2.0.""" + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def child_bits(n, digit_bits, k): + """Attained maximum magnitude bit length at declared parent width n.""" + need(all(type(x) is int for x in (n, digit_bits, k)), "integer widths") + need(1 <= digit_bits <= 64 and 1 <= k <= digit_bits, "digit/residue width") + need(1 <= n <= 228 * digit_bits, "parent capacity") + length = (n + digit_bits - 1) // digit_bits + top = n - digit_bits * (length - 1) + slot = 2 * k - 1 + (length - 1).bit_length() + return min(k, top) + (length - 1) * slot + + +def centered_digits(values, k): + need(type(k) is int and 1 <= k <= 64, "residue width") + need(type(values) in (list, tuple) and 1 <= len(values) <= 228, "array capacity") + need(all(type(x) is int and 0 <= x < 1 << 64 for x in values), "unsigned digits") + half = 1 << (k - 1) + modulus = 2 * half + return tuple((x + half) % modulus - half for x in values) + + +def decode(packed_product, left_length, right_length, k, slot): + """Decode using the asymmetric interval, including its positive endpoint.""" + need(type(packed_product) is int, "integer product") + need(all(type(x) is int and 1 <= x <= 228 for x in (left_length, right_length)), + "decode capacity") + need(type(k) is int and 1 <= k <= 64, "residue width") + expected = 2 * k - 1 + (min(left_length, right_length) - 1).bit_length() + need(type(slot) is int and slot == expected, "signed slot width") + need(abs(packed_product).bit_length() <= 2 * k + (left_length + right_length - 2) * slot, + "product capacity") + half = 1 << (k - 1) + base = 1 << slot + coefficients = [] + remaining = packed_product + for j in range(left_length + right_length - 1): + overlap = min(left_length - 1, j) - max(0, j - right_length + 1) + 1 + lower = -overlap * half * (half - 1) + upper = overlap * half * half + need(upper - lower < base, "separated signed interval") + coefficient = lower + (remaining - lower) % base + need(coefficient <= upper, "coefficient outside signed interval") + coefficients.append(coefficient) + remaining = (remaining - coefficient) // base + need(remaining == 0, "unconsumed packed product") + return coefficients + + +def residue_lane(left, right, k): + """One nonnegative magnitude multiplication; signs and extraction are charged work.""" + a = centered_digits(left, k) + b = centered_digits(right, k) + overlap = min(len(a), len(b)) + slot = 2 * k - 1 + (overlap - 1).bit_length() + packed_a = sum(x << (j * slot) for j, x in enumerate(a)) + packed_b = sum(x << (j * slot) for j, x in enumerate(b)) + magnitude_product = abs(packed_a) * abs(packed_b) + signed_product = -magnitude_product if (packed_a < 0) != (packed_b < 0) else magnitude_product + coefficients = decode(signed_product, len(a), len(b), k, slot) + modulus = 1 << k + bill = { + "exact_child_calls": 1, "residue_bits": k, "slot_bits": slot, + "overlap": overlap, "coefficient_count": len(coefficients), + "left_child_bits": abs(packed_a).bit_length(), + "right_child_bits": abs(packed_b).bit_length(), + "left_child_bound": k + (len(a) - 1) * slot, + "right_child_bound": k + (len(b) - 1) * slot, + "signed_coefficient_lower": -overlap * (modulus // 2) * (modulus // 2 - 1), + "signed_coefficient_upper": overlap * (modulus // 2) ** 2, + "slot_capacity": 1 << slot, + } + need(bill["left_child_bits"] <= bill["left_child_bound"], "left magnitude bound") + need(bill["right_child_bits"] <= bill["right_child_bound"], "right magnitude bound") + return [x % modulus for x in coefficients], bill diff --git a/research/centered-gaussian-residue/verify.py b/research/centered-gaussian-residue/verify.py new file mode 100644 index 0000000000..d3331569d5 --- /dev/null +++ b/research/centered-gaussian-residue/verify.py @@ -0,0 +1,152 @@ +"""Exact new packing checks. Produced by Nick Petalas. Apache-2.0.""" +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path +import sys + +ROOT = Path(__file__).resolve().parent +sys.path.insert(0, str(ROOT)) +from packing import child_bits, decode, residue_lane + + +def check(condition, message): + if not condition: + raise AssertionError(message) + + +def convolution(a, b): + result = [0] * (len(a) + len(b) - 1) + for i, x in enumerate(a): + for j, y in enumerate(b): + result[i + j] += x * y + return result + + +def exhaustive(): + cases = coefficients = 0 + for k, maximum_length in ((1, 4), (2, 3), (3, 2)): + modulus = 1 << k + arrays = [a for length in range(1, maximum_length + 1) + for a in product(range(modulus), repeat=length)] + for a in arrays: + for b in arrays: + residues, bill = residue_lane(a, b, k) + expected = convolution(a, b) + check(residues == [x % modulus for x in expected], "literal residue convolution") + signed_a = tuple(x if x < modulus // 2 else x - modulus for x in a) + signed_b = tuple(x if x < modulus // 2 else x - modulus for x in b) + signed = convolution(signed_a, signed_b) + slot = bill["slot_bits"] + packed = sum(x << (j * slot) for j, x in enumerate(signed)) + check(decode(packed, len(a), len(b), k, slot) == signed, "every signed coefficient") + check(bill["exact_child_calls"] == 1, "one paid magnitude product") + cases += 1 + coefficients += len(expected) + return {"array_pairs": cases, "coefficients": coefficients} + + +def literal_size(n, digit_bits, k, original): + length = (n + digit_bits - 1) // digit_bits + base = 1 << digit_bits + digits = [(original >> (j * digit_bits)) % base for j in range(length)] + residues, bill = residue_lane(digits, [0] * length, k) + check(residues == [0] * (2 * length - 1), "zero partner") + return bill["left_child_bits"] + + +def size_checks(): + cases = inputs = 0 + for digit_bits in range(1, 5): + for n in range(1, 11): + for k in range(1, digit_bits + 1): + largest = max(literal_size(n, digit_bits, k, x) for x in range(1 << n)) + check(largest == child_bits(n, digit_bits, k), "attained small maximum") + inputs += 1 << n + cases += 1 + admitted = old_admitted = width_pairs = tail_widths = 0 + for n in range(1, 14593): + length = (n + 63) // 64 + top = n - 64 * (length - 1) + h = (length - 1).bit_length() + for k in range(1, 65): + exact = child_bits(n, 64, k) + old = min(k, top) + (length - 1) * (2 * k + h) + check(old - exact == length - 1, "slot saving") + admitted += exact < n + old_admitted += old < n + width_pairs += 1 + if n >= 29: + check(child_bits(n, 64, 28) < n, "uniform k28 tail") + tail_widths += 1 + for n, k in ((14592, 28), (8193, 28), (8193, 29), (65, 28), (29, 28)): + length = (n + 63) // 64 + top = n - 64 * (length - 1) + attainer = 1 << (64 * (length - 1) + min(k, top) - 1) + check(literal_size(n, 64, k, attainer) == child_bits(n, 64, k), "large attainer") + check(child_bits(8193, 64, 29) == 8321, "k29 boundary obstruction") + return {"small_size_cases": cases, "small_inputs": inputs, + "width_pairs": width_pairs, "admitted": admitted, + "unsigned_admitted": old_admitted, "k28_tail_widths": tail_widths, + "full_k28_bits": child_bits(14592, 64, 28)} + + +def controls(): + rejected = 0 + for a, b, k in (([], [1], 2), ([1], [], 2), ([True], [1], 2), + ([-1], [1], 2), ([1 << 64], [1], 2), ([1], [1], 0), + ([1], [1], 65), ([0] * 229, [1], 2)): + try: + residue_lane(a, b, k) + except ValueError: + rejected += 1 + else: + raise AssertionError("invalid lane accepted") + for args in ((0, 64, 28), (14593, 64, 28), (100, 0, 1), (100, 64, 65)): + try: + child_bits(*args) + except ValueError: + rejected += 1 + else: + raise AssertionError("invalid size accepted") + # All -half gives the positive half-base endpoint, which symmetric + # half-open centered extraction would turn into a negative coefficient. + signed = convolution((-2, -2), (-2, -2)) + check(signed == [4, 8, 4], "positive endpoint fixture") + check(decode(4 + 8 * 16 + 4 * 256, 2, 2, 2, 4) == signed, "asymmetric endpoint") + check(((8 + 8) % 16) - 8 != 8, "symmetric decoder must fail") + # One fewer bit puts the attainable middle coefficients -4 and +4 + # in the same residue class modulo eight. + check(convolution((-1, -1), (-2, -2))[1] == 4, "positive collision attainer") + check(convolution((-2, -2), (1, 1))[1] == -4, "negative collision attainer") + check(4 % 8 == (-4) % 8, "undersized-slot collision") + actual, _ = residue_lane((3, 0), (1, 0), 2) + check(actual == [3, 0, 0], "negative packed product") + naive = [((-1 >> (4 * j)) & 15) % 4 for j in range(3)] + check(naive != actual, "unsigned extraction must fail on negative pack") + for args in ((0, 2, 2, 2, 3), (16 ** 3, 2, 2, 2, 4)): + try: + decode(*args) + except ValueError: + rejected += 1 + else: + raise AssertionError("invalid decoder accepted") + return {"rejections": rejected, "semantic_controls": 4} + + +def receipt(): + result = {"status": "PASS_CENTERED_GAUSSIAN_RESIDUE", "claim_type": "scoped proof", + "exhaustive": exhaustive(), "sizes": size_checks(), "controls": controls()} + files = sorted(p for p in ROOT.iterdir() if p.is_file()) + check(len(files) == 8, "package file count") + result["sha256"] = {} + for path in files: + with path.open("rb") as stream: + raw = stream.read(1024 * 1024 + 1) + check(len(raw) <= 1024 * 1024, "receipt file capacity") + result["sha256"][path.name] = sha256(raw).hexdigest() + print(json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + receipt()