diff --git a/research/gaussian-expansion-reflection/BENCHMARK.json b/research/gaussian-expansion-reflection/BENCHMARK.json new file mode 100644 index 0000000000..43311bd671 --- /dev/null +++ b/research/gaussian-expansion-reflection/BENCHMARK.json @@ -0,0 +1,181 @@ +{ + "bindings": { + "SOURCES.json": "b04619c7852aa7f209bad196b2618e621ce27de1561b062572e088d842b823eb", + "VERIFY.json": "a673fb74b7176a46fc46740aacb9e3a42ad4b10304b67cdc054b83fbf6413468", + "adapter.py": "0092de2cccf46468afe11b366f74a89d7631fc54e1aab4a858e016ad5b0b2a05", + "benchmark.py": "c16b28576c2c75ebf29ad7efa7947f39277837a9c7ccfbe53a03286170585965", + "run.py": "f5736d55b939bec53b39a0c23cca009b08cfcf9c18dd43a5959bf87cde3a7075", + "verify.py": "d4da85fe08928524e45944f3490e3c7fe83d882f9f927ad1f7a8bd672c4917a1" + }, + "environment": { + "initial_load": [ + 5.16064453125, + 7.3486328125, + 5.09033203125 + ], + "logical_cpus": 18, + "platform": "macOS-27.0.1-arm64-arm-64bit", + "python": "3.12.15 (main, Oct 14 2026, 00:55:37) [Clang 23.1.3 ]" + }, + "errors": 0, + "records": [ + { + "counts": { + "computed_rows": 0, + "constructors": 0, + "exp_negative_calls": 26464, + "expansion_terms": 0, + "reflected_rows": 0 + }, + "mode": "baseline", + "returncode": 0, + "seconds": 26.577768749790266, + "stdout_sha256": "76cc0204268ac88e4819865c26be01ef7ded9bf96859a6ae805ff053c326cab6" + }, + { + "counts": { + "computed_rows": 76, + "constructors": 8, + "exp_negative_calls": 14994, + "expansion_terms": 14474, + "reflected_rows": 60 + }, + "mode": "reflected", + "returncode": 0, + "seconds": 24.81019241688773, + "stdout_sha256": "76cc0204268ac88e4819865c26be01ef7ded9bf96859a6ae805ff053c326cab6" + }, + { + "counts": { + "computed_rows": 0, + "constructors": 0, + "exp_negative_calls": 26464, + "expansion_terms": 0, + "reflected_rows": 0 + }, + "mode": "baseline", + "returncode": 0, + "seconds": 25.890081041958183, + "stdout_sha256": "76cc0204268ac88e4819865c26be01ef7ded9bf96859a6ae805ff053c326cab6" + }, + { + "counts": { + "computed_rows": 76, + "constructors": 8, + "exp_negative_calls": 14994, + "expansion_terms": 14474, + "reflected_rows": 60 + }, + "mode": "reflected", + "returncode": 0, + "seconds": 26.06416704203002, + "stdout_sha256": "76cc0204268ac88e4819865c26be01ef7ded9bf96859a6ae805ff053c326cab6" + }, + { + "counts": { + "computed_rows": 0, + "constructors": 0, + "exp_negative_calls": 26464, + "expansion_terms": 0, + "reflected_rows": 0 + }, + "mode": "baseline", + "returncode": 0, + "seconds": 26.234504041960463, + "stdout_sha256": "76cc0204268ac88e4819865c26be01ef7ded9bf96859a6ae805ff053c326cab6" + }, + { + "counts": { + "computed_rows": 76, + "constructors": 8, + "exp_negative_calls": 14994, + "expansion_terms": 14474, + "reflected_rows": 60 + }, + "mode": "reflected", + "returncode": 0, + "seconds": 26.03246737504378, + "stdout_sha256": "76cc0204268ac88e4819865c26be01ef7ded9bf96859a6ae805ff053c326cab6" + }, + { + "counts": { + "computed_rows": 0, + "constructors": 0, + "exp_negative_calls": 26464, + "expansion_terms": 0, + "reflected_rows": 0 + }, + "mode": "baseline", + "returncode": 0, + "seconds": 27.549147834070027, + "stdout_sha256": "76cc0204268ac88e4819865c26be01ef7ded9bf96859a6ae805ff053c326cab6" + }, + { + "counts": { + "computed_rows": 76, + "constructors": 8, + "exp_negative_calls": 14994, + "expansion_terms": 14474, + "reflected_rows": 60 + }, + "mode": "reflected", + "returncode": 0, + "seconds": 26.07967729214579, + "stdout_sha256": "76cc0204268ac88e4819865c26be01ef7ded9bf96859a6ae805ff053c326cab6" + }, + { + "counts": { + "computed_rows": 0, + "constructors": 0, + "exp_negative_calls": 26464, + "expansion_terms": 0, + "reflected_rows": 0 + }, + "mode": "baseline", + "returncode": 0, + "seconds": 25.931223541032523, + "stdout_sha256": "76cc0204268ac88e4819865c26be01ef7ded9bf96859a6ae805ff053c326cab6" + }, + { + "counts": { + "computed_rows": 76, + "constructors": 8, + "exp_negative_calls": 14994, + "expansion_terms": 14474, + "reflected_rows": 60 + }, + "mode": "reflected", + "returncode": 0, + "seconds": 25.74069912498817, + "stdout_sha256": "76cc0204268ac88e4819865c26be01ef7ded9bf96859a6ae805ff053c326cab6" + } + ], + "status": "PASS_GAUSSIAN_REFLECTION_BENCHMARK", + "summary": { + "baseline": { + "counts": { + "computed_rows": 0, + "constructors": 0, + "exp_negative_calls": 26464, + "expansion_terms": 0, + "reflected_rows": 0 + }, + "maximum_seconds": 27.549147834070027, + "median_seconds": 26.234504041960463, + "minimum_seconds": 25.890081041958183 + }, + "reduction_percent": 0.7701181108418775, + "reflected": { + "counts": { + "computed_rows": 76, + "constructors": 8, + "exp_negative_calls": 14994, + "expansion_terms": 14474, + "reflected_rows": 60 + }, + "maximum_seconds": 26.07967729214579, + "median_seconds": 26.03246737504378, + "minimum_seconds": 24.81019241688773 + } + } +} diff --git a/research/gaussian-expansion-reflection/PROOF.md b/research/gaussian-expansion-reflection/PROOF.md new file mode 100644 index 0000000000..e90153edf6 --- /dev/null +++ b/research/gaussian-expansion-reflection/PROOF.md @@ -0,0 +1,111 @@ +# Exact reflection of the truncated expansion + +This scoped implementation-preservation proof was produced by Nick Petalas. +Reflection of an even Gaussian is classical. The new step is an exact +substitution in Mason Hale's PR2313 interval backend, including its finite +truncation, per-summand rounding and outward tail units. The predecessor's +Gaussian transform, recovery theorem and controls are cited premises. + +Let positive integers `s0` be fixed. The pinned constructor uses + +``` +c_k = s*k/t +J_k = [floor(c_k)-r, ceil(c_k)+r] intersect Z +E[k,a] = sum_{j in J_k, j mod s = a} + exp_negative(pi * (j-c_k)^2 / alpha^2) / (2*alpha), +``` + +then adds one working-grid unit to each upper endpoint. Every expression +above is evaluated by the pinned rational/dyadic implementation. `E` is +the interval matrix, rather than merely the underlying exact real operator. + +For `1<=k s-j` is a bijection from the complete finite interval `J_k` +to `J_k'`. It preserves the exact rational squared argument. Consequently +the interval exponential receives identical integer endpoints and working +precision, and its division by the same positive integer is identical. +The two sums have exactly the same multiset of interval summands in +corresponding cyclic positions. + +The pinned interval addition adds lower endpoints and upper endpoints as +integers, without intermediate rescaling. It is therefore exactly associative +and commutative. Reversing the summation order changes neither endpoint. +Both rows receive the same final upper-endpoint unit. Hence + +``` +E[t-k,a] = E[k,(-a) mod s] +``` + +as equality of the stored `(lo,hi,bits)` triples. This proves preservation +of the actual computed enclosures, without appealing to floating-point +agreement or assuming that reflected intervals merely overlap. + +Compute rows `0,...,floor(t/2)` by the original formula. For every later +row, copy its partner with cyclic column reversal. Row zero is computed +directly. If `t` is even, the self-paired middle row is also computed +directly. This constructs every matrix entry and skips no downstream work. +The proof applies to odd `t` and noncoprime `s,t` too; the retained caller +uses its stricter coprime, power-of-two-target domain. + +The replacement allocates a fresh list for every row. It may reuse interval +objects across rows because the pinned `Interval` class is a frozen +dataclass and every arithmetic operation returns a new object. The +unchanged consumers read the expansion matrix and never mutate its +interval objects. All later constructor attributes, norm bounds, operator +certificates, rounded calls, inverse corrections and recovered products +therefore have their original values. + +## Exact work reduction + +The number of directly evaluated rows falls from `t` to `floor(t/2)+1`. +When `gcd(s,t)=1`, only `c_0` is integral. Its finite sum has `2r+1` +terms, while every other row has `2r+2`. Accordingly, + +``` +original exponentials = t*(2r+2)-1 +reflected exponentials = (floor(t/2)+1)*(2r+2)-1 +saved exponentials = (ceil(t/2)-1)*(2r+2). +``` + +The copy work is `(ceil(t/2)-1)*s` interval references. Matrix storage +remains `s*t` entries; there is no retained cross-invocation cache. +For the first source fixture `(s,t,alpha,b)=(5,8,5,448)`, the original +radius is `r=115`; exactly 696 expansion exponential calls disappear. +The complete retained replay finishes eight constructors and saves 11,470 +such calls. Counts from the instrumented complete executions corroborate +these formulas. This is a work-count reduction, not a fixed-tape tariff. + +## Binding and evidence + +`adapter.py` authenticates twelve live files before loading the captured +Python source bytes. In the reflected mode, one source-bound AST edit +replaces the expansion allocation and its adjacent row loop by the new +builder. The original radius, tail guard, `self.expansion` consumer, +remaining constructor and verifier stay in place. The baseline loads the +original AST without this edit. Both modes count calls through the same +exponential wrapper, execute the complete retained verifier, and require +its original scientific receipt. + +`verify.py` checks rational term bijections and literal interval equality +on additional finite fixtures, including odd targets and noncoprime +geometry. Mutation controls distinguish wrong cyclic reversal, wrong row +selection and a missing outward unit. Frozen-object and source-layout +controls check the implementation assumptions. The complete baseline and +replacement commands both execute all 289 predecessor product fixtures. +These are conformance checks of a new substitution, not an independent +audit or a new acceptance claim for the predecessor mathematics. + +The universal preservation statement rests on the argument above. It is +not a proof-kernel theorem. Timing evidence is local to the declared +complete command and machine; it supplies no new multiplication exponent, +physical tape implementation, native admission or framework assumption. diff --git a/research/gaussian-expansion-reflection/README.md b/research/gaussian-expansion-reflection/README.md new file mode 100644 index 0000000000..64abf62bb1 --- /dev/null +++ b/research/gaussian-expansion-reflection/README.md @@ -0,0 +1,160 @@ +# Exact reflection reuse in periodic Gaussian setup + +The complete PR2313 Gaussian recovery replay eliminates **11,470 interval +exponential evaluations** by constructing one row of each reflected pair. +Every stored interval endpoint and the complete scientific output remain +identical. The replacement runs all 289 retained integer-product fixtures; +it changes the coefficient setup and preserves the original numerical path. + +Claim type: scoped implementation-preservation proof, exact operation +reduction and finite conformance evidence. The measured complete-command +runtime is **inconclusive**, as recorded in [BENCHMARK.json](BENCHMARK.json). This is a +verification-engineering side result. No new kappa, supplier admission or +selected-frontier change is claimed. + +This contribution was produced by Nick Petalas. Apache-2.0. + +## What changes + +For source length `s`, target length `t` and the original finite radius, +the actual expansion matrix satisfies the exact interval identity + +``` +E[t-k,a] = E[k,(-a) mod s], 1 <= k < t. +``` + +The new builder evaluates rows `0,...,floor(t/2)` and fills the remaining +rows by cyclic reflection. It retains the original radius, finite summands, +per-term outward division and one-unit upper tail enlargement. The proof +in [PROOF.md](PROOF.md) uses an exact bijection of the truncated summands; +it establishes equality of the computed dyadic intervals, rather than +agreement only of the underlying real Gaussian. + +For coprime `s,t` and radius `r`, the exact saved exponential count is +`(ceil(t/2)-1)*(2r+2)`. The first source fixture `(5,8,5,448)` saves 696. +The complete command directly computes 76 rows and reflects 60, retaining +all 136 rows needed by its eight completed setup paths. Gaussian-module +exponential calls fall from 26,464 to 14,994. Matrix storage remains `s*t` +entries, and no cross-invocation cache exists. +The baseline row/constructor adapter counters are zero because it executes +the original loop; the common exponential counter measures both modes. + +[adapter.py](adapter.py) authenticates twelve inputs, loads their captured +source bytes and substitutes only the expansion allocation/row loop in +the pinned constructor. It leaves the remaining constructor and complete +verifier in place. The baseline mode loads the original constructor. +Every original conformance check and scientific receipt comparison executes +in both modes. Frozen predecessor files and their credit are unchanged. + +## Evidence and reproduction + +From the repository root, with CPython 3.12 and the standard library: + +```sh +/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 +``` + +Other machines may substitute their CPython 3.12 executable. The direct +verifier prints `PASS_GAUSSIAN_EXPANSION_REFLECTION` in a generated JSON +report bound to the executable sources and manifest. Default replay writes +nothing. The registered normal and optimized checks execute the same +explicit predicates and compare the same retained scientific output. + +New conformance checks cover 5,016 reflected row pairs and 43,223 exact +term bijections; literal interval comparison covers 269 entries in five +fixtures, including an odd target and noncoprime geometry. Four semantic +controls detect wrong cyclic reversal, wrong row, missing outward tail +unit and mutable interval objects. Four additional controls reject changed +source layouts and an unknown execution mode. These checks concern the +new substitution. They are not an independent audit of PR2313's numerical +or uniform-recovery proof. + +Run either complete caller or repeat the measurement outside the checkout: + +```sh +python3.12 -I -W error -B research/gaussian-expansion-reflection/run.py --mode baseline +python3.12 -I -W error -B research/gaussian-expansion-reflection/run.py --mode reflected +python3.12 -I -W error -B research/gaussian-expansion-reflection/benchmark.py --output /absolute/scratch/new-benchmark.json +``` + +The harness refuses an existing output or a destination inside the checkout. +It times five alternating fresh subprocesses per side, including startup, +source authentication, all setup and the complete retained replay. All +ten exit codes and scientific stdout hashes must agree. Timings are +observations, not CI pass conditions. The verifier authenticates their +source bindings and recomputes their medians and ranges. + +The measured complete-replay medians are 26.234504 s for the baseline and +26.032467 s for the replacement. Baseline range is 25.890081–27.549148 s; +replacement range is 24.810192–26.079677 s. The 0.202037 s median difference +is smaller than the observed run variation: **no runtime improvement is +established**. All ten complete executions succeed with identical scientific +stdout. The exact operation reduction is the delivered improvement; the +initial runtime prediction was narrowed in the Discussion finding. + +The measurement uses CPython 3.12.15 on macOS arm64 with 18 logical CPUs. +Initial load averages are 5.16, 7.35 and 5.09. Other work could run +concurrently; alternating subprocesses expose both sides to that load. + +A separate baseline profile identifies the limiter: the rounded matrix and +FFT executions dominate; the ten constructor calls take about 9.1% of the +profiled complete runtime. The coefficient replacement can improve only +part of this setup. The profile is excluded from timing samples. Reproduce +it with `python3.12 -I -B -m cProfile -o /absolute/scratch/baseline.pstats +research/certified-gaussian-recovery/verify.py`. + +## Scope and code discipline + +The proof covers the stated exact expansion formula and its finite +truncation for all positive integer geometries. The executable adapter is +source-bound to PR2313 and its existing caller. A future source edit must +update the pins and be assessed again. No fast sequential Gaussian backend, +physical movement/cleanup tariff, new precision policy, selected cold replay, +native operator proof, compiler closure, stock or outer theorem is supplied. +The five inherited framework assumptions retain their status. Independent +human and formal proof-kernel review are unclaimed. + +New loops have bounds from `s,t,r` or fixed verifier families. Every new +function is below 60 lines. The new builder has no recursion. The frozen +predecessor's recursive FFT and finite numerical iteration remain unchanged. +Python allocation and its immutable integer/interval objects are a managed +runtime deviation from fixed allocation: the matrix has exactly `s*t` +entries and the builder retains no query history. Captured-source compilation +and a partial function are bounded dynamic-loading deviations restricted to +three authenticated modules and the one declared constructor substitution. +All loaded modules, arguments and import paths are restored on every exit. +Measurement children have a 290-second bound. Warning-strict normal and +optimized replay provide the interpreted diagnostics. + +## Open next questions + +Can an actual fixed-tape Gaussian coefficient producer exploit this +reflection with a favorable complete movement and cleanup bill? Start by +binding one emitted table and its sequential order, then price reflected +reads, writes, head returns and cleanup. The physical producer, ordering +and tariff are missing here. No further optimization is reserved. + +## Credit and overlap + +Mason Hale / mason-hale's [PR2313](https://github.com/CrocSwap/integer-mult-bounds/pull/2313) +supplies the completed Gaussian backend, interval arithmetic, operator and +uniform integer-recovery certificates, fixtures and controls. Cinna Davis's +PR2298 supplies its caller question. The retained Harvey–van der Hoeven, +Gaussian, CRT, Neumann-rounding and numerical lineage remains credited in +the unchanged predecessor [NOTICE](../certified-gaussian-recovery/NOTICE.md). +Reflection symmetry is classical; priority for that identity is unclaimed. +The new implementation, exact preservation argument and operation reduction +are the contribution here. + +Base: canonical main `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority +revision 8. The drawn `uniform-transfer-audit` card is explicitly changed +to this original verification-engineering question in [TASK.json](TASK.json). +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19360807) +preceded implementation. Entry searches checked live claims and local +reservations, open PRs, recent account work, merged titles/bodies and main +README terms. The cached overlap search has incomplete sparse local coverage; +unpublished work and arbitrary historical diffs remain limits. Predecessor +science and selected-frontier files are untouched. diff --git a/research/gaussian-expansion-reflection/SOURCES.json b/research/gaussian-expansion-reflection/SOURCES.json new file mode 100644 index 0000000000..e35918f46b --- /dev/null +++ b/research/gaussian-expansion-reflection/SOURCES.json @@ -0,0 +1,90 @@ +{ + "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/certified-gaussian-recovery/gaussian.py", + "usage": "input", + "git_blob": "ac444a242caba128754615227ad6057545822a34", + "sha256": "572c2a88b12dd6e9f8fe4387ba2f8fa58e9bc01c6a4e01d2945be4d4277c6d3e" + }, + { + "path": "research/certified-gaussian-recovery/intervals.py", + "usage": "input", + "git_blob": "91d458865aa026bdf0d59653a4ecbfe3a178ecbc", + "sha256": "159d2a7d32a8cc7c8f56632a8ef127308b984a0a6753c9d6bdccacc6e7d6d4df" + }, + { + "path": "research/certified-gaussian-recovery/pipeline.py", + "usage": "input", + "git_blob": "8b5fbc26b38fce5f917d214f987eda8a55d34bd1", + "sha256": "3cceae8665d06f72275258acf8e2bc17b816a0bde45d8f109aa7364a30861728" + }, + { + "path": "research/certified-gaussian-recovery/verify.py", + "usage": "input", + "git_blob": "f88d26791c35955f1c2898dce346e59827947037", + "sha256": "2c6ded7940b5ec41d60774a0c2ffbb01899446529a6dc3b59acd67901c198014" + }, + { + "path": "research/certified-gaussian-recovery/RESULT.json", + "usage": "input", + "git_blob": "3756e9c9256439e340fc2a5ac0099161cb49681a", + "sha256": "7b5bc593f2f633b1b84198a590fe0dcf124c037a3b785d82d8aeb77f81f236df" + }, + { + "path": "research/certified-gaussian-recovery/SOURCES.json", + "usage": "input", + "git_blob": "b7a3ab865a4936026140824e643beca213794c29", + "sha256": "e679b7d6534b46f8f975dd2d4ecadc50ca67fee34d863f0bb59ef170fe39a08b" + }, + { + "path": "research/certified-gaussian-recovery/README.md", + "usage": "input", + "git_blob": "2eab8b4ae48c81b195a682e44a6ea69bfa18f4f9", + "sha256": "eb8d2f13c9482fe6b556bd115cec9006a16d843324a9cbfa6cf8b3adf1704c06" + }, + { + "path": "research/certified-gaussian-recovery/PROOF.md", + "usage": "input", + "git_blob": "9dace009004a4336d6ce57764c255190fbf87e64", + "sha256": "65480dd23fb1aae314365aeea4aacbc146e160e5c8a7a4ac4f602f22ae4581de" + }, + { + "path": "research/certified-gaussian-recovery/NOTICE.md", + "usage": "input", + "git_blob": "5e3269b5afe5e11f044ffae45216c4731b42c7af", + "sha256": "10acae9e78402ca70c6afd0e8d6da8fefc0da519c646cf43d93f923aba85b86d" + }, + { + "path": "research/neumann-rounding-audit/README.md", + "usage": "input", + "git_blob": "6c6c0899fc00144c2ba97f1760ecd50a22ba6d57", + "sha256": "332a166718e3671b0db06c8cb73ca7673ee0224ac2645eea61972041d50a110e" + }, + { + "path": "upstream/build/sections/07-resampling.tex", + "usage": "input", + "git_blob": "256243bf9416baefb82bf9203f80215b9ebe28f2", + "sha256": "8a6b91670f9163afb54892489fa2210c77fe1b058f0325ec7d18b44b94be6e2c" + }, + { + "path": "upstream/build/sections/08-assembly.tex", + "usage": "input", + "git_blob": "337810a1d9a58a2ecf14123420923c039ba322a6", + "sha256": "763d7945b1e1ec4ebae9b799bcefcc45fa9bae6e2ffad799868a9c3d513dbd4a" + } + ] +} diff --git a/research/gaussian-expansion-reflection/TASK.json b/research/gaussian-expansion-reflection/TASK.json new file mode 100644 index 0000000000..b8639826f7 --- /dev/null +++ b/research/gaussian-expansion-reflection/TASK.json @@ -0,0 +1,89 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "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" + ], + "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": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "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": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "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": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "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": "Exact interval-preserving reflection reuse in PR2313 periodic Gaussian expansion setup, with complete-replay conformance and timing evidence.", + "scope_change_reason": "This changes the audit card to a newly posed implementation-preservation question at the Gaussian coefficient-generation boundary; no inherited all-size assumption is claimed discharged.", + "bottleneck_link": "This reduces coefficient-generation exponential calls in an executed Gaussian/recovery reference without weakening its output. No runtime improvement or gain in the binding complex supplier is claimed.", + "budget_minutes": 60, + "stop_rule": "Ship the first strict verified operation reduction; measure the complete command once with five alternating runs per side and make no further optimization.", + "outcome": "completed", + "evidence": "PROOF.md; adapter.py; verify.py; generated BENCHMARK.json; complete retained 289-product replay in both modes. Exact exponential reduction: 11470. Five alternating complete timings per side are inconclusive; no runtime improvement is claimed.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can one actual fixed-tape Gaussian coefficient producer exploit the same reflection with a favorable complete movement and cleanup bill?", + "why_it_matters": "The current gain concerns a dense reference implementation and cannot reduce the physical supplier invoice by itself.", + "first_step": "Bind one emitted coefficient table and its sequential order, then price the reflected read, write, head return and cleanup operations.", + "blocked_by": "No fixed-tape producer, coefficient order or movement tariff is implemented here." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19360807", + "predecessor": { + "pull_request": 2313, + "author": "mason-hale", + "package": "research/certified-gaussian-recovery" + } +} diff --git a/research/gaussian-expansion-reflection/VERIFY.json b/research/gaussian-expansion-reflection/VERIFY.json new file mode 100644 index 0000000000..a1dc0327d5 --- /dev/null +++ b/research/gaussian-expansion-reflection/VERIFY.json @@ -0,0 +1,47 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/certified-gaussian-recovery/gaussian.py", + "research/certified-gaussian-recovery/intervals.py", + "research/certified-gaussian-recovery/pipeline.py", + "research/certified-gaussian-recovery/verify.py", + "research/certified-gaussian-recovery/RESULT.json", + "research/certified-gaussian-recovery/SOURCES.json", + "research/certified-gaussian-recovery/README.md", + "research/certified-gaussian-recovery/PROOF.md", + "research/certified-gaussian-recovery/NOTICE.md", + "research/neumann-rounding-audit/README.md", + "upstream/build/sections/07-resampling.tex", + "upstream/build/sections/08-assembly.tex" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 290, + "checks": "Exact reflected term bijections, identical interval endpoints, semantic rejection controls, full unchanged 289-product replay on both implementations and measurement bindings." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 290, + "checks": "Same reflection conformance, complete caller and evidence checks with assertions disabled." + } + ] +} diff --git a/research/gaussian-expansion-reflection/adapter.py b/research/gaussian-expansion-reflection/adapter.py new file mode 100644 index 0000000000..2d7c24788b --- /dev/null +++ b/research/gaussian-expansion-reflection/adapter.py @@ -0,0 +1,143 @@ +"""Exact reflection reuse for the pinned periodic Gaussian expansion. + +Produced by Nick Petalas. Apache-2.0. +""" +import ast +from contextlib import contextmanager, redirect_stdout +from fractions import Fraction +from functools import partial +import hashlib +from io import StringIO +import json +from pathlib import Path +import sys +from types import ModuleType + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parent.parent +SOURCE = ROOT / "research/certified-gaussian-recovery" +NAMES = ("intervals", "gaussian", "pipeline") + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def authenticated_sources(): + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + rows = [r for r in manifest["files"] if r["usage"] == "input"] + require(len(rows) == 12, "exact twelve-input closure") + captured = {} + for row in rows: + path = ROOT / row["path"] + data = path.read_bytes() + require(hashlib.sha256(data).hexdigest() == row["sha256"], + "source drift: " + row["path"]) + captured[row["path"]] = data + return captured + + +def reflected_expansion(module, counts, s, t, alpha, bits, radius): + """Return the same integer interval endpoints as the complete row loop.""" + require(2 <= s < t and alpha >= 2 and bits > 0 and radius > 0, + "positive expansion geometry") + out = module.zeros(t, s, bits) + pi = module.pi_interval(bits) + for k in range(t // 2 + 1): + center = Fraction(s * k, t) + left = center.numerator // center.denominator - radius + right = module.ceildiv(center.numerator, center.denominator) + radius + for j in range(left, right + 1): + x = pi * ((Fraction(j) - center) ** 2 / alpha ** 2) + out[k][j % s] += module.exp_negative(x) / (2 * alpha) + counts["expansion_terms"] += 1 + out[k] = [module.Interval(x.lo, x.hi + 1, bits) for x in out[k]] + counts["computed_rows"] += 1 + for k in range(t // 2 + 1, t): + out[k] = [out[t - k][(-j) % s] for j in range(s)] + counts["reflected_rows"] += 1 + counts["constructors"] += 1 + return out + + +def replace_expansion(tree): + classes = [n for n in tree.body if isinstance(n, ast.ClassDef) + and n.name == "GaussianLine"] + require(len(classes) == 1, "one pinned GaussianLine") + inits = [n for n in classes[0].body if isinstance(n, ast.FunctionDef) + and n.name == "__init__"] + require(len(inits) == 1, "one pinned constructor") + body = inits[0].body + locations = [i for i, n in enumerate(body) if isinstance(n, ast.Assign) + and len(n.targets) == 1 and isinstance(n.targets[0], ast.Name) + and n.targets[0].id == "expansion"] + require(len(locations) == 1, "one expansion allocation") + index = locations[0] + require(isinstance(body[index + 1], ast.For), "adjacent complete row loop") + following = body[index + 2] + require(isinstance(following, ast.Assign) + and ast.unparse(following.targets[0]) == "self.expansion", + "unchanged expansion consumer") + replacement = ast.parse( + "expansion = _reflected_expansion(s, t, alpha, bits, radius)").body[0] + body[index:index + 2] = [ast.copy_location(replacement, body[index])] + return ast.fix_missing_locations(tree) + + +def load_module(name, data, reflected, counts): + module = ModuleType(name) + module.__file__ = str(SOURCE / (name + ".py")) + sys.modules[name] = module + tree = ast.parse(data, filename=module.__file__) + if name == "gaussian" and reflected: + tree = replace_expansion(tree) + module._reflected_expansion = partial(reflected_expansion, module, counts) + exec(compile(tree, module.__file__, "exec"), module.__dict__) + return module + + +@contextmanager +def runtime(mode): + require(mode in ("baseline", "reflected"), "known execution mode") + captured = authenticated_sources() + saved = {name: sys.modules.get(name) for name in NAMES} + old_path, old_argv = sys.path[:], sys.argv[:] + counts = dict.fromkeys(("exp_negative_calls", "expansion_terms", + "computed_rows", "reflected_rows", "constructors"), 0) + try: + modules = {} + for name in NAMES: + path = "research/certified-gaussian-recovery/" + name + ".py" + modules[name] = load_module(name, captured[path], mode == "reflected", counts) + original = modules["gaussian"].exp_negative + + def counted_exponential(value): + counts["exp_negative_calls"] += 1 + return original(value) + + modules["gaussian"].exp_negative = counted_exponential + yield modules, captured, counts + finally: + sys.path[:] = old_path + sys.argv[:] = old_argv + for name, previous in saved.items(): + if previous is None: + sys.modules.pop(name, None) + else: + sys.modules[name] = previous + + +def complete_replay(mode): + with runtime(mode) as (_, captured, counts): + path = "research/certified-gaussian-recovery/verify.py" + verifier = ModuleType("retained_gaussian_verifier") + verifier.__file__ = str(ROOT / path) + exec(compile(captured[path], verifier.__file__, "exec"), verifier.__dict__) + sys.argv[:] = [verifier.__file__] + output = StringIO() + with redirect_stdout(output): + verifier.main() + require(output.getvalue().startswith("PASS_CERTIFIED_GAUSSIAN_RECOVERY "), + "complete retained replay succeeded") + return output.getvalue(), dict(counts) diff --git a/research/gaussian-expansion-reflection/benchmark.py b/research/gaussian-expansion-reflection/benchmark.py new file mode 100644 index 0000000000..fe728d83b2 --- /dev/null +++ b/research/gaussian-expansion-reflection/benchmark.py @@ -0,0 +1,77 @@ +"""Measure complete fresh-process replays; author evidence outside the checkout.""" +import argparse +import hashlib +import json +import os +from pathlib import Path +import platform +import statistics +import subprocess +import sys +import time + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parent.parent + + +def bindings(): + names = ("adapter.py", "run.py", "verify.py", "benchmark.py", "SOURCES.json", "VERIFY.json") + return {name: hashlib.sha256((PACKAGE / name).read_bytes()).hexdigest() for name in names} + + +def sample(mode): + command = [sys.executable, "-I", "-W", "error", "-B", str(PACKAGE / "run.py"), "--mode", mode] + started = time.perf_counter() + result = subprocess.run(command, cwd=ROOT, capture_output=True, timeout=290, check=False) + seconds = time.perf_counter() - started + if result.returncode != 0: + raise ValueError("complete replay failed: " + result.stderr.decode()) + counts = json.loads(result.stderr) + if not result.stdout.startswith(b"PASS_CERTIFIED_GAUSSIAN_RECOVERY "): + raise ValueError("missing completed scientific replay") + return {"mode": mode, "seconds": seconds, "returncode": result.returncode, + "stdout_sha256": hashlib.sha256(result.stdout).hexdigest(), "counts": counts["counts"]} + + +def measure(): + records = [] + for _ in range(5): + for mode in ("baseline", "reflected"): + records.append(sample(mode)) + if len({r["stdout_sha256"] for r in records}) != 1: + raise ValueError("complete scientific output changed") + summary = {} + for mode in ("baseline", "reflected"): + selected = [r for r in records if r["mode"] == mode] + times = [r["seconds"] for r in selected] + if any(r["counts"] != selected[0]["counts"] for r in selected): + raise ValueError("work count changed between repetitions") + summary[mode] = {"median_seconds": statistics.median(times), + "minimum_seconds": min(times), "maximum_seconds": max(times), + "counts": selected[0]["counts"]} + summary["reduction_percent"] = 100 * (1 - summary["reflected"]["median_seconds"] / + summary["baseline"]["median_seconds"]) + return records, summary + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, required=True) + args = parser.parse_args() + target = args.output.resolve() + if ROOT == target or ROOT in target.parents or target.exists(): + raise ValueError("new output must be outside the checkout") + environment = {"python": sys.version, "platform": platform.platform(), + "logical_cpus": os.cpu_count(), "initial_load": os.getloadavg()} + records, summary = measure() + report = {"status": "PASS_GAUSSIAN_REFLECTION_BENCHMARK", "errors": 0, + "bindings": bindings(), "environment": environment, + "records": records, "summary": summary} + with target.open("x") as stream: + json.dump(report, stream, indent=2, sort_keys=True) + stream.write("\n") + print(json.dumps(summary, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/gaussian-expansion-reflection/run.py b/research/gaussian-expansion-reflection/run.py new file mode 100644 index 0000000000..ee1f34316b --- /dev/null +++ b/research/gaussian-expansion-reflection/run.py @@ -0,0 +1,22 @@ +"""Run the complete retained Gaussian caller with one setup substitution.""" +import argparse +import json +from pathlib import Path +import sys + +PACKAGE = Path(__file__).resolve().parent +sys.path.insert(0, str(PACKAGE)) +from adapter import complete_replay + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--mode", choices=("baseline", "reflected"), required=True) + args = parser.parse_args() + output, counts = complete_replay(args.mode) + print(output, end="") + print(json.dumps({"mode": args.mode, "counts": counts}, sort_keys=True), file=sys.stderr) + + +if __name__ == "__main__": + main() diff --git a/research/gaussian-expansion-reflection/verify.py b/research/gaussian-expansion-reflection/verify.py new file mode 100644 index 0000000000..cc8287ffcf --- /dev/null +++ b/research/gaussian-expansion-reflection/verify.py @@ -0,0 +1,162 @@ +"""Check the new reflection substitution and run the unchanged complete caller.""" +import argparse +import ast +from dataclasses import FrozenInstanceError +from fractions import Fraction +import hashlib +import json +from math import isqrt +from pathlib import Path +import statistics +import sys + +PACKAGE = Path(__file__).resolve().parent +sys.path.insert(0, str(PACKAGE)) +from adapter import (complete_replay, reflected_expansion, replace_expansion, + require, runtime) +from benchmark import bindings + + +def signature(matrix): + return [[(x.lo, x.hi, x.bits) for x in row] for row in matrix] + + +def literal_expansion(module, s, t, alpha, bits, radius): + matrix = module.zeros(t, s, bits) + pi = module.pi_interval(bits) + for k in range(t): + center = Fraction(s * k, t) + start = center.numerator // center.denominator - radius + stop = module.ceildiv(center.numerator, center.denominator) + radius + for j in range(start, stop + 1): + exponent = (Fraction(j) - center) ** 2 / alpha ** 2 + matrix[k][j % s] += module.exp_negative(pi * exponent) / (2 * alpha) + matrix[k] = [module.Interval(x.lo, x.hi + 1, bits) for x in matrix[k]] + return matrix + + +def geometry_checks(): + pairs = terms = 0 + for s in range(2, 17): + for t in range(s + 1, 25): + for radius in (1, 2, 7): + for k in range(t // 2 + 1, t): + a, b = Fraction(s * k, t), Fraction(s * (t - k), t) + lower = a.numerator // a.denominator - radius + upper = -((-a.numerator) // a.denominator) + radius + low_b = b.numerator // b.denominator - radius + high_b = -((-b.numerator) // b.denominator) + radius + require((s - upper, s - lower) == (low_b, high_b), + "exact reflected truncation endpoints") + for j in range(lower, upper + 1): + require((j - a) ** 2 == (s - j - b) ** 2, + "identical exact exponential argument") + require((s - j) % s == (-j) % s, + "correct cyclic reflection slot") + terms += 1 + pairs += 1 + return {"reflected_row_pairs": pairs, "exact_term_bijections": terms} + + +def interval_checks(): + fixtures = ((3, 4, 2, 48), (5, 8, 2, 48), (7, 16, 3, 64), + (5, 9, 2, 48), (6, 10, 3, 64)) + entries = saved = 0 + with runtime("baseline") as (modules, _, _): + module = modules["gaussian"] + for s, t, alpha, bits in fixtures: + radius = alpha * (isqrt(bits + 16) + 2) + expected = literal_expansion(module, s, t, alpha, bits, radius) + counts = dict.fromkeys(("expansion_terms", "computed_rows", + "reflected_rows", "constructors"), 0) + actual = reflected_expansion(module, counts, s, t, alpha, bits, radius) + require(signature(actual) == signature(expected), "all interval endpoints identical") + require(len({id(row) for row in actual}) == t, "distinct mutable row lists") + entries += s * t + saved += counts["reflected_rows"] + wanted = signature(expected) + mutations = [list(row) for row in wanted] + mutations[-1] = list(wanted[1]) + require(mutations != wanted, "omitting cyclic coordinate reversal is detected") + mutations = [list(row) for row in wanted] + mutations[-1] = list(wanted[2]) + require(mutations != wanted, "wrong partner row is detected") + mutations = [list(row) for row in wanted] + lo, hi, bits = mutations[-1][0] + mutations[-1][0] = (lo, hi - 1, bits) + require(mutations != wanted, "omitted outward tail unit is detected") + try: + actual[-1][0].lo = 0 + except FrozenInstanceError: + pass + else: + raise ValueError("reused interval objects must be immutable") + return {"fixtures": len(fixtures), "identical_entries": entries, + "reflected_rows": saved, "semantic_controls": 4} + + +def rejected_controls(): + controls = 0 + for source in ("x = 1", "class GaussianLine: pass", "class GaussianLine:\n def __init__(self): pass"): + try: + replace_expansion(ast.parse(source)) + except ValueError: + controls += 1 + else: + raise ValueError("changed source layout accepted") + try: + with runtime("unknown"): + raise RuntimeError("unreachable") + except ValueError: + controls += 1 + return controls + + +def measured_evidence(): + report = json.loads((PACKAGE / "BENCHMARK.json").read_text()) + require(report["bindings"] == bindings(), "benchmark executable/source bindings") + require(report["errors"] == 0 and len(report["records"]) == 10, "ten successful timed replays") + require(len({r["stdout_sha256"] for r in report["records"]}) == 1, "timed scientific output") + for index, row in enumerate(report["records"]): + require(row["mode"] == ("baseline", "reflected")[index % 2] + and row["returncode"] == 0 and row["seconds"] > 0, "alternating completed samples") + for mode in ("baseline", "reflected"): + selected = [r for r in report["records"] if r["mode"] == mode] + times = [r["seconds"] for r in selected] + summary = report["summary"][mode] + require(summary["median_seconds"] == statistics.median(times) + and summary["minimum_seconds"] == min(times) + and summary["maximum_seconds"] == max(times), "recomputed measurement summary") + require(all(r["counts"] == summary["counts"] for r in selected), "deterministic measured work") + expected = 100 * (1 - report["summary"]["reflected"]["median_seconds"] / + report["summary"]["baseline"]["median_seconds"]) + require(report["summary"]["reduction_percent"] == expected, "derived percentage") + return report["summary"] + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--allow-unmeasured", action="store_true") + args = parser.parse_args() + geometry = geometry_checks() + intervals = interval_checks() + controls = rejected_controls() + baseline, before = complete_replay("baseline") + reflected, after = complete_replay("reflected") + require(baseline == reflected, "complete scientific stdout unchanged") + require(before["exp_negative_calls"] > after["exp_negative_calls"], "strict exact work reduction") + require(after["constructors"] == 8 and after["reflected_rows"] == 60, + "all eight completed setup paths used the replacement") + summary = None if args.allow_unmeasured else measured_evidence() + files = ("adapter.py", "run.py", "verify.py", "benchmark.py", "SOURCES.json", "VERIFY.json") + receipt = {"status": "PASS_GAUSSIAN_EXPANSION_REFLECTION", "geometry": geometry, + "intervals": intervals, "source_layout_controls": controls, + "before": before, "after": after, "complete_products_per_side": 289, + "stdout_sha256": hashlib.sha256(baseline.encode()).hexdigest(), + "bindings": {p: hashlib.sha256((PACKAGE / p).read_bytes()).hexdigest() for p in files}, + "measurement": summary} + print(json.dumps(receipt, sort_keys=True)) + + +if __name__ == "__main__": + main()