From 81fed971e2269b62eae2ee8e3b6bda394930992c Mon Sep 17 00:00:00 2001 From: Charles Bethin Date: Wed, 14 Oct 2026 23:16:10 -0400 Subject: [PATCH] Prove the deferred R439 scatter optimum over all undo ideals --- .../CERTIFICATE.json | 1662 +++++++++++++++++ research/r439-deferred-ideal-optimum/PROOF.md | 173 ++ .../r439-deferred-ideal-optimum/README.md | 71 + .../r439-deferred-ideal-optimum/SOURCES.json | 24 + .../r439-deferred-ideal-optimum/TASK.json | 106 ++ .../VALIDATION.json | 44 + .../r439-deferred-ideal-optimum/VERIFY.json | 33 + .../independent.py | 127 ++ .../r439-deferred-ideal-optimum/verify.py | 220 +++ 9 files changed, 2460 insertions(+) create mode 100644 research/r439-deferred-ideal-optimum/CERTIFICATE.json create mode 100644 research/r439-deferred-ideal-optimum/PROOF.md create mode 100644 research/r439-deferred-ideal-optimum/README.md create mode 100644 research/r439-deferred-ideal-optimum/SOURCES.json create mode 100644 research/r439-deferred-ideal-optimum/TASK.json create mode 100644 research/r439-deferred-ideal-optimum/VALIDATION.json create mode 100644 research/r439-deferred-ideal-optimum/VERIFY.json create mode 100644 research/r439-deferred-ideal-optimum/independent.py create mode 100644 research/r439-deferred-ideal-optimum/verify.py diff --git a/research/r439-deferred-ideal-optimum/CERTIFICATE.json b/research/r439-deferred-ideal-optimum/CERTIFICATE.json new file mode 100644 index 0000000000..a0911d709d --- /dev/null +++ b/research/r439-deferred-ideal-optimum/CERTIFICATE.json @@ -0,0 +1,1662 @@ +{ + "status": "PASS_R439_DEFERRED_IDEAL_OPTIMUM", + "lower_bound": 94, + "attaining_ideal": [ + 31, + 51, + 52 + ], + "initial_scatter": 97, + "original_scatter": 527, + "undo_gates": 306, + "dependency_edges": 850, + "row_subsets": 1386, + "row_certificates": [ + { + "row": 0, + "initial": 0, + "gates": [ + 149, + 304 + ], + "minimum": 0, + "subsets": 4 + }, + { + "row": 1, + "initial": 21, + "gates": [ + 106 + ], + "minimum": 3, + "subsets": 2 + }, + { + "row": 2, + "initial": 0, + "gates": [ + 180, + 257 + ], + "minimum": 0, + "subsets": 4 + }, + { + "row": 3, + "initial": 16, + "gates": [ + 13, + 63, + 86, + 156 + ], + "minimum": 1, + "subsets": 16 + }, + { + "row": 4, + "initial": 0, + "gates": [ + 141, + 181 + ], + "minimum": 0, + "subsets": 4 + }, + { + "row": 5, + "initial": 130, + "gates": [ + 24, + 61, + 290 + ], + "minimum": 2, + "subsets": 8 + }, + { + "row": 6, + "initial": 0, + "gates": [ + 36, + 124, + 288 + ], + "minimum": 0, + "subsets": 8 + }, + { + "row": 7, + "initial": 129, + "gates": [ + 20, + 151, + 188 + ], + "minimum": 2, + "subsets": 8 + }, + { + "row": 8, + "initial": 96, + "gates": [ + 173 + ], + "minimum": 2, + "subsets": 2 + }, + { + "row": 9, + "initial": 2, + "gates": [ + 113, + 118, + 155, + 261 + ], + "minimum": 1, + "subsets": 16 + }, + { + "row": 10, + "initial": 0, + "gates": [ + 231, + 287 + ], + "minimum": 0, + "subsets": 4 + }, + { + "row": 11, + "initial": 0, + "gates": [ + 139, + 301 + ], + "minimum": 0, + "subsets": 4 + }, + { + "row": 12, + "initial": 0, + "gates": [ + 117, + 166, + 232 + ], + "minimum": 0, + "subsets": 8 + }, + { + "row": 13, + "initial": 1, + "gates": [ + 102, + 175, + 228 + ], + "minimum": 1, + "subsets": 8 + }, + { + "row": 14, + "initial": 0, + "gates": [ + 135, + 269, + 270 + ], + "minimum": 0, + "subsets": 8 + }, + { + "row": 15, + "initial": 0, + "gates": [ + 111, + 207, + 271 + ], + "minimum": 0, + "subsets": 8 + }, + { + "row": 16, + "initial": 0, + "gates": [ + 197, + 251 + ], + "minimum": 0, + "subsets": 4 + }, + { + "row": 17, + "initial": 256, + "gates": [ + 97, + 279 + ], + "minimum": 1, + "subsets": 4 + }, + { + "row": 18, + "initial": 0, + "gates": [ + 57, + 120, + 161, + 198 + ], + "minimum": 0, + "subsets": 16 + }, + { + "row": 19, + "initial": 261, + "gates": [ + 43, + 100, + 171 + ], + "minimum": 3, + "subsets": 8 + }, + { + "row": 20, + "initial": 0, + "gates": [ + 50, + 68, + 116, + 144, + 239 + ], + "minimum": 0, + "subsets": 32 + }, + { + "row": 21, + "initial": 0, + "gates": [ + 244, + 282 + ], + "minimum": 0, + "subsets": 4 + }, + { + "row": 22, + "initial": 256, + "gates": [ + 91, + 121, + 191 + ], + "minimum": 1, + "subsets": 8 + }, + { + "row": 23, + "initial": 0, + "gates": [ + 245, + 297 + ], + "minimum": 0, + "subsets": 4 + }, + { + "row": 24, + "initial": 171, + "gates": [ + 2, + 31, + 186 + ], + "minimum": 4, + "subsets": 8 + }, + { + "row": 25, + "initial": 64, + "gates": [ + 25, + 32, + 216 + ], + "minimum": 1, + "subsets": 8 + }, + { + "row": 26, + "initial": 39, + "gates": [ + 11, + 208 + ], + "minimum": 4, + "subsets": 4 + }, + { + "row": 27, + "initial": 320, + "gates": [ + 126, + 299 + ], + "minimum": 2, + "subsets": 4 + }, + { + "row": 28, + "initial": 3, + "gates": [ + 48, + 49, + 51, + 52, + 53, + 54, + 196 + ], + "minimum": 0, + "subsets": 128 + }, + { + "row": 29, + "initial": 0, + "gates": [ + 263, + 285 + ], + "minimum": 0, + "subsets": 4 + }, + { + "row": 30, + "initial": 0, + "gates": [ + 199, + 227 + ], + "minimum": 0, + "subsets": 4 + }, + { + "row": 31, + "initial": 290, + "gates": [ + 67 + ], + "minimum": 3, + "subsets": 2 + }, + { + "row": 32, + "initial": 0, + "gates": [ + 87, + 109, + 125, + 260 + ], + "minimum": 0, + "subsets": 16 + }, + { + "row": 33, + "initial": 0, + "gates": [ + 246, + 247 + ], + "minimum": 0, + "subsets": 4 + }, + { + "row": 34, + "initial": 1, + "gates": [ + 56, + 58, + 218 + ], + "minimum": 1, + "subsets": 8 + }, + { + "row": 35, + "initial": 34, + "gates": [ + 179 + ], + "minimum": 2, + "subsets": 2 + }, + { + "row": 36, + "initial": 0, + "gates": [ + 9, + 233, + 258 + ], + "minimum": 0, + "subsets": 8 + }, + { + "row": 37, + "initial": 0, + "gates": [ + 235, + 236 + ], + "minimum": 0, + "subsets": 4 + }, + { + "row": 38, + "initial": 64, + "gates": [ + 5, + 115, + 164 + ], + "minimum": 1, + "subsets": 8 + }, + { + "row": 39, + "initial": 64, + "gates": [ + 131, + 157, + 224 + ], + "minimum": 1, + "subsets": 8 + }, + { + "row": 40, + "initial": 64, + "gates": [ + 84, + 167, + 243 + ], + "minimum": 1, + "subsets": 8 + }, + { + "row": 41, + "initial": 0, + "gates": [ + 10, + 212, + 213 + ], + "minimum": 0, + "subsets": 8 + }, + { + "row": 42, + "initial": 0, + "gates": [ + 255, + 265 + ], + "minimum": 0, + "subsets": 4 + }, + { + "row": 43, + "initial": 192, + "gates": [ + 59, + 221 + ], + "minimum": 2, + "subsets": 4 + }, + { + "row": 44, + "initial": 34, + "gates": [ + 178 + ], + "minimum": 2, + "subsets": 2 + }, + { + "row": 45, + "initial": 310, + "gates": [ + 18 + ], + "minimum": 5, + "subsets": 2 + }, + { + "row": 46, + "initial": 0, + "gates": [ + 137, + 302 + ], + "minimum": 0, + "subsets": 4 + }, + { + "row": 47, + "initial": 96, + "gates": [ + 47, + 266, + 298 + ], + "minimum": 1, + "subsets": 8 + }, + { + "row": 48, + "initial": 100, + "gates": [ + 19, + 162 + ], + "minimum": 3, + "subsets": 4 + }, + { + "row": 49, + "initial": 4, + "gates": [ + 8, + 46, + 98, + 146, + 183 + ], + "minimum": 1, + "subsets": 32 + }, + { + "row": 50, + "initial": 17, + "gates": [ + 3, + 65, + 72, + 295 + ], + "minimum": 2, + "subsets": 16 + }, + { + "row": 51, + "initial": 1, + "gates": [ + 101, + 184, + 242 + ], + "minimum": 1, + "subsets": 8 + }, + { + "row": 52, + "initial": 256, + "gates": [ + 143, + 145, + 272 + ], + "minimum": 1, + "subsets": 8 + }, + { + "row": 53, + "initial": 67, + "gates": [ + 128 + ], + "minimum": 3, + "subsets": 2 + }, + { + "row": 54, + "initial": 128, + "gates": [ + 163, + 252 + ], + "minimum": 1, + "subsets": 4 + }, + { + "row": 55, + "initial": 256, + "gates": [ + 4, + 127, + 203 + ], + "minimum": 1, + "subsets": 8 + }, + { + "row": 56, + "initial": 0, + "gates": [ + 85, + 112, + 296 + ], + "minimum": 0, + "subsets": 8 + }, + { + "row": 57, + "initial": 0, + "gates": [ + 154, + 305 + ], + "minimum": 0, + "subsets": 4 + }, + { + "row": 58, + "initial": 67, + "gates": [ + 70, + 219 + ], + "minimum": 3, + "subsets": 4 + }, + { + "row": 59, + "initial": 0, + "gates": [ + 34, + 182, + 286 + ], + "minimum": 0, + "subsets": 8 + }, + { + "row": 60, + "initial": 0, + "gates": [ + 0, + 55, + 69, + 148, + 283 + ], + "minimum": 0, + "subsets": 32 + }, + { + "row": 61, + "initial": 2, + "gates": [ + 83, + 195 + ], + "minimum": 1, + "subsets": 4 + }, + { + "row": 62, + "initial": 4, + "gates": [ + 134, + 201, + 294 + ], + "minimum": 1, + "subsets": 8 + }, + { + "row": 63, + "initial": 0, + "gates": [ + 12, + 280, + 291 + ], + "minimum": 0, + "subsets": 8 + }, + { + "row": 64, + "initial": 256, + "gates": [ + 27, + 138 + ], + "minimum": 1, + "subsets": 4 + }, + { + "row": 65, + "initial": 24, + "gates": [ + 16, + 281 + ], + "minimum": 2, + "subsets": 4 + }, + { + "row": 66, + "initial": 0, + "gates": [ + 152, + 303 + ], + "minimum": 0, + "subsets": 4 + }, + { + "row": 67, + "initial": 16, + "gates": [ + 1, + 82, + 132, + 153 + ], + "minimum": 1, + "subsets": 16 + }, + { + "row": 68, + "initial": 257, + "gates": [ + 33, + 62, + 92, + 93, + 94, + 95, + 119, + 289 + ], + "minimum": 1, + "subsets": 256 + }, + { + "row": 69, + "initial": 16, + "gates": [ + 15, + 123, + 202 + ], + "minimum": 1, + "subsets": 8 + }, + { + "row": 70, + "initial": 0, + "gates": [ + 35, + 240, + 241 + ], + "minimum": 0, + "subsets": 8 + }, + { + "row": 71, + "initial": 0, + "gates": [ + 214, + 215 + ], + "minimum": 0, + "subsets": 4 + }, + { + "row": 72, + "initial": 32, + "gates": [ + 160, + 300 + ], + "minimum": 1, + "subsets": 4 + }, + { + "row": 73, + "initial": 0, + "gates": [ + 129, + 259, + 284 + ], + "minimum": 0, + "subsets": 8 + }, + { + "row": 74, + "initial": 0, + "gates": [ + 104, + 108, + 268 + ], + "minimum": 0, + "subsets": 8 + }, + { + "row": 75, + "initial": 2, + "gates": [ + 41, + 71, + 89, + 172, + 200 + ], + "minimum": 1, + "subsets": 32 + }, + { + "row": 76, + "initial": 2, + "gates": [ + 105, + 174 + ], + "minimum": 1, + "subsets": 4 + }, + { + "row": 77, + "initial": 0, + "gates": [ + 40, + 60, + 66, + 130, + 253 + ], + "minimum": 0, + "subsets": 32 + }, + { + "row": 78, + "initial": 0, + "gates": [ + 114, + 205, + 206 + ], + "minimum": 0, + "subsets": 8 + }, + { + "row": 79, + "initial": 0, + "gates": [ + 76, + 77, + 78, + 79, + 80, + 81, + 168 + ], + "minimum": 0, + "subsets": 128 + }, + { + "row": 80, + "initial": 0, + "gates": [ + 17, + 122, + 147, + 234 + ], + "minimum": 0, + "subsets": 16 + }, + { + "row": 81, + "initial": 8, + "gates": [ + 185, + 256 + ], + "minimum": 1, + "subsets": 4 + }, + { + "row": 82, + "initial": 0, + "gates": [ + 29, + 30, + 165 + ], + "minimum": 0, + "subsets": 8 + }, + { + "row": 83, + "initial": 0, + "gates": [ + 21, + 142, + 169 + ], + "minimum": 0, + "subsets": 8 + }, + { + "row": 84, + "initial": 0, + "gates": [ + 229, + 230 + ], + "minimum": 0, + "subsets": 4 + }, + { + "row": 85, + "initial": 0, + "gates": [ + 262, + 293 + ], + "minimum": 0, + "subsets": 4 + }, + { + "row": 86, + "initial": 256, + "gates": [ + 42, + 211 + ], + "minimum": 1, + "subsets": 4 + }, + { + "row": 87, + "initial": 0, + "gates": [ + 44, + 45, + 267 + ], + "minimum": 0, + "subsets": 8 + }, + { + "row": 88, + "initial": 128, + "gates": [ + 64, + 133 + ], + "minimum": 1, + "subsets": 4 + }, + { + "row": 89, + "initial": 0, + "gates": [ + 26, + 96, + 136, + 237 + ], + "minimum": 0, + "subsets": 16 + }, + { + "row": 90, + "initial": 0, + "gates": [ + 140, + 217 + ], + "minimum": 0, + "subsets": 4 + }, + { + "row": 91, + "initial": 0, + "gates": [ + 192, + 193, + 194 + ], + "minimum": 0, + "subsets": 8 + }, + { + "row": 92, + "initial": 2, + "gates": [ + 90, + 292 + ], + "minimum": 1, + "subsets": 4 + }, + { + "row": 93, + "initial": 3, + "gates": [ + 37, + 38, + 39, + 150, + 159 + ], + "minimum": 1, + "subsets": 32 + }, + { + "row": 94, + "initial": 0, + "gates": [ + 23, + 73, + 74, + 75, + 177 + ], + "minimum": 0, + "subsets": 32 + }, + { + "row": 95, + "initial": 1, + "gates": [ + 22, + 88, + 158 + ], + "minimum": 1, + "subsets": 8 + }, + { + "row": 96, + "initial": 272, + "gates": [ + 6, + 7 + ], + "minimum": 2, + "subsets": 4 + }, + { + "row": 97, + "initial": 96, + "gates": [ + 220 + ], + "minimum": 2, + "subsets": 2 + }, + { + "row": 98, + "initial": 0, + "gates": [ + 238, + 275 + ], + "minimum": 0, + "subsets": 4 + }, + { + "row": 99, + "initial": 0, + "gates": [ + 250, + 264 + ], + "minimum": 0, + "subsets": 4 + }, + { + "row": 100, + "initial": 0, + "gates": [ + 248, + 249 + ], + "minimum": 0, + "subsets": 4 + }, + { + "row": 101, + "initial": 0, + "gates": [ + 103, + 107, + 204, + 209 + ], + "minimum": 0, + "subsets": 16 + }, + { + "row": 102, + "initial": 5, + "gates": [ + 28, + 99, + 210, + 254 + ], + "minimum": 2, + "subsets": 16 + }, + { + "row": 103, + "initial": 0, + "gates": [ + 110, + 276, + 278 + ], + "minimum": 0, + "subsets": 8 + }, + { + "row": 104, + "initial": 0, + "gates": [ + 273, + 274 + ], + "minimum": 0, + "subsets": 4 + }, + { + "row": 105, + "initial": 74, + "gates": [ + 14 + ], + "minimum": 3, + "subsets": 2 + }, + { + "row": 106, + "initial": 257, + "gates": [ + 170, + 190 + ], + "minimum": 2, + "subsets": 4 + }, + { + "row": 107, + "initial": 0, + "gates": [ + 176, + 187 + ], + "minimum": 0, + "subsets": 4 + }, + { + "row": 108, + "initial": 0, + "gates": [ + 189, + 277 + ], + "minimum": 0, + "subsets": 4 + }, + { + "row": 109, + "initial": 0, + "gates": [ + 225, + 226 + ], + "minimum": 0, + "subsets": 4 + }, + { + "row": 110, + "initial": 0, + "gates": [ + 222, + 223 + ], + "minimum": 0, + "subsets": 4 + } + ], + "essential_dependencies": [ + [ + 47, + 6 + ], + [ + 93, + 37 + ], + [ + 37, + 36 + ], + [ + 39, + 36 + ] + ], + "initial_rows": [ + 0, + 21, + 0, + 16, + 0, + 130, + 0, + 129, + 96, + 2, + 0, + 0, + 0, + 1, + 0, + 0, + 0, + 256, + 0, + 261, + 0, + 0, + 256, + 0, + 171, + 64, + 39, + 320, + 3, + 0, + 0, + 290, + 0, + 0, + 1, + 34, + 0, + 0, + 64, + 64, + 64, + 0, + 0, + 192, + 34, + 310, + 0, + 96, + 100, + 4, + 17, + 1, + 256, + 67, + 128, + 256, + 0, + 0, + 67, + 0, + 0, + 2, + 4, + 0, + 256, + 24, + 0, + 16, + 257, + 16, + 0, + 0, + 32, + 0, + 0, + 2, + 2, + 0, + 0, + 0, + 0, + 8, + 0, + 0, + 0, + 0, + 256, + 0, + 128, + 0, + 0, + 0, + 2, + 3, + 0, + 1, + 272, + 96, + 0, + 0, + 0, + 0, + 5, + 0, + 0, + 74, + 257, + 0, + 0, + 0, + 0 + ], + "increments": [ + 0, + 0, + 0, + 0, + 0, + 96, + 96, + 4, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 24, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 32, + 257, + 0, + 2, + 128, + 0, + 0, + 0, + 0, + 3, + 257, + 0, + 2, + 128, + 0, + 4, + 0, + 0, + 128, + 96, + 32, + 0, + 0, + 0, + 1, + 2, + 67, + 256, + 4, + 0, + 0, + 64, + 0, + 4, + 0, + 3, + 17, + 64, + 3, + 0, + 0, + 64, + 0, + 0, + 3, + 0, + 128, + 32, + 130, + 0, + 0, + 8, + 8, + 2, + 3, + 0, + 64, + 0, + 4, + 0, + 0, + 32, + 0, + 256, + 0, + 0, + 256, + 0, + 0, + 0, + 32, + 0, + 32, + 32, + 0, + 128, + 0, + 0, + 0, + 3, + 24, + 3, + 24, + 0, + 0, + 32, + 0, + 0, + 0, + 0, + 36, + 0, + 67, + 64, + 3, + 64, + 3, + 0, + 36, + 3, + 0, + 43, + 0, + 0, + 67, + 36, + 74, + 0, + 0, + 258, + 36, + 372, + 3, + 129, + 3, + 132, + 0, + 100, + 100, + 64, + 67, + 52, + 3, + 0, + 257, + 24, + 3, + 24, + 256, + 24, + 36, + 310, + 96, + 4, + 100, + 24, + 32, + 132, + 356, + 39, + 67, + 260, + 124, + 293, + 25, + 25, + 22, + 260, + 0, + 260, + 164, + 138, + 372, + 3, + 22, + 36, + 84, + 25, + 11, + 372, + 164, + 124, + 36, + 22, + 36, + 292, + 316, + 372, + 25, + 104, + 36, + 352, + 24, + 358, + 11, + 48, + 129, + 3, + 60, + 310, + 39, + 372, + 138, + 316, + 25, + 3, + 168, + 36, + 104, + 129, + 124, + 134, + 36, + 138, + 103, + 3, + 74, + 285, + 36, + 21, + 171, + 285, + 3, + 358, + 3, + 118, + 3, + 382, + 3, + 290, + 25, + 36, + 279, + 36, + 385, + 385, + 310, + 39, + 39, + 3, + 342, + 36, + 299, + 36, + 138, + 342, + 502, + 134, + 3, + 285, + 508, + 179, + 60, + 248, + 234, + 60, + 36, + 351, + 314, + 124, + 3, + 370, + 36, + 253, + 134, + 234, + 3, + 416, + 193, + 36, + 508, + 511, + 502, + 60, + 55, + 364, + 502, + 309, + 145, + 409, + 412, + 25, + 488, + 369, + 398, + 499, + 199, + 454, + 499, + 59, + 158, + 425, + 398, + 502, + 488, + 457, + 454, + 499, + 481 + ], + "dirty_columns": 661, + "complete_ADDs": [ + 11500, + 11067 + ], + "controls": [ + "nonideal relaxed 93-ADD proposal", + "missing essential dependency", + "erased compensating row cost", + "old scatter with changed basis", + "omitted undo on dirty targets" + ], + "scope": "All dependency ideals of this pinned undo circuit, not arbitrary circuits or supplier admission" +} diff --git a/research/r439-deferred-ideal-optimum/PROOF.md b/research/r439-deferred-ideal-optimum/PROOF.md new file mode 100644 index 0000000000..23e8f98b4a --- /dev/null +++ b/research/r439-deferred-ideal-optimum/PROOF.md @@ -0,0 +1,173 @@ +# Exact optimum over all dependency ideals + +## Statement and scope + +Take the PR1062 word pinned in SOURCES.json. Number its 111 target rows from 0 through 110. +Number the 306 elementary gates in its literal target-basis undo from 0 through 305. +These are local target indices; physical target register r is 111+r. + +Let E be the target-basis preparation and S the 111-by-9 binary scatter matrix. +The undo is the literal reverse of E. Every undo gate has the form d ^= s. +All target-basis gates use frame zero. + +For every subset I of the 306 undo gates, impose this condition: +if i belongs to I and an earlier gate j does not commute with i, then j belongs to I. +Such subsets are precisely the dependency ideals used in PR2115, section 5. +There is no restriction on the size of I. +Let G_I apply its selected gates in their original order. + +**Theorem.** The minimum of nnz(G_I E S), over all these ideals I, is exactly 94. +The ideal {31,51,52} attains the minimum. + +Here nnz counts ones over F2. Each scatter entry costs one ADD. +All 306 undo gates remain present, either before or after the scatter. +This result does not optimize a different basis circuit, interleaving within the scatter, frame paths, or extra workspace. +It does not assert supplier admission or a new exponent. + +## Constant increments from a complete circuit + +Write P=ES. Execute the complete undo on P once. +For gate i=(d_i,s_i), let a_i be its source row immediately before that gate in this complete execution. +For an ideal I, the resulting row d is + +```text +P_d XOR XOR_{i in I, d_i=d} a_i. (1) +``` + +**Proof.** Proceed in the order of selected gates. +Every earlier gate that writes s_i does not commute with gate i, so the ideal contains it. +By induction, each such earlier selected gate adds the same source row as in the complete execution. +Thus s_i has its complete-execution value when gate i runs. +This proves the claim about its increment, and summing the increments gives (1). + +The empty prefix supplies the induction base. + +For completeness, two elementary transvections (d,s) and (e,t) commute exactly when d is not t and e is not s. +The source binding contains 850 earlier noncommuting pairs. +The independent checker reconstructs these pairs by multiplying their small coefficient matrices. + +Equation (1) is a consequence of the ideal condition. +An arbitrary nonideal subset does not establish a valid circuit through this equation. +In particular, {31,47,51,52} has relaxed cost 93 but omits necessary predecessors of gate 47. +The verifier rejects that subset. + +## A certificate using row weights + +Represent each nine-bit row by its integer mask, with scatter column 0 as the least significant bit. +Let w_d be the Hamming weight of row d after applying (1). +For each row, temporarily allow every subset of the gates that write that row, ignoring dependencies. +This only enlarges the feasible set, so a row lower bound remains valid for every ideal. + +There are 1,386 such row subsets in total. +The most populated row has eight writer gates, so its table has 256 cases. +CERTIFICATE.json lists each row's initial mask, writer indices, case count, and minimum. +The initial total is 97. +Every row except 24,28,47,68,93 has minimum equal to its initial weight. +The five exceptional minima are respectively 4,0,1,1,1, with initial weights 5,2,2,2,2. + +The following seven exact row expressions contain every nonzero coefficient needed for the stronger bound. +Here z_i is 1 when gate i belongs to I, and multiplication by z_i selects a mask or zero. +All displayed additions are bitwise XOR, not integer addition. +Zero increments do not appear. + +| Row d | Row mask after selected increments | +|---:|---| +| 6 | 3 z_36 XOR 25 z_288 | +| 24 | 171 XOR 128 z_31 XOR 372 z_186 | +| 28 | 3 XOR z_51 XOR 2 z_52 XOR 67 z_53 XOR 256 z_54 XOR 104 z_196 | +| 47 | 96 XOR 32 z_47 XOR 124 z_266 XOR 425 z_298 | +| 68 | 257 XOR 3 z_62 XOR 256 z_93 XOR 67 z_119 XOR 488 z_289 | +| 93 | 3 XOR 257 z_37 XOR 2 z_39 XOR 96 z_159 | +| 96 | 272 XOR 96 z_6 XOR 4 z_7 | + +Their complete truth tables give these implications: + +1. w_47 < 2 implies z_47=1; z_6=1 implies w_96 >= 4. +2. w_68 < 2 implies z_93=1. +3. w_93 < 2 implies z_39=1; z_36=1 implies w_6 >= 2. + +These are small explicit finite statements, not numerical approximations. +Both checkers exhaust their truth tables, including choices that violate the ideal condition. +The relevant ideal implications are + +```text +z_47 <= z_6, +z_93 <= z_37 <= z_36, +z_39 <= z_36. (2) +``` + +Each implication in (2) is a direct noncommuting dependency, not a guessed relation. + +First group rows 47 and 96. If w_47 >= 2, their sum is at least 2+2=4. +Otherwise (2) forces z_6=1, and their sum is at least 1+4=5. +Thus w_47+w_96 >= 4 in either case. + +Next group rows 68,93,6. If neither of the first two weights drops, their sum is at least 2+2+0=4. +If either drops, (2) forces z_36=1, giving a sum of at least 1+1+2=4. +Thus this second group always costs at least 4. + +The other 104 rows exclude these five grouped rows and rows 24,28. +Their individual minima sum to 82. +Rows 24 and 28 cost at least 4 and 0. +Adding the disjoint groups proves + +```text +nnz(G_I E S) >= 82 + 4 + 0 + 4 + 4 = 94. (3) +``` + +No search over a bounded ideal size enters (3). +The certificate covers every ideal, through the row relaxation and its four necessary dependencies. + +## Attainment and complete word boundary + +Gates 31,51,52 have no earlier noncommuting predecessor, so their set is an ideal. +Their literal execution changes only row 24 from 171 to 43 and row 28 from 3 to 0. +The total weight falls from 97 to 94. +This is the same attaining split already reported by Sagar Thakrar in PR2115. +The new contribution is its optimality over every ideal. + +To connect the optimization with the stated circuit class, write the complete undo as U. +Any omitted gate that precedes a selected gate commutes with it, by the ideal condition. +Repeatedly exchanging these pairs puts selected gates first without changing the product. +Thus U equals the remaining undo after G_I, in execution order. + +Keep G_I in D, use listing G_I E S, and put the remaining undo before the original B. +A never reads or writes a target, so the target basis commutes past A. +The copied totals depend only on sources and helpers and remain unchanged. +The modified scatter contributes G_I E S c to the targets for arbitrary copied values c. +The remaining undo cancels G_I E and restores the original S c contribution. +After this undo, the entire state agrees with the original word before B. + +The unchanged B and C therefore give the same boundary. + +This argument is a binary coefficient identity on arbitrary source, target, and helper inputs. +It extends to any F2-module through the same coefficients. +The verifier also executes the literal COPY/ERASE stream on all 661 input columns, in both directions. +It obtains (x,y,h) -> (x,y+x,h), including restoration of every arbitrary helper. + +The 306 undo ADDs move but remain charged. The scatter decreases from 527 to 94. +The complete local ADD count is therefore 11,500-527+94=11,067. +Nine COPY/ERASE pairs, preparation, helpers, A, C, and the original B remain present. + +All moved gates use frame zero and preserve the target paths and recursive profile under the inherited realization. +PR2115 supplies the chronological argument and its reported guards for this exact attaining split. +This package does not repeat its native, hosting, precision, or supplier-admission obligations. + +## Independent validation and limits + +The primary checker follows forward row states to derive P and all 306 increments. +It enumerates row subsets and checks (2), (3), and the complete attaining word. + +The separate checker imports no primary or predecessor implementation. +It derives every coefficient through backward propagation of a row functional through the original circuit. +It evaluates all row choices as Boolean truth-table bit planes. +It reconstructs the dependency relation by literal multiplication of transvection matrices. +It also checks the attaining reorder as a complete 111-by-111 coefficient map. +These checks validate the crucial coefficients and lower-bound premises through different traversals and models. + +They do not constitute independent human review or proof-assistant verification. + +Z3 4.15.3 first found that the exact full-ideal model has no solution of cost at most 93. +That exploratory answer is not a premise of the proof or a runtime dependency. +The small certificate above replaces solver trust and large ideal enumeration. +The finite source facts remain tied to the pinned word and the stated gate ordering. diff --git a/research/r439-deferred-ideal-optimum/README.md b/research/r439-deferred-ideal-optimum/README.md new file mode 100644 index 0000000000..07522c6dd1 --- /dev/null +++ b/research/r439-deferred-ideal-optimum/README.md @@ -0,0 +1,71 @@ +# The deferred R439 scatter has exact ideal optimum 94 + +**Independent verification / finite optimality result; no new supplier or kappa.** +For the pinned PR1062 word, every dependency ideal of its 306-gate target-basis undo has scatter cost at least 94 ADDs. +The known ideal {31,51,52} attains 94. +This closes PR2115's larger-ideal question for this word, with no bound on ideal size. + +Sagar Thakrar's [PR2115](https://github.com/CrocSwap/integer-mult-bounds/pull/2115), head `b56dceffad83c88e8ad39ffd82a1bdd55c4130da`, supplies the construction and attaining split. +Its search checks ideals of size at most four and explicitly leaves larger ideals open. +The new result is a complete lower bound, not a new circuit or a repeated small census. + +[PROOF.md](PROOF.md) gives the exact claim, constant-increment lemma, row inequalities, dependency argument, and attainment. +Only five rows can improve over the 97-ADD start. +Necessary dependencies charge three possible improvements back to two other rows. +The resulting disjoint row bounds sum to 94. +All 1,386 unrestricted row subsets certify the premises; the proof avoids enumeration of all ideals. + +## Reproduce + +Standard library only, from the repository root: + +```sh +python3 -I -O -B research/r439-deferred-ideal-optimum/verify.py && python3 -I -O -B research/r439-deferred-ideal-optimum/independent.py +``` + +Expected: + +```text +PASS_R439_DEFERRED_IDEAL_OPTIMUM minimum=94 gates=306 row_subsets=1386 dirty_columns=661 controls=5 no_new_kappa +PASS_INDEPENDENT_IDEAL_AUDIT backward_coefficients=417 row_subsets=1386 matrix_dependencies=850 minimum=94 +``` + +The primary checker uses forward row states and complete arbitrary-dirty input columns. +The separate checker uses backward coefficient cones, Boolean truth tables, and literal small-matrix commutators. +It imports no primary or predecessor engine. +Five controls reject a cheaper nonideal subset, a missing dependency, a missing compensating cost, an old scatter, and an omitted undo. +Checks remain active under Python optimization. + +The frozen certificate records every row minimum and all consumed coefficients. +An exact SMT model helped discover the bound; replay uses neither Z3 nor its answer. + +## Accounting and scope + +The complete attaining word costs 11,500-527+94=11,067 scalar ADDs, as already reported by PR2115. +All 306 undo gates remain charged, with nine COPY/ERASE pairs and all helpers restored. +The verifier independently checks all 661 dirty input columns in both directions through the literal stream. +The construction preserves the inherited frame paths and paid profile; this package does not regenerate their invoice. + +The theorem concerns one fixed undo circuit, its nine-column scatter, and every commutation-closed split into D and B. +It does not cover new basis circuits, different frame paths, scatter interleavings, or extra workspace. +Native address action, stage hosting, precision/tape, all-size realization, and the multiplication theorem remain inherited or unverified here. +We claim neither independent human review nor a full selected-frontier replay. + +## Open next questions + +A different target-basis circuit could improve the deferred objective. +First price both basis directions and the resulting scatter, then verify the dirty boundary and full precision charge. +The present optimum applies only to the frozen 306-gate circuit; it supplies no global lower bound for that changed problem. +Structured scope and blockers appear in [TASK.json](TASK.json). + +## Credit + +Credit Sagar Thakrar for PR2115's deferred basis and PR1062's composed word. +Credit Gareth Davidson for the PR915 target basis, with commdata2338, Scott Woolsey Biggart, and Sagar Thakrar in its lineage. +The R439 word retains Sricharan Vagvala's helper stars, Aaron Wang's B circuits, Ross Richardson's frame circuit, and DreamingOfClouds' tuning. +The interface and exporter lineage includes eumemic, Zhihao Chen, woklerx, Arham Tahir, and Dylan Crow. +All predecessor source files remain unchanged. + +Prepared for Charles Bethin with substantial OpenAI Codex assistance in the proof, implementation, checks, and writing. +The two implementations have the same AI author; their independence is algorithmic, not human. +New material is Apache-2.0. diff --git a/research/r439-deferred-ideal-optimum/SOURCES.json b/research/r439-deferred-ideal-optimum/SOURCES.json new file mode 100644 index 0000000000..46e8c6fdf9 --- /dev/null +++ b/research/r439-deferred-ideal-optimum/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "research/r439-bsection-stars-seed01/candidate.json.gz", + "usage": "input", + "git_blob": "9a17b4920334878d6c949191f6931bd97126fe3c", + "sha256": "b452d2c2b0b2a546d1105b1da9769aa78e5c54d6f00e97b30c77e3f54ce445ee" + } + ] +} diff --git a/research/r439-deferred-ideal-optimum/TASK.json b/research/r439-deferred-ideal-optimum/TASK.json new file mode 100644 index 0000000000..08ae8c6279 --- /dev/null +++ b/research/r439-deferred-ideal-optimum/TASK.json @@ -0,0 +1,106 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "bit-helper-contract", + "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?", + "starting_points": [ + "research/r439-bsection-stars-seed01/README.md", + "research/r439-copy-path-sharing-barrier/README.md" + ], + "methods": [ + "Derive a replacement interface lemma and price its implementation.", + "Seek an exact dirty-input or chronological-cut counterexample to the proposed replacement." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient.", + "first_step": { + "command": [ + "python3", + "-B", + "research/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.", + "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.", + "allowed_variations": [ + "Choose one helper-star or quartet instance; narrow to one boundary implication." + ], + "scope_change_triggers": [ + "Changing only source count or scalar addition count without an interface argument." + ], + "overlap_terms": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D", + "helper-star" + ] + }, + "scope_status": "changed", + "actual_scope": "Prove the exact minimum scatter ADD count over all dependency ideals of the pinned PR1062 306-gate target-basis undo, answering the explicit PR2115 open question without an ideal-size bound.", + "scope_change_reason": "The user assigned bit-supplier seed 9. The retained semantic D lemma already covers restored helper mixing. This side result completes the finite optimization question in PR2115 rather than deriving that existing lemma again.", + "bottleneck_link": "This closes a specific local optimization route under a changed target-basis interface. It does not change paid recursive rank mass, the selected bit supplier, or kappa.", + "budget_minutes": 45, + "stop_rule": "Prove the full ideal bound or save the incomplete model locally. No further size-bounded census merits publication. Reserve the final quarter for verification and handoff.", + "outcome": "completed", + "evidence": "PROOF.md and CERTIFICATE.json: exact lower bound 94, attained by {31,51,52}, 1386 unrestricted row subsets, four essential dependencies, separate backward coefficients and matrix commutators, 661 dirty columns in both directions, and five negative controls.", + "author": "Charles Bethin with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in mathematics, implementation, verification and writing. Same AI author for both algorithms; no independent human review or proof-assistant verification.", + "open_questions": [ + { + "question": "Can a different target-basis circuit beat the fully priced deferred objective?", + "why_it_matters": "The exact 94 bound covers only this fixed undo word. A new circuit changes the feasible problem.", + "first_step": "Price preparation, undo and scatter together, then verify the arbitrary-dirty boundary and precision charge.", + "blocked_by": "No such completed candidate or physical supplier invoice is supplied." + } + ], + "session_id": "01a1335e-7a24-73c3-a549-9bcb5496a363", + "start_time": "2026-10-15T02:56:33Z", + "experiment_seed": 9, + "seed_method": "secrets.randbelow(100), operating-system random", + "track": "bit supplier", + "coordination": "No pinned coordination issue at the 03:00 UTC query. Local claim saved in the originating research capture.", + "predecessors": [ + { + "pr": 2115, + "head": "b56dceffad83c88e8ad39ffd82a1bdd55c4130da", + "author": "Sagar Thakrar", + "credit": "Deferred target-basis contract, ideal-split construction and known 94-ADD attaining split", + "proof_sha256": "3a921c0e7cb8670dc28980e08635e0c1361f88f5391b14254438b56a699e488b" + }, + { + "pr": 1062, + "author": "Sagar Thakrar", + "credit": "Pinned 11500-ADD R439 B/star word, retained at the base commit" + } + ], + "overlap": { + "open_prs": 495, + "open_prs_complete_pagination": true, + "recent_discussions": 12, + "targeted_discussion_searches": [ + "order ideal", + "deferred target" + ], + "limits": "Targeted search is not a complete comment or code-diff index. Local package READMEs and review ledger also checked. Final live refresh recorded before publication.", + "prepublication": { + "checked_at": "2026-10-15T03:14:32.459445Z", + "canonical_main": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "open_prs": 501, + "open_prs_complete_pagination": true, + "matching_prs": [ + 2115 + ], + "predecessor_head": "b56dceffad83c88e8ad39ffd82a1bdd55c4130da", + "predecessor_comments": 0, + "predecessor_reviews": 0, + "cached_discussions": 937, + "cached_discussions_fetched_at": "2026-10-15T01:39:09.767583Z", + "cached_discussions_complete_pagination": true, + "cached_warning": "Offline snapshot may miss later comments; 12 recent live discussions and targeted live searches supplement it." + } + } +} diff --git a/research/r439-deferred-ideal-optimum/VALIDATION.json b/research/r439-deferred-ideal-optimum/VALIDATION.json new file mode 100644 index 0000000000..61f36f07f3 --- /dev/null +++ b/research/r439-deferred-ideal-optimum/VALIDATION.json @@ -0,0 +1,44 @@ +{ + "status": "locally verified; hosted CI and external human review not claimed", + "checked_at": "2026-10-15T03:15:34.122114+00:00", + "runtime": { + "sys_version": "3.15.0 (main, Oct 9 2026, 11:16:41) [Clang 21.0.0 (clang-2100.3.34.2)]", + "sys_executable": "/opt/homebrew/opt/python@3.15/bin/python3.15", + "wrapper": "research-python", + "official_release": "https://www.python.org/downloads/", + "latest_stable_confirmed": "3.15.0" + }, + "registered_runtime": { + "version": "3.12.12", + "executable": "/opt/homebrew/opt/python@3.12/bin/python3.12", + "exception": "Repository VERIFY.json explicitly pins Python 3.12; direct research checks use latest stable 3.15.0." + }, + "checks": { + "optimized_primary": "PASS", + "optimized_independent": "PASS", + "registered_package": "PASS", + "metadata_and_source_pins": "PASS", + "minimal_git_free_relocation": "both commands PASS", + "corrupt_source": "both actual entry points reject", + "corrupt_coefficient": "both actual entry points reject", + "falsely_stronger_bound": "primary actual entry point rejects", + "STE": "PASS", + "mathematical_review": "Written ideal lemma, disjoint row inequalities and attainment reviewed separately from the executable package." + }, + "discovery": { + "solver": "Z3 4.15.3", + "result": "Full 306-variable ideal model rejects scatter cost at most 93; replaced by an elementary lower-bound certificate.", + "not_a_dependency": true + }, + "limitations": [ + "No independent human review or proof assistant.", + "No native address action, hosted invoice, guard regeneration, selected cold replay, or new kappa.", + "Algorithmic independence covers coefficients, row truth tables, dependencies and attaining target matrix; the full 661-column word replay has one implementation." + ], + "verified_code_sha256": { + "verify.py": "94598d648780ffe6d35d4df75f2fde6dccb504bd47b7477c406dfbbd762f0a99", + "independent.py": "73eb9e4c521b233d8965d97da276cfb1c8b8d4c2b95873a81bada09e030f7b0b", + "CERTIFICATE.json": "9ebeb9837bf4a3b0a6a5d6b2d5ad10520a8bbab9743fd499e609e1680a552f34", + "PROOF.md": "2afff55067fcc854c5aaf87a84884de8ea100238c56f52c4c34ab6b8acbd983d" + } +} diff --git a/research/r439-deferred-ideal-optimum/VERIFY.json b/research/r439-deferred-ideal-optimum/VERIFY.json new file mode 100644 index 0000000000..30e285dcd2 --- /dev/null +++ b/research/r439-deferred-ideal-optimum/VERIFY.json @@ -0,0 +1,33 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/r439-bsection-stars-seed01/candidate.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Source-bound complete all-ideal proof certificate, attaining literal forward/reverse dirty boundary and five negative controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Separate backward coefficient reconstruction, Boolean truth-table minima, matrix-derived dependencies and complete attaining reorder." + } + ] +} diff --git a/research/r439-deferred-ideal-optimum/independent.py b/research/r439-deferred-ideal-optimum/independent.py new file mode 100644 index 0000000000..80cd93f177 --- /dev/null +++ b/research/r439-deferred-ideal-optimum/independent.py @@ -0,0 +1,127 @@ +#!/usr/bin/env python3 +"""Backward coefficient-cone and Boolean truth-table audit, no verifier imports. +Apache-2.0. Substantial OpenAI Codex assistance; not independent human review. +""" +import gzip +import hashlib +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def check(value, label): + if not value: + raise RuntimeError(label) + + +def pullback(row, gates): + """Apply a row functional backward through the circuit.""" + support = set(row) + for d, s in reversed(gates): + if d in support: + support.symmetric_difference_update((s,)) + return support + + +def evaluate(support, source_rows): + result = [0] * 9 + for k in support: + for j in source_rows[k]: + result[j] ^= 1 + return sum(b << j for j, b in enumerate(result)) + + +def two_gate_matrix(a, b): + labels = set(a + b) + rows = {i: {i} for i in labels} + for d, s in (a, b): + rows[d] = rows[d] ^ rows[s] + return rows + + +def audit(): + pins = json.loads((HERE / 'SOURCES.json').read_text()) + source = next(x for x in pins['files'] if x['usage'] == 'input') + raw = (ROOT / source['path']).read_bytes() + check(hashlib.sha256(raw).hexdigest() == source['sha256'], 'source pin') + word = json.loads(gzip.decompress(raw)) + certificate = json.loads((HERE / 'CERTIFICATE.json').read_text()) + v = word['v'] + preparation, undo = [], [] + reading = False + for frame, dest, sources in word['D']: + if dest not in range(v, 2*v): + continue + if all(s in range(2*v, 2*v + word['R']) for s in sources): + reading = True + else: + check(frame == 0 and len(sources) == 1 and sources[0] in range(v, 2*v), 'target gate') + (undo if reading else preparation).append((dest-v, sources[0]-v)) + check(len(undo) == 306 and preparation == undo[::-1], 'circuit pin') + # No forward row-state traversal is used to reconstruct these coefficients. + initial = [evaluate(pullback((d,), preparation), word['scatter']) for d in range(v)] + coefficients = [evaluate(pullback((s,), preparation + undo[:i]), word['scatter']) + for i, (_, s) in enumerate(undo)] + check(initial == certificate['initial_rows'], 'backward initial rows') + check(coefficients == certificate['increments'], 'backward gate coefficients') + # Reconstruct noncommutation by literal multiplication of tiny matrices. + deps = {(i, j) for i, a in enumerate(undo) for j, b in enumerate(undo[:i]) + if two_gate_matrix(a, b) != two_gate_matrix(b, a)} + check(len(deps) == 850, 'matrix commutator count') + check(all(tuple(x) in deps for x in certificate['essential_dependencies']), 'essential matrix commutators') + lower = [] + weights = {} + variables = {} + total = 0 + for row in range(v): + gates = [i for i, (d, _) in enumerate(undo) if d == row] + assignments = 1 << len(gates) + all_bits = (1 << assignments) - 1 + # A truth table is one integer whose bits enumerate all gate choices. + variables[row] = {g: sum(((a >> k) & 1) << a for a in range(assignments)) + for k, g in enumerate(gates)} + columns = [] + for b in range(9): + truth = all_bits if initial[row] >> b & 1 else 0 + for g in gates: + if coefficients[g] >> b & 1: + truth ^= variables[row][g] + columns.append(truth) + ws = [sum((column >> a) & 1 for column in columns) for a in range(assignments)] + weights[row] = ws + lower.append(min(ws)) + total += assignments + check(min(ws) == certificate['row_certificates'][row]['minimum'], 'independent row minimum') + check(assignments == certificate['row_certificates'][row]['subsets'], 'independent row coverage') + for row, gate, threshold in ((47,47,2),(68,93,2),(93,39,2)): + check(all(w >= threshold or (variables[row][gate] >> a & 1) + for a,w in enumerate(weights[row])), 'saving implies gate') + for row, gate, threshold in ((96,6,4),(6,36,2)): + check(all(not (variables[row][gate] >> a & 1) or w >= threshold + for a,w in enumerate(weights[row])), 'gate forces cost') + others = set(range(v)) - {24,28,47,96,68,93,6} + # Rebuild the sum-of-groups lower bound, independently of the stored 94. + result = sum(lower[d] for d in others) + lower[24] + lower[28] + 4 + 4 + check(result == 94 and total == 1386, 'global certificate arithmetic') + chosen = {31,51,52} + check(all(i not in chosen or j in chosen for i,j in deps), 'attaining ideal') + first = [g for i,g in enumerate(undo) if i in chosen] + rest = [g for i,g in enumerate(undo) if i not in chosen] + for d in range(v): + check(pullback((d,), first+rest) == pullback((d,), undo), 'commuted undo matrix') + final = [evaluate(pullback((d,), preparation+first),word['scatter']) for d in range(v)] + check(sum(x.bit_count() for x in final) == result, 'backward sharpness') + # A relaxed cheaper assignment must fail the matrix-derived ideal condition. + relaxed = chosen | {47} + relaxed_rows = initial.copy() + for g in relaxed: + relaxed_rows[undo[g][0]] ^= coefficients[g] + check(sum(x.bit_count() for x in relaxed_rows) == 93, 'relaxed control cost') + check(any(i in relaxed and j not in relaxed for i,j in deps), 'reject relaxed control') + print('PASS_INDEPENDENT_IDEAL_AUDIT backward_coefficients=417 row_subsets=1386 matrix_dependencies=850 minimum=94') + + +if __name__ == '__main__': + audit() diff --git a/research/r439-deferred-ideal-optimum/verify.py b/research/r439-deferred-ideal-optimum/verify.py new file mode 100644 index 0000000000..01dd725751 --- /dev/null +++ b/research/r439-deferred-ideal-optimum/verify.py @@ -0,0 +1,220 @@ +#!/usr/bin/env python3 +"""Exact all-ideal certificate; standard library, Apache-2.0. +Charles Bethin with substantial OpenAI Codex assistance. +""" +import argparse +import copy +import gzip +import hashlib +import itertools +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = 'research/r439-bsection-stars-seed01/candidate.json.gz' +WITNESS = (31, 51, 52) +EXCEPTIONAL = {24, 28, 47, 68, 93} + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def load(): + pins = json.loads((HERE / 'SOURCES.json').read_text()) + pin = next(p for p in pins['files'] if p['path'] == SOURCE) + raw = (ROOT / SOURCE).read_bytes() + need(hashlib.sha256(raw).hexdigest() == pin['sha256'], 'source digest') + return json.loads(gzip.decompress(raw)) + + +def extract(w): + v = w['v'] + need(v == 111 and w['R'] == 439 and len(w['ret']) == 9, 'source dimensions') + yy = lambda g: v <= g[1] < 2*v and all(v <= s < 2*v for s in g[2]) + reads = [i for i, g in enumerate(w['D']) + if v <= g[1] < 2*v and all(s >= 2*v for s in g[2])] + lo, hi = min(reads), max(reads) + prep = [g for i, g in enumerate(w['D']) if i < lo and yy(g)] + undo_positions = [i for i, g in enumerate(w['D']) if i > hi and yy(g)] + undo = [w['D'][i] for i in undo_positions] + need(not any(yy(g) for g in w['D'][lo:hi+1]), 'interspersed target gate') + need(prep == undo[::-1] and len(undo) == 306, 'literal undo binding') + need(all(not v <= g[1] < 2*v and all(not v <= s < 2*v for s in g[2]) for g in w['A']), 'A target isolation') + need(all(not v <= r < 2*v for r in w['ret']), 'scatter source isolation') + need(all(g[0] == 0 and len(g[2]) == 1 and g[1] != g[2][0] + for g in prep + undo), 'elementary zero-frame gates') + need(all(len(r) == len(set(r)) and all(type(j) is int and 0 <= j < 9 for j in r) + for r in w['scatter']), 'scatter indices') + S = [sum(1 << j for j in row) for row in w['scatter']] + P = S.copy() + for _, d, (s,) in prep: + P[d-v] ^= P[s-v] + q = P.copy() + increments, predecessors = [], [] + for i, (_, d, (s,)) in enumerate(undo): + increments.append(q[s-v]) + q[d-v] ^= q[s-v] + predecessors.append([j for j, (_, e, (t,)) in enumerate(undo[:i]) if e == s or t == d]) + need(q == S, 'undo of scatter') + return dict(v=v, prep=prep, undo=undo, undo_positions=undo_positions, + initial_rows=P, scatter_rows=S, increments=increments, predecessors=predecessors) + + +def row_certificate(m): + P, U, inc, v = m['initial_rows'], m['undo'], m['increments'], m['v'] + rows, cases = [], 0 + for d, p in enumerate(P): + ids = [i for i, g in enumerate(U) if g[1]-v == d] + minimum = 10 + for bits in itertools.product((0, 1), repeat=len(ids)): + chosen = dict(zip(ids, bits)) + q = p + for i in ids: + if chosen[i]: + q ^= inc[i] + weight = q.bit_count() + minimum = min(minimum, weight) + cases += 1 + if d == 47 and weight < 2: + need(chosen[47] == 1, 'row47 saving requires gate47') + if d == 68 and weight < 2: + need(chosen[93] == 1, 'row68 saving requires gate93') + if d == 93 and weight < 2: + need(chosen[39] == 1, 'row93 saving requires gate39') + if d == 96 and chosen[6]: + need(weight >= 4, 'gate6 forces row96 weight4') + if d == 6 and chosen[36]: + need(weight >= 2, 'gate36 forces row6 weight2') + if d not in EXCEPTIONAL: + need(minimum >= p.bit_count(), 'unlisted improving row') + rows.append(dict(row=d, initial=p, gates=ids, minimum=minimum, subsets=1 << len(ids))) + need(sum(p.bit_count() for p in P) == 97, 'initial charge') + need([P[d].bit_count() for d in (24, 28, 47, 68, 93)] == [5, 2, 2, 2, 2], 'exceptional initial weights') + need([rows[d]['minimum'] for d in (24, 28, 47, 68, 93)] == [4, 0, 1, 1, 1], 'exceptional minima') + need(P[96].bit_count() == 2 and P[6] == 0, 'compensating row baseline') + dependencies = [[47, 6], [93, 37], [37, 36], [39, 36]] + need(all(j in m['predecessors'][i] for i, j in dependencies), 'essential dependency') + # Group {47,96} costs at least its initial 4. Group {68,93,6} costs at least 4. + # The only remaining reductions are <=1 on row24 and <=2 on row28. + lower = sum(p.bit_count() for p in P) - 1 - 2 + need(cases == 1386 and lower == 94, 'certificate coverage') + return dict(rows=rows, row_subsets=cases, essential_dependencies=dependencies, lower_bound=lower) + + +def is_ideal(m, I): + return all(set(m['predecessors'][i]) <= I for i in I) + + +def split_word(w, m, I): + need(is_ideal(m, I), 'not a dependency ideal') + v, undo = m['v'], m['undo'] + q = m['initial_rows'].copy() + for i, (_, d, (s,)) in enumerate(undo): + if i in I: + q[d-v] ^= q[s-v] + fixed = m['initial_rows'].copy() + for i in I: + fixed[undo[i][1]-v] ^= m['increments'][i] + need(q == fixed, 'fixed-increment witness binding') + result = copy.deepcopy(w) + removed = set(m['undo_positions']) + result['D'] = [g for j, g in enumerate(w['D']) if j not in removed] + [undo[i] for i in sorted(I)] + result['B'] = [g for i, g in enumerate(undo) if i not in I] + w['B'] + result['scatter'] = [[b for b in range(9) if r >> b & 1] for r in q] + return result, q + + +def literal(w, reverse=False): + n = 2*w['v'] + w['R'] + state = [1 << i for i in range(n)] + operations = [] + for section in ('D', 'A', 'scatter', 'B', 'C'): + if section != 'scatter': + operations += [('xor', d, s) for _, d, ss in w[section] for s in ss] + else: + for j, r in enumerate(w['ret']): + operations.append(('copy', n, r)) + operations += [('xor', w['v']+t, n) for t, row in enumerate(w['scatter']) if j in row] + operations.append(('erase', n, r)) + if reverse: + operations = [('copy' if op == 'erase' else 'erase' if op == 'copy' else op, d, s) + for op, d, s in operations[::-1]] + for op, d, s in operations: + if op == 'copy': + need(len(state) == n, 'temporary already live') + state.append(state[s]) + elif op == 'erase': + need(len(state) == n+1 and state[d] == state[s], 'COPY lifetime') + state.pop() + else: + state[d] ^= state[s] + expected = [1 << i for i in range(n)] + for i in range(w['v']): + expected[w['v']+i] ^= 1 << i + need(state == expected, 'arbitrary-dirty boundary') + return len([op for op, _, _ in operations if op == 'xor']) + + +def controls(w, m, candidate): + names = [] + def reject(name, f): + try: + f() + except ValueError: + names.append(name) + else: + raise ValueError('control accepted: ' + name) + reject('nonideal relaxed 93-ADD proposal', lambda: split_word(w, m, set(WITNESS) | {47})) + broken = copy.deepcopy(m) + broken['predecessors'][47].remove(6) + reject('missing essential dependency', lambda: row_certificate(broken)) + broken = copy.deepcopy(m) + broken['increments'][36] = 0 + reject('erased compensating row cost', lambda: row_certificate(broken)) + broken = copy.deepcopy(candidate) + broken['scatter'] = w['scatter'] + reject('old scatter with changed basis', lambda: literal(broken)) + broken = copy.deepcopy(candidate) + # Removing the first deferred gate can be invisible on a scatter column; + # arbitrary dirty target columns still detect the missing undo. + broken['B'].pop(0) + reject('omitted undo on dirty targets', lambda: literal(broken)) + return names + + +def compute(): + w = load() + m = extract(w) + cert = row_certificate(m) + candidate, q = split_word(w, m, set(WITNESS)) + cost = sum(x.bit_count() for x in q) + need(cost == cert['lower_bound'], 'sharpness') + counts = [literal(word, rev) for word in (w, candidate) for rev in (False, True)] + need(counts == [11500, 11500, 11067, 11067], 'complete local ADD count') + need(candidate['A'] == w['A'] and candidate['C'] == w['C'] and candidate['ret'] == w['ret'], 'unchanged continuation') + return dict(status='PASS_R439_DEFERRED_IDEAL_OPTIMUM', lower_bound=94, attaining_ideal=list(WITNESS), + initial_scatter=97, original_scatter=527, undo_gates=306, dependency_edges=sum(map(len, m['predecessors'])), + row_subsets=cert['row_subsets'], row_certificates=cert['rows'], essential_dependencies=cert['essential_dependencies'], + initial_rows=m['initial_rows'], increments=m['increments'], + dirty_columns=661, complete_ADDs=[11500,11067], controls=controls(w,m,candidate), + scope='All dependency ideals of this pinned undo circuit, not arbitrary circuits or supplier admission') + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument('--write', action='store_true') + args = ap.parse_args() + result = compute() + path = HERE / 'CERTIFICATE.json' + if args.write: + path.write_text(json.dumps(result, indent=2) + '\n') + else: + need(result == json.loads(path.read_text()), 'certificate mismatch') + print('PASS_R439_DEFERRED_IDEAL_OPTIMUM minimum=94 gates=306 row_subsets=1386 dirty_columns=661 controls=5 no_new_kappa') + + +if __name__ == '__main__': + main()