From b6d6934092c063ab2575ebee00f48bbc7b1c9d82 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar Date: Tue, 13 Oct 2026 10:35:57 +0530 Subject: [PATCH] Research: certify single-scale relocation in CK cleanup --- .../complex-ck-scaling-fold/CERTIFICATE.json | 964 ++++++++++++++++++ research/complex-ck-scaling-fold/CLAIM.md | 24 + research/complex-ck-scaling-fold/README.md | 184 ++++ .../complex-ck-scaling-fold/VALIDATION.md | 30 + .../complex-ck-scaling-fold/independent.py | 144 +++ research/complex-ck-scaling-fold/verify.py | 238 +++++ 6 files changed, 1584 insertions(+) create mode 100644 research/complex-ck-scaling-fold/CERTIFICATE.json create mode 100644 research/complex-ck-scaling-fold/CLAIM.md create mode 100644 research/complex-ck-scaling-fold/README.md create mode 100644 research/complex-ck-scaling-fold/VALIDATION.md create mode 100644 research/complex-ck-scaling-fold/independent.py create mode 100644 research/complex-ck-scaling-fold/verify.py diff --git a/research/complex-ck-scaling-fold/CERTIFICATE.json b/research/complex-ck-scaling-fold/CERTIFICATE.json new file mode 100644 index 0000000000..7e5a90594b --- /dev/null +++ b/research/complex-ck-scaling-fold/CERTIFICATE.json @@ -0,0 +1,964 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "boundary_columns_per_orientation": 38, + "boundary_registers": [ + 7, + 10, + 11, + 57, + 69, + 79, + 92, + 97, + 224, + 225, + 228, + 229, + 232, + 233, + 235, + 236, + 237, + 238, + 242, + 244, + 245, + 246, + 247, + 248, + 252, + 253, + 254, + 255, + 256, + 257, + 258, + 259, + 261, + 264, + 268, + 269, + 337, + 344 + ], + "changed_cleanup_sha256": "25a522c63a720152a819135027221dffb1627fa312c2b9f5e4af1c28c7024cf9", + "controls": 6, + "programs": { + "backward": { + "after": { + "prefix_bits": 62, + "prefix_l1": "146068000389976309073/32", + "real_primitives": 224924, + "scalar_macros": 21936 + }, + "before": { + "prefix_bits": 62, + "prefix_l1": "146068000389976309073/32", + "real_primitives": 224986, + "scalar_macros": 21936 + }, + "events": 27256, + "program_sha256": "cd40f05de90a031696da3d6e5b541f00eccda1265d8d7045e0d73938af256143" + }, + "forward": { + "after": { + "prefix_bits": 40, + "prefix_l1": "920709848294", + "real_primitives": 224876, + "scalar_macros": 21936 + }, + "before": { + "prefix_bits": 40, + "prefix_l1": "920709848294", + "real_primitives": 224938, + "scalar_macros": 21936 + }, + "events": 27256, + "program_sha256": "54182c8a62b63f573cff59f5a253cdf18cb6f9b08932b9cb572c20791e7cb629" + } + }, + "search": { + "candidates": 1022007, + "coverage_sha256": "da7d9dac9e3ee7e324098f645094adc27e54e38e998a499851b852b63597de3f", + "records": [ + { + "delta": -6, + "destination": 6648, + "factor": "2", + "register": 608, + "source": 61 + }, + { + "delta": 0, + "destination": 66, + "factor": "2", + "register": 616, + "source": 66 + }, + { + "delta": 0, + "destination": 71, + "factor": "2", + "register": 624, + "source": 71 + }, + { + "delta": 0, + "destination": 76, + "factor": "2", + "register": 632, + "source": 76 + }, + { + "delta": 0, + "destination": 81, + "factor": "2", + "register": 640, + "source": 81 + }, + { + "delta": 0, + "destination": 86, + "factor": "2", + "register": 648, + "source": 86 + }, + { + "delta": 0, + "destination": 91, + "factor": "2", + "register": 656, + "source": 91 + }, + { + "delta": 0, + "destination": 96, + "factor": "2", + "register": 664, + "source": 96 + }, + { + "delta": 0, + "destination": 101, + "factor": "2", + "register": 672, + "source": 101 + }, + { + "delta": 0, + "destination": 106, + "factor": "2", + "register": 680, + "source": 106 + }, + { + "delta": 0, + "destination": 111, + "factor": "2", + "register": 688, + "source": 111 + }, + { + "delta": 0, + "destination": 116, + "factor": "2", + "register": 696, + "source": 116 + }, + { + "delta": 0, + "destination": 121, + "factor": "2", + "register": 704, + "source": 121 + }, + { + "delta": 0, + "destination": 126, + "factor": "2", + "register": 712, + "source": 126 + }, + { + "delta": 0, + "destination": 182, + "factor": "2", + "register": 520, + "source": 182 + }, + { + "delta": 0, + "destination": 213, + "factor": "-1", + "register": 224, + "source": 213 + }, + { + "delta": -2, + "destination": 6, + "factor": "-2", + "register": 536, + "source": 246 + }, + { + "delta": 0, + "destination": 271, + "factor": "1/2", + "register": 607, + "source": 271 + }, + { + "delta": 0, + "destination": 288, + "factor": "1/2", + "register": 615, + "source": 288 + }, + { + "delta": 0, + "destination": 305, + "factor": "1/2", + "register": 623, + "source": 305 + }, + { + "delta": -2, + "destination": 77, + "factor": "1/2", + "register": 631, + "source": 322 + }, + { + "delta": -2, + "destination": 82, + "factor": "1/2", + "register": 639, + "source": 339 + }, + { + "delta": -2, + "destination": 87, + "factor": "1/2", + "register": 647, + "source": 356 + }, + { + "delta": -2, + "destination": 92, + "factor": "1/2", + "register": 655, + "source": 373 + }, + { + "delta": 0, + "destination": 390, + "factor": "1/2", + "register": 663, + "source": 390 + }, + { + "delta": 0, + "destination": 407, + "factor": "1/2", + "register": 671, + "source": 407 + }, + { + "delta": -1, + "destination": 159, + "factor": "1/2", + "register": 679, + "source": 424 + }, + { + "delta": -1, + "destination": 161, + "factor": "1/2", + "register": 687, + "source": 441 + }, + { + "delta": -1, + "destination": 164, + "factor": "1/2", + "register": 695, + "source": 458 + }, + { + "delta": -1, + "destination": 167, + "factor": "1/2", + "register": 703, + "source": 475 + }, + { + "delta": -1, + "destination": 253, + "factor": "1/2", + "register": 711, + "source": 492 + }, + { + "delta": 0, + "destination": 628, + "factor": "1/2", + "register": 484, + "source": 628 + }, + { + "delta": 0, + "destination": 686, + "factor": "1/2", + "register": 229, + "source": 686 + }, + { + "delta": -17, + "destination": 7774, + "factor": "-1/2", + "register": 231, + "source": 695 + }, + { + "delta": -1, + "destination": 699, + "factor": "2", + "register": 27, + "source": 698 + }, + { + "delta": 0, + "destination": 705, + "factor": "-1", + "register": 432, + "source": 705 + }, + { + "delta": -1, + "destination": 899, + "factor": "1/2", + "register": 437, + "source": 898 + }, + { + "delta": -2, + "destination": 1189, + "factor": "-1/2", + "register": 439, + "source": 909 + }, + { + "delta": 0, + "destination": 912, + "factor": "2", + "register": 111, + "source": 912 + }, + { + "delta": -2, + "destination": 1061, + "factor": "1/2", + "register": 0, + "source": 1051 + }, + { + "delta": 0, + "destination": 1181, + "factor": "-1", + "register": 20, + "source": 1181 + }, + { + "delta": -5, + "destination": 1204, + "factor": "1/2", + "register": 36, + "source": 1197 + }, + { + "delta": -3, + "destination": 1265, + "factor": "-1/8", + "register": 436, + "source": 1264 + }, + { + "delta": 0, + "destination": 1313, + "factor": "1/8", + "register": 228, + "source": 1313 + }, + { + "delta": -2, + "destination": 1457, + "factor": "2", + "register": 424, + "source": 1455 + }, + { + "delta": -2, + "destination": 1512, + "factor": "-1/4", + "register": 275, + "source": 1511 + }, + { + "delta": -2, + "destination": 1552, + "factor": "-1/4", + "register": 291, + "source": 1551 + }, + { + "delta": -2, + "destination": 1643, + "factor": "-1/4", + "register": 307, + "source": 1642 + }, + { + "delta": 0, + "destination": 1723, + "factor": "2", + "register": 25, + "source": 1723 + }, + { + "delta": 0, + "destination": 1917, + "factor": "2", + "register": 102, + "source": 1917 + }, + { + "delta": 0, + "destination": 2177, + "factor": "2", + "register": 99, + "source": 2177 + }, + { + "delta": 0, + "destination": 2227, + "factor": "2", + "register": 31, + "source": 2227 + }, + { + "delta": -3, + "destination": 611, + "factor": "2", + "register": 286, + "source": 2293 + }, + { + "delta": -1, + "destination": 2306, + "factor": "2", + "register": 56, + "source": 2301 + }, + { + "delta": -2, + "destination": 511, + "factor": "2", + "register": 396, + "source": 2338 + }, + { + "delta": -1, + "destination": 2431, + "factor": "2", + "register": 85, + "source": 2430 + }, + { + "delta": -1, + "destination": 2510, + "factor": "2", + "register": 32, + "source": 2509 + }, + { + "delta": 0, + "destination": 2687, + "factor": "2", + "register": 52, + "source": 2687 + }, + { + "delta": 0, + "destination": 2810, + "factor": "2", + "register": 90, + "source": 2810 + }, + { + "delta": 0, + "destination": 2814, + "factor": "1/2", + "register": 254, + "source": 2814 + }, + { + "delta": 0, + "destination": 2925, + "factor": "1/2", + "register": 245, + "source": 2925 + }, + { + "delta": 0, + "destination": 2977, + "factor": "-1", + "register": 62, + "source": 2977 + }, + { + "delta": -4, + "destination": 2788, + "factor": "1/2", + "register": 240, + "source": 3016 + }, + { + "delta": 0, + "destination": 3038, + "factor": "1/2", + "register": 71, + "source": 3038 + }, + { + "delta": -2, + "destination": 1643, + "factor": "1/4", + "register": 243, + "source": 3043 + }, + { + "delta": -2, + "destination": 3062, + "factor": "-1/2", + "register": 247, + "source": 3056 + }, + { + "delta": 0, + "destination": 3088, + "factor": "-1/8", + "register": 416, + "source": 3088 + }, + { + "delta": 0, + "destination": 3196, + "factor": "1/2", + "register": 421, + "source": 3196 + }, + { + "delta": 0, + "destination": 3261, + "factor": "1/2", + "register": 78, + "source": 3261 + }, + { + "delta": -1, + "destination": 1372, + "factor": "-1/2", + "register": 423, + "source": 3267 + }, + { + "delta": -2, + "destination": 3304, + "factor": "-1/2", + "register": 104, + "source": 3344 + }, + { + "delta": -24, + "destination": 3437, + "factor": "2", + "register": 109, + "source": 3393 + }, + { + "delta": 0, + "destination": 3489, + "factor": "-1/2", + "register": 320, + "source": 3489 + }, + { + "delta": -10, + "destination": 3682, + "factor": "-1/2", + "register": 333, + "source": 3650 + }, + { + "delta": -1, + "destination": 3951, + "factor": "1/2", + "register": 12, + "source": 3950 + }, + { + "delta": -3, + "destination": 2269, + "factor": "1/2", + "register": 272, + "source": 3964 + }, + { + "delta": -1, + "destination": 3951, + "factor": "1/2", + "register": 100, + "source": 3987 + }, + { + "delta": -5, + "destination": 4094, + "factor": "1/2", + "register": 98, + "source": 4081 + }, + { + "delta": -3, + "destination": 2496, + "factor": "1/2", + "register": 304, + "source": 4098 + }, + { + "delta": -3, + "destination": 4128, + "factor": "1/2", + "register": 48, + "source": 4121 + }, + { + "delta": 0, + "destination": 4190, + "factor": "1/2", + "register": 14, + "source": 4190 + }, + { + "delta": -1, + "destination": 4254, + "factor": "2", + "register": 334, + "source": 4253 + }, + { + "delta": -6, + "destination": 4318, + "factor": "-1/32", + "register": 323, + "source": 4316 + }, + { + "delta": 0, + "destination": 4435, + "factor": "-1", + "register": 336, + "source": 4435 + }, + { + "delta": 0, + "destination": 4501, + "factor": "-1/4", + "register": 400, + "source": 4501 + }, + { + "delta": 0, + "destination": 4570, + "factor": "-1", + "register": 407, + "source": 4570 + }, + { + "delta": 0, + "destination": 4628, + "factor": "1/4", + "register": 405, + "source": 4628 + }, + { + "delta": 0, + "destination": 4728, + "factor": "-1/4", + "register": 41, + "source": 4728 + }, + { + "delta": -25, + "destination": 4803, + "factor": "2", + "register": 402, + "source": 4770 + }, + { + "delta": -5, + "destination": 4811, + "factor": "2", + "register": 53, + "source": 4804 + }, + { + "delta": 0, + "destination": 4816, + "factor": "1/2", + "register": 15, + "source": 4816 + }, + { + "delta": -31, + "destination": 4869, + "factor": "2", + "register": 97, + "source": 4832 + }, + { + "delta": -5, + "destination": 4970, + "factor": "-1/2", + "register": 384, + "source": 4963 + }, + { + "delta": 0, + "destination": 5126, + "factor": "2", + "register": 4, + "source": 5126 + }, + { + "delta": -1, + "destination": 5012, + "factor": "1/2", + "register": 261, + "source": 5185 + }, + { + "delta": 0, + "destination": 5257, + "factor": "1/4", + "register": 259, + "source": 5257 + }, + { + "delta": 0, + "destination": 5272, + "factor": "1/2", + "register": 2, + "source": 5272 + }, + { + "delta": -2, + "destination": 5305, + "factor": "-1/2", + "register": 9, + "source": 5303 + }, + { + "delta": 0, + "destination": 5391, + "factor": "-1/4", + "register": 64, + "source": 5391 + }, + { + "delta": -2, + "destination": 5477, + "factor": "1/2", + "register": 69, + "source": 5475 + }, + { + "delta": -10, + "destination": 5045, + "factor": "-1/8", + "register": 387, + "source": 5524 + }, + { + "delta": 0, + "destination": 5581, + "factor": "1/2", + "register": 68, + "source": 5581 + }, + { + "delta": 0, + "destination": 5763, + "factor": "-1", + "register": 349, + "source": 5763 + }, + { + "delta": -4, + "destination": 5883, + "factor": "1/2", + "register": 342, + "source": 5832 + }, + { + "delta": 0, + "destination": 6232, + "factor": "2", + "register": 74, + "source": 6232 + }, + { + "delta": -3, + "destination": 564, + "factor": "2", + "register": 84, + "source": 6489 + }, + { + "delta": -4, + "destination": 6712, + "factor": "1/2", + "register": 83, + "source": 6708 + }, + { + "delta": -12, + "destination": 6542, + "factor": "1/8", + "register": 354, + "source": 6768 + }, + { + "delta": -11, + "destination": 6891, + "factor": "1/2", + "register": 73, + "source": 6850 + }, + { + "delta": -4, + "destination": 7079, + "factor": "1/64", + "register": 339, + "source": 7223 + }, + { + "delta": -13, + "destination": 7429, + "factor": "2", + "register": 39, + "source": 7396 + }, + { + "delta": 0, + "destination": 7450, + "factor": "-1", + "register": 40, + "source": 7450 + }, + { + "delta": 0, + "destination": 7516, + "factor": "1/16", + "register": 288, + "source": 7516 + }, + { + "delta": 0, + "destination": 7574, + "factor": "1/2", + "register": 54, + "source": 7574 + }, + { + "delta": 0, + "destination": 7585, + "factor": "-1", + "register": 371, + "source": 7585 + }, + { + "delta": -4, + "destination": 7757, + "factor": "2", + "register": 3, + "source": 7751 + }, + { + "delta": 0, + "destination": 7766, + "factor": "-1/2", + "register": 368, + "source": 7766 + }, + { + "delta": 0, + "destination": 7841, + "factor": "1/2", + "register": 370, + "source": 7841 + }, + { + "delta": -31, + "destination": 6033, + "factor": "1/128", + "register": 379, + "source": 8061 + }, + { + "delta": 0, + "destination": 8219, + "factor": "-1", + "register": 8, + "source": 8219 + }, + { + "delta": -4, + "destination": 8237, + "factor": "2", + "register": 88, + "source": 8227 + }, + { + "delta": 0, + "destination": 8239, + "factor": "1/2", + "register": 80, + "source": 8239 + }, + { + "delta": -18, + "destination": 8300, + "factor": "-1/4", + "register": 381, + "source": 8277 + } + ], + "winner": { + "delta": -31, + "destination": 4869, + "factor": "2", + "register": 97, + "source": 4832 + } + }, + "seed": 34, + "source_pins": { + "certificates/selected-result.json": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53", + "docs/research/community-k492-review.md": "3b731d30e80010b15408a289b0b32192700885474c8b36d48ee3320a7a8c5c47", + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/CANONICAL-WORD.json.gz": "9bbc75dede090cfd7a0a0252424ea9d9f6211e2350d2a801d4e4f2f0784167c7", + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/LOCAL-PROGRAMS.json.gz": "854f17274092263dc25e60367f4cd0d29f60a8446becd17cc1883ebed7a97900", + "research/complex-k492-owner-repair/code/hpe_emit_local.py": "7e4a6fbc38c8228157b6311457d1496bf460291393043932d2c365f004f77805", + "research/complex-k492-owner-repair/data/SPEC.json": "2a2577ac526535826fed9d5f7f83f6e2e0ec058a146c64f7286720b995fa2323" + }, + "status": "PASS_CK_SINGLE_SCALE_RELOCATION" +} diff --git a/research/complex-ck-scaling-fold/CLAIM.md b/research/complex-ck-scaling-fold/CLAIM.md new file mode 100644 index 0000000000..1727ce3e0f --- /dev/null +++ b/research/complex-ck-scaling-fold/CLAIM.md @@ -0,0 +1,24 @@ +# CK cleanup diagonal scaling, seed 34 + +- Track: complex supplier. OS assignment seed: 34, drawn with Python `secrets.randbelow(100)`. +- Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +- Claimed at 2026-10-13 04:53 UTC; expected finish 05:25 UTC. +- Object: selected #626 CK cleanup scalar word. Seed 34 selects CK from the ordered CK/JP8 pair by parity, and forward-first examination. +- Method: carry exact diagonal factors through cleanup additions, adjust coefficients, settle factors at the cleanup boundary, and price every resulting scalar primitive. Stop if the complete cost fails to improve. Check frame boundaries and exact arithmetic envelopes before making any circuit claim. +- Deliverable: one finite circuit result or scoped negative result with reproducible exact checks and source pins. No kappa claim or frontier edit. +- Candidates considered: coefficient-work sharing, fixed-boundary B-frame reassignment, cleanup diagonal scaling. #722 and #698 already cover the first two classes. #696 and #723 change within-macro lowering; #719 studies rank-one replacements of repeated addition pairs. This task changes coefficients by conjugating diagonal scales through additions. +- Coordination: GitHub reports no pinned issues. The open-PR scan covered 542 entries through #723; body searches found no diagonal scaling-fold claim. The local claim is used as requested when no coordination issue exists. +- Contributor: @thakrarsagar, with substantial OpenAI Codex assistance. New work uses the repository Apache-2.0 license. + +## Completed result + +The all-to-end hypothesis increased the primitive bill. One pivot to exhaustive +single-scale relocation found a 62-real-primitive saving per orientation, moving +the register-97 doubling across 37 cleanup additions. Both implementations +checked all 1,022,007 placements and both 38-column boundary maps. Complete CK +prefix bounds remain unchanged. No kappa claim. + +Result and reproduction: [README](README.md), [exact certificate](CERTIFICATE.json), +[validation](VALIDATION.md). The final overlap scan covered 566 open PRs through +#747; #734 and #739 are distinct and credited in the result. The separate worker +remained within this claim and produced the valuation/integer-matrix check. diff --git a/research/complex-ck-scaling-fold/README.md b/research/complex-ck-scaling-fold/README.md new file mode 100644 index 0000000000..0ecbb17607 --- /dev/null +++ b/research/complex-ck-scaling-fold/README.md @@ -0,0 +1,184 @@ +# One CK cleanup scale relocation saves 62 primitives per orientation + +Status: finite complex-supplier circuit improvement and scoped exhaustive search. +No new kappa is claimed. + +In the selected #626 CK cleanup, move the doubling of register 97 from +zero-based operation 4832 to operation 4869. Double the coefficients of the +37 intervening additions, which all read register 97. This saves 62 +real-component primitives in each orientation under the retained binary-Horner +lowering. The complete interval map, including arbitrary incoming values, is +unchanged. Both complete-program prefix envelopes remain unchanged. + +| Complete CK scalar program | Original | Replacement | Saving | +| --- | ---: | ---: | ---: | +| Forward real-component primitives | 224,938 | 224,876 | 62 | +| Inverse-transpose real-component primitives | 224,986 | 224,924 | 62 | +| Scalar macros, either orientation | 21,936 | 21,936 | 0 | +| Events, either orientation | 27,256 | 27,256 | 0 | + +The saving is small. It establishes a checked improvement to a specific +cleanup circuit and an exact limit for all single-scale relocations of that +fixed word. It is not a practical runtime benchmark or an exponent improvement. + +## Reproduce + +From the repository root, using Python 3.9+ and only the standard library: + +```sh +python3 -B research/complex-ck-scaling-fold/verify.py +``` + +Expected: + +```text +PASS_CK_SINGLE_SCALE_RELOCATION candidates=1022007 saving=62/62 columns=38/38 controls=6 +``` + +The independently implemented check is: + +```sh +python3 -B research/complex-ck-scaling-fold/independent.py +``` + +It reports 1,022,007 positions, minimum complex-component delta -31, +644 minimizing placements, 38 columns in each orientation and eight rejected +controls. Both scripts are offline and read-only. `verify.py --emit-certificate` +prints the complete deterministic certificate to stdout; the default command +compares the recomputed result with `CERTIFICATE.json`. + +## Exact circuit argument + +Let S multiply register r by nonzero q. While delaying S to the right, replace +each crossed addition `t += a*s` by `t += a*q*s` if s=r, or by +`t += (a/q)*s` if t=r. Other additions and all diagonal scales commute with S. +For motion to the left, use the reciprocal adjustments. The invariant is +`original_state = D * replacement_state`, with D equal to q on register r +and one elsewhere. Executing S at the chosen boundary makes D the identity. +This proves equality for every input, including dirty helper coordinates. + +Here q=2, r=97, and all 37 crossed additions use r only as a source. +Thirty-four adjusted coefficients cost one fewer complex primitive. Three +original integral coefficients cost one more. The net change is +`-34 + 3 = -31`, doubled to -62 for real and imaginary components. The +doubling itself is still paid once. There is no omitted restoration operation. + +The same-order gatewise inverse transpose respects equality of the complete +product. Its additions swap source and target and negate the coefficient; +its scale is 1/2. The programs are not reversed. The two checkers explicitly +compare the 38-by-38 rational boundary maps in both orientations. All other +678 register columns are unaffected because the changed interval never reads +or writes those registers. The surrounding selected program is byte-for-byte +preserved as parsed events outside the cleanup replacement. + +## Complete local accounting and interface + +Each addition keeps the existing cleared-private-work binary Horner recipe. +The bill includes the initial clear, every source read, doubling, halving, +signed target accumulation and final clear. Relocation does not introduce +scratch, copies, recursive calls or frame changes. Private work is still +cleared after each macro. All 38 involved registers have final frame 1, the +full frame; settlement occurs before any post residual wrapper. + +The selected 492 helpers, eight private centres, 3,698 paid children, 238 pre +and 238 post residual wrappers, 426,400 local adapters and compiler charge +25,934,336 are retained. The paid histogram remains +`{1:2596, 2:552, 3:304, 4:160, 5:70, 6:8, 8:8}`. No changes to a bank, owner, +source-access interface, tail operation or early-ended helper are used. + +`recount` traverses both complete event streams and expands Horner billing by +digits. This is checked against the separate closed-form cost used by the +search. It also propagates positive rational envelopes through scalar registers +and private coefficient work. Forward remains `920709848294`, charged at +40 bits; inverse transpose remains `146068000389976309073/32`, charged at +62 bits. Both fit the inherited 192-bit local allowance. The inverse-transpose +intermediate value on register 97 can be larger before settlement, so these +full recounts are necessary even though the boundary maps agree. + +This package reconstructs the revised local programs and binds their exact +hashes. It does not install them into the selected emitter or regenerate the +global invoice, owner certificate, assembly inequalities or selected frontier. +Such integration remains a separate obligation. Inherited all-size compilation, +common-label and mutable-basis realization, pooled whole-call hosting, +normalized residuals, precision/tape/exact recovery and analytic transfer +assumptions remain. Finite exact replay is not a formal proof of the full +multiplication theorem. + +## Search domain, stopping rule and negative evidence + +OS seed 34 assigned the complex-supplier track and selected CK from CK/JP8 +by parity. The first hypothesis moved every cleanup scale to the end; its +complex-component bill increased from 42,309 to 45,275. Moving all scales to +the beginning also lost, giving 42,497. The single evidence-driven pivot was +to relocate one scale while leaving every other operation in relative order. + +The completed domain contains all 123 original scales and all 8,309 insertion +positions after removing the selected scale, including its original position. +The scan stops after all 1,022,007 placements. It has no sampling, timeout, +floating arithmetic or external solver. For each placement the search prices +every changed coefficient; the scale's cost is unchanged. The certificate +contains every scale's best placement and a digest of the complete ordered +score stream. Ties choose the shortest displacement, then the lower source +and destination indices. This selects 4832 to 4869. + +The independent implementation instead uses the valuation identity +`cost(a) = 2 + bit_length(abs(odd)) + popcount(abs(odd)) + abs(e)` for +`a = odd * 2**e`. It finds exactly 644 optimal placements: 4832 to 4869 and +8061 to any position from 5391 through 6033 inclusive. Its matrix check uses +integer linear forms with denominator 16 and checks divisibility at every +step. It imports neither the first checker nor the native emitter. + +The -31 bound applies only to a single original scale relocated in this fixed +word, with forced conjugation coefficients and the original Horner price. +It does not bound multiple relocations, new scales, different scalar +factorizations, different lowerings or supplier constructions. Per-scale +improvements are not asserted additive. Omitted settlement, an unadjusted +coefficient, wrong settlement factors and sign errors are rejected by the +exact boundary controls. + +## Pins, overlap and credit + +Base commit: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +The accepted conditional value at that base is +`51110230636731/31250000000000000`, from selected #626, not an open-PR title. +The source chain is: + +- #626, Chafik Boukhalfa: `660de893d27bb7abd1d5b01b1640207528a5c851`. +- #622, Jeremy Kothe: `f69477f4f6d3c7eb1f740b166881bffed4ffa9f6`. +- Retained #543 bit supplier, eumemic: `2065fe4f72a914d907f1046603f5a36f17018535`. + +`CERTIFICATE.json` pins the consumed native word, event stream, emitter, +supplier specification, selected record and maintainer review. Gzip pins hash +the entire decompressed payload, so container recompression does not invalidate +the mathematical source binding. Other source pins hash file bytes. + +The review ledger, current status and selected construction review were read +before selection. No pinned coordination issue existed; `CLAIM.md` records the +scope. The initial open queue contained 542 PRs through #723. A later refresh +contained 551 through #732. The pre-submission scan covered 566 through #747. +No cleanup diagonal-scale relocation was found. +#414's body match concerns relocated target prefixes in an older entrance +construction, not this scale relocation. + +Related pending work is credited as context, with no code imported: +#696 `5a3f983715027c4fd83f50bc9001d4b18463bed1` lowers individual macros; +#722 `a0766ab0fab379e1997fadc3ca157578d57986c1` shares JP8 coefficient work; +#723 `d3bc41b87fc7d23f50d064a0f06f1a89e3ab02a7` uses signed digits in JP8; +#719 `a3d9c0aa0a16b68b1f4dd064671ad018013e6dd4` obstructs rank-one fusion +of repeated CK addition pairs. #698 studies fixed-boundary CK B frames. +The final refresh also found #734 +`ba76ba3321d000c8996b0b254bcf0d7260e1bbb6`, which bounds signed-Horner +prefixes, and #739 `abb9825202dba6f9bc95c7df8d12d86088fdff1a`, which rescales +shared JP8 private coefficient work. Neither relocates a live CK register scale. +The present result changes the scalar coefficients and scale order of a +full-frame cleanup interval. Savings are relative to the selected base and +are not asserted additive to those pending changes without a composed recount. + +The retained construction and accounting descend from icekylinx's direct +delivery and emitter work, Jeremy Kothe's CK/K-triangle lineage, +DreamingOfClouds' cold-helper and native checks, and the contributors credited +by the selected review. Their notices and code are unchanged. + +Prepared for @thakrarsagar with substantial OpenAI Codex assistance, including +one separately implemented AI verification worker. This is implementation +independence, not independent human review. New files are Apache-2.0. diff --git a/research/complex-ck-scaling-fold/VALIDATION.md b/research/complex-ck-scaling-fold/VALIDATION.md new file mode 100644 index 0000000000..01e9b8f63b --- /dev/null +++ b/research/complex-ck-scaling-fold/VALIDATION.md @@ -0,0 +1,30 @@ +# Validation + +Executed on 2026-10-13, macOS 26.5.2 arm64, CPython 3.14.8. +Base `66849e1475c930fd7732b1a0067ffee7e1e95f60`; new files are confined to +`research/complex-ck-scaling-fold/`. The upstream main head remained equal to +that base at the pre-submission refresh. + +| Check | Result | +| --- | --- | +| `python3 -I -B research/complex-ck-scaling-fold/verify.py` | PASS, 1,022,007 placements, 62/62 real primitives saved, 38/38 exact boundary columns, six controls | +| `python3 -I -O -B research/complex-ck-scaling-fold/independent.py` | PASS, valuation-only search, 644 minimizers, integer matrices, eight controls | +| Main verifier with `-I -O -B`, invoked by absolute path from outside the repo | PASS | +| `python3 -B scripts/verify_selected_result.py` | PASS, exact selected kappa and source/proof inventory | +| Same native payload in an alternate level-1 gzip container | PASS | +| One newline appended to the decompressed native payload | Rejected by source hash before search | +| Certificate primitive total reduced by one | Rejected by certificate comparison | + +The last three checks patched file reads in memory and ran the normal verifier +entry point. No committed input or certificate was altered. Arithmetic controls +are part of the shipped commands. Validation does not depend on Python asserts. + +The independent AI worker used a different cost representation and integer +boundary implementation. Its review identified two duplicate mutations in an +early main-checker draft; the third mutation now changes the settlement factor, +and the final checks above include that correction. This is not human review. + +Full `make verify`, selected cold replay, global invoice/admission regeneration, +Lean and remote Linux execution were not run. This additive research package +does not change a selected source, generator or construction. The scoped checks +verify its finite claim; the full construction's inherited assumptions remain. diff --git a/research/complex-ck-scaling-fold/independent.py b/research/complex-ck-scaling-fold/independent.py new file mode 100644 index 0000000000..3a0ff10af7 --- /dev/null +++ b/research/complex-ck-scaling-fold/independent.py @@ -0,0 +1,144 @@ +#!/usr/bin/env python3 +"""Independent finite CK search and boundary check. Apache-2.0. + +Prepared for @thakrarsagar with substantial OpenAI Codex assistance. +Credits the selected #626 CK construction and icekylinx's Horner accounting. +Uses dyadic valuations and integer matrices; imports no construction/verifier. +""" +import gzip +import hashlib +import json +from math import gcd +from pathlib import Path + + +ROOT = Path(__file__).resolve().parents[2] +SOURCE = "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/CANONICAL-WORD.json.gz" +SOURCE_SHA256 = "9bbc75dede090cfd7a0a0252424ea9d9f6211e2350d2a801d4e4f2f0784167c7" + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def valuation(n): + n = abs(n) + need(n > 0, "zero coefficient") + return (n & -n).bit_length() - 1 + + +def exponent(numerator, denominator): + need(denominator > 0 and denominator & (denominator - 1) == 0, "non-dyadic denominator") + return valuation(numerator) - valuation(denominator) + + +def scan(ops): + # For a = odd * 2**e, Horner cost is 2 + bits(odd) + popcount(odd) + abs(e). + best, minimizers, candidates, shortest = 0, 0, 0, None + for i, scale in enumerate(ops): + if scale[0] != "scale": + continue + _, register, numerator, denominator, _ = scale + need(abs(numerator) & (abs(numerator) - 1) == 0, "nonbinary scale") + shift = exponent(numerator, denominator) + deltas = [0] * len(ops) + for direction in (-1, 1): + delta = 0 + stop = -1 if direction < 0 else len(ops) + for j in range(i + direction, stop, direction): + e = ops[j] + if e[0] == "add": + power = exponent(e[3], e[4]) + change = shift * ((e[2] == register) - (e[1] == register)) * direction + delta += abs(power + change) - abs(power) + deltas[j] = delta + candidates += len(deltas) + for j, delta in enumerate(deltas): + if delta < best: + best, minimizers, shortest = delta, 0, None + if delta == best: + minimizers += 1 + choice = (abs(j - i), i, j) + shortest = choice if shortest is None else min(shortest, choice) + return candidates, best, minimizers, shortest + + +def dual(e): + if e[0] == "add": + return ["add", e[2], e[1], -e[3], e[4], e[-1]] + return ["scale", e[1], e[3], e[2], e[-1]] + + +def integer_matrix(word, registers, backward): + # Sixteenths cover this pinned 38-gate interval and all four mutations. + # Every division is checked, so insufficient precision fails explicitly. + rows = {r: {r: 16} for r in registers} + for raw in word: + e = dual(raw) if backward else raw + target = e[1] + if e[0] == "add": + for column, value in rows[e[2]].items(): + product = e[3] * value + need(product % e[4] == 0, "integer matrix lost precision") + rows[target][column] = rows[target].get(column, 0) + product // e[4] + rows[target] = {c: v for c, v in rows[target].items() if v} + else: + for column, value in rows[target].items(): + product = e[2] * value + need(product % e[3] == 0, "integer matrix lost precision") + rows[target][column] = product // e[3] + return rows + + +def main(): + raw = gzip.decompress((ROOT / SOURCE).read_bytes()) + need(hashlib.sha256(raw).hexdigest() == SOURCE_SHA256, "native source hash mismatch") + word = json.loads(raw) + ops = word["cleanup"] + need(len(ops) == 8309 and sum(e[0] == "scale" for e in ops) == 123, "search domain changed") + for e in ops: + need(e[0] in ("add", "scale") and e[-1] == 1, "invalid cleanup operation/frame") + registers = e[1:3] if e[0] == "add" else e[1:2] + need(all(word["final"][r] == 1 for r in registers), "non-FULL terminal frame") + if e[0] == "add": + need(e[1] != e[2], "self-addition") + result = scan(ops) + need(result == (1022007, -31, 644, (37, 4832, 4869)), "independent search mismatch") + + before = ops[4832:4870] + need(before[0] == ["scale", 97, 2, 1, 1], "unexpected selected scale") + need(all(e[0] == "add" and e[2] == 97 for e in before[1:]), "interval is not source fanout") + need(len({e[1] for e in before[1:]}) == 37, "fanout targets repeat") + after = [] + for original in before[1:]: + e = original.copy() + divisor = gcd(2 * e[3], e[4]) + e[3], e[4] = 2 * e[3] // divisor, e[4] // divisor + after.append(e) + after.append(before[0].copy()) + registers = sorted({r for e in before for r in (e[1:3] if e[0] == "add" else e[1:2])}) + need(len(registers) == 38, "boundary register count") + controls = 0 + for backward in (False, True): + expected = integer_matrix(before, registers, backward) + need(expected == integer_matrix(after, registers, backward), "boundary map differs") + mutations = [after[:-1]] + unadjusted = [e.copy() for e in after] + unadjusted[0] = before[1].copy() + mutations.append(unadjusted) + wrong_scale = [e.copy() for e in after] + wrong_scale[-1][2] = 4 + mutations.append(wrong_scale) + wrong_sign = [e.copy() for e in after] + wrong_sign[0][3] *= -1 + mutations.append(wrong_sign) + for mutation in mutations: + need(expected != integer_matrix(mutation, registers, backward), "negative control accepted") + controls += 1 + need(controls == 8, "missing negative controls") + print("PASS_INDEPENDENT_CK_SCALE positions=1022007 min_delta=-31 minimizers=644 columns=38/38 controls=8") + + +if __name__ == "__main__": + main() diff --git a/research/complex-ck-scaling-fold/verify.py b/research/complex-ck-scaling-fold/verify.py new file mode 100644 index 0000000000..ccfc61c6b6 --- /dev/null +++ b/research/complex-ck-scaling-fold/verify.py @@ -0,0 +1,238 @@ +#!/usr/bin/env python3 +"""Exact finite CK cleanup scale relocation. Apache-2.0. + +Prepared for @thakrarsagar with substantial OpenAI Codex assistance. +Horner accounting follows icekylinx's emitter/invoice lineage retained in #626. +This does not certify an all-size multiplication theorem or a new kappa. +""" +import copy +import gzip +import hashlib +import json +import sys +from fractions import Fraction as Q +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PROVIDER = "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/" +PINS = { + PROVIDER + "CANONICAL-WORD.json.gz": "9bbc75dede090cfd7a0a0252424ea9d9f6211e2350d2a801d4e4f2f0784167c7", + PROVIDER + "LOCAL-PROGRAMS.json.gz": "854f17274092263dc25e60367f4cd0d29f60a8446becd17cc1883ebed7a97900", + "research/complex-k492-owner-repair/code/hpe_emit_local.py": "7e4a6fbc38c8228157b6311457d1496bf460291393043932d2c365f004f77805", + "research/complex-k492-owner-repair/data/SPEC.json": "2a2577ac526535826fed9d5f7f83f6e2e0ec058a146c64f7286720b995fa2323", + "certificates/selected-result.json": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53", + "docs/research/community-k492-review.md": "3b731d30e80010b15408a289b0b32192700885474c8b36d48ee3320a7a8c5c47", +} + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def digest(value): + return hashlib.sha256(json.dumps(value, sort_keys=True, separators=(",", ":")).encode()).hexdigest() + + +def load(): + sources = {} + for name, expected in PINS.items(): + data = (ROOT / name).read_bytes() + if name.endswith(".gz"): + data = gzip.decompress(data) + need(hashlib.sha256(data).hexdigest() == expected, "source pin: " + name) + if name.endswith((".json", ".json.gz")): + sources[name] = json.loads(data) + return sources[PROVIDER + "CANONICAL-WORD.json.gz"], sources[PROVIDER + "LOCAL-PROGRAMS.json.gz"] + + +def add_cost(q): + a, b = abs(q.numerator), q.denominator + need(a > 0 and b & (b - 1) == 0, "nonzero dyadic addition required") + return 3 + a.bit_length() - 1 + bin(a).count("1") + b.bit_length() - 1 + + +def coefficient(e): + return Q(e[-3], e[-2]) + + +def relocated(ops, source, destination): + """Move one scale to its final index, preserving the full register map.""" + out = copy.deepcopy(ops) + scale = out[source] + need(scale[0] == "scale", "relocation source must be a scale") + r, q = scale[1], coefficient(scale) + right = destination > source + for k in range(min(source, destination), max(source, destination) + 1): + e = out[k] + if e[0] == "add" and r in e[1:3]: + factor = q if (e[2] == r) == right else 1 / q + a = coefficient(e) * factor + e[3:5] = [a.numerator, a.denominator] + out.insert(destination, out.pop(source)) + return out + + +def search(ops): + """Exhaust all final positions for each single scale; no composition.""" + records = [] + coverage = hashlib.sha256() + candidates = 0 + for i, scale in enumerate(ops): + if scale[0] != "scale": + continue + r, q = scale[1], coefficient(scale) + best = (0, 0, i) + coverage.update(f"{i},{i},0\n".encode()) + candidates += 1 + for direction in (-1, 1): + delta = 0 + stop = -1 if direction < 0 else len(ops) + for j in range(i + direction, stop, direction): + e = ops[j] + if e[0] == "add" and r in e[1:3]: + a = coefficient(e) + factor = q if (e[2] == r) == (direction > 0) else 1 / q + delta += add_cost(a * factor) - add_cost(a) + coverage.update(f"{i},{j},{delta}\n".encode()) + candidates += 1 + best = min(best, (delta, abs(j - i), j)) + records.append(dict(source=i, register=r, factor=str(q), delta=best[0], destination=best[2])) + winner = min(records, key=lambda x: (x["delta"], abs(x["destination"] - x["source"]), x["source"], x["destination"])) + return dict(candidates=candidates, coverage_sha256=coverage.hexdigest(), records=records, winner=winner) + + +def dual(e): + e = list(e) + if e[0] == "add": + e[1], e[2], e[3] = e[2], e[1], -e[3] + else: + e[2], e[3] = e[3], e[2] + return e + + +def matrix(ops, registers): + rows = {r: {r: Q(1)} for r in registers} + for e in ops: + r, q = e[1], coefficient(e) + if e[0] == "scale": + rows[r] = {k: q * v for k, v in rows[r].items()} + else: + for k, v in list(rows[e[2]].items()): + value = rows[r].get(k, 0) + q * v + if value: + rows[r][k] = value + else: + rows[r].pop(k, None) + return rows + + +def scalar(e): + if e[0] == "add": + return ["add", ["L", e[1]], ["L", e[2]], e[3], e[4]] + return ["scale", ["L", e[1]], e[2], e[3]] + + +def recount(events, n): + """Independent digit-loop billing, including private-work peaks and clears.""" + env = {("L", r): Q(1) for r in range(n)} + peak, real, macros = Q(1), 0, 0 + for event in events: + if event[0] != "scalar": + continue + e = event[1] + tag, t = e[0], tuple(e[1]) + macros += 1 + if tag == "clear": + env[t], count = Q(0), 1 + elif tag == "copy": + env[t], count = env[tuple(e[2])], 1 + elif tag == "scale": + q = Q(e[2], e[3]) + a, b = abs(q.numerator), q.denominator + need(a > 0 and a & (a - 1) == 0 and b & (b - 1) == 0, "power-of-two scale") + count = abs(a.bit_length() - b.bit_length()) + int(q < 0) + env[t] *= abs(q) + elif tag == "add": + s, q = tuple(e[2]), Q(e[3], e[4]) + need(s != t, "distinct addition registers") + acc, count = Q(0), 1 + for i, bit in enumerate(bin(abs(q.numerator))[2:]): + if i: + acc *= 2 + count += 1 + peak = max(peak, acc * env[s]) + if bit == "1": + acc += 1 + count += 1 + peak = max(peak, acc * env[s]) + for _ in range(q.denominator.bit_length() - 1): + acc /= 2 + count += 1 + peak = max(peak, acc * env[s]) + count += 2 # signed accumulation and final private-work clear + need(acc == abs(q) and count == add_cost(q), "Horner recipe mismatch") + env[t] += acc * env[s] + else: + raise ValueError("unknown scalar " + tag) + peak = max(peak, env[t]) + real += 2 * count + need(all(v == 0 for r, v in env.items() if r[0] == "C"), "private centres not cleared") + return dict(real_primitives=real, scalar_macros=macros, prefix_l1=str(peak), prefix_bits=peak.numerator.bit_length() - peak.denominator.bit_length() + 1) + + +def run(): + word, programs = load() + ops = word["cleanup"] + need(len(ops) == 8309, "cleanup length") + for e in ops: + need(e[0] in ("add", "scale") and e[-1] == 1, "cleanup gate/frame") + regs = e[1:3] if e[0] == "add" else e[1:2] + need(all(word["final"][r] == 1 for r in regs), "low-ended helper touched") + if e[0] == "add": + need(e[1] != e[2], "self-addition") + add_cost(coefficient(e)) + scan = search(ops) + win = scan["winner"] + need((win["source"], win["destination"], win["delta"]) == (4832, 4869, -31), "unexpected optimum") + changed = relocated(ops, win["source"], win["destination"]) + start, end = win["source"], win["destination"] + 1 + need(ops[:start] == changed[:start] and ops[end:] == changed[end:], "nonlocal edit") + before, after = ops[start:end], changed[start:end] + regs = sorted({r for e in before for r in (e[1:3] if e[0] == "add" else e[1:2])}) + results = {} + controls = 0 + for orientation in ("forward", "backward"): + convert = dual if orientation == "backward" else lambda e: e + old, new = [convert(e) for e in before], [convert(e) for e in after] + need(matrix(old, regs) == matrix(new, regs), "exact boundary mismatch") + # Omit settlement, leave a crossed coefficient unchanged, or double settlement. + mutations = [new[:-1], copy.deepcopy(new), copy.deepcopy(new)] + mutations[1][0][3:5] = old[1][3:5] + mutations[2][-1][2] *= 2 + for mutation in mutations: + need(matrix(old, regs) != matrix(mutation, regs), "negative control accepted") + controls += 1 + events = programs[orientation] + cleanup = events.index(["phase", "full_frame_cleanup"]) + 1 + expected = [["scalar", scalar(convert(e)), 1] for e in ops] + need(events[cleanup:cleanup + len(ops)] == expected, "native/event binding") + replacement = [["scalar", scalar(convert(e)), 1] for e in changed] + revised = events[:cleanup] + replacement + events[cleanup + len(ops):] + old_bill, new_bill = recount(events, 716), recount(revised, 716) + need(old_bill["real_primitives"] - new_bill["real_primitives"] == 62, "full cost saving") + need(new_bill["prefix_bits"] <= 192, "local precision allowance") + need(len(events) == len(revised), "event count changed") + results[orientation] = dict(before=old_bill, after=new_bill, events=len(events), program_sha256=digest(revised)) + return dict(status="PASS_CK_SINGLE_SCALE_RELOCATION", base_commit="66849e1475c930fd7732b1a0067ffee7e1e95f60", seed=34, source_pins=PINS, search=scan, changed_cleanup_sha256=digest(changed), boundary_registers=regs, boundary_columns_per_orientation=len(regs), controls=controls, programs=results) + + +if __name__ == "__main__": + result = run() + if sys.argv[1:] == ["--emit-certificate"]: + print(json.dumps(result, indent=2, sort_keys=True)) + else: + need(not sys.argv[1:], "usage: verify.py [--emit-certificate]") + need(result == json.loads((HERE / "CERTIFICATE.json").read_text()), "certificate mismatch") + print("PASS_CK_SINGLE_SCALE_RELOCATION candidates=1022007 saving=62/62 columns=38/38 controls=6")