Admit uniform 28-bit Gaussian residues with centered packing (no κ)

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<k the top digit never reaches a, and
+its largest possible bit length is t. This proves the formula for L=1.
+
+Suppose L>=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 t<k, the top digit is nonnegative and at most 2^t-1. Also beta>a+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<n. Therefore every declared width
+29<=n<=14592 has a strictly smaller k=28 child. The old fixed uniform
+tail used k=27; its k=28 layout fails at n=8193, as already proved in
+PR3926. This is a changed layout, not a correction of that exclusion.
+
+At n=14592, L=228 and t=64, the new k=28 child has sharp maximum
+28+227*63=14329 bits. The cited unsigned bound is 14556 bits.
+At n=8193, L=129 and t=1, the new sharp bound is 8065 bits.
+
+The new layout does not permit a uniform k=29 tail: at n=8193 its
+sharp bound is 1+128*65=8321 bits, which exceeds the parent width.
+The formula increases with k, so every k>=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.

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.