From a125b7535b1cc43b2fea46460a36ba834b4bf1d6 Mon Sep 17 00:00:00 2001 From: mightyOil <82899331+mightyOil@users.noreply.github.com> Date: Tue, 13 Oct 2026 23:53:27 +0200 Subject: [PATCH 1/2] Audit commuting interval precision for target-dependent dirty words --- .../CERTIFICATE.json | 687 ++++++++++++++++++ research/commuting-dirty-precision/NOTICE.md | 26 + research/commuting-dirty-precision/PROOF.md | 194 +++++ research/commuting-dirty-precision/README.md | 131 ++++ .../commuting-dirty-precision/SOURCES.json | 18 + research/commuting-dirty-precision/TASK.json | 80 ++ .../commuting-dirty-precision/VALIDATION.json | 53 ++ .../VENDOR-PINS.json | 81 +++ .../commuting-dirty-precision/VERIFY.json | 20 + .../commuting-dirty-precision/precision.py | 91 +++ .../commuting-dirty-precision/test_package.py | 79 ++ .../commuting-dirty-precision/vendor/LICENSE | 201 +++++ .../vendor/pr1054/NOTICE.md | 46 ++ .../vendor/pr1054/PROOF.md | 338 +++++++++ .../vendor/pr1054/budget.py | 120 +++ .../vendor/pr1054/dirty_stride.py | 422 +++++++++++ .../vendor/pr1085/PROOF.md | 145 ++++ .../vendor/pr1085/README.md | 74 ++ .../vendor/pr1278/NOTICE.md | 17 + .../vendor/pr1278/PROOF.md | 177 +++++ .../vendor/pr628/NOTICE.md | 24 + .../vendor/pr628/dirty.py | 133 ++++ research/commuting-dirty-precision/verify.py | 267 +++++++ 23 files changed, 3424 insertions(+) create mode 100644 research/commuting-dirty-precision/CERTIFICATE.json create mode 100644 research/commuting-dirty-precision/NOTICE.md create mode 100644 research/commuting-dirty-precision/PROOF.md create mode 100644 research/commuting-dirty-precision/README.md create mode 100644 research/commuting-dirty-precision/SOURCES.json create mode 100644 research/commuting-dirty-precision/TASK.json create mode 100644 research/commuting-dirty-precision/VALIDATION.json create mode 100644 research/commuting-dirty-precision/VENDOR-PINS.json create mode 100644 research/commuting-dirty-precision/VERIFY.json create mode 100644 research/commuting-dirty-precision/precision.py create mode 100644 research/commuting-dirty-precision/test_package.py create mode 100644 research/commuting-dirty-precision/vendor/LICENSE create mode 100644 research/commuting-dirty-precision/vendor/pr1054/NOTICE.md create mode 100644 research/commuting-dirty-precision/vendor/pr1054/PROOF.md create mode 100644 research/commuting-dirty-precision/vendor/pr1054/budget.py create mode 100644 research/commuting-dirty-precision/vendor/pr1054/dirty_stride.py create mode 100644 research/commuting-dirty-precision/vendor/pr1085/PROOF.md create mode 100644 research/commuting-dirty-precision/vendor/pr1085/README.md create mode 100644 research/commuting-dirty-precision/vendor/pr1278/NOTICE.md create mode 100644 research/commuting-dirty-precision/vendor/pr1278/PROOF.md create mode 100644 research/commuting-dirty-precision/vendor/pr628/NOTICE.md create mode 100644 research/commuting-dirty-precision/vendor/pr628/dirty.py create mode 100644 research/commuting-dirty-precision/verify.py diff --git a/research/commuting-dirty-precision/CERTIFICATE.json b/research/commuting-dirty-precision/CERTIFICATE.json new file mode 100644 index 0000000000..7e8440492c --- /dev/null +++ b/research/commuting-dirty-precision/CERTIFICATE.json @@ -0,0 +1,687 @@ +{ + "status": "PASS_COMMUTING_DIRTY_PRECISION", + "seed": 64, + "sources": 11, + "dispatch": { + "cases": 78, + "literal_leaves": 150126, + "sha256": "fb7d5476ca29aabf5a49a993f9c2e6d9e5a804ae3969486461e0478d90e14fe5" + }, + "budgets": { + "uniform_cases": 5220, + "uniform_sha256": "919a727d5cadca551d90c777eae5c4c6a1db8a873ab930f806f455aad8db9e4f", + "generic_cases": 216, + "generic_sha256": "033f418dc7ffc6194a00cbb5a0cefdcce2dcfc9a9a131c466ed19f9cf361679d", + "comparison": [ + { + "radix": 3, + "old_fractional": 447, + "new_fractional": 397, + "old_integer": 306, + "new_integer": 305, + "leaf_calls": 4, + "borrowed_arrays": 1, + "factor_bits": 236 + }, + { + "radix": 4, + "old_fractional": 606, + "new_fractional": 523, + "old_integer": 447, + "new_integer": 444, + "leaf_calls": 10, + "borrowed_arrays": 2, + "factor_bits": 287 + }, + { + "radix": 8, + "old_fractional": 2921, + "new_fractional": 2418, + "old_integer": 2556, + "new_integer": 2552, + "leaf_calls": 52, + "borrowed_arrays": 3, + "factor_bits": 1107 + }, + { + "radix": 16, + "old_fractional": 21768, + "new_fractional": 17838, + "old_integer": 19701, + "new_integer": 19695, + "leaf_calls": 232, + "borrowed_arrays": 4, + "factor_bits": 7923 + }, + { + "radix": 32, + "old_fractional": 175583, + "new_fractional": 143690, + "old_integer": 159558, + "new_integer": 159550, + "leaf_calls": 976, + "borrowed_arrays": 5, + "factor_bits": 63787 + }, + { + "radix": 64, + "old_fractional": 1420902, + "new_fractional": 1162598, + "old_integer": 1291719, + "new_integer": 1291709, + "leaf_calls": 4000, + "borrowed_arrays": 6, + "factor_bits": 516499 + }, + { + "radix": 128, + "old_fractional": 11447117, + "new_fractional": 9365893, + "old_integer": 10406568, + "new_integer": 10406557, + "leaf_calls": 16192, + "borrowed_arrays": 7, + "factor_bits": 4162139 + }, + { + "radix": 256, + "old_fractional": 91919604, + "new_fractional": 75207073, + "old_integer": 83563593, + "new_integer": 83563580, + "leaf_calls": 65152, + "borrowed_arrays": 8, + "factor_bits": 33424355 + }, + { + "radix": 512, + "old_fractional": 736765979, + "new_fractional": 602808765, + "old_integer": 669788010, + "new_integer": 669787995, + "leaf_calls": 261376, + "borrowed_arrays": 9, + "factor_bits": 267912939 + } + ] + }, + "rounded": { + "cases": 20, + "signed_words": 80, + "signed_leaf_calls": 2336, + "nonzero_error_words": 80, + "target_dependent": true, + "rows": [ + { + "n": 2, + "length": 3, + "stride": 1, + "tau": [ + "1", + "0" + ], + "working_bits": 72, + "old_working_bits": 78, + "integer_bits": 32, + "error_log2_squared": [ + -141, + -141, + -142, + -142 + ], + "forward_bill": { + "reads": 505, + "writes": 396, + "tape_moves": 1323, + "products": 70, + "power_products": 16, + "divisions": 8, + "nodes": 12, + "leaves": 4 + } + }, + { + "n": 2, + "length": 3, + "stride": 1, + "tau": [ + "3/5", + "4/5" + ], + "working_bits": 72, + "old_working_bits": 78, + "integer_bits": 32, + "error_log2_squared": [ + -140, + -140, + -140, + -140 + ], + "forward_bill": { + "reads": 505, + "writes": 396, + "tape_moves": 1323, + "products": 76, + "power_products": 16, + "divisions": 8, + "nodes": 12, + "leaves": 4 + } + }, + { + "n": 2, + "length": 5, + "stride": -2, + "tau": [ + "1", + "0" + ], + "working_bits": 72, + "old_working_bits": 78, + "integer_bits": 32, + "error_log2_squared": [ + -142, + -142, + -142, + -142 + ], + "forward_bill": { + "reads": 1455, + "writes": 1196, + "tape_moves": 4129, + "products": 186, + "power_products": 240, + "divisions": 16, + "nodes": 28, + "leaves": 4 + } + }, + { + "n": 2, + "length": 5, + "stride": -2, + "tau": [ + "3/5", + "4/5" + ], + "working_bits": 72, + "old_working_bits": 78, + "integer_bits": 32, + "error_log2_squared": [ + -141, + -141, + -141, + -141 + ], + "forward_bill": { + "reads": 1455, + "writes": 1196, + "tape_moves": 4129, + "products": 196, + "power_products": 240, + "divisions": 16, + "nodes": 28, + "leaves": 4 + } + }, + { + "n": 3, + "length": 3, + "stride": 1, + "tau": [ + "1", + "0" + ], + "working_bits": 77, + "old_working_bits": 89, + "integer_bits": 34, + "error_log2_squared": [ + -152, + -152, + -152, + -152 + ], + "forward_bill": { + "reads": 1276, + "writes": 1014, + "tape_moves": 3416, + "products": 178, + "power_products": 40, + "divisions": 20, + "nodes": 30, + "leaves": 10 + } + }, + { + "n": 3, + "length": 3, + "stride": 1, + "tau": [ + "3/5", + "4/5" + ], + "working_bits": 77, + "old_working_bits": 89, + "integer_bits": 34, + "error_log2_squared": [ + -151, + -151, + -151, + -151 + ], + "forward_bill": { + "reads": 1276, + "writes": 1014, + "tape_moves": 3416, + "products": 190, + "power_products": 40, + "divisions": 20, + "nodes": 30, + "leaves": 10 + } + }, + { + "n": 3, + "length": 5, + "stride": -2, + "tau": [ + "1", + "0" + ], + "working_bits": 77, + "old_working_bits": 89, + "integer_bits": 34, + "error_log2_squared": [ + -150, + -150, + -150, + -150 + ], + "forward_bill": { + "reads": 3660, + "writes": 3030, + "tape_moves": 10472, + "products": 470, + "power_products": 600, + "divisions": 40, + "nodes": 70, + "leaves": 10 + } + }, + { + "n": 3, + "length": 5, + "stride": -2, + "tau": [ + "3/5", + "4/5" + ], + "working_bits": 77, + "old_working_bits": 89, + "integer_bits": 34, + "error_log2_squared": [ + -150, + -150, + -150, + -150 + ], + "forward_bill": { + "reads": 3660, + "writes": 3030, + "tape_moves": 10472, + "products": 490, + "power_products": 600, + "divisions": 40, + "nodes": 70, + "leaves": 10 + } + }, + { + "n": 4, + "length": 3, + "stride": 1, + "tau": [ + "1", + "0" + ], + "working_bits": 81, + "old_working_bits": 94, + "integer_bits": 36, + "error_log2_squared": [ + -160, + -160, + -160, + -160 + ], + "forward_bill": { + "reads": 1996, + "writes": 1584, + "tape_moves": 5304, + "products": 280, + "power_products": 64, + "divisions": 32, + "nodes": 48, + "leaves": 16 + } + }, + { + "n": 4, + "length": 3, + "stride": 1, + "tau": [ + "3/5", + "4/5" + ], + "working_bits": 81, + "old_working_bits": 94, + "integer_bits": 36, + "error_log2_squared": [ + -159, + -159, + -159, + -159 + ], + "forward_bill": { + "reads": 1996, + "writes": 1584, + "tape_moves": 5304, + "products": 304, + "power_products": 64, + "divisions": 32, + "nodes": 48, + "leaves": 16 + } + }, + { + "n": 4, + "length": 5, + "stride": -2, + "tau": [ + "1", + "0" + ], + "working_bits": 81, + "old_working_bits": 94, + "integer_bits": 36, + "error_log2_squared": [ + -158, + -158, + -158, + -158 + ], + "forward_bill": { + "reads": 5780, + "writes": 4784, + "tape_moves": 16528, + "products": 744, + "power_products": 960, + "divisions": 64, + "nodes": 112, + "leaves": 16 + } + }, + { + "n": 4, + "length": 5, + "stride": -2, + "tau": [ + "3/5", + "4/5" + ], + "working_bits": 81, + "old_working_bits": 94, + "integer_bits": 36, + "error_log2_squared": [ + -157, + -157, + -157, + -157 + ], + "forward_bill": { + "reads": 5780, + "writes": 4784, + "tape_moves": 16528, + "products": 784, + "power_products": 960, + "divisions": 64, + "nodes": 112, + "leaves": 16 + } + }, + { + "n": 7, + "length": 3, + "stride": 1, + "tau": [ + "1", + "0" + ], + "working_bits": 91, + "old_working_bits": 112, + "integer_bits": 41, + "error_log2_squared": [ + -179, + -179, + -179, + -179 + ], + "forward_bill": { + "reads": 6511, + "writes": 5196, + "tape_moves": 17671, + "products": 916, + "power_products": 208, + "divisions": 104, + "nodes": 156, + "leaves": 52 + } + }, + { + "n": 7, + "length": 3, + "stride": 1, + "tau": [ + "3/5", + "4/5" + ], + "working_bits": 91, + "old_working_bits": 112, + "integer_bits": 41, + "error_log2_squared": [ + -178, + -178, + -178, + -178 + ], + "forward_bill": { + "reads": 6511, + "writes": 5196, + "tape_moves": 17671, + "products": 988, + "power_products": 208, + "divisions": 104, + "nodes": 156, + "leaves": 52 + } + }, + { + "n": 7, + "length": 5, + "stride": -2, + "tau": [ + "1", + "0" + ], + "working_bits": 91, + "old_working_bits": 112, + "integer_bits": 41, + "error_log2_squared": [ + -178, + -178, + -178, + -178 + ], + "forward_bill": { + "reads": 18825, + "writes": 15628, + "tape_moves": 54377, + "products": 2428, + "power_products": 3120, + "divisions": 208, + "nodes": 364, + "leaves": 52 + } + }, + { + "n": 7, + "length": 5, + "stride": -2, + "tau": [ + "3/5", + "4/5" + ], + "working_bits": 91, + "old_working_bits": 112, + "integer_bits": 41, + "error_log2_squared": [ + -176, + -176, + -176, + -176 + ], + "forward_bill": { + "reads": 18825, + "writes": 15628, + "tape_moves": 54377, + "products": 2548, + "power_products": 3120, + "divisions": 208, + "nodes": 364, + "leaves": 52 + } + }, + { + "n": 8, + "length": 3, + "stride": 1, + "tau": [ + "1", + "0" + ], + "working_bits": 94, + "old_working_bits": 116, + "integer_bits": 43, + "error_log2_squared": [ + -185, + -185, + -184, + -184 + ], + "forward_bill": { + "reads": 7951, + "writes": 6336, + "tape_moves": 21465, + "products": 1120, + "power_products": 256, + "divisions": 128, + "nodes": 192, + "leaves": 64 + } + }, + { + "n": 8, + "length": 3, + "stride": 1, + "tau": [ + "3/5", + "4/5" + ], + "working_bits": 94, + "old_working_bits": 116, + "integer_bits": 43, + "error_log2_squared": [ + -186, + -186, + -186, + -186 + ], + "forward_bill": { + "reads": 7951, + "writes": 6336, + "tape_moves": 21465, + "products": 1216, + "power_products": 256, + "divisions": 128, + "nodes": 192, + "leaves": 64 + } + }, + { + "n": 8, + "length": 5, + "stride": -2, + "tau": [ + "1", + "0" + ], + "working_bits": 94, + "old_working_bits": 116, + "integer_bits": 43, + "error_log2_squared": [ + -184, + -184, + -184, + -184 + ], + "forward_bill": { + "reads": 23065, + "writes": 19136, + "tape_moves": 66519, + "products": 2976, + "power_products": 3840, + "divisions": 256, + "nodes": 448, + "leaves": 64 + } + }, + { + "n": 8, + "length": 5, + "stride": -2, + "tau": [ + "3/5", + "4/5" + ], + "working_bits": 94, + "old_working_bits": 116, + "integer_bits": 43, + "error_log2_squared": [ + -183, + -183, + -183, + -183 + ], + "forward_bill": { + "reads": 23065, + "writes": 19136, + "tape_moves": 66519, + "products": 3136, + "power_products": 3840, + "divisions": 256, + "nodes": 448, + "leaves": 64 + } + } + ] + }, + "controls": [ + "non-prime-power", + "negative-target-precision", + "missing-feedback", + "unsafe-length-admission", + "unpaid-subset-budget", + "second-subset-factor-retained", + "inverse-preimage-reserve-retained", + "noncommuting-interval-rejects-linear-G" + ] +} diff --git a/research/commuting-dirty-precision/NOTICE.md b/research/commuting-dirty-precision/NOTICE.md new file mode 100644 index 0000000000..4e2d71bf78 --- /dev/null +++ b/research/commuting-dirty-precision/NOTICE.md @@ -0,0 +1,26 @@ +# Attribution and boundaries + +Prepared for Philipp (@mightyOil) with substantial OpenAI Codex / GPT-6 Astra +assistance in mathematics, implementation, verification and writing. New +material is under the repository Apache-2.0 license. No literature-priority, +independent human-review or proof-assistant claim is made. + +This package composes, credits and depends on: +- Ali Romman's PR1054 target-dependent rounded dirty stride contract, on + PR985/621, with the unchanged source, beta^-8 inverse-preimage reserve, + preparation and full operation bill. +- Hanson Sun's PR1085 sharp prefix coefficient lemma and PR1244's explicit + noncommuting interval obstruction, reproduced solely as a negative control. +- Charles Bethin's PR1278 squarefree all-size interval lemma and explicit + handoff asking for this PR1054 substitution. +- Chafik Boukhalfa's PR628 balanced dispatcher and PR862/905 common-operator + preparation and prefix arguments; Gareth Davidson's PR877 perturbation + method; 0xkilgore's PR663 exact leaf count; the PR846/764 predecessor lineage. + +The small consumed subset is copied byte-for-byte with exact commit, Git-blob +and SHA256 pins. Preserved notices describe their original packages; references +within them to a full retained vendor tree apply to those source packages. +This audit vendors only its declared subset and does not modify the sources. +Separate exact arithmetic implementations mean separate code paths, not +independent human validation. No new supplier, kappa, optimal width, measured +speedup or complete multiplication proof is claimed. diff --git a/research/commuting-dirty-precision/PROOF.md b/research/commuting-dirty-precision/PROOF.md new file mode 100644 index 0000000000..d7ef8832ae --- /dev/null +++ b/research/commuting-dirty-precision/PROOF.md @@ -0,0 +1,194 @@ +# Commuting interval transport for the target-dependent PR1054 word + +This is a conditional local accuracy theorem for the unchanged rounded word. +The all-size argument below uses the pinned written lemmas of PR1085 and +PR1278, not extrapolation from our finite tests. No minimum-precision or +multiplication-exponent claim follows. + +## 1. Interface and source binding + +Retain Ali Romman's PR1054 at `6bc675be1554b3a3be771147f21f9dc2c6dae50a`: +its constant-coefficient PR985 rounded leaves, length-independent admission, +effective-depth/zero-subtree argument, exact inverse grid word, preparation +and complete operation accounting. Source, target and reserved-depth scratch +are distinct; phases are immutable and do not alias mutable data. Cuts are +complete outer-leaf boundaries, not internal rounded-operation boundaries. + +For n factors, the positive ideal word executes U,V,U^-1,V^-1, where +U adds the complete left factor product into the depth's connector and V +adds the complete right product into the target. The negative word is the +literal inverse. The actual PR1054 nested `run` uses exactly the floor/ceil +split, argument wiring, signs and shared deeper scratch of PR628 `compose`. +Their frozen source ASTs are compared with numerical leaves instrumented; +the source itself exhibits the same four recursive calls for every n. +The physical carrier swaps conjugate a logical leaf by a swap and its inverse; +PR1054's already charged two-tape realization and distinct-array requirements +remain inherited. They do not change the logical leaf-boundary word. + +Let the ideal factors commute pairwise, with every subset product (including +empty) of norm at most G >= 1. PR1054's actual cyclic factors satisfy this +conditional premise because every factor is a rational function of the same +immutable isometry U=tau Z_L^w; the single scalar r also commutes. The inherited +complementary-factor argument gives the stated G. Different mutable phases or +unrelated operators do not satisfy this premise automatically. + +Put h=ceil(log2 n), C=h+2. Hanson Sun's PR1085 proves every prefix and inverse +prefix has coefficient absolute row sum at most C in the free factor algebra. +Charles Bethin's PR1278 proves every monomial surviving in every two-cut +interval uses each factor index at most once, including intervals crossing two +occurrences of the same child and the reused deeper scratch. Multiplication +of the prefix and inverse-prefix matrices has coefficient row sum at most C^2. +Cancellation cannot increase it. Commutation puts each squarefree monomial +in subset order, so, in the maximum joint-register norm, + + B = C G bounds every prefix and inverse prefix, + L = C^2 G bounds every interval in either cut order. + +Both ingredients are needed. The generic ordered-subset case has only B^2. +PR1244's noncommuting obstruction remains valid; this does not weaken its +hypothesis or claim that unordered products have the ordered-subset bound. + +## 2. Nonlinear errors and inverse targets + +Let r >= 1 bound the inherited leaf scale, 0 < beta <= 1/2, u=2^-W, +and D >= 0 bound every incoming array. Retain PR1054's all-length admission +`48(g+ceil(log2(W+1))+1) u <= beta^3`, where g=ceil(log2(1/beta)). +In particular W >= 4g+16 suffices. The exact paid leaf count is + + N = 3 q n - 2 q^2, q=2^floor(log2 n). + +PR1054 supplies the target-independent *error bound* (not a target-independent +rounded increment) + + ||delta|| <= a u (||source||+1), a=68(r+1) beta^-5. + +For a negative leaf with input y and output z, exact inversion gives +`y=z+A x+delta(x,z)`. The positive estimate holds for every preimage target z, +so the negative error satisfies the same bound at its unchanged source x. +This step does not treat a rounded leaf as linear or additive in its source. + +Let T be the largest actual joint norm at complete leaf boundaries. Insert +the actual nonlinear error of each executed leaf into the ideal linear word. +Variation of constants and the interval bound, applied to these fixed error +vectors after the execution, give + + T <= B D + t(T+1), t=N L a u. + +If t <= 1/2, then T <= Dstar=2 B D+1. The final execution error is at most + + E = 2 N L a u (B D+1). (1) + +The execution is finite by the retained stable-closure admission. Thus taking +its maximum T and rearranging this inequality does not assume a prior bound +on rounded intermediate targets. This is the same argument as PR1054, with +its B^2 replaced only at the interval step by L. + +## 3. Internal inverse preimages remain paid + +Accuracy alone does not control internal leaf values. PR1054 supplies the +forward internal bound `512(r+1)(Dstar+1)/beta^7`, including zero tails. +For an inverse leaf, first bound its positive preimage: + + Dpre <= (2+r/beta) Dstar+1. + +Indeed the preimage differs by an ideal factor of norm at most r/beta and an +error at most a u(Dstar+1); t <= 1/2 implies a u <= 1. Reversing the positive +word traverses that preimage's entire forward path. Since +`Dpre+1 <= (r+2)(Dstar+1)/beta`, both directions are covered by + + V = 1024(r+1)(r+2)(B D+1)/beta^8. (2) + +The eighth power of beta is retained. Reducing G in error transport does not +license deleting the inverse-preimage factor or substituting the negative +call's incoming target for its positive preimage. A signed component reserve +of `ceil(log2 V)+2` remains sufficient. Block swaps add no magnitude. + +## 4. Explicit budgets and a cubic envelope + +For generic rational parameters, a sufficient width is + + W = max(w_input, 4g+16, + p+2+ceil(log2(N L a (B D+1)))). (3) + +Then (1) is at most 2^(-p-1). Since B D+1 >= 1 and p >= 0, (3) also ensures +t <= 1/4, hence the required feedback bound. No incoming grid is coarsened. +The signed integer width is given after (2). + +For the certified prime-power interface r >= 3, retain all PR1054 preparation +parameters, with n=r-1, ell=ceil(log2 r), phi=EulerPhi(r), m>=0, D<=2^m: + + d0 = 1+2ell+r n phi, + a0 = 2d0+r+2, + g = d0+ell+2r+2, beta=2^-g, + e = max(d0+1,a0+1,p+2a0+m+4), + b_factor = max(n ell,e+r+3). + +These inherited analytic/factor-preparation assumptions give G<=2^K where +`K=a0+2r+ell`. Let + + c = ceil(log2(h+2)), + J = K+c, B <= 2^J, + H = K+2c, L <= 2^H, + A = 5g+ceil(log2(68(r+1))). + +The resulting fully explicit sufficient widths are + + W = max(w_input, 4g+16, p+3+ceil(log2 N)+A+m+J+H), + I = J+m+8g+2ell+16. (4) + +Indeed B D+1 <= 2^(J+m+1), and (1) is bounded by +`2^(ceil(log2 N)+H+A-W+J+m+2) <= 2^(-p-1)`. +The integer reserve (2) follows from the same algebra as PR1054 with the +smaller J. Its coefficient error still costs at most 2^(-p-3); preparation +plus execution is less than 2^-p. The supplied root factorizer, stable margin, +Neumann estimate and original kernel approximation are not new results here. + +For an all-size coarse envelope use phi<=r, ell,h,c<=r, +`ceil(log2 N)<=1+2h`, and `ceil(log2(68(r+1)))<=ell+8`. +The third term in (4), minus p+m, is at most + + 9r^3 - 9r^2 + 47r + 35 <= 15r^3. + +The difference is `(r-3)(6r^2+27r+34)+67`, nonnegative for r>=3. +The admission term obeys `4g+16 <= 4r^3-4r^2+20r+28 <= 15r^3`: +its difference is `(r-3)(11r^2+37r+91)+245`. Therefore + + W <= max(p,w_input)+m+15r^3. + +The signed integer width only decreases from PR1054's bound, so +`I<=m+15r^3`; the unchanged factor width remains `b_factor<=p+m+7r^3`. +These are convenient sufficient envelopes, not sharp constants. In particular +the leading bound is still cubic, and the lower-order coarse envelope is not +used to choose the explicit widths. + +At r=64, p=128, m=20 and w_input=0, (4) gives W=1,162,598 and I=1,291,709, +compared with PR1054's W=1,420,902 and I=1,291,719. Fractional reduction: +258,304 bits. Preparation still uses 516,499 factor bits, 4,000 leaf calls +and six borrowed arrays. This is a comparison to that exact PR1054 contract; +PR1085's similar-looking 1,162,523 number concerns PR905's different leaf +budget and is not superseded or combined numerically here. + +## 5. Complete cost and limits + +The actual word, source access, carrier swaps, restoration, coefficients and +child calls are unchanged. Retain PR1054's per-leaf bounds 1280L scalar +products/divisions and 4096L record moves, and full-kernel bound +`8192(N+1)(h+2)L` data-record moves on two tapes. Let Aword=W+I and Bdesc +include the actual immutable root, margin, multiplier and unit gauge lengths. +With M(s) paying for rounded multiplication and division, the complete bill is + + preparation + O(N L M(Aword+Bdesc)) + + O(N(h+2)L(Aword+Bdesc)) + O(N L). + +Long stride/gauge descriptors remain extra input work; preparation retains +its supplied soft-O(r^3(p+m+r^3)) bill. Effective numerical depth cannot +replace structural depth in movement or recursion counts. No additional clean +array, early exit, removed leaf, or free access is used. + +Our rounded controls execute small stable rational factor families at their +new generic widths, compare the complete ideal product by a finite geometric +oracle, check both standalone signs, dirty restoration, literal indexed +accesses, signed internal guards, and unchanged paid-operation counts versus +the old finer grid. They are not an execution of the million-bit radix-64 +example, an all-size root factorizer, physical compiler, full supplier cold +replay, complete transform, formal proof, or new kappa. diff --git a/research/commuting-dirty-precision/README.md b/research/commuting-dirty-precision/README.md new file mode 100644 index 0000000000..7a5215011c --- /dev/null +++ b/research/commuting-dirty-precision/README.md @@ -0,0 +1,131 @@ +# Smaller sufficient precision for the commuting dirty word + +**Conditional precision audit; no new kappa.** This applies PR1278's commuting +interval lemma and PR1085's sharp prefix count to PR1054's actual +target-dependent rounded leaf contract. Both standalone word directions are +covered, including the positive preimage visited inside a negative leaf. + +For n factors, put h=ceil(log2 n), C=h+2, and suppose every subset product +has norm at most G>=1. The prefix bound is B=CG and the interval bound is +L=C²G. For N paid leaves with source-only error bound `a u (X+1)`, initial +array bound D and grid unit u, the sufficient execution error becomes + + 2 N L a u (B D+1), provided N L a u <= 1/2. + +This removes one factor G from generic two-prefix transport. The rounded +increment may still depend on the incoming target: its error bound applies +uniformly at the positive preimage. The internal reserve retains beta^-8, +including the inverse-preimage factor. [PROOF.md](PROOF.md) gives the complete +all-size substitution, explicit integer formulas, and unchanged cost bill. + +For PR1054's prime-power preparation contract, the convenient coarse envelope +improves from `max(p,w_input)+m+18r³` to `max(p,w_input)+m+15r³` fractional +bits. It remains cubic and sufficient, not an optimum. Explicit formulas +are considerably tighter than this coarse envelope. + +At p=128, m=20 and w_input=0: + +| Radix | PR1054 fractional bits | New fractional bits | PR1054 signed integer bits | New signed integer bits | Paid leaves | +|---:|---:|---:|---:|---:|---:| +| 8 | 2,921 | 2,418 | 2,556 | 2,552 | 52 | +| 16 | 21,768 | 17,838 | 19,701 | 19,695 | 232 | +| 32 | 175,583 | 143,690 | 159,558 | 159,550 | 976 | +| 64 | 1,420,902 | **1,162,598** | 1,291,719 | **1,291,709** | 4,000 | + +At radix 64 this saves 258,304 fractional bits. The six borrowed arrays, +516,499 factor-preparation bits and complete leaf/routing word are unchanged. +The radix-64 row is an exact budget comparison, **not an execution at those +million-bit widths**. PR1085's 1,162,523-bit example concerns PR905's different +leaf contract; the similar figures are not interchangeable. + +## Reproduce and evidence + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 scripts/research_package.py --package research/commuting-dirty-precision +``` + +Expected: `PASS_COMMUTING_DIRTY_PRECISION`, six passing package tests, +`PASS_COMMUTING_DIRTY_PRECISION_PACKAGE`, then `PASS_REGISTERED_RESEARCH_PACKAGE`. +The standalone `python3 -I -O -B research/commuting-dirty-precision/test_package.py` +also works from a source export with this complete package. + +The exact deterministic [certificate](CERTIFICATE.json) contains: + +- 5,220 uniform prime-power budget certificates through radix 512, independently + recounted phi/leaf counts and checked integer exponent inequalities; 216 + generic rational budget checks, including incoming-grid domination. +- Literal PR1054/PR628 recursive dispatcher comparisons in both signs at every + n=1..33 and n=63,64,65,127,128,129. The numerical leaf body is instrumented; + split, signs, wiring and scratch reuse come from the pinned source AST. +- 20 stable rational factor fixtures at n=2,3,4,7,8; two cyclic geometries and + two shared unit gauges. All 80 signed rounded words are actually executed, + with odd lowest input bits, a finite-geometric ideal oracle, exact source + and scratch restoration, complete positive/negative inverse cancellation, + literal data-access counts and full internal/routing bounds. +- Each fixture's forward paid-operation census also matches the old finer-grid + execution on the same incoming data. This compares every counted read, + write, product, powering product, division, node, leaf and tape move; it does + not equate rounded numerical answers on different grids. +- Eight mathematical/admission controls, including PR1244's seven-factor + noncommuting interval obstruction (the latter is + a credited inherited witness, not a new counterexample). The rounded tests + additionally demonstrate actual target dependence. Five actual package + corruptions fail, including missing proof, source/receipt drift, a deleted + interval G and a deleted inverse-preimage guard. Relocated read-only inputs + replay with isolated optimized Python. + +The direct oracle and budget checker are separate implementations. They are +AI-assisted and are not independent human reviews. Written predecessor lemmas +supply the quantified all-size proof; these finite checks support the source +binding and arithmetic. [VALIDATION.json](VALIDATION.json) records performed +and omitted checks. No selected supplier cold replay or hosted CI is claimed. + +## Pins, overlap and scope + +Base: `dadfea6e8a78ff6ba901705f87532a71c6f5bbb8`. OS seed **64**, adversarial +audit under the original user track mapping. [TASK.json](TASK.json) records +scope and stopping rule. The initial three candidates were a sharp interval +coefficient bound, this rounded-contract substitution, and sign-asymmetric +connector prices. This chosen task is explicitly left open by PR1278. +The [claim and result discussion](https://github.com/CrocSwap/integer-mult-bounds/discussions/1283) +records its narrow boundary. + +Pinned pending predecessors: + +| PR | Contributor | Exact head | Retained obligation | +|---|---|---|---| +| [#1054](https://github.com/CrocSwap/integer-mult-bounds/pull/1054) | Ali Romman | `6bc675be1554b3a3be771147f21f9dc2c6dae50a` | Rounded word, admission, nonlinear leaf error, inverse preimage, preparation and complete cost | +| [#1085](https://github.com/CrocSwap/integer-mult-bounds/pull/1085) | Hanson Sun | `82b99c7d12dac009d35636562df4c6c91e885409` | Sharp C=h+2 prefix coefficient lemma | +| [#1278](https://github.com/CrocSwap/integer-mult-bounds/pull/1278) | Charles Bethin | `06b8c006891ae78abe24b30d2fe9d8c188deafe8` | All-size squarefree interval lemma with shared deeper scratch | + +These are dependency pins, not a claim of maintainer acceptance. Each consumed +source byte is recorded in [VENDOR-PINS.json](VENDOR-PINS.json). The small +vendored subset serves this audit's proof and actual executions; frozen +predecessor packages are not modified. Existing generic precision bounds stay +valid. PR1244's noncommuting obstruction and PR1135's nonadditive borrowing +obstruction are not removed. We retain the original reserved-depth allocation. + +Only this package is added. The selected PR1094 record, upstream sources, +source-access/restoration charges, paid rank profiles and all-size/compiler, +physical hosting, fast scalar arithmetic, supplied factorizer and analytic +interfaces remain unchanged. No new supplier, optimal precision, measured +speedup, full transform, or multiplication theorem is asserted. + +## Open next questions + +A sharp two-cut coefficient recurrence could improve the remaining logarithmic +constant. Start from PR1278's six phase cases; an all-size proof is needed, +not merely more finite maxima. This audit deliberately uses C². + +To use this at a complete supplier caller, bind one caller and regenerate its +native/physical invoice with the smaller width. Preparation, source routing, +compiler and analytic interfaces are the blockers. A local sufficient width +does not itself change the selected moment. Structured next steps are in TASK.json. + +Prepared for **Philipp (@mightyOil)** with substantial **OpenAI Codex / GPT-6 +Astra assistance** in mathematics, code, verification and writing. Apache-2.0. +Credit PR1054/985/621 (Ali Romman), PR1085/1244 (Hanson Sun), PR1278 (Charles +Bethin), PR628/862/905 (Chafik Boukhalfa), PR877 (Gareth Davidson), PR663 +(0xkilgore), and the retained lineage. [NOTICE.md](NOTICE.md) preserves scope. diff --git a/research/commuting-dirty-precision/SOURCES.json b/research/commuting-dirty-precision/SOURCES.json new file mode 100644 index 0000000000..35b6e45c02 --- /dev/null +++ b/research/commuting-dirty-precision/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "dadfea6e8a78ff6ba901705f87532a71c6f5bbb8", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + } + ] +} diff --git a/research/commuting-dirty-precision/TASK.json b/research/commuting-dirty-precision/TASK.json new file mode 100644 index 0000000000..f2e003c79b --- /dev/null +++ b/research/commuting-dirty-precision/TASK.json @@ -0,0 +1,80 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 2, + "base_commit": "dadfea6e8a78ff6ba901705f87532a71c6f5bbb8", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one exact all-size/compiler, precision, hosting or restoration implication be proved or falsified?", + "starting_points": [ + "certificates/selected-result.json", + "docs/audit.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the selected review scope and choose one exact all-size or precision implication.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write its quantified inputs and conclusion; find a missing hypothesis or construct a minimal exact adversarial instance.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "Choose one tape, precision, hosting or restoration lemma." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision" + ] + }, + "scope_status": "refined", + "actual_scope": "Commuting interval transport plus sharp prefix count in PR1054 sufficient precision, with inverse preimage integer guards and unchanged paid word.", + "scope_change_reason": "The explicit user seed assigns an adversarial audit. PR1278 leaves substitution into the target-dependent PR1054 rounded contract open; this fixes that boundary.", + "bottleneck_link": "Side precision-interface result: lowers a sufficient local arithmetic word width under inherited common-operator assumptions. It does not alter the paid rank profile or selected kappa.", + "budget_minutes": 40, + "stop_rule": "One source-bound conditional budget; finite full rounded controls at n=2,3,4,7,8. No search for optimal precision or supplier adoption.", + "outcome": "completed", + "evidence": "CERTIFICATE.json, PROOF.md, verify.py, test_package.py", + "author": "Philipp (@mightyOil)", + "ai_assistance": "Substantial OpenAI Codex / GPT-6 Astra assistance in mathematics, implementation, verification and writing.", + "open_questions": [ + { + "question": "Can the sharp interval coefficient count improve the remaining logarithmic constants?", + "why_it_matters": "The product of sharp prefix bounds is still conservative.", + "first_step": "Derive a two-cut coefficient recurrence from PR1278 six phase cases.", + "blocked_by": "Requires an all-size bound; a finite census is not proof." + }, + { + "question": "Can this smaller sufficient precision be admitted at a complete supplier caller?", + "why_it_matters": "A local working-width theorem alone does not change the selected moment or kappa.", + "first_step": "Bind one exact caller and regenerate its complete native and physical invoice.", + "blocked_by": "Preparation, physical compiler, routing, analytic and full-transform interfaces remain inherited." + } + ], + "seed": 64, + "assignment_track": "Adversarial mathematical audit, original user mapping 60-74", + "coordination": { + "discussion": 1283, + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1283", + "initial_open_prs": 870, + "initial_discussions": 18, + "no_pinned_sprint_issue": true + }, + "candidates": [ + "Sharp all-interval coefficient bound after PR1278", + "Commuting interval transport in PR1054 target-dependent precision", + "Sign-asymmetric connector prices" + ] +} diff --git a/research/commuting-dirty-precision/VALIDATION.json b/research/commuting-dirty-precision/VALIDATION.json new file mode 100644 index 0000000000..896a4b81a2 --- /dev/null +++ b/research/commuting-dirty-precision/VALIDATION.json @@ -0,0 +1,53 @@ +{ + "status": "local verification passed", + "base_commit": "dadfea6e8a78ff6ba901705f87532a71c6f5bbb8", + "refreshed_main": "bdd4c63ac7c5d8a46ce070ba133df8d7ba9cb92c", + "refreshed_selected_and_guidance": "unchanged by git diff from base", + "platform": "macOS-27.0.1-arm64-arm-64bit-Mach-O", + "generator_python": "3.14.7", + "registered_python": "3.12.13", + "registered_replay_seconds": 60.128, + "registered_package": "PASS_REGISTERED_RESEARCH_PACKAGE", + "package_tests": 6, + "actual_package_corruptions": 5, + "readonly_relocation": true, + "mathematical_controls": 8, + "selected_record_check": "PASS", + "selected_unit_tests": 25, + "source_pins": 11, + "dispatch": { + "cases": 78, + "literal_leaves": 150126, + "sha256": "fb7d5476ca29aabf5a49a993f9c2e6d9e5a804ae3969486461e0478d90e14fe5" + }, + "uniform_budget_cases": 5220, + "generic_budget_cases": 216, + "rounded_cases": 20, + "actual_signed_words": 80, + "actual_signed_leaf_calls": 2336, + "nonzero_error_words": 80, + "certificate_sha256": "01487beccdf49b8ec7aab59f9b837da6628a60c5e1ec42e62539f1d882348f3f", + "final_overlap": { + "open_prs": 815, + "discussion_records": 21, + "nearest_sources": [ + 1054, + 1085, + 1244, + 1278 + ], + "dependency_heads_rechecked_unchanged": true, + "scope": "All open PR titles/bodies and latest 21 discussion records, no matching PR1054 substitution found. Explicit dependency views remain OPEN; historical closures changed overall queue count. No novelty guarantee." + }, + "unrun": [ + "Million-bit radix64 word", + "All-size factor preparation", + "Full predecessor PR1054 test suite", + "Full selected supplier cold replay", + "Hosted CI", + "Proof-assistant verification", + "Native/physical supplier integration" + ], + "ai_assistance": "Substantial OpenAI Codex / GPT-6 Astra assistance; no independent human review", + "checked_utc": "2026-10-13T21:52:58.221213+00:00" +} diff --git a/research/commuting-dirty-precision/VENDOR-PINS.json b/research/commuting-dirty-precision/VENDOR-PINS.json new file mode 100644 index 0000000000..332f2217f0 --- /dev/null +++ b/research/commuting-dirty-precision/VENDOR-PINS.json @@ -0,0 +1,81 @@ +{ + "sources": [ + { + "path": "vendor/pr1054/budget.py", + "source_path": "research/dirty-stride-precision/budget.py", + "commit": "6bc675be1554b3a3be771147f21f9dc2c6dae50a", + "sha256": "49538c697067525e5d4dc061c84f1e5cb5af459afd811b41663ee4607ba1fbc7", + "git_blob": "f90742b4d15b0e52861114889dc82f7063847087" + }, + { + "path": "vendor/pr1054/dirty_stride.py", + "source_path": "research/dirty-stride-precision/dirty_stride.py", + "commit": "6bc675be1554b3a3be771147f21f9dc2c6dae50a", + "sha256": "e2ebf6a2233901e116b8de6bcc8762aee0e0832098b194a112b51736f4ea9f21", + "git_blob": "7c8cdd77a47aedf58efa33256d506b3780738977" + }, + { + "path": "vendor/pr1054/PROOF.md", + "source_path": "research/dirty-stride-precision/PROOF.md", + "commit": "6bc675be1554b3a3be771147f21f9dc2c6dae50a", + "sha256": "11c23a39b91fe6acbda1d7f0e3aa640a983b106ac4733ae03530d79c952d6919", + "git_blob": "89cde9241919e479708146e07afe031fda100ea9" + }, + { + "path": "vendor/pr1054/NOTICE.md", + "source_path": "research/dirty-stride-precision/NOTICE.md", + "commit": "6bc675be1554b3a3be771147f21f9dc2c6dae50a", + "sha256": "d8059542dc8b2cebe6747a1334f2e03b97311dc4210d32b8f177c2ceb6b5c485", + "git_blob": "10dd84845b8b4ee59ee6eb315033028b04c6c239" + }, + { + "path": "vendor/pr1085/PROOF.md", + "source_path": "research/dirty-prefix-monomial-audit/PROOF.md", + "commit": "82b99c7d12dac009d35636562df4c6c91e885409", + "sha256": "b21febd8202b433f3f7c046e2c62e29c5772c8bee79327c51729d500c024a8b2", + "git_blob": "b794f4253b30f9af1d29c875097d04349715582b" + }, + { + "path": "vendor/pr1085/README.md", + "source_path": "research/dirty-prefix-monomial-audit/README.md", + "commit": "82b99c7d12dac009d35636562df4c6c91e885409", + "sha256": "15ddf36d0ebdfb6366661ddb1d895ccd445969158a9af9656cb6f891516be7e1", + "git_blob": "d71db72637bb22c204d521787d5c1c002930d7ec" + }, + { + "path": "vendor/pr1278/PROOF.md", + "source_path": "research/commuting-interval-audit/PROOF.md", + "commit": "06b8c006891ae78abe24b30d2fe9d8c188deafe8", + "sha256": "17d346b53eb71780410e1ec5e87d56bc444215a540e98c84283f12553c0c81e9", + "git_blob": "de9c8fca358c225e2ef30180c553717208015252" + }, + { + "path": "vendor/pr1278/NOTICE.md", + "source_path": "research/commuting-interval-audit/NOTICE.md", + "commit": "06b8c006891ae78abe24b30d2fe9d8c188deafe8", + "sha256": "e5d70a6492de305c914b1bd96b84506f6124c5fbfc3d09434ab241d1f4e2b438", + "git_blob": "b543c9e72463cb495ed380d5ded4c4235571483a" + }, + { + "path": "vendor/pr628/dirty.py", + "source_path": "research/dirty-stride-precision/vendor/pr985/vendor/pr628/dirty.py", + "commit": "6bc675be1554b3a3be771147f21f9dc2c6dae50a", + "sha256": "09e7f41141594e6540828330d27be27c083ee6569660ae42c0cd519b09fc8d21", + "git_blob": "2b9471083706a37519a1af7598e012f5fecf2636" + }, + { + "path": "vendor/pr628/NOTICE.md", + "source_path": "research/dirty-stride-precision/vendor/pr985/vendor/pr628/NOTICE.md", + "commit": "6bc675be1554b3a3be771147f21f9dc2c6dae50a", + "sha256": "abeacf1ad1491d5797cfcf1f3832799bbf3b24b99597229d7bc884059a51ec68", + "git_blob": "22fbeb8ef0a28dd6b3feea718492091319ceb96e" + }, + { + "path": "vendor/LICENSE", + "source_path": "LICENSE", + "commit": "dadfea6e8a78ff6ba901705f87532a71c6f5bbb8", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64" + } + ] +} diff --git a/research/commuting-dirty-precision/VERIFY.json b/research/commuting-dirty-precision/VERIFY.json new file mode 100644 index 0000000000..c365b8ae23 --- /dev/null +++ b/research/commuting-dirty-precision/VERIFY.json @@ -0,0 +1,20 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 300, + "checks": "Exact budgets, nonlinear literal word replays, source/receipt faults and read-only relocation." + } + ] +} diff --git a/research/commuting-dirty-precision/precision.py b/research/commuting-dirty-precision/precision.py new file mode 100644 index 0000000000..c34399ccaf --- /dev/null +++ b/research/commuting-dirty-precision/precision.py @@ -0,0 +1,91 @@ +"""Conditional commuting-factor budget; exact arithmetic, no supplier claim. +Philipp (@mightyOil), substantial OpenAI Codex assistance. Apache-2.0. +""" +from fractions import Fraction as F +from math import gcd, isqrt + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def clog(x): + x = F(x) + need(x > 0, 'positive logarithm') + k = x.numerator.bit_length() - x.denominator.bit_length() + return k + (x > F(2)**k) + + +def structure(n): + need(type(n) is int and n >= 1, 'positive factor count') + h = (n-1).bit_length() + q = 1 << (n.bit_length()-1) + return h, 3*q*n - 2*q*q, h+2 + + +def execute(n, r, beta, G, D, W): + need(all(type(x) in (int, F) for x in (r, beta, G, D)) + and r >= 1 and 0 < beta <= F(1, 2) and G >= 1 and D >= 0 + and type(W) is int and W >= 0, 'execution domain') + h, N, C = structure(n) + B, L = C*G, C*C*G + a = 68*(r+1)/beta**5 + u = F(1, 1 << W) + need(48*(clog(1/beta)+W.bit_length()+1)*u <= beta**3, + 'all-length admission') + t = N*L*a*u + need(t <= F(1, 2), 'feedback smallness') + return dict(leaf_calls=N, dirty_arrays=h, coefficient_mass=C, + prefix_bound=B, interval_bound=L, local_error=a, + feedback=t, boundary_magnitude=2*B*D+1, + error=2*t*(B*D+1), + internal_magnitude=1024*(r+1)*(r+2)*(B*D+1)/beta**8) + + +def choose(n, r, beta, G, D, p, incoming): + need(all(type(x) is int and x >= 0 for x in (p, incoming)), 'precision domain') + need(all(type(x) in (int, F) for x in (r, beta, G, D)) + and r >= 1 and 0 < beta <= F(1, 2) and G >= 1 and D >= 0, 'budget domain') + _, N, C = structure(n) + B, L, a = C*G, C*C*G, 68*(r+1)/beta**5 + W = max(incoming, 4*clog(1/beta)+16, + p+2+clog(N*L*a*(B*D+1))) + row = execute(n, r, beta, G, D, W) + row.update(working_bits=W, integer_bits=clog(row['internal_magnitude'])+2) + need(row['error'] <= F(1, 1 << (p+1)), 'execution error target') + return row + + +def prime_power(r): + if type(r) is not int or r < 3: + return False + p = next((j for j in range(2, isqrt(r)+1) if r % j == 0), r) + while r % p == 0: + r //= p + return r == 1 + + +def uniform(r, p, m, incoming): + need(prime_power(r), 'prime-power radix >= 3') + need(all(type(x) is int and x >= 0 for x in (p, m, incoming)), 'precision domain') + n = r-1 + h, N, C = structure(n) + ell = clog(r) + phi = sum(gcd(i, r) == 1 for i in range(1, r)) + d0 = 1+2*ell+r*n*phi + a0 = 2*d0+r+2 + g = d0+ell+2*r+2 + e = max(d0+1, a0+1, p+2*a0+m+4) + K, c = a0+2*r+ell, clog(C) + J, H = K+c, K+2*c + A = 5*g+clog(68*(r+1)) + W = max(incoming, 4*g+16, p+3+clog(N)+A+m+J+H) + I = J+m+8*g+2*ell+16 + return dict(radix=r, target_bits=p, magnitude_bits=m, incoming_bits=incoming, + factors=n, depth=h, leaf_calls=N, coefficient_mass=C, phi=phi, + circle_exponent=d0, inverse_exponent=a0, margin_exponent=g, + preparation_error_exponent=e, factor_bits=max(n*ell,e+r+3), + subset_exponent=K, coefficient_exponent=c, prefix_exponent=J, + interval_exponent=H, local_error_exponent=A, + working_bits=W, integer_bits=I) diff --git a/research/commuting-dirty-precision/test_package.py b/research/commuting-dirty-precision/test_package.py new file mode 100644 index 0000000000..ab02118893 --- /dev/null +++ b/research/commuting-dirty-precision/test_package.py @@ -0,0 +1,79 @@ +"""Bounded package replay, relocated read-only execution and actual corruptions.""" +import json +import os +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +HERE=Path(__file__).resolve().parent + +def call(directory,*args): + return subprocess.run([sys.executable,'-I','-O','-B',str(directory/'verify.py'),*map(str,args)], + cwd=directory.parent,text=True,capture_output=True,timeout=120) + +class Package(unittest.TestCase): + def test_full_replay(self): + result=call(HERE) + self.assertEqual(result.returncode,0,result.stdout+result.stderr) + self.assertIn('PASS_COMMUTING_DIRTY_PRECISION',result.stdout) + print(result.stdout.strip()) + + def test_readonly_relocation_and_receipt_fault(self): + with tempfile.TemporaryDirectory(prefix='commuting precision ') as temp: + package=Path(temp)/'package with spaces';shutil.copytree(HERE,package) + for f in package.rglob('*'): + if f.is_file():f.chmod(0o444) + result=call(package) + self.assertEqual(result.returncode,0,result.stdout+result.stderr) + receipt=package/'CERTIFICATE.json';receipt.chmod(0o644) + value=json.loads(receipt.read_text());value['budgets']['comparison'][5]['new_fractional']-=1 + receipt.write_text(json.dumps(value)) + result=call(package) + self.assertNotEqual(result.returncode,0) + self.assertIn('certificate mismatch',result.stderr) + + def test_source_drift(self): + with tempfile.TemporaryDirectory() as temp: + package=Path(temp)/'p';shutil.copytree(HERE,package) + source=package/'vendor/pr1054/dirty_stride.py' + source.write_text(source.read_text()+'\n# drift\n') + result=call(package) + self.assertNotEqual(result.returncode,0) + self.assertIn('source SHA256',result.stderr) + + def test_missing_proof(self): + with tempfile.TemporaryDirectory() as temp: + package=Path(temp)/'p';shutil.copytree(HERE,package) + (package/'vendor/pr1278/PROOF.md').unlink() + result=call(package) + self.assertNotEqual(result.returncode,0) + self.assertIn('FileNotFoundError',result.stderr) + + def test_changed_interval_exponent(self): + with tempfile.TemporaryDirectory() as temp: + package=Path(temp)/'p';shutil.copytree(HERE,package) + src=package/'precision.py';text=src.read_text() + self.assertEqual(text.count('J, H = K+c, K+2*c'),1) + src.write_text(text.replace('J, H = K+c, K+2*c','J, H = K+c, 2*c')) + result=call(package) + self.assertNotEqual(result.returncode,0) + self.assertIn('transport exponents',result.stderr) + + def test_changed_inverse_guard(self): + with tempfile.TemporaryDirectory() as temp: + package=Path(temp)/'p';shutil.copytree(HERE,package) + src=package/'precision.py';text=src.read_text() + self.assertEqual(text.count('I = J+m+8*g+2*ell+16'),1) + src.write_text(text.replace('I = J+m+8*g+2*ell+16','I = J+m+7*g+2*ell+16')) + result=call(package) + self.assertNotEqual(result.returncode,0) + self.assertIn('inverse preimage guard',result.stderr) + +if __name__=='__main__': + suite=unittest.defaultTestLoader.loadTestsFromTestCase(Package) + result=unittest.TextTestRunner(verbosity=2).run(suite) + if not result.wasSuccessful():raise SystemExit(1) + print('PASS_COMMUTING_DIRTY_PRECISION_PACKAGE tests=6 relocation=1 corruptions=5') diff --git a/research/commuting-dirty-precision/vendor/LICENSE b/research/commuting-dirty-precision/vendor/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/commuting-dirty-precision/vendor/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/research/commuting-dirty-precision/vendor/pr1054/NOTICE.md b/research/commuting-dirty-precision/vendor/pr1054/NOTICE.md new file mode 100644 index 0000000000..10dd84845b --- /dev/null +++ b/research/commuting-dirty-precision/vendor/pr1054/NOTICE.md @@ -0,0 +1,46 @@ +# Source credit and scope + +Prepared for Ali Romman (@aliromman) with substantial OpenAI Codex +assistance. One assigned research agent prepared this package in the +eight-contribution sprint. The coordinator reviews it separately. No +independent human review or formal verification is claimed. + +The new work proves the effective-depth and zero-subtree transfer for +PR985's actual constant-coefficient dirty word. It also transfers the +common-operator prefix estimate to that target-dependent rounded word, +with explicit inverse-preimage magnitude guards, exact budgets, and +supporting checks. The code changes precision admission in the leaf and +caches two validation reads. The simultaneous phase lane found the +duplicate-read accounting mismatch with an independent array observer. +That finding is credited here; the rounded data word does not change. +The source and test files are under the repository's Apache-2.0 license. + +Credit the following predecessor contributions: + +- Ali Romman, PR985, for source-prefix closure reuse, reversible block + transport on two tapes, the target-dependent rounded leaf, and its + local accuracy and complete cost proof. Its complete package is + retained unchanged in `vendor/pr985/`. +- Chafik Boukhalfa (@chafreaky), PR905, for the free-algebra prefix lemma + and its use with the common-operator subset bound in a dirty word. +- Chafik Boukhalfa, PR862, for the complementary-factor/common-isometry + estimate and cubic analytic preparation budgets. +- Chafik Boukhalfa, PR977, for effective-depth analysis of PR846's + clean-scratch solver. Its source is retained for comparison. Its + clean-scratch identity is not used as a dirty-word theorem. +- Rohan Guliani, PR846, for the Euclidean chain and closure decomposition. +- Chafik Boukhalfa, PR628, for certified kernel factors and the balanced + dirty commutator. Gareth Davidson (@bitplane), PR877, for the nonlinear + prefix perturbation method. 0xkilgore, PR663, for the exact leaf count + and restoration audit. Charles Bethin, PR764, for the shared-suffix + estimate. Ali Romman, PR621, for the retained kernel proof lineage. + +All retained notices remain in place. `SOURCES.json` gives the exact +heads, source paths, Git blobs, and SHA256 values. The proof identifies +which claims are inherited and which implications this package adds. +No priority claim is made for the classical Mahler-measure, Neumann, +variation-of-constants, or approximate-factorization methods. + +The result does not change the selected bound. It does not implement +variable site phases, a new transport scheme, a Lean proof, a fast +arithmetic compiler, a complete transform, or a multiplication reduction. diff --git a/research/commuting-dirty-precision/vendor/pr1054/PROOF.md b/research/commuting-dirty-precision/vendor/pr1054/PROOF.md new file mode 100644 index 0000000000..89cde92419 --- /dev/null +++ b/research/commuting-dirty-precision/vendor/pr1054/PROOF.md @@ -0,0 +1,338 @@ +# Cubic precision for the constant-coefficient dirty stride word + +## Result and fixed interface + +This result applies to PR985 at +`9df42a99dd8497b6e7d46cd2507bb89071372640`. The unchanged source is in +`vendor/pr985/`. The new `dirty_stride.py` changes the precision admission, +adds its effective-depth formula, and caches two validation reads. It retains every rounded +operation, recursive child, block swap, coefficient computation, and head +return. In particular, it does not add an early exit or a clean data array. + +The two validation loops now read each datum once, check that cached value, +and discard it. PR985's Python expression read the same entry twice while +charging one access. The simultaneous phase lane found that mismatch with +an independent array observer. The derived source corrects it without a +new data operation or a changed validation result. An observer separate +from the meter checks every literal indexed read and write in the new +leaf and kernel executions. The original source remains unchanged. + +Let `u=2^-W`, `0=4g+16` implies (1) at every length and stride. The +unscaled leaf error remains `64 (X+1) u / beta^5` for source norm at most +`X`. For a multiplier with modulus at most `R>=1`, it is at most + + [64 R (X+1)/beta^5 + 3] u. (2) + +For the inherited certified prime-power kernels, the complete balanced +dirty word has sufficient fractional precision + + W <= max(p,w_input) + m + 18r^3, + +where every initial array has norm at most `2^m`. A sufficient signed +integer reserve per component is at most `m+15r^3`. The bound applies to +both signs of the word. Exact source and scratch restoration, two data +tapes, the logarithmic borrowed-array count, and the full PR985 movement +bill remain. No new multiplication exponent follows. + +## 1. Extinction for the coefficients that PR985 computes + +At a normalized non-base level, `0M`, that level cannot +occur. Reversal changes orientation but does not change these counts. + +PR985 computes each coefficient afresh as `power(b,e,W)`. It does not +multiply a stored array of child coefficients. Its binary powering +truncates both components toward zero after each product. Truncation +cannot increase complex modulus. Induction over the multiplication tree +therefore gives + + |power(b,e,W)| <= |b|^e. + +For `e>=2`, the returned number is on the grid of spacing `u`; the final +operation includes truncation. At level `k>=D_eff`, + + beta e >= 2^-g 2^k >= W+1, + |b|^e <= (1-beta)^e <= exp(-beta e) + <= exp(-(W+1)) < 2^-W. + +The last inequality is strict, also when `W=0`. Since `g>=1`, these +levels have `e>=2`. Each component of the returned grid number thus has +absolute value below one grid unit and must be zero. This proof uses +complex modulus and the actual truncation rule. It does not assume a +positive real coefficient, a dyadic root descriptor, or monotonicity of +individual rounded powers. Every descendant meets the same bound. The +terminal cycle exponent is also at most `M` and meets the lower bound. + +## 2. The full dirty zero subtree + +Consider a subtree in which the two prepared coefficients at every level, +including every diagonal coefficient, are zero. A causal map with zero +coefficient is the identity on both arrays. Its physical implementation +still makes all the prescribed swaps, but only permutes values temporarily. +An expansion is a causal inverse, a zero injection, and a causal map. +It is the identity, including when its target contains arbitrary data. + +At a non-base node, the closure calls are consequently adjacent inverse +maps after the identity expansions are removed. The first call adds its +result to the source prefix; the inverse sees the exact state that the +first call left. Both calls restore their tail input. The pair cancels +exactly. The baseline addition is the only remaining operation. At a +diagonal node, division by one and grid rounding leave the source value +unchanged. Thus, with the internal multiplier one, the whole subtree is +exactly `y += sign*x`. Both signs satisfy the identity. This is an +induction on the actual dirty word, not a use of PR977's clean-scratch +identity and not an assumption of target-independent rounding elsewhere. + +The identity also has an internal magnitude bound. Let the incoming source +and target norms be at most `S` and `T`. Each recursive source is an +unchanged tail of its caller's source. Its target is a disjoint prefix of +that source. No recursive source includes an already changed connector. +Each temporary connector therefore contains at most the sum of two +source values, with norm at most `2S`. The outer target has norm at most +`T+S`. The inverse sign has the same bound. All other data movement is +swaps. The peak in the entire zero subtree is at most + + max(T+S, 2S), + +independently of its structural depth. Endpoint equality alone would not +have proved this internal bound. + +For the accuracy proof only, replace each subtree at depth `D_eff` by +its exact addition. This preserves the complete rounded output. There +are now at most `min(K,D_eff)` active non-base levels. PR985's power +error, shared-suffix, coefficient mismatch, and weighted source estimates +apply to those levels without any change. The new terminal has zero +error, which satisfies the former terminal allowance `u`. Beyond the +cutoff, the actual source causal maps are identities; their weighted +source bound does not accumulate more error. The preceding magnitude +lemma also controls all data in the untruncated zero tail. This proves +(1), (2), and the use of PR985's internal forward-leaf bound below. + +No runtime subtree is removed. The structural depth, recursive call +count, two-tape movement, metadata stack, and coefficient preparation +still have their original costs. + +## 3. A length-independent sufficient threshold + +For fixed `g`, `(D_eff+1)2^-W` decreases as integer `W` increases: the +ceiling logarithm increases by at most one at a step, while the power of +two doubles. It is enough to check `W0=4g+16`. For `g>=1`, + + 4g+17 <= 2^(g+5), + D_eff(W0)+1 <= 2g+6 <= 8*2^(g-1), + 48(D_eff(W0)+1) <= 192*2^g <= 2^(g+16). + +As `beta>=2^-g`, this proves `48(D_eff+1)2^-W<=beta^3`. The first two +elementary inequalities hold at `g=1` and persist after incrementing +`g`: each right side doubles and each left side grows by at most four. + +The executable admission uses (1), which can be weaker than this simple +threshold. For example, `beta=1/2`, `W=12`, `L=5741`, `w=2378` has +`K=10` and `D_eff=5`. The original admission fails and (1) holds. The +checker executes the full rounded word on this case, checks its residual +and exact inverse, and charges every data movement. A residual check is +numerical evidence for this one input; the preceding proof covers all +lengths. + +## 4. Transfer to the actual target-dependent kernel leaves + +Let `U=tau Z_L^w`, with one immutable unit scalar `tau` shared by all +factors. Let `Q(z)=r^-1 product_j(z-rho_j)`, of degree `n=r-1`. +The outer leaf has coefficient `tau/rho_j` and multiplier `-1/rho_j`. +The inner leaf has coefficient `rho_j conjugate(tau)`, stride `-w`, +multiplier `conjugate(tau)`, and output shift `-w`. Both ideal maps are +`(U-rho_j I)^-1`. Exactly one factor also has scale `r`. These are the +maps in PR985's unchanged dispatcher, and all use the same `U`. + +Let `||Q||_1<=M_Q` and `||Q(U)^-1||<=H_Q`. PR862's complementary-factor +argument gives a norm bound for every subset of the scaled factors: + + G = max(1, r 2^n M_Q H_Q). (3) + +Indeed `product max(1,|rho_j|)<=||rQ||_1<=r M_Q` by the elementary +Mahler-measure inequality. A complementary polynomial has coefficient +norm at most `2^n r M_Q`. Multiplication by `Q(U)^-1/r` bounds the +unscaled subset inverse, and the one factor `r` is then paid. The same +unit isometry must occur in all factors; this is not a bound for +arbitrary unrelated operators. + +Use PR905's free-algebra prefix lemma for the balanced four-call word. +With `h=ceil(log2 n)`, every ideal prefix and inverse prefix has +coefficient row sum at most `C=2*3^h`, and each monomial uses a strictly +decreasing subset of factor occurrences. Its proof includes both signs +of every child word. It depends on the ideal shear word, not on the +implementation of a rounded leaf. PR985's ideal dispatcher is exactly +that word. Equation (3) therefore gives + + B = C G + +for every ideal prefix and inverse prefix, and `B^2` for every interval +propagator. The retained PR905 proof gives the universal induction. The +new contribution here is the transfer to the PR985 leaf contract and its +physical word, not a new prefix lemma. + +For a positive PR985 leaf, (2) implies error at most + + a u (||source||+1), a=68(r+1) beta^-5. (4) + +For a negative leaf, write its input target as `y` and its output as +`z`. Exact inversion of the positive word gives + + y = z + A x + delta(x,z), + z = y - A x - delta(x,z). + +The source is unchanged. The positive bound (4) holds for every target +`z`, without a target magnitude hypothesis. Thus the negative leaf has +the same error bound with the same source norm. No bound on the unknown +preimage target is used for this accuracy step. Its magnitude is paid +separately in Section 5. + +Let all initial arrays have norm at most `D0`. The exact leaf count is +`N=3qn-2q^2<=2n^2`, with `q=2^floor(log2 n)`. Let `T` be the largest +actual joint norm at complete leaf boundaries. Every computed prefix is +finite because all closure denominators have modulus at least `beta`. +Insert the actual nonlinear errors into the ideal word by variation of +constants. For either sign, the prefix bounds and (4) give + + T <= B D0 + t(T+1), t=N B^2 a u. + +If `t<=1/2`, then `T<=2 B D0+1`, and the final execution error is at most + + 2 N B^2 a u (B D0+1). (5) + +This argument uses neither linearity nor target independence of a rounded +call. Each closure and each whole-word inverse is still the exact inverse +grid word. Distinct ancestor operands and the original scratch-depth +condition remain required by the implementation. + +## 5. Integer guards, including inverse preimages + +At a leaf boundary put `D*=2 B D0+1`. PR985's forward-leaf bound is + + 512 (r+1)(D*+1)/beta^7. + +Section 2 justifies the same bound in the full zero tails. To apply it +inside an inverse leaf, first bound that leaf's positive preimage. Its +source has norm at most `D*`, and its ideal operator has norm at most +`r/beta`. Since `a u<=1` follows from `t<=1/2`, the preimage target has +norm at most + + D_pre <= (2+r/beta)D*+1. + +The inverse traverses the positive word at this preimage in reverse. +Use `D_pre+1<=(r+2)(D*+1)/beta` in the forward bound. A bound for every +data value, in either sign of every leaf, is consequently + + V = 1024 (r+1)(r+2)(B D0+1)/beta^8. (6) + +Two extra bits above `ceil(log2 V)` suffice for a signed component +reserve. This extra preimage factor is necessary in this proof; the +incoming negative target was not assumed to obey the forward preimage +bound. Block transport only moves these values and adds no new magnitude. + +## 6. Explicit prime-power budgets + +Retain the PR621/628/862 analytic and supplied factor-preparation +hypotheses. Let `r>=3` be a prime power, `n=r-1`, `ell=ceil(log2 r)`, +`h=ceil(log2 n)`, `phi=EulerPhi(r)`, and `D0<=2^m`, `m>=0`. Define + + d0 = 1+2ell+r n phi, + a0 = 2d0+r+2, + g = d0+ell+2r+2, beta=2^-g, + e = max(d0+1,a0+1,p+2a0+m+4), + b_factor = max(n ell,e+r+3). + +The original inverse has norm at most `2^a0`. The supplied dyadic-root +polynomial `Q` has coefficient error at most `2^-e`, norm at most `2^r`, +and stable factor margin `beta`. The common-isometry Neumann argument +gives `||Q(U)^-1||<=2^(a0+1)`. On a source of norm at most `2^m`, the +original-versus-prepared inverse error is at most `2^(-p-3)`. These are +inherited hypotheses and algorithms; this package does not implement +an all-size root factorizer. + +Equations (3)--(6) are paid by the integer exponents + + J = a0+2r+ell+1+2h, + A = 5g+ceil(log2(68(r+1))), + W = max(w_input,4g+16,p+3+ceil(log2 N)+A+m+3J), + I = J+m+8g+2ell+16. + +Here `B<=2^J`, `a<=2^A`, and `B D0+1<=2^(J+m+1)`. Thus (5) is at +most `2^(-p-1)`, with `t<=1/2`. Admission follows from Section 3. The +bound (6), plus a sign reserve, is below `2^I`. No incoming grid is +coarsened. Preparation plus execution error is below `2^-p`. + +For completeness, use `phi,ell,h<=r`, +`ceil(log2 N)<=1+2h`, and `ceil(log2(68(r+1)))<=ell+8`. The fractional +overhead is at most + + 11r^3-11r^2+58r+42 <= 18r^3. + +The difference is `(r-3)(7r^2+32r+38)+72`. The term `4g+16` is smaller +than this same majorant. Likewise + + I-m <= 10r^3-10r^2+52r+45 <= 15r^3, + +with difference `(r-3)(5r^2+25r+23)+24`. The inherited factor width obeys +`b_factor<=p+m+7r^3`. These polynomial identities prove the all-size +bounds; the finite budget rows check their implementation. + +At `r=64`, `p=128`, `m=20`, and `w_input=0`, the fractional budget is +`1,420,902` bits. PR985's full-word bound with the same margin and initial +norm needs `517,236,859` bits before any larger structural-depth admission. +Both words have `4,000` leaf calls and six borrowed arrays. These are +sufficient bounds, not optimal widths or measured execution times. + +## 7. Complete cost and scope + +Every leaf still uses two data arrays, a constant number of clean complex +arithmetic registers, and `O(log^2 L)` integer metadata bits. PR985 proves +at most `1280L` scalar products and divisions and `4096L` record moves +per leaf, including the complete structural recursion and returns. The +kernel retains `h` arbitrary dirty arrays and routes all of them over +two physical tapes. Its unchanged bound is + + 8192 (N+1)(h+2)L + +data-record moves. The effective depth is only for error analysis. It +must not replace structural depth in these resource counts. + +Let `A_word=W+I` and let `B_desc` include the actual immutable root, +margin, multiplier, and unit-gauge descriptor lengths. Let `M(s)` pay +for rounded multiplication and division of words of width `s`. The bill +remains + + preparation + O(N L M(A_word+B_desc)) + + O(N(h+2)L(A_word+B_desc)) + O(NL). + +The last term pays the inherited integer-control bound. Reading a stride +descriptor longer than `O(log L)` is additional input work. The supplied +preparation bill is `soft-O(r^3(p+m+r^3))` under the retained algorithms. +An arbitrarily long exact gauge description remains an extra charge. +There is no new coefficient array, tape, or borrowed data allocation. + +This is a written accuracy proof with exact-rational supporting checks. +It is not a Lean proof, a fast arithmetic compiler, a measured runtime +gain, a variable-site-phase construction, a complete transform, or a +multiplication reduction. The selected certificate and `upstream/` do +not change. Source credit and substantial AI assistance are in `NOTICE.md`. diff --git a/research/commuting-dirty-precision/vendor/pr1054/budget.py b/research/commuting-dirty-precision/vendor/pr1054/budget.py new file mode 100644 index 0000000000..f90742b4d1 --- /dev/null +++ b/research/commuting-dirty-precision/vendor/pr1054/budget.py @@ -0,0 +1,120 @@ +"""Precision bounds for the constant-coefficient PR985 word. + +The common-operator hypotheses are mathematical inputs. See PROOF.md. +""" +from fractions import Fraction as F +from math import gcd, isqrt + + +def need(ok, label): + if not ok: + raise ValueError(label) + + +def ceil_log2(value): + value = F(value) + need(value > 0, 'positive logarithm') + k = value.numerator.bit_length() - value.denominator.bit_length() + return k + (value > F(2)**k) + + +def prime_power(r): + if type(r) is not int or r < 3: + return False + p = next((d for d in range(2, isqrt(r)+1) if r % d == 0), r) + while r % p == 0: + r //= p + return r == 1 + + +def resources(count): + need(type(count) is int and count >= 1, 'positive factor count') + h = (count-1).bit_length() + q = 1 << (count.bit_length()-1) + return h, 3*q*count-2*q*q, 2*3**h + + +def execution(count, scale, beta, subset_bound, initial_bound, bits): + """Bound both signs of the complete rounded dirty word.""" + need(type(bits) is int and bits >= 0 and scale >= 1 + and 0 < beta <= F(1, 2) and subset_bound >= 1 + and initial_bound >= 0, 'execution domain') + h, calls, mass = resources(count) + prefix = mass*subset_bound + local = 68*(scale+1)/beta**5 + unit = F(1, 1 << bits) + g = ceil_log2(1/beta) + active = g+bits.bit_length() + need(48*(active+1)*unit <= beta**3, 'all-length admission') + feedback = calls*prefix**2*local*unit + need(feedback <= F(1, 2), 'feedback smallness') + boundary = 2*prefix*initial_bound+1 + peak = 1024*(scale+1)*(scale+2)*(prefix*initial_bound+1)/beta**8 + return dict(leaf_calls=calls, dirty_arrays=h, prefix_bound=prefix, + effective_depth=active, local_error_coefficient=local, + feedback=feedback, boundary_magnitude=boundary, + internal_magnitude=peak, + error=2*feedback*(prefix*initial_bound+1)) + + +def choose(count, scale, beta, subset_bound, initial_bound, target_bits, incoming_bits): + """Choose sufficient precision without a length or stride input.""" + need(all(type(v) is int and v >= 0 for v in (target_bits, incoming_bits)), + 'integer precision') + need(scale >= 1 and 0 < beta <= F(1, 2) and subset_bound >= 1 + and initial_bound >= 0, 'budget domain') + _, calls, mass = resources(count) + prefix = mass*subset_bound + local = 68*(scale+1)/beta**5 + bits = max(incoming_bits, 4*ceil_log2(1/beta)+16, + target_bits+2+ceil_log2(calls*prefix**2*local*(prefix*initial_bound+1))) + result = execution(count, scale, beta, subset_bound, initial_bound, bits) + need(result['error'] <= F(1, 1 << (target_bits+1)), 'execution target') + result['working_bits'] = bits + result['integer_bits'] = ceil_log2(result['internal_magnitude'])+2 + return result + + +def uniform(r, target_bits, magnitude_bits, incoming_bits): + """Use the inherited prime-power preparation bounds as exponents.""" + need(prime_power(r), 'prime-power radix >=3') + need(all(type(v) is int and v >= 0 for v in + (target_bits, magnitude_bits, incoming_bits)), 'integer precision') + n = r-1 + h, calls, mass = resources(n) + ell = (r-1).bit_length() + phi = sum(gcd(j, r) == 1 for j in range(1, r)) + d0 = 1+2*ell+r*n*phi + a0 = 2*d0+r+2 + g = d0+ell+2*r+2 + e = max(d0+1, a0+1, target_bits+2*a0+magnitude_bits+4) + factor_bits = max(n*ell, e+r+3) + prefix = a0+2*r+ell+1+2*h + local = 5*g+ceil_log2(68*(r+1)) + bits = max(incoming_bits, 4*g+16, + target_bits+3+ceil_log2(calls)+local+magnitude_bits+3*prefix) + integer = prefix+magnitude_bits+8*g+2*ell+16 + return dict(radix=r, target_bits=target_bits, magnitude_bits=magnitude_bits, + incoming_bits=incoming_bits, factors=n, depth=h, leaf_calls=calls, + coefficient_mass=mass, phi=phi, circle_exponent=d0, + inverse_exponent=a0, margin_exponent=g, + preparation_error_exponent=e, factor_bits=factor_bits, + prefix_exponent=prefix, local_error_exponent=local, + working_bits=bits, integer_bits=integer) + + +def check_uniform(row): + """Check a supplied exponent certificate with exact integer bounds.""" + need(all(type(v) is int for v in row.values()), 'integer certificate') + r, p, m, incoming = (row[k] for k in + ('radix', 'target_bits', 'magnitude_bits', 'incoming_bits')) + need(row == uniform(r, p, m, incoming), 'certificate fields') + w, g, j, a, calls = (row[k] for k in + ('working_bits', 'margin_exponent', 'prefix_exponent', + 'local_error_exponent', 'leaf_calls')) + need(w >= incoming and w >= 4*g+16, 'input grid and all-length admission') + exponent = w-p-m-3*j-a-3 + need(exponent >= 0 and calls <= 1 << exponent, 'execution exponent') + need(w <= max(p, incoming)+m+18*r**3, 'fractional cubic bound') + need(row['integer_bits'] <= m+15*r**3, 'integer cubic bound') + need(row['factor_bits'] <= p+m+7*r**3, 'preparation cubic bound') diff --git a/research/commuting-dirty-precision/vendor/pr1054/dirty_stride.py b/research/commuting-dirty-precision/vendor/pr1054/dirty_stride.py new file mode 100644 index 0000000000..7c8cdd77a4 --- /dev/null +++ b/research/commuting-dirty-precision/vendor/pr1054/dirty_stride.py @@ -0,0 +1,422 @@ +"""Add a cyclic inverse to a target and restore the source exactly. + +This extends PR985 at 9df42a99dd8497b6e7d46cd2507bb89071372640. +The precision admission and two validation reads change. The rounded word +and its two-tape movement are unchanged. See PROOF.md for the bounds. +""" +from dataclasses import dataclass, field +from fractions import Fraction as F +from math import gcd + +ZERO = (F(0), F(0)) +ONE = (F(1), F(0)) + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def add(a, b): + return (a[0] + b[0], a[1] + b[1]) + + +def sub(a, b): + return (a[0] - b[0], a[1] - b[1]) + + +def mul(a, b): + return (a[0]*b[0] - a[1]*b[1], a[0]*b[1] + a[1]*b[0]) + + +def norm2(a): + return a[0]*a[0] + a[1]*a[1] + + +def div(a, b): + d = norm2(b) + need(d != 0, 'zero divisor') + v = mul(a, (b[0], -b[1])) + return (v[0]/d, v[1]/d) + + +def rnd(a, bits): + """Use nearest dyadic rounding, with ties toward positive infinity.""" + scale = 1 << bits + def component(v): + t = v*scale + F(1, 2) + return F(t.numerator // t.denominator, scale) + return (component(a[0]), component(a[1])) + + +def trunc(a, bits): + """Truncate each component toward zero. This cannot increase the norm.""" + scale = 1 << bits + return tuple(F(int(v*scale), scale) for v in a) + + +@dataclass +class Meter: + reads: int = 0 + writes: int = 0 + tape_moves: int = 0 + products: int = 0 + power_products: int = 0 + divisions: int = 0 + nodes: int = 0 + leaves: int = 0 + validation_reads: int = 0 + max_depth: int = 0 + heads: dict = field(default_factory=dict) + layout: dict = field(default_factory=dict) + + def access(self, data, index, write=False): + tape, start = self.layout[id(data)] + position = start+index + self.tape_moves += abs(position - self.heads.get(tape, 0)) + 1 + self.heads[tape] = position + if write: + self.writes += 1 + else: + self.reads += 1 + + def rewind(self): + for tape, position in self.heads.items(): + self.tape_moves += position + self.heads[tape] = 0 + + +@dataclass(frozen=True) +class View: + data: list + start: int + step: int + length: int + meter: Meter + + def index(self, i): + need(0 <= i < self.length, 'view index') + return (self.start + self.step*i) % len(self.data) + + def get(self, i): + j = self.index(i) + self.meter.access(self.data, j) + return self.data[j] + + def put(self, i, value): + j = self.index(i) + self.meter.access(self.data, j, True) + self.data[j] = value + + def part(self, first, length): + need(0 <= first and first + length <= self.length, 'view interval') + return View(self.data, self.start + self.step*first, self.step, length, self.meter) + + def reverse(self): + return View(self.data, self.start + self.step*(self.length-1), + -self.step, self.length, self.meter) + + +def depth(length, stride): + count = 0 + while True: + stride %= length + stride = min(stride, length-stride) + if stride == 0: + return count + length, stride = stride, (-length) % stride + count += 1 + + +def effective_depth(beta, bits): + """Bound the nonzero levels of the unchanged rounded word.""" + need(0 < beta <= F(1, 2) and type(bits) is int and bits >= 0, + 'effective depth domain') + return ceil_log2(1/beta) + bits.bit_length() + + +def admitted(beta, bits, levels): + if not (type(bits) is int and bits >= 0 and type(levels) is int + and levels >= 0 and 0 < beta <= F(1, 2)): + return False + active = min(levels, effective_depth(beta, bits)) + return 48*(active+1)*F(1, 1 << bits) <= beta**3 + + +def power(b, exponent, bits, meter): + """Use a left-to-right binary product and scalar working storage.""" + need(exponent >= 1, 'positive exponent') + result = b + for k in range(exponent.bit_length()-2, -1, -1): + result = trunc(mul(result, result), bits) + meter.power_products += 1 + if (exponent >> k) & 1: + result = trunc(mul(result, b), bits) + meter.power_products += 1 + return result + + +@dataclass(frozen=True) +class Geometry: + root: tuple + divisor: int + cycle: int + inverse: int + bits: int + meter: Meter + + def exponents(self, length, stride, orientation): + if stride == 0: + return (self.cycle, self.cycle) + def exponent(displacement): + need(displacement % self.divisor == 0, 'cycle lattice') + return ((displacement // self.divisor)*self.inverse) % self.cycle or self.cycle + return (exponent(orientation*stride), exponent(orientation*(stride-length))) + + def coefficients(self, length, stride, orientation): + a, b = self.exponents(length, stride, orientation) + left = power(self.root, a, self.bits, self.meter) + right = left if a == b else power(self.root, b, self.bits, self.meter) + return (left, right) + + +def emit(target, i, value, multiplier, sign, bits): + if multiplier != ONE: + target.meter.products += 1 + value = rnd(mul(multiplier, value), bits) + old = target.get(i) + target.put(i, add(old, value) if sign == 1 else sub(old, value)) + + +def swap(source, target): + for i in range(source.length): + left, right = source.get(i), target.get(i) + source.put(i, right) + target.put(i, left) + + +def causal(source, carrier, stride, geometry, undo=False): + """Apply the causal lifts with block swaps; restore the dirty carrier.""" + a, _ = geometry.coefficients(source.length, stride, source.step) + n = source.length + if undo: + swap(source, carrier) + for first in range(((n-1)//stride)*stride, -1, -stride): + size = min(stride, n-first) + swap(source.part(first, size), carrier.part(first, size)) + if first: + for i in range(first+size-1, first-1, -1): + value = rnd(mul(a, carrier.get(i-stride)), geometry.bits) + geometry.meter.products += 1 + source.put(i, sub(source.get(i), value)) + else: + for first in range(0, n, stride): + size = min(stride, n-first) + if first: + for i in range(first, first+size): + value = rnd(mul(a, carrier.get(i-stride)), geometry.bits) + geometry.meter.products += 1 + source.put(i, add(source.get(i), value)) + swap(source.part(first, size), carrier.part(first, size)) + swap(source, carrier) + + +def expand(source, target, stride, geometry, multiplier, sign): + """Conjugate the seed injection by exact inverse causal grid maps.""" + causal(target, source, stride, geometry, undo=True) + _, b = geometry.coefficients(source.length, stride, source.step) + coefficient = mul(multiplier, b) + geometry.meter.products += 1 + for i in range(stride): + value = rnd(mul(coefficient, source.get(i)), geometry.bits) + geometry.meter.products += 1 + emit(target, i, value, ONE, sign, geometry.bits) + causal(target, source, stride, geometry) + + +def closure(source, target, stride, geometry, sign, level): + """Move the child target to the other tape and restore the carrier.""" + borrowed = source.part(0, stride) + carrier = target.part(0, stride) + ends = source.part(source.length-stride, stride) + swap(borrowed, carrier) + solve(ends, carrier, (-source.length) % stride, geometry, sign=sign, level=level+1) + swap(borrowed, carrier) + + +def diagonal(source, target, geometry, multiplier, sign): + coefficient = power(geometry.root, geometry.cycle, geometry.bits, geometry.meter) + denominator = sub(ONE, coefficient) + for i in range(source.length): + value = rnd(div(source.get(i), denominator), geometry.bits) + geometry.meter.divisions += 1 + emit(target, i, value, multiplier, sign, geometry.bits) + + +def solve(source, target, stride, geometry, multiplier=ONE, sign=1, level=0): + """Use integer metadata at each level; scalar temporaries stay in helpers.""" + length = source.length + stride %= length + if 2*stride > length: + source, target, stride = source.reverse(), target.reverse(), length-stride + geometry.meter.nodes += 1 + geometry.meter.max_depth = max(geometry.meter.max_depth, level) + if stride == 0: + diagonal(source, target, geometry, multiplier, sign) + return + causal(source, target, stride, geometry) + if sign == 1: + for i in range(length): + emit(target, i, source.get(i), multiplier, 1, geometry.bits) + closure(source, target, stride, geometry, 1, level) + expand(source, target, stride, geometry, multiplier, 1) + closure(source, target, stride, geometry, -1, level) + expand(source, target, stride, geometry, multiplier, -1) + else: + expand(source, target, stride, geometry, multiplier, 1) + closure(source, target, stride, geometry, 1, level) + expand(source, target, stride, geometry, multiplier, -1) + closure(source, target, stride, geometry, -1, level) + for i in range(length): + emit(target, i, source.get(i), multiplier, -1, geometry.bits) + causal(source, target, stride, geometry, undo=True) + + +def lift(x, y, b, beta, bits, stride, sign=1, multiplier=ONE, shift=0, meter=None): + """Add multiplier*(I-b Z^stride)^-1 x at output indices i+shift.""" + need(type(stride) is int and type(shift) is int and type(sign) is int + and sign in (-1, 1), 'integer stride and sign') + need(x is not y and len(x) == len(y) and len(x) > 0, 'distinct equal arrays') + need(shift % len(x) in (0, stride % len(x)), 'output shift must be zero or the leaf stride') + need(isinstance(b, tuple) and len(b) == 2 and norm2(b) <= (1-beta)**2, 'stable constant coefficient') + need(isinstance(multiplier, tuple) and len(multiplier) == 2, 'constant multiplier') + need(admitted(beta, bits, depth(len(x), stride)), 'precision admission') + meter = meter if meter is not None else Meter() + if not meter.layout: + meter.layout = {id(x): (0, 0), id(y): (1, 0)} + need(id(x) in meter.layout and id(y) in meter.layout + and {meter.layout[id(x)][0], meter.layout[id(y)][0]} == {0, 1}, 'two distinct data tapes') + for data in (x, y): + for i in range(len(data)): + meter.access(data, i) + meter.validation_reads += 1 + datum = data[i] + need(rnd(datum, bits) == datum, 'fixed grid data') + del datum + divisor = gcd(len(x), stride) + cycle = len(x)//divisor + inverse = pow((stride//divisor) % cycle, -1, cycle) if cycle > 1 else 0 + geometry = Geometry(b, divisor, cycle, inverse, bits, meter) + solve(View(x, 0, 1, len(x), meter), View(y, shift, 1, len(y), meter), + stride, geometry, multiplier, sign) + meter.leaves += 1 + meter.rewind() + return meter + + +def leaf_bound(bound, beta, bits, multiplier_bound=1): + return (64*multiplier_bound*(bound+1)/beta**5 + 3)*F(1, 1 << bits) + + +def leaf_calls(count): + need(type(count) is int and count >= 1, 'positive factor count') + if count == 1: + return 1 + return 2*leaf_calls(count//2) + 2*leaf_calls(count-count//2) + + +def compose(x, y, factors, scratch, tau, beta, bits, stride, sign=1, meter=None): + """Use PR628's balanced dirty commutator with the new arbitrary-stride leaf.""" + need(factors and len(scratch) >= (len(factors)-1).bit_length(), 'dirty depth') + arrays = [x, y] + scratch + need(len({id(a) for a in arrays}) == len(arrays), 'all arrays distinct') + need(len(x) > 0 and all(len(a) == len(x) for a in arrays), 'array lengths') + need(isinstance(tau, tuple) and norm2(tau) == 1, 'immutable unit gauge') + need(type(sign) is int and sign in (-1, 1) and type(stride) is int, 'integer stride and sign') + need(admitted(beta, bits, depth(len(x), stride)), 'precision admission') + for factor in factors: + need(isinstance(factor, tuple) and len(factor) == 3, 'factor descriptor') + inside, b, scale = factor + need(type(inside) is bool and isinstance(b, tuple) and len(b) == 2 + and norm2(b) <= (1-beta)**2 and isinstance(scale, (int, F)), 'stable factor descriptor') + meter = meter if meter is not None else Meter() + if scratch: + layout = {id(a): (0, i*len(x)) for i, a in enumerate(arrays[:-1])} + layout[id(scratch[-1])] = (1, 0) + else: + layout = {id(x): (0, 0), id(y): (1, 0)} + need(not meter.layout or meter.layout == layout, 'kernel tape layout') + meter.layout = layout + for data in arrays: + for i in range(len(data)): + meter.access(data, i) + meter.validation_reads += 1 + datum = data[i] + need(rnd(datum, bits) == datum, 'fixed grid data') + del datum + def run(src, dst, lo, hi, level, direction): + if hi-lo == 1: + inside, b, scale = factors[lo] + phase = (tau[0], -tau[1]) if inside else tau + coefficient = mul(b, phase) + m = phase if inside else (-b[0], -b[1]) + m = (m[0]*scale, m[1]*scale) + if meter.layout[id(src)][0] == meter.layout[id(dst)][0]: + spare = scratch[-1] + destination = View(dst, 0, 1, len(dst), meter) + carrier = View(spare, 0, 1, len(spare), meter) + swap(destination, carrier) + lift(src, spare, coefficient, beta, bits, -stride if inside else stride, + direction, m, -stride if inside else 0, meter) + swap(destination, carrier) + else: + lift(src, dst, coefficient, beta, bits, -stride if inside else stride, + direction, m, -stride if inside else 0, meter) + return + mid = (lo+hi)//2 + z = scratch[level] + if direction == 1: + run(src, z, lo, mid, level+1, 1) + run(z, dst, mid, hi, level+1, 1) + run(src, z, lo, mid, level+1, -1) + run(z, dst, mid, hi, level+1, -1) + else: + run(z, dst, mid, hi, level+1, 1) + run(src, z, lo, mid, level+1, 1) + run(z, dst, mid, hi, level+1, -1) + run(src, z, lo, mid, level+1, -1) + run(x, y, 0, len(factors), 0, sign) + meter.rewind() + return meter + + +def ceil_log2(value): + value = F(value) + need(value > 0, 'positive logarithm') + k = value.numerator.bit_length() - value.denominator.bit_length() + power_of_two = F(2)**k + return k if value <= power_of_two else k+1 + + +def execution_bound(count, r, beta, initial_bound, bits): + need(r >= 1 and initial_bound >= 0 and 0 < beta <= F(1, 2) + and type(bits) is int and bits >= 0, 'execution budget domain') + calls = leaf_calls(count) + a = 68*(r+1)/beta**5 + growth = 2+F(r)/beta + need(a*F(1, 1 << bits) <= 1, 'execution precision') + return calls*a*(initial_bound+1)*F(1, 1 << bits)*growth**(calls-1) + + +def working_bits(count, r, beta, initial_bound, target_bits, incoming_bits, length, stride): + need(r >= 1 and initial_bound >= 0 and 0 < beta <= F(1, 2) + and type(target_bits) is int and target_bits >= 0 + and type(incoming_bits) is int and incoming_bits >= 0 + and type(length) is int and length > 0 and type(stride) is int, 'working budget domain') + calls = leaf_calls(count) + a = 68*(r+1)/beta**5 + growth = 2+F(r)/beta + levels = depth(length, stride) + return max(incoming_bits, target_bits+1+ceil_log2(calls*a*(initial_bound+1)) + +(calls-1)*ceil_log2(growth), ceil_log2(a), + ceil_log2(48*(levels+1)/beta**3)) diff --git a/research/commuting-dirty-precision/vendor/pr1085/PROOF.md b/research/commuting-dirty-precision/vendor/pr1085/PROOF.md new file mode 100644 index 0000000000..b794f4253b --- /dev/null +++ b/research/commuting-dirty-precision/vendor/pr1085/PROOF.md @@ -0,0 +1,145 @@ +# A sharp coefficient bound for the reserved-depth balanced word + +This sharpens the free-algebra lemma in Chafik Boukhalfa's PR905, using +the unchanged PR628 dispatcher. It does not change a rounded leaf, +borrowed-array allocation, or multiplication exponent. + +## Statement + +Let `A_0,...,A_(n-1)` be formal noncommuting operators, `n >= 1`. +Use the balanced split `floor(n/2), ceil(n/2)`, distinct source and target, +and one distinct dirty register per recursion depth. A positive node executes +`U,V,U^-1,V^-1` chronologically, where `U: z += B x`, `V: y += A z`, +and `B,A` are the ordered left and right products. Negative calls reverse +the complete instruction word. Every prefix ends at a complete ideal leaf +`target += sign A_j source`. + +Put `h = ceil(log2 n)`. Every entry of every prefix matrix and its inverse, +for either call direction, is zero or one signed monomial. Each nonempty +monomial has strictly decreasing factor indices. Therefore the coefficient +absolute row sum is at most **`h+2`**, replacing PR905's `2*3^h`. +The uniform constant is sharp, even for scalar identity factors. + +The source row and target column are identity. For a call of sign `s` and +full ordered product `T`, its target/source entry is either zero or `s T`; +the corresponding entry of an inverse prefix is zero or `-s T`. +These additional assertions are part of the induction. + +## Induction, including the cancellations + +The leaf case is immediate: its two prefixes are identity and one elementary +shear. Suppose all assertions hold for both children. A parent prefix is +`P = R C`, where `C` comprises completed children and `R` is a prefix of +the active child; hence `P^-1 = C^-1 R^-1`. Completed children restore +every deeper register. Write `T = A B`. Their outer states are: + +| Parent sign | Completed children | z after C | y after C | Active child | +|---|---:|---|---|---| +| + | 0 | z | y | left + | +| + | 1 | z+Bx | y | right + | +| + | 2 | z+Bx | y+Az+Tx | left - | +| + | 3 | z | y+Az+Tx | right - | +| - | 0 | z | y | right + | +| - | 1 | z | y+Az | left + | +| - | 2 | z+Bx | y+Az | right - | +| - | 3 | z+Bx | y-Tx | left - | + +Let the active child's sign be `t` and full product be `F`. By induction, +`R[target,source] = t e F` and `R^-1[target,source] = -t f F`, for +`e,f` in `{0,1}`. No relation between `e` and `f` is needed. Multiplication +gives the following parent endpoint coefficients, in units of `T`: + +| Parent sign | Completed children | P[y,x]/T | P^-1[y,x]/T | +|---|---:|---:|---:| +| + | 0 | 0 | 0 | +| + | 1 | e | 0 | +| + | 2 | 1 | -f | +| + | 3 | 1 | -1 | +| - | 0 | 0 | 0 | +| - | 1 | 0 | f | +| - | 2 | -e | 1 | +| - | 3 | -1 | 1 | + +Here is why no other entry hides a sum of distinct monomials. In a left +child, the source row `x` and target column `z` are identity. Right +multiplication by `C` can therefore add `Bx` only to row `z`; an existing +entry there is zero or `-B` in precisely the phases that add `B`. +The separate row `y` is fixed by the child. In `C^-1 R^-1`, a new parent +row `y` may contain `A` times the child's row `z`. Each of its entries is +one monomial; the only possible overlap with the other outer entries is +the endpoint governed by `f`. The remaining changed row `z` has the same +endpoint cancellation. + +For a right child, `x` is outside the child, its source row `z` is identity, +and its target column `y` is identity. Substitution of `z+Bx` in `R C` +adds a new column `x` by appending `B` to each occupied column-`z` entry. +This column was absent inside the child. Only row `y` can also receive +an outer contribution; the table and `e` control that collision. In +`C^-1 R^-1`, the identity source row leaves only the target/source +cancellation governed by `f`, and additions in the external column `x`. +All collisions thus give zero or a signed coefficient one, never two +different surviving monomials in one entry. Every new product prepends +the complete right product to a left monomial, or appends the complete +left product to a right monomial. The index sets are disjoint and ordered. + +The source row and target column remain identity because no instruction +writes the source or reads the target. The final boundary is the product +shear and satisfies the same assertions. This closes the induction for +both directions and inverse prefixes. The abstract eight-case checker +is supporting exact algebra, not the basis for extrapolation to all n. + +## Row bound and sharpness + +There are `h+2` registers: source, target, and `h` reserved dirty registers. +The entry invariant proves the row bound. To attain it, set every factor +to the scalar identity. Follow the first positive execution down the +rightmost branch. At each level the completed left child adds the current +source to the next connector. The first execution of the last factor then +adds all `h` original connector values and the original source to the +original target. Its row has exactly `h+2` positive coefficients. The +rightmost branch has height `h` because it repeatedly takes `ceil(n/2)`. +The receipt retains an explicit 74-factor, nine-term witness. + +If every ordered subset product of actual operators has norm at most +`G >= 1`, including the empty product, substitution gives + +``` +||P||, ||P^-1|| <= B = (h+2) G, +||P_j P_i^-1|| <= B^2. +``` + +No commutation is required for this implication. Obtaining the particular +small `G` used for cyclic inverses still requires PR905/PR862's common +immutable isometry and preparation hypotheses. The theorem concerns leaf +boundaries; internal leaf growth retains its separate inherited bound. + +## Consequence for the existing sufficient precision formula + +Keep PR905's definitions `a0, ell, Aerr, g, N, m, p` and all preparation +budgets. Its subset bound is `G <= 2^(a0+2r+ell)`. Replace only + +``` +J_old = a0+2r+ell+1+2h +J_new = a0+2r+ell+ceil(log2(h+2)). +w_new = max(w_input, Aerr, 2g+1, + p+3+ceil(log2 N)+Aerr+m+3J_new). +``` + +PR877/905's unchanged perturbation estimate is +`2 N B^2 a u (B D+1)`, provided `N B^2 a u <= 1/2`. +Here `B <= 2^J_new`, `a <= 2^Aerr`, `D <= 2^m`, and `u=2^-w_new`. +Since `B D+1 <= 2^(J_new+m+1)`, the displayed choice bounds execution +error by `2^(-p-1)` and ensures the feedback condition. The unchanged +coefficient perturbation allowance completes the inherited `2^-p` +budget. Initial finer grids and stable closure remain explicitly charged. + +At radix 64, `p=128`, `m=20`, and `w_input=0`, the source formula falls +from **1,162,553 to 1,162,523 fractional bits**. This is a sufficient-bound +comparison, not a measurement or an optimal-precision claim. Exact paid +leaf calls, logarithmic dirty storage, scalar/preparation/phase costs, +routing, and asymptotic cubic precision remain unchanged. No new rounded +kernel execution, compiler, physical hosting, transform, or multiplication +reduction is supplied. + +Proof and audit by Hanson Sun, with substantial OpenAI Codex assistance. +Apache-2.0. Predecessor credit and exact pins are in README.md and SOURCES.json. diff --git a/research/commuting-dirty-precision/vendor/pr1085/README.md b/research/commuting-dirty-precision/vendor/pr1085/README.md new file mode 100644 index 0000000000..d71db72637 --- /dev/null +++ b/research/commuting-dirty-precision/vendor/pr1085/README.md @@ -0,0 +1,74 @@ +# Sharp coefficient growth in the balanced dirty commutator + +**Research audit; no new kappa.** The unchanged PR628 balanced word has a +sharp coefficient row bound of `ceil(log2 n)+2` at every ideal leaf boundary, +for prefixes and inverse prefixes in either direction. This improves +PR905's sufficient bound `2*3^ceil(log2 n)`. + +The new invariant is stronger: each matrix entry is zero or a single signed +ordered monomial. [PROOF.md](PROOF.md) gives an induction through every +recursive phase and an attaining identity-factor family. The mathematical +statement covers every positive factor count. Finite replays support the +proof; they are not formal verification or independent human peer review. + +Substitution into PR905's existing sufficient precision formula reduces its +radix-64 example from **1,162,553 to 1,162,523 fractional bits**, with +target precision 128 and initial magnitude at most `2^20`. It preserves the +4,000 leaf calls and six borrowed arrays. This is a comparison of conservative +proof budgets, not a runtime improvement. The asymptotic cubic guard and +selected multiplication exponent are unchanged. + +## Reproduce + +Python 3.10 or later, standard library only, from the repository root: + +```sh +python3 -I -O -B research/dirty-prefix-monomial-audit/verify.py +python3 -I -O -B research/dirty-prefix-monomial-audit/test_package.py +``` + +The first command checks source pins and the complete deterministic receipt +without writing artifacts. Expected output: + +```text +PASS_DIRTY_PREFIX_MONOMIAL traces=168 boundaries=1184622 budgets=1242 controls=10 kappa=unchanged +``` + +The second command runs eight package tests, including a read-only relocated +replay using only declared dependencies and rejection of a changed receipt. + +The exact evidence comprises 168 signed traces at 84 factor counts through +257; every prefix and inverse prefix; literal comparisons with the pinned +dispatcher; 32 abstract induction cases; 430 dense noncommuting matrix +boundaries with 44 independent Gauss-Jordan prefix inversions; 1,242 exact +precision comparisons; and ten mathematical controls. The frozen domain, +OS assignment seed **72**, stopping rule, and three candidate tasks are in +[DOMAIN.json](DOMAIN.json). In particular, this is additional invariant +coverage rather than an extension of PR905's existing search domain. + +## Pins, scope, and credit + +Base: `2921874911956718fcaaaf9396fe8267b3cfa9f0`. +[SOURCES.json](SOURCES.json) pins every consumed source by SHA256 and Git blob, +with predecessor heads and original locations. [VALIDATION.json](VALIDATION.json) +records the executed checks and their limits. + +Credit Chafik Boukhalfa for PR628's dispatcher and PR905's ordered-prefix +lemma and cubic analysis; Gareth Davidson for PR877's prefix/perturbation +method; PR862 for the common-isometry subset bound; and 0xkilgore's PR663 +for the exact leaf count. Their source notices remain intact. PR896 covers +nonlinear restoration. Concurrent PR1057 changes dirty-register allocation +under an exact-additive interface; this result keeps PR628's reserved-depth +allocation. No code from PR896 or PR1057 is consumed. + +The operator and precision consequences inherit the common immutable +isometry, distinct mutable arrays, deterministic inverse, leaf error, +coefficient preparation, and phase-access assumptions. Internal leaf +growth, integer guards, restoration, routing and all paid costs remain +charged. No rounded kernel, physical compiler, full transform or multiplication +reduction is newly implemented or audited here. The selected construction +and `upstream/` are unchanged. No literature-priority claim is made. + +Prepared for **Hanson Sun (@bbMisk)** with substantial **OpenAI Codex +assistance** in derivation, coding, verification and writing. New material +is Apache-2.0, under the repository license. diff --git a/research/commuting-dirty-precision/vendor/pr1278/NOTICE.md b/research/commuting-dirty-precision/vendor/pr1278/NOTICE.md new file mode 100644 index 0000000000..b543c9e724 --- /dev/null +++ b/research/commuting-dirty-precision/vendor/pr1278/NOTICE.md @@ -0,0 +1,17 @@ +# Attribution + +New proof, verifier, tests and documentation: Charles Bethin, with substantial +OpenAI Codex assistance, 2026. Apache-2.0. + +The unchanged `vendor/dirty.py` and `PR905-PROOF.md` come from Chafik +Boukhalfa's retained PR628 and PR905 packages. Their notices remain in +`PR628-NOTICE.md` and `PR905-NOTICE.md`. +`PR1085-PROOF.md` and `PR1244-README.md` retain Hanson Sun's source text +and its AI disclosure. `SOURCES.json` records exact source commits, +original paths, Git blobs and SHA256 digests. The repository license +is retained as `vendor/LICENSE`. + +The new recursive word constructor and polynomial/dense checkers are separately +written. AST isolation of the predecessor dispatcher follows the method +used in Hanson Sun's PR1244; the original function itself stays byte-exact. +Independent models do not constitute independent human review. diff --git a/research/commuting-dirty-precision/vendor/pr1278/PROOF.md b/research/commuting-dirty-precision/vendor/pr1278/PROOF.md new file mode 100644 index 0000000000..de9c8fca35 --- /dev/null +++ b/research/commuting-dirty-precision/vendor/pr1278/PROOF.md @@ -0,0 +1,177 @@ +# Squarefree interval matrices for the balanced dirty word + +Status: all-size lemma with exact local checks; external review remains open. +No multiplication exponent, numerical implementation, or precision minimum follows. + +## Statement + +Let n >= 1. Use the exact PR628 balanced dispatcher, with distinct source x, +target y, and one distinct connector per depth. Factors A_0,...,A_(n-1) +are free noncommuting indeterminates. Each leaf is the ideal linear shear +`target += sign A_j source`. Every cut is a complete leaf boundary. + +For every two cuts s,t, in either direction, every surviving monomial in +`P_t P_s^-1` uses each factor index at most once. The cuts may occur in +any order. Deeper connectors remain shared between siblings, as in PR628. +No allocation of fresh scratch per subtree is assumed. + +Consequently, suppose actual factors are bounded linear endomorphisms of one +normed space, commute pairwise, and every subset +product, including the empty product, has operator norm at most G >= 1. +Put h=ceil(log2 n) and C=2*3^h. In the maximum joint-register norm, + +``` +||P_t P_s^-1|| <= C^2 G. +``` + +This replaces the generic `C^2 G^2` interval estimate from PR905 under +the additional commuting hypothesis. PR1244's noncommuting obstruction +remains valid. It contains a squarefree product in the wrong order. + +## Prefix input + +We use PR905 Section 1's free-algebra prefix lemma: every prefix and inverse +prefix has ordered squarefree monomials, with coefficient row sum at most C. +A suffix also has this property: it is the inverse of a prefix of the +inverse word. All statements include both signs. + +For completeness, its induction uses four completed-child states and one +active child. Write B for the complete left product and A for the complete +right product. A completed child restores every deeper connector. Its outer +maps only add Bx to z or Az to y. A child never writes its source or reads +its target. Thus a new nontrivial product in a prefix or inverse prefix +only appends B to a right-child term or prepends A to a left-child term. +The supports are disjoint and ordered. The completed outer maps and their +inverses have coefficient row sum at most three. The leaf bound is two. +This gives C=2*3^h. The eight signed cases and their outer states appear +in the retained PR905 proof. We do not assume PR1085's sharper coefficient +claim for the displayed theorem. + +## Two-cut induction + +Write e_x,e_y,e_z for coordinate injections and their transposes for +coordinate projections. Products below act on column vectors. Chronological +execution is right-to-left matrix multiplication. Put + +``` +U = I + e_z B e_x^T, +V = I + e_y A e_z^T, +F = V^-1 U^-1 V U = I + e_y AB e_x^T. +``` + +U and V denote the completed child maps, not their expanded instruction +words. Let P_a denote any prefix of the expanded positive U word. Let Q_b +denote any prefix of the expanded positive V word. These operators act on +the shared deeper connectors too. They fix every external parent coordinate. +The displayed identity for F also proves the completed-map and restoration +claim inductively, starting from the one-leaf shear. + +A prefix of the inverse U word equals `P_a U^-1` for a complementary cut a. +Similarly a prefix of the inverse V word equals `Q_b V^-1`. +Therefore the four phases of the positive parent have prefix matrices + +``` +phase 0: P_a +phase 1: Q_b U +phase 2: P_a U^-1 V U +phase 3: Q_b F. +``` + +These formulas also include child boundaries and the final boundary. +Changing a cut's boundary representation does not change its matrix. + +Induct on n for *all ordered pairs of cuts*, including reverse intervals. +The leaf case consists of I and one signed shear. If both cuts lie in the +same phase, the completed prefix cancels. The resulting two-cut matrix is +inside one child, in either order, so the induction applies. + +There are six distinct phase pairs. Adjacent phases give, respectively, + +``` +0 -> 1: Q_b (U P_a^-1) +1 -> 2: (P_b U^-1) (V Q_a^-1) +2 -> 3: (Q_b V^-1) P_a^-1. +``` + +Each parenthesized term is a child prefix, inverse prefix, or suffix. +The left and right factor sets are disjoint. The prefix input therefore +makes every monomial squarefree, even when a shared connector joins the +matrix product. Inverses reverse these products; the same argument applies. + +For the first repeated family, phases 0 -> 2 give + +``` +I_02 = P_b (U^-1 V U) P_a^-1 + = P_b P_a^-1 + e_y A [e_z^T U P_a^-1]. +``` + +The first term is a two-cut child matrix. The bracket is a row of a suffix +of U. It contains only squarefree left factors. The extra A contains every +right factor once. Their supports are disjoint. For the inverse interval, +interchange a,b and negate the rank-one term. The bracket becomes +`e_z^T U P_b^-1`, so the same reasoning applies. + +For the second repeated family, phases 1 -> 3 give + +``` +I_13 = Q_b (V^-1 U^-1 V) Q_a^-1 + = Q_b Q_a^-1 - [(Q_b V^-1)e_z] B e_x^T. +``` + +Here x is external to the right child. The bracket is a column of a prefix +of the inverse V word, so it contains only squarefree right factors. +The extra B contains every left factor once. For the inverse interval, +interchange a,b and change the minus sign to plus. The same proof applies. + +Finally, phases 0 -> 3 give + +``` +I_03 = Q_b F P_a^-1 = Q_b P_a^-1 + e_y AB e_x^T, +I_03^-1 = P_a F^-1 Q_b^-1 = P_a Q_b^-1 - e_y AB e_x^T. +``` + +P fixes the external y coordinate; Q fixes the external x coordinate. +Their source rows and target columns also remain identities. Each first +term joins disjoint factor sets; the added product AB is squarefree. + +Addition and cancellation cannot create a monomial with a repeated index. +This proves the claim for every pair of cuts in the positive word. +Every interval of the negative word is the inverse of an interval in the +positive word. Since the induction includes both cut orders, it proves +both signs. All six phase pairs explicitly retain the shared deeper scratch. + +## Norm and sufficient error transport + +Before cancellation, the coefficient row sum in `P_t P_s^-1` is at most C^2, +by submultiplicativity of the two prefix bounds. Cancellation cannot increase +this sum. Commutation reorders each squarefree word into a subset product. +Substituting actual operators and applying the triangle inequality gives +`||P_t P_s^-1|| <= C^2 G`. No invertibility of individual factors is needed; +every leaf shear is invertible regardless of its coefficient. + +This lemma alone does not certify actual rounded leaves. If one separately +has N ideal leaves, initial norm at most D, and a per-leaf error bound +`a*u*(M_actual+1)`, variation of constants gives + +``` +M_actual <= C G D + t(M_actual+1), t=N C^2 G a u. +``` + +If t <= 1/2, this implies `M_actual <= 2 C G D+1` and final error at most +`2 N C^2 G a u (C G D+1)`. These are conditional sufficient bounds. +Compared with the original generic transport argument, one factor G drops +out. Source admission, internal leaf magnitudes, coefficient preparation, +rounding correlations and the complete implementation bill remain separate. +We do not substitute a new cyclic working precision or claim a new kappa. + +## Attribution and limits + +PR628 supplies the dispatcher; PR905 supplies the prefix and common-operator +lemmas. Credit Chafik Boukhalfa for both. Hanson Sun's PR1244 poses the +all-size interval question and gives the noncommuting obstruction. PR1085 +sharpens the prefix coefficient but is not required by this norm estimate. +Gareth Davidson's PR877 supplies the predecessor error-transport context. + +Prepared for Charles Bethin with substantial OpenAI Codex assistance. +The written induction is the all-size argument. Finite tests support it; +they do not constitute a proof-assistant or independent human review. diff --git a/research/commuting-dirty-precision/vendor/pr628/NOTICE.md b/research/commuting-dirty-precision/vendor/pr628/NOTICE.md new file mode 100644 index 0000000000..22fbeb8ef0 --- /dev/null +++ b/research/commuting-dirty-precision/vendor/pr628/NOTICE.md @@ -0,0 +1,24 @@ +# Attribution and scope + +Ali Romman's PR621, exact head 520774462b19b29af41554b74def31f9d01e997e, +supplies the prime-power kernel circle bound. Its kernel attribution is +OpenAI's exact-DFT preprint at adc7f1241b42e322a6451854ab7e4b4c146bf78a +(`loc:newton`, `loc:fourier-factorization`) and classical q-Pochhammer/Newton +factorization, including Alexey Kuznetsov's cited q-calculus work. This +package does not claim to originate those constructions. + +Pan's approximate-factorization theorem is used in the form stated by +Mehlhorn, Sagraloff and Wang; Brent's work supplies fast elementary-function +evaluation. Causal/anticausal recursive filtering is standard, as illustrated +by the Briand-Davy source listed in SOURCE.json. Sources are cited for these +specific tools, not as proofs of this package's complete claim. + +The scan rounding analysis, explicit budget composition, interval and +factor certificates, routed reference execution, and packaging were +prepared with substantial OpenAI Codex assistance for chafreaky. The dense +matrix solver and algebraic coefficient crosschecks provide independent +computational paths, not human peer review or formal Lean verification. + +No new multiplication exponent, literature priority, maintainer acceptance, +physical tape execution, or production performance result is claimed. +The code and documents use the repository's Apache-2.0 license. diff --git a/research/commuting-dirty-precision/vendor/pr628/dirty.py b/research/commuting-dirty-precision/vendor/pr628/dirty.py new file mode 100644 index 0000000000..2b94710837 --- /dev/null +++ b/research/commuting-dirty-precision/vendor/pr628/dirty.py @@ -0,0 +1,133 @@ +"""Integer lifting for cyclic inverse shears using borrowed dirty arrays. +Exact rational prototype. Arithmetic workspace and phase access are charged in the proof; +this is not a common-label Clifford word or a bit-reversible arithmetic compiler. +""" +from pathlib import Path +from fractions import Fraction as F +import importlib.util,json,argparse,itertools +P=Path(__file__).resolve().parent +s=importlib.util.spec_from_file_location('weighted',P/'weighted.py');w=importlib.util.module_from_spec(s);s.loader.exec_module(w);c=w.c + +def scaled(z,q):return(z[0]*q,z[1]*q) +def conj(z):return(z[0],-z[1]) +def ordered(n,d):return range(n)if d==1 else range(n-1,-1,-1) + +def lift(x,y,coefficient,beta,bits,d,sign=1,destination=None,multiplier=None,stats=None): + """y += sign*F(x), restoring x exactly; no length-dependent clean data array.""" + n=len(x);c.need(x is not y and n==len(y)>0,'distinct equally sized arrays') + c.need(d in(-1,1)and sign in(-1,1),'orientation and sign') + c.need(0=(beta/2)**2,'closure denominator') + seed=c.rounded(c.div(x[previous],denominator),bits) + power=c.ONE + for i in ordered(n,d): + power=c.rounded(c.mul(coefficient(i),power),bits) + value=c.add(x[i],c.rounded(c.mul(power,seed),bits)) + value=c.rounded(c.mul(multiplier(i),value),bits) + j=destination(i);y[j]=c.add(y[j],scaled(value,sign)) + # The scalar seed and coefficient scratch may be cleared by ordinary classical + # arithmetic. The dirty data itself is restored by exact inverse integer lifts. + first=0 if d==1 else n-1 + for i in ordered(n,-d): + if i!=first:x[i]=c.sub(x[i],c.rounded(c.mul(coefficient(i),x[i-d]),bits)) + if stats is not None:stats['leaves']+=1;stats['scalar_steps']+=3*n + +def leaf(x,y,factor,phases,beta,bits,d,sign,stats): + inside,b,scale=factor;n=len(x) + if inside: + lift(x,y,lambda i:c.mul(b,conj(phases[(i+d)%n])),beta,bits,-d,sign, + lambda i:(i-d)%n,lambda i:scaled(conj(phases[i]),scale),stats) + else: + lift(x,y,lambda i:c.mul(b,phases[i]),beta,bits,d,sign, + multiplier=lambda i:scaled(c.neg(b),scale),stats=stats) + +def compose(x,y,factors,scratch,phases,beta,bits,d,sign=1,stats=None): + """Balanced commutator; negative call is the exact inverse instruction word.""" + c.need(sign in(-1,1)and d in(-1,1),'orientation and sign') + c.need(factors and len(scratch)>=(len(factors)-1).bit_length(),'dirty depth') + arrays=[x,y]+scratch;c.need(len({id(v)for v in arrays})==len(arrays),'all ancestor arrays distinct') + c.need(len(x)>0 and all(len(v)==len(x)for v in arrays)and len(phases)==len(x),'array lengths') + c.need(all(c.norm2(t)==1 for t in phases),'unit phases') + if len(factors)==1:return leaf(x,y,factors[0],phases,beta,bits,d,sign,stats) + mid=len(factors)//2;B,A=factors[:mid],factors[mid:];z=scratch[0];rest=scratch[1:] + operations=[(x,z,B,1),(z,y,A,1),(x,z,B,-1),(z,y,A,-1)] + if sign==-1:operations=[(src,dst,fs,-sgn)for src,dst,fs,sgn in reversed(operations)] + for src,dst,fs,sgn in operations:compose(src,dst,fs,rest,phases,beta,bits,d,sgn,stats) + +def exact_operator(x,factors,phases,d): + # Dense rational oracle constructed independently from the lifting recurrence. + n=len(x);out=x[:] + for inside,b,scale in factors: + a=[[c.ZERO for _ in range(n)]for _ in range(n)] + if inside: + for i in range(n):a[i][i]=c.neg(b);a[i][(i-d)%n]=c.add(a[i][(i-d)%n],phases[i]) + else: + rho=c.div(c.ONE,b) + for i in range(n):a[i][i]=c.neg(rho);a[i][(i-d)%n]=c.add(a[i][(i-d)%n],phases[i]) + out=[scaled(z,scale)for z in w.solve(a,out)] + return out + +def certificate(n,beta,r,D,bits): + N=4*n*n;a=13*(r+1)/beta**3;G=2+F(r)/beta;u=F(1,1<=0 and N <= 1<=incoming and W>=4*g+16,'grid and admission') + need(W>=A+K+2*c+ceil_power(N)+1,'feedback') + need(z['integer_bits']==K+c+m+8*g+2*ell+16,'inverse preimage guard') + need(z['factor_bits']==v['factor_bits'] and z['preparation_error_exponent']==v['preparation_error_exponent'],'preparation unchanged') + need(z['leaf_calls']==v['leaf_calls'] and z['depth']==v['depth'],'paid recursion unchanged') + need(W<=v['working_bits'] and z['integer_bits']<=v['integer_bits'],'monotone improvement') + need(W<=max(target,incoming)+m+15*r**3 and z['integer_bits']<=m+15*r**3,'cubic envelopes') + rows.append(z) + table=[] + for r in (3,4,8,16,32,64,128,256,512): + z=p.uniform(r,128,20,0);v=old.uniform(r,128,20,0) + table.append(dict(radix=r,old_fractional=v['working_bits'],new_fractional=z['working_bits'], + old_integer=v['integer_bits'],new_integer=z['integer_bits'], + leaf_calls=z['leaf_calls'],borrowed_arrays=z['depth'], + factor_bits=z['factor_bits'])) + generic=[] + for n in (1,2,3,4,7,8,15,16): + for beta in (F(1,2),F(1,3),F(1,16)): + for G in (F(1),F(7,3),F(32)): + for D in (F(0),F(1,3),F(4)): + z=p.choose(n,8,beta,G,D,32,16);v=old.choose(n,8,beta,G,D,32,16) + need(z['working_bits']<=v['working_bits'],'generic precision monotonicity') + B=z['prefix_bound'];L=z['interval_bound'];a=z['local_error'];u=F(1,1<0,'rounded tests must exercise nonlinear errors') + # Concrete target dependence: a target-independent surrogate is insufficient. + inc=[] + for salt in (1,2): + x=Bank(values(3,48,36));y=Bank(values(3,48,salt));before=y.data[:] + d.lift(x,y,(F(3,10),F(2,5)),F(1,2),48,1) + inc.append([d.sub(a,b) for a,b in zip(y.data,before)]) + need(inc[0]!=inc[1],'actual target dependence control') + return dict(cases=len(rows),signed_words=4*len(rows),signed_leaf_calls=total_leaves, + nonzero_error_words=nonzero,target_dependent=True,rows=rows) + +def controls(): + names=[] + def reject(name,fn): + try:fn() + except (ValueError,ZeroDivisionError):names.append(name) + else:raise ValueError('accepted '+name) + reject('non-prime-power',lambda:p.uniform(6,1,0,0)) + reject('negative-target-precision',lambda:p.uniform(3,-1,0,0)) + reject('missing-feedback',lambda:p.execute(8,8,F(1,2),10**30,4,20)) + reject('unsafe-length-admission',lambda:p.execute(1,1,F(1,2),1,0,4)) + reject('unpaid-subset-budget',lambda:p.choose(2,3,F(1,2),F(1,2),1,40,0)) + z=p.uniform(64,128,20,0) + K=z['subset_exponent'];c=z['coefficient_exponent'];A=z['local_error_exponent'];N=z['leaf_calls'] + wrong=z['working_bits']-K + need(wrong<128+3+p.clog(N)+A+20+2*K+3*c,'dropping second subset factor detected') + names.append('second-subset-factor-retained') + oldI=z['prefix_exponent']+20+7*z['margin_exponent']+2*p.clog(64)+16 + need(oldI C^2 M. + M=100 + J=((F(0),F(M)),(F(-1,M),F(0)));D=((F(1,M),F(0)),(F(0),F(M))) + mm=lambda a,b:[[sum(a[i][k]*b[k][j] for k in range(2)) for j in range(2)] for i in range(2)] + norm=lambda a:max(sum(abs(t) for t in row) for row in a) + need(norm(J)==M and norm(D)==M and norm(mm(D,J))==1,'ordered subset premise') + def word(lo,n,x,y,depth): + if n==1:return [(x,y,lo,1)] + k=n//2;left=word(lo,k,x,depth+2,depth+1);right=word(lo+k,n-k,depth+2,y,depth+1) + inverse=lambda w:[(x,y,j,-sign) for x,y,j,sign in reversed(w)] + return left+right+inverse(left)+inverse(right) + literal=word(0,7,0,1,0) + E=[[F(i==j) for j in range(10)] for i in range(10)] + factors=[((F(1),F(0)),(F(0),F(1))) for _ in range(7)] + factors[1]=J;factors[4]=D + for x,y,j,sign in literal[13:27]: + original=[row[:] for row in E] + for a in range(2): + for b in range(10):E[2*y+a][b]+=sign*sum(factors[j][a][k]*original[2*x+k][b] for k in range(2)) + need(abs(E[8][8])+abs(E[8][9])==1+M*M and norm(E)>25*M,'actual noncommuting interval counterexample') + names.append('noncommuting-interval-rejects-linear-G') + return names + +def main(): + parser=argparse.ArgumentParser();parser.add_argument('--write',type=Path);args=parser.parse_args() + receipt=dict(status='PASS_COMMUTING_DIRTY_PRECISION',seed=64,sources=pins(),dispatch=binding_checks(),budgets=budget_checks(),rounded=rounded_checks(),controls=controls()) + if args.write: + with args.write.open('x') as f:json.dump(receipt,f,indent=2);f.write('\n') + else:need(receipt==json.loads((HERE/'CERTIFICATE.json').read_text()),'certificate mismatch') + print(receipt['status'], 'uniform='+str(receipt['budgets']['uniform_cases']), 'rounded_words='+str(receipt['rounded']['signed_words']), 'controls='+str(len(receipt['controls']))) +if __name__=='__main__':main() From 3a6773708f0d73f7dbee164f4c6e7658b0b41509 Mon Sep 17 00:00:00 2001 From: mightyOil <82899331+mightyOil@users.noreply.github.com> Date: Tue, 13 Oct 2026 23:55:25 +0200 Subject: [PATCH 2/2] Clarify data-length notation and credit concurrent phase audit --- research/commuting-dirty-precision/PROOF.md | 15 +++++++++------ research/commuting-dirty-precision/README.md | 4 ++++ .../commuting-dirty-precision/VALIDATION.json | 8 +++++++- 3 files changed, 20 insertions(+), 7 deletions(-) diff --git a/research/commuting-dirty-precision/PROOF.md b/research/commuting-dirty-precision/PROOF.md index d7ef8832ae..5c7b140a49 100644 --- a/research/commuting-dirty-precision/PROOF.md +++ b/research/commuting-dirty-precision/PROOF.md @@ -28,7 +28,8 @@ remain inherited. They do not change the logical leaf-boundary word. Let the ideal factors commute pairwise, with every subset product (including empty) of norm at most G >= 1. PR1054's actual cyclic factors satisfy this conditional premise because every factor is a rational function of the same -immutable isometry U=tau Z_L^w; the single scalar r also commutes. The inherited +immutable isometry U=tau Z_M_len^w, where M_len is the cyclic array length; +the single scalar r also commutes. The inherited complementary-factor argument gives the stated G. Different mutable phases or unrelated operators do not satisfy this premise automatically. @@ -171,14 +172,16 @@ budget and is not superseded or combined numerically here. ## 5. Complete cost and limits The actual word, source access, carrier swaps, restoration, coefficients and -child calls are unchanged. Retain PR1054's per-leaf bounds 1280L scalar -products/divisions and 4096L record moves, and full-kernel bound -`8192(N+1)(h+2)L` data-record moves on two tapes. Let Aword=W+I and Bdesc +child calls are unchanged. Write M_len for the data-array length, distinct +from the interval norm bound L above. Retain PR1054's per-leaf bounds +1280 M_len scalar products/divisions and 4096 M_len record moves, and +full-kernel bound `8192(N+1)(h+2) M_len` data-record moves on two tapes. +Let Aword=W+I and Bdesc include the actual immutable root, margin, multiplier and unit gauge lengths. With M(s) paying for rounded multiplication and division, the complete bill is - preparation + O(N L M(Aword+Bdesc)) - + O(N(h+2)L(Aword+Bdesc)) + O(N L). + preparation + O(N M_len M(Aword+Bdesc)) + + O(N(h+2) M_len (Aword+Bdesc)) + O(N M_len). Long stride/gauge descriptors remain extra input work; preparation retains its supplied soft-O(r^3(p+m+r^3)) bill. Effective numerical depth cannot diff --git a/research/commuting-dirty-precision/README.md b/research/commuting-dirty-precision/README.md index 7a5215011c..ee0bab4f50 100644 --- a/research/commuting-dirty-precision/README.md +++ b/research/commuting-dirty-precision/README.md @@ -106,6 +106,10 @@ vendored subset serves this audit's proof and actual executions; frozen predecessor packages are not modified. Existing generic precision bounds stay valid. PR1244's noncommuting obstruction and PR1135's nonadditive borrowing obstruction are not removed. We retain the original reserved-depth allocation. +Concurrent [PR1294](https://github.com/CrocSwap/integer-mult-bounds/pull/1294) +by Philipp / mightyOil (`03025ca1d51091a9525203000e77dacccfa6a70d`) supplies +universal local algebra certificates for PR1278. That is complementary; no +PR1294 implementation or stronger local-hypothesis claim is consumed here. Only this package is added. The selected PR1094 record, upstream sources, source-access/restoration charges, paid rank profiles and all-size/compiler, diff --git a/research/commuting-dirty-precision/VALIDATION.json b/research/commuting-dirty-precision/VALIDATION.json index 896a4b81a2..f4911aa75f 100644 --- a/research/commuting-dirty-precision/VALIDATION.json +++ b/research/commuting-dirty-precision/VALIDATION.json @@ -49,5 +49,11 @@ "Native/physical supplier integration" ], "ai_assistance": "Substantial OpenAI Codex / GPT-6 Astra assistance; no independent human review", - "checked_utc": "2026-10-13T21:52:58.221213+00:00" + "checked_utc": "2026-10-13T21:52:58.221213+00:00", + "coordinator_review": "Read written argument and scope, no substantive scope blocker; not independent full proof verification. Clarified data-array length M_len versus interval bound L.", + "concurrent_complementary_pr": { + "number": 1294, + "head": "03025ca1d51091a9525203000e77dacccfa6a70d", + "status": "credited; no implementation dependency" + } }