[petalas]

Summary

Eliminate 11,470 interval exponential evaluations in the complete PR2313 Gaussian recovery replay while preserving every computed interval endpoint and all scientific output. Claim type: scoped implementation-preservation proof, exact work reduction and finite conformance evidence. No runtime improvement or new kappa is established.

compute E[k] normally for 0 <= k <= floor(t/2)
fill E[k,a] = E[t-k,(-a) mod s] for the remaining rows
execute the unchanged complete integer-recovery verifier

The new proof includes the actual finite truncation, per-summand outward rounding and final tail unit. The source-bound adapter changes only expansion setup. It computes 76 rows directly and reflects 60; all 136 rows remain available to the eight completed setup paths. Reflection is classical; the exact interval-preserving substitution and work reduction are the new contribution.

This contribution was produced by Nick Petalas. Credit Mason Hale / PR2313 for the backend, interval arithmetic, numerical/recovery proof and controls; Cinna Davis / PR2298 for its caller question; and the unchanged Harvey–van der Hoeven, Gaussian, CRT, Neumann-rounding and numerical lineage in the retained NOTICE. Predecessor mathematics is cited, not an audit deliverable.

Proof, package, advance CLAIM, scope/timing finding.

Evidence

• Before: 26,464 Gaussian-module exponential calls in the complete replay. After: 14,994, with identical retained scientific output and all 289 integer-product fixtures executed on each side.
• New checks enumerate 5,016 reflected row pairs and 43,223 exact term bijections, compare all 269 interval entries in five fixtures, and exercise four semantic and four source-layout/mode controls.
• Normal and optimized direct replays pass with identical JSON receipts in 53.26 s and 51.77 s. The registered two-command package replay passes in 104.61 s total. Every registered check is below its 290-second bound locally.
• Committed-byte, mode and declared source-history checks pass for all 22 package/input files at 3376b28a77491fd3d11b0e93724025211c3afd6b. The official committed export and input-coverage/integrity check also pass.
• Five alternating fresh-process runs per side all succeed and agree on scientific stdout. The complete-command median difference is smaller than the observed variation, so timing is inconclusive. The generated measurement retains all samples, work counts, environment and executable/source bindings. A separate profile identifies matrix/FFT execution as the dominant cost. Profiling is excluded from samples.

Reproduce from the repository root, CPython 3.12.15, standard library only:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/gaussian-expansion-reflection/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/gaussian-expansion-reflection/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/gaussian-expansion-reflection
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/gaussian-expansion-reflection --check-source-history --check-modes

Other machines can substitute their CPython 3.12 executable. Expected statuses are PASS_GAUSSIAN_EXPANSION_REFLECTION, PASS_REGISTERED_RESEARCH_PACKAGE and PASS_RESEARCH_COMMIT_BYTES. All generated verification reports bind the executable sources and manifests; no mathematical receipt is handwritten.

Limitations and unrun obligations

This is an isolated coefficient-setup module for the pinned dense reference backend. It supplies no fast sequential backend, physical movement/cleanup tariff, new precision policy, native/caller admission or compiler/stock/outer theorem. All five inherited framework assumptions remain. The selected frontier is unchanged. The universal preservation proof is written, with finite executable corroboration; independent human and formal proof-kernel review are unclaimed.

Selected cold replay, physical native/tape execution, Lean and Docker were unrun and are outside this claim. The export's integrity was checked; an additional exported scientific replay was not run. No required local check was deferred to CI. The initial complete-runtime prediction is narrowed to exact work reduction, as recorded in the finding.

Open next questions

Can an actual fixed-tape Gaussian coefficient producer exploit the reflection with a favorable complete movement and cleanup bill? Start by binding one emitted table and its sequential order, then price the reflected reads, writes, head returns and cleanup. That physical producer and tariff are missing here. Optimization stopped at this first verified work reduction; no follow-up is reserved.

Related open work

The refreshed exact-backend search found no open PR studying PR2313 periodic expansion setup. Nearby Gaussian work has different contracts:

• PR6404 gives a determinant/rank obstruction for a linearly truncated Gaussian Schur boundary; this package changes periodic expansion coefficient generation and computes no cross-rim determinant.

• PR6405 gives a sharp sign range for linearly truncated real Gaussian kernels; this package makes no sign-range or Schur-fill claim. No additional computations checked either contribution.

• PR6412 gives an adjacent-modulus remainder correction tree at a different arithmetic stage; it changes neither this Gaussian expansion matrix nor its setup counts. No common numerical output is compared.

Completion refresh inspected the fourteen other account PRs created since the advance CLAIM. No additional exact-backend overlap or conflicting computed quantity was found. Searches cover retained public evidence and the live claim/PR scope, not unpublished work or arbitrary historical diffs.

CI notes

Both hosted checks passed at exact head 3376b28a77491fd3d11b0e93724025211c3afd6b in run 41529237574: plan and replay (research/gaussian-expansion-reflection). The completed checks were read once; separate run metadata confirms successful completion at this head.

Hosted replay certifies the registered normal/optimized conformance and complete retained caller checks, plus package/input validation. The universal preservation argument remains a written proof. All required local checks listed above also pass. No CI failure remains, and no runtime improvement, new kappa, supplier admission, independent human review or formal proof-kernel acceptance is implied.

Related open work was refreshed against this account's open PRs created since the CLAIM. Fourteen other contributions were inspected; no additional PR studies the exact periodic-expansion setup quantity, and no common computed number disagrees. No extra computation checked another contribution.

Merge Danger

Door: two-way; the isolated package can be reverted.

Blast Radius: isolated. Ten new package files; no shared implementation, predecessor source, pinned evidence or selected-frontier file is changed.