diff --git a/research/r439-later-retirement-cuts/CERTIFICATE.json b/research/r439-later-retirement-cuts/CERTIFICATE.json new file mode 100644 index 0000000000..ffce862911 --- /dev/null +++ b/research/r439-later-retirement-cuts/CERTIFICATE.json @@ -0,0 +1,2036 @@ +{ + "all_helper_join_ranks": [ + [ + 222, + 8 + ], + [ + 223, + 8 + ], + [ + 224, + 8 + ], + [ + 225, + 8 + ], + [ + 226, + 8 + ], + [ + 227, + 8 + ], + [ + 228, + 8 + ], + [ + 229, + 8 + ], + [ + 230, + 8 + ], + [ + 231, + 8 + ], + [ + 232, + 8 + ], + [ + 233, + 8 + ], + [ + 234, + 8 + ], + [ + 235, + 8 + ], + [ + 236, + 8 + ], + [ + 237, + 8 + ], + [ + 238, + 8 + ], + [ + 239, + 8 + ], + [ + 240, + 8 + ], + [ + 241, + 8 + ], + [ + 242, + 8 + ], + [ + 243, + 8 + ], + [ + 244, + 8 + ], + [ + 245, + 8 + ], + [ + 246, + 8 + ], + [ + 247, + 8 + ], + [ + 248, + 8 + ], + [ + 249, + 8 + ], + [ + 250, + 8 + ], + [ + 251, + 8 + ], + [ + 252, + 8 + ], + [ + 253, + 8 + ], + [ + 254, + 8 + ], + [ + 255, + 8 + ], + [ + 256, + 8 + ], + [ + 257, + 8 + ], + [ + 258, + 8 + ], + [ + 259, + 8 + ], + [ + 260, + 8 + ], + [ + 261, + 8 + ], + [ + 262, + 8 + ], + [ + 263, + 8 + ], + [ + 264, + 8 + ], + [ + 265, + 8 + ], + [ + 266, + 8 + ], + [ + 267, + 8 + ], + [ + 268, + 8 + ], + [ + 269, + 8 + ], + [ + 270, + 8 + ], + [ + 271, + 8 + ], + [ + 272, + 8 + ], + [ + 273, + 8 + ], + [ + 274, + 8 + ], + [ + 275, + 8 + ], + [ + 276, + 8 + ], + [ + 277, + 8 + ], + [ + 278, + 8 + ], + [ + 279, + 8 + ], + [ + 280, + 8 + ], + [ + 281, + 8 + ], + [ + 282, + 8 + ], + [ + 283, + 8 + ], + [ + 284, + 8 + ], + [ + 285, + 8 + ], + [ + 286, + 8 + ], + [ + 287, + 8 + ], + [ + 288, + 8 + ], + [ + 289, + 8 + ], + [ + 290, + 8 + ], + [ + 291, + 8 + ], + [ + 292, + 8 + ], + [ + 293, + 8 + ], + [ + 294, + 8 + ], + [ + 295, + 8 + ], + [ + 296, + 8 + ], + [ + 297, + 8 + ], + [ + 298, + 8 + ], + [ + 299, + 8 + ], + [ + 300, + 8 + ], + [ + 301, + 8 + ], + [ + 302, + 8 + ], + [ + 303, + 8 + ], + [ + 304, + 8 + ], + [ + 305, + 8 + ], + [ + 306, + 8 + ], + [ + 307, + 8 + ], + [ + 308, + 8 + ], + [ + 309, + 8 + ], + [ + 310, + 8 + ], + [ + 311, + 8 + ], + [ + 312, + 8 + ], + [ + 313, + 8 + ], + [ + 314, + 8 + ], + [ + 315, + 8 + ], + [ + 316, + 8 + ], + [ + 317, + 8 + ], + [ + 318, + 8 + ], + [ + 319, + 8 + ], + [ + 320, + 8 + ], + [ + 321, + 8 + ], + [ + 322, + 8 + ], + [ + 323, + 8 + ], + [ + 324, + 8 + ], + [ + 325, + 8 + ], + [ + 326, + 8 + ], + [ + 327, + 8 + ], + [ + 328, + 8 + ], + [ + 329, + 8 + ], + [ + 330, + 8 + ], + [ + 331, + 8 + ], + [ + 332, + 8 + ], + [ + 333, + 8 + ], + [ + 334, + 8 + ], + [ + 335, + 8 + ], + [ + 336, + 8 + ], + [ + 337, + 8 + ], + [ + 338, + 8 + ], + [ + 339, + 8 + ], + [ + 340, + 8 + ], + [ + 341, + 8 + ], + [ + 342, + 8 + ], + [ + 343, + 8 + ], + [ + 344, + 8 + ], + [ + 345, + 8 + ], + [ + 346, + 8 + ], + [ + 347, + 8 + ], + [ + 348, + 8 + ], + [ + 349, + 8 + ], + [ + 350, + 8 + ], + [ + 351, + 8 + ], + [ + 352, + 8 + ], + [ + 353, + 8 + ], + [ + 354, + 8 + ], + [ + 355, + 8 + ], + [ + 356, + 8 + ], + [ + 357, + 8 + ], + [ + 358, + 8 + ], + [ + 359, + 8 + ], + [ + 360, + 8 + ], + [ + 361, + 8 + ], + [ + 362, + 8 + ], + [ + 363, + 8 + ], + [ + 364, + 8 + ], + [ + 365, + 8 + ], + [ + 366, + 8 + ], + [ + 367, + 8 + ], + [ + 368, + 8 + ], + [ + 369, + 8 + ], + [ + 370, + 8 + ], + [ + 371, + 8 + ], + [ + 372, + 8 + ], + [ + 373, + 8 + ], + [ + 374, + 8 + ], + [ + 375, + 8 + ], + [ + 376, + 8 + ], + [ + 377, + 8 + ], + [ + 378, + 8 + ], + [ + 379, + 8 + ], + [ + 380, + 8 + ], + [ + 381, + 8 + ], + [ + 382, + 8 + ], + [ + 383, + 8 + ], + [ + 384, + 8 + ], + [ + 385, + 8 + ], + [ + 386, + 8 + ], + [ + 387, + 8 + ], + [ + 388, + 8 + ], + [ + 389, + 8 + ], + [ + 390, + 8 + ], + [ + 391, + 8 + ], + [ + 392, + 8 + ], + [ + 393, + 8 + ], + [ + 394, + 8 + ], + [ + 395, + 8 + ], + [ + 396, + 8 + ], + [ + 397, + 8 + ], + [ + 398, + 8 + ], + [ + 399, + 8 + ], + [ + 400, + 8 + ], + [ + 401, + 8 + ], + [ + 402, + 8 + ], + [ + 403, + 8 + ], + [ + 404, + 8 + ], + [ + 405, + 8 + ], + [ + 406, + 8 + ], + [ + 407, + 8 + ], + [ + 408, + 8 + ], + [ + 409, + 8 + ], + [ + 410, + 8 + ], + [ + 411, + 8 + ], + [ + 412, + 8 + ], + [ + 413, + 8 + ], + [ + 414, + 8 + ], + [ + 415, + 8 + ], + [ + 416, + 8 + ], + [ + 417, + 8 + ], + [ + 418, + 8 + ], + [ + 419, + 8 + ], + [ + 420, + 8 + ], + [ + 421, + 8 + ], + [ + 422, + 8 + ], + [ + 423, + 8 + ], + [ + 424, + 8 + ], + [ + 425, + 8 + ], + [ + 426, + 8 + ], + [ + 427, + 8 + ], + [ + 428, + 8 + ], + [ + 429, + 8 + ], + [ + 430, + 8 + ], + [ + 431, + 8 + ], + [ + 432, + 8 + ], + [ + 433, + 8 + ], + [ + 434, + 8 + ], + [ + 435, + 8 + ], + [ + 436, + 8 + ], + [ + 437, + 8 + ], + [ + 438, + 8 + ], + [ + 439, + 8 + ], + [ + 440, + 8 + ], + [ + 441, + 8 + ], + [ + 442, + 8 + ], + [ + 443, + 8 + ], + [ + 444, + 8 + ], + [ + 445, + 8 + ], + [ + 446, + 8 + ], + [ + 447, + 8 + ], + [ + 448, + 8 + ], + [ + 449, + 8 + ], + [ + 450, + 8 + ], + [ + 451, + 8 + ], + [ + 452, + 8 + ], + [ + 453, + 8 + ], + [ + 454, + 8 + ], + [ + 455, + 8 + ], + [ + 456, + 8 + ], + [ + 457, + 8 + ], + [ + 458, + 8 + ], + [ + 459, + 8 + ], + [ + 460, + 8 + ], + [ + 461, + 8 + ], + [ + 462, + 8 + ], + [ + 463, + 8 + ], + [ + 464, + 8 + ], + [ + 465, + 7 + ], + [ + 466, + 7 + ], + [ + 467, + 8 + ], + [ + 468, + 7 + ], + [ + 469, + 7 + ], + [ + 470, + 7 + ], + [ + 471, + 8 + ], + [ + 472, + 8 + ], + [ + 473, + 8 + ], + [ + 474, + 8 + ], + [ + 475, + 8 + ], + [ + 476, + 7 + ], + [ + 477, + 8 + ], + [ + 478, + 8 + ], + [ + 479, + 8 + ], + [ + 480, + 8 + ], + [ + 481, + 8 + ], + [ + 482, + 8 + ], + [ + 483, + 8 + ], + [ + 484, + 8 + ], + [ + 485, + 8 + ], + [ + 486, + 8 + ], + [ + 487, + 8 + ], + [ + 488, + 8 + ], + [ + 489, + 8 + ], + [ + 490, + 8 + ], + [ + 491, + 8 + ], + [ + 492, + 8 + ], + [ + 493, + 8 + ], + [ + 494, + 8 + ], + [ + 495, + 8 + ], + [ + 496, + 8 + ], + [ + 497, + 8 + ], + [ + 498, + 8 + ], + [ + 499, + 8 + ], + [ + 500, + 8 + ], + [ + 501, + 8 + ], + [ + 502, + 8 + ], + [ + 503, + 8 + ], + [ + 504, + 8 + ], + [ + 505, + 8 + ], + [ + 506, + 8 + ], + [ + 507, + 8 + ], + [ + 508, + 8 + ], + [ + 509, + 8 + ], + [ + 510, + 8 + ], + [ + 511, + 8 + ], + [ + 512, + 8 + ], + [ + 513, + 8 + ], + [ + 514, + 8 + ], + [ + 515, + 8 + ], + [ + 516, + 8 + ], + [ + 517, + 8 + ], + [ + 518, + 8 + ], + [ + 519, + 8 + ], + [ + 520, + 8 + ], + [ + 521, + 8 + ], + [ + 522, + 8 + ], + [ + 523, + 8 + ], + [ + 524, + 8 + ], + [ + 525, + 8 + ], + [ + 526, + 8 + ], + [ + 527, + 8 + ], + [ + 528, + 8 + ], + [ + 529, + 8 + ], + [ + 530, + 8 + ], + [ + 531, + 8 + ], + [ + 532, + 8 + ], + [ + 533, + 8 + ], + [ + 534, + 8 + ], + [ + 535, + 8 + ], + [ + 536, + 8 + ], + [ + 537, + 8 + ], + [ + 538, + 8 + ], + [ + 539, + 8 + ], + [ + 540, + 8 + ], + [ + 541, + 8 + ], + [ + 542, + 8 + ], + [ + 543, + 8 + ], + [ + 544, + 8 + ], + [ + 545, + 8 + ], + [ + 546, + 8 + ], + [ + 547, + 8 + ], + [ + 548, + 8 + ], + [ + 549, + 8 + ], + [ + 550, + 8 + ], + [ + 551, + 8 + ], + [ + 552, + 8 + ], + [ + 553, + 8 + ], + [ + 554, + 8 + ], + [ + 555, + 8 + ], + [ + 556, + 8 + ], + [ + 557, + 8 + ], + [ + 558, + 8 + ], + [ + 559, + 8 + ], + [ + 560, + 8 + ], + [ + 561, + 8 + ], + [ + 562, + 8 + ], + [ + 563, + 8 + ], + [ + 564, + 8 + ], + [ + 565, + 8 + ], + [ + 566, + 8 + ], + [ + 567, + 8 + ], + [ + 568, + 8 + ], + [ + 569, + 8 + ], + [ + 570, + 8 + ], + [ + 571, + 8 + ], + [ + 572, + 8 + ], + [ + 573, + 8 + ], + [ + 574, + 8 + ], + [ + 575, + 8 + ], + [ + 576, + 8 + ], + [ + 577, + 8 + ], + [ + 578, + 8 + ], + [ + 579, + 8 + ], + [ + 580, + 8 + ], + [ + 581, + 8 + ], + [ + 582, + 8 + ], + [ + 583, + 8 + ], + [ + 584, + 8 + ], + [ + 585, + 8 + ], + [ + 586, + 8 + ], + [ + 587, + 8 + ], + [ + 588, + 8 + ], + [ + 589, + 8 + ], + [ + 590, + 8 + ], + [ + 591, + 8 + ], + [ + 592, + 8 + ], + [ + 593, + 8 + ], + [ + 594, + 8 + ], + [ + 595, + 8 + ], + [ + 596, + 8 + ], + [ + 597, + 8 + ], + [ + 598, + 8 + ], + [ + 599, + 8 + ], + [ + 600, + 8 + ], + [ + 601, + 8 + ], + [ + 602, + 8 + ], + [ + 603, + 8 + ], + [ + 604, + 8 + ], + [ + 605, + 8 + ], + [ + 606, + 8 + ], + [ + 607, + 8 + ], + [ + 608, + 8 + ], + [ + 609, + 8 + ], + [ + 610, + 8 + ], + [ + 611, + 8 + ], + [ + 612, + 8 + ], + [ + 613, + 8 + ], + [ + 614, + 8 + ], + [ + 615, + 8 + ], + [ + 616, + 8 + ], + [ + 617, + 8 + ], + [ + 618, + 8 + ], + [ + 619, + 8 + ], + [ + 620, + 8 + ], + [ + 621, + 8 + ], + [ + 622, + 8 + ], + [ + 623, + 8 + ], + [ + 624, + 8 + ], + [ + 625, + 8 + ], + [ + 626, + 8 + ], + [ + 627, + 8 + ], + [ + 628, + 8 + ], + [ + 629, + 8 + ], + [ + 630, + 8 + ], + [ + 631, + 8 + ], + [ + 632, + 8 + ], + [ + 633, + 8 + ], + [ + 634, + 8 + ], + [ + 635, + 8 + ], + [ + 636, + 8 + ], + [ + 637, + 8 + ], + [ + 638, + 8 + ], + [ + 639, + 8 + ], + [ + 640, + 8 + ], + [ + 641, + 8 + ], + [ + 642, + 8 + ], + [ + 643, + 8 + ], + [ + 644, + 8 + ], + [ + 645, + 8 + ], + [ + 646, + 8 + ], + [ + 647, + 8 + ], + [ + 648, + 8 + ], + [ + 649, + 8 + ], + [ + 650, + 8 + ], + [ + 651, + 8 + ], + [ + 652, + 8 + ], + [ + 653, + 8 + ], + [ + 654, + 8 + ], + [ + 655, + 8 + ], + [ + 656, + 8 + ], + [ + 657, + 8 + ], + [ + 658, + 8 + ], + [ + 659, + 8 + ], + [ + 660, + 8 + ] + ], + "join_rank_counts": { + "7": 6, + "8": 433 + }, + "legal_helpers": [ + 469, + 470, + 476 + ], + "no_new_kappa": true, + "rank_seven_cases": [ + { + "dirt": [ + 163, + 381, + 465, + 474 + ], + "endpoint_blockers": [ + 163 + ], + "helper": 465, + "isolation_gates": [ + [ + 465, + 0 + ], + [ + 163, + 465 + ], + [ + 381, + 465 + ], + [ + 474, + 465 + ] + ], + "legal": false, + "restore": [ + 0, + 465 + ], + "station": 512 + }, + { + "dirt": [ + 198, + 385, + 466, + 476 + ], + "endpoint_blockers": [ + 198 + ], + "helper": 466, + "isolation_gates": [ + [ + 466, + 19 + ], + [ + 198, + 466 + ], + [ + 385, + 466 + ], + [ + 476, + 466 + ] + ], + "legal": false, + "restore": [ + 19, + 466 + ], + "station": 514 + }, + { + "dirt": [ + 208, + 444, + 468, + 475 + ], + "endpoint_blockers": [ + 208 + ], + "helper": 468, + "isolation_gates": [ + [ + 468, + 38 + ], + [ + 208, + 468 + ], + [ + 444, + 468 + ], + [ + 475, + 468 + ] + ], + "legal": false, + "restore": [ + 38, + 468 + ], + "station": 513 + }, + { + "dirt": [ + 413, + 469, + 479 + ], + "endpoint_blockers": [], + "first_fixed_B_conflict": { + "frame": 52, + "gate_index": 60, + "registers": [ + 50 + ] + }, + "helper": 469, + "isolation_gates": [ + [ + 469, + 50 + ], + [ + 413, + 469 + ], + [ + 479, + 469 + ] + ], + "legal": true, + "minimum_adds": 3, + "promotions": [ + { + "from_frame": 52, + "rank_increment": 6, + "register": 50, + "to_frame": 517 + } + ], + "restore": [ + 50, + 469 + ], + "station": 517 + }, + { + "dirt": [ + 444, + 470, + 475 + ], + "endpoint_blockers": [], + "first_fixed_B_conflict": { + "frame": 186, + "gate_index": 35, + "registers": [ + 77 + ] + }, + "helper": 470, + "isolation_gates": [ + [ + 470, + 77 + ], + [ + 444, + 470 + ], + [ + 475, + 470 + ] + ], + "legal": true, + "minimum_adds": 3, + "promotions": [ + { + "from_frame": 186, + "rank_increment": 5, + "register": 77, + "to_frame": 513 + }, + { + "from_frame": 79, + "rank_increment": 6, + "register": 470, + "to_frame": 513 + } + ], + "restore": [ + 77, + 470 + ], + "station": 513 + }, + { + "dirt": [ + 476 + ], + "endpoint_blockers": [], + "first_fixed_B_conflict": { + "frame": 509, + "gate_index": 284, + "registers": [ + 67 + ] + }, + "helper": 476, + "isolation_gates": [ + [ + 476, + 67 + ], + [ + 476, + 328 + ], + [ + 476, + 331 + ], + [ + 476, + 385 + ] + ], + "legal": true, + "minimum_adds": 4, + "promotions": [ + { + "from_frame": 192, + "rank_increment": 5, + "register": 67, + "to_frame": 514 + }, + { + "from_frame": 431, + "rank_increment": 1, + "register": 331, + "to_frame": 514 + } + ], + "restore": [ + 67, + 328, + 331, + 385, + 476 + ], + "station": 514 + } + ], + "schema_version": 1, + "seed": 17, + "status": "SCOPED_SINGLE_STATION_CLASSIFICATION", + "word_sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f" +} diff --git a/research/r439-later-retirement-cuts/LATER-CUTS.json b/research/r439-later-retirement-cuts/LATER-CUTS.json new file mode 100644 index 0000000000..4540d66ea3 --- /dev/null +++ b/research/r439-later-retirement-cuts/LATER-CUTS.json @@ -0,0 +1,572 @@ +{ + "B_gate_count": 712, + "cut_convention": "cut k is after exactly the first k B records, with D/A/scatter fixed", + "cuts_per_helper": 713, + "helper_cut_pairs": 4278, + "helpers": [ + { + "helper": 465, + "joint_rank_seven_cuts": 49, + "necessary_condition_pass_count": 39, + "runs": [ + { + "conditions": { + "joint_rank": 7, + "lost_targets": [ + 122 + ], + "restoration_rank": 4, + "restore_donors": [ + 0, + 465 + ] + }, + "first_cut": 0, + "last_cut": 9 + }, + { + "conditions": { + "joint_rank": 7, + "lost_targets": [], + "restoration_rank": 4, + "restore_donors": [ + 0, + 465 + ] + }, + "first_cut": 10, + "last_cut": 48 + }, + { + "conditions": { + "joint_rank": 8 + }, + "first_cut": 49, + "last_cut": 712 + } + ], + "windows": [ + [ + 10, + 48 + ] + ] + }, + { + "helper": 466, + "joint_rank_seven_cuts": 79, + "necessary_condition_pass_count": 0, + "runs": [ + { + "conditions": { + "joint_rank": 7, + "lost_targets": [ + 208 + ], + "restoration_rank": 4, + "restore_donors": [ + 19, + 466 + ] + }, + "first_cut": 0, + "last_cut": 78 + }, + { + "conditions": { + "joint_rank": 8 + }, + "first_cut": 79, + "last_cut": 712 + } + ], + "windows": [] + }, + { + "helper": 468, + "joint_rank_seven_cuts": 89, + "necessary_condition_pass_count": 58, + "runs": [ + { + "conditions": { + "joint_rank": 7, + "lost_targets": [ + 144 + ], + "restoration_rank": 4, + "restore_donors": [ + 38, + 468 + ] + }, + "first_cut": 0, + "last_cut": 30 + }, + { + "conditions": { + "joint_rank": 7, + "lost_targets": [], + "restoration_rank": 4, + "restore_donors": [ + 38, + 468 + ] + }, + "first_cut": 31, + "last_cut": 88 + }, + { + "conditions": { + "joint_rank": 8 + }, + "first_cut": 89, + "last_cut": 712 + } + ], + "windows": [ + [ + 31, + 88 + ] + ] + }, + { + "helper": 469, + "joint_rank_seven_cuts": 556, + "necessary_condition_pass_count": 0, + "runs": [ + { + "conditions": { + "joint_rank": 7, + "lost_targets": [ + 130, + 138, + 146, + 154, + 168, + 177, + 178, + 185, + 200, + 208 + ], + "restoration_rank": 7, + "restore_donors": [ + 50, + 469 + ] + }, + "first_cut": 0, + "last_cut": 60 + }, + { + "conditions": { + "joint_rank": 7, + "lost_targets": [ + 130, + 138, + 146, + 154, + 168, + 177, + 185, + 200, + 208 + ], + "restoration_rank": 7, + "restore_donors": [ + 50, + 469 + ] + }, + "first_cut": 61, + "last_cut": 288 + }, + { + "conditions": { + "joint_rank": 7, + "lost_targets": [ + 176 + ], + "restoration_rank": 7, + "restore_donors": [ + 50, + 469 + ] + }, + "first_cut": 289, + "last_cut": 301 + }, + { + "conditions": { + "joint_rank": 7, + "lost_targets": [ + 130, + 138, + 154, + 168, + 176, + 177, + 185, + 200 + ], + "restoration_rank": 7, + "restore_donors": [ + 50, + 87, + 469 + ] + }, + "first_cut": 302, + "last_cut": 302 + }, + { + "conditions": { + "joint_rank": 7, + "lost_targets": [ + 130, + 138, + 154, + 168, + 176, + 177, + 185, + 200 + ], + "restoration_rank": 7, + "restore_donors": [ + 17, + 50, + 87, + 469 + ] + }, + "first_cut": 303, + "last_cut": 303 + }, + { + "conditions": { + "joint_rank": 7, + "lost_targets": [ + 130, + 138, + 154, + 168, + 176, + 177, + 185, + 200 + ], + "restoration_rank": 7, + "restore_donors": [ + 17, + 50, + 67, + 87, + 469 + ] + }, + "first_cut": 304, + "last_cut": 305 + }, + { + "conditions": { + "joint_rank": 7, + "lost_targets": [ + 130, + 138, + 154, + 168, + 176, + 185, + 200 + ], + "restoration_rank": 7, + "restore_donors": [ + 17, + 50, + 67, + 87, + 469 + ] + }, + "first_cut": 306, + "last_cut": 306 + }, + { + "conditions": { + "joint_rank": 7, + "lost_targets": [ + 130, + 138, + 154, + 168, + 176, + 185 + ], + "restoration_rank": 7, + "restore_donors": [ + 17, + 50, + 67, + 87, + 469 + ] + }, + "first_cut": 307, + "last_cut": 309 + }, + { + "conditions": { + "joint_rank": 7, + "lost_targets": [ + 130, + 138, + 168, + 176, + 185 + ], + "restoration_rank": 7, + "restore_donors": [ + 17, + 50, + 67, + 87, + 469 + ] + }, + "first_cut": 310, + "last_cut": 310 + }, + { + "conditions": { + "joint_rank": 7, + "lost_targets": [ + 168, + 176, + 185 + ], + "restoration_rank": 7, + "restore_donors": [ + 17, + 50, + 67, + 469 + ] + }, + "first_cut": 311, + "last_cut": 311 + }, + { + "conditions": { + "joint_rank": 7, + "lost_targets": [ + 176, + 185 + ], + "restoration_rank": 7, + "restore_donors": [ + 50, + 67, + 469 + ] + }, + "first_cut": 312, + "last_cut": 555 + }, + { + "conditions": { + "joint_rank": 8 + }, + "first_cut": 556, + "last_cut": 712 + } + ], + "windows": [] + }, + { + "helper": 470, + "joint_rank_seven_cuts": 518, + "necessary_condition_pass_count": 518, + "runs": [ + { + "conditions": { + "joint_rank": 7, + "lost_targets": [], + "restoration_rank": 2, + "restore_donors": [ + 77, + 470 + ] + }, + "first_cut": 0, + "last_cut": 289 + }, + { + "conditions": { + "joint_rank": 7, + "lost_targets": [], + "restoration_rank": 4, + "restore_donors": [ + 77, + 470 + ] + }, + "first_cut": 290, + "last_cut": 294 + }, + { + "conditions": { + "joint_rank": 7, + "lost_targets": [], + "restoration_rank": 4, + "restore_donors": [ + 77, + 87, + 470 + ] + }, + "first_cut": 295, + "last_cut": 295 + }, + { + "conditions": { + "joint_rank": 7, + "lost_targets": [], + "restoration_rank": 4, + "restore_donors": [ + 17, + 77, + 87, + 470 + ] + }, + "first_cut": 296, + "last_cut": 296 + }, + { + "conditions": { + "joint_rank": 7, + "lost_targets": [], + "restoration_rank": 4, + "restore_donors": [ + 17, + 33, + 77, + 87, + 470 + ] + }, + "first_cut": 297, + "last_cut": 306 + }, + { + "conditions": { + "joint_rank": 7, + "lost_targets": [], + "restoration_rank": 4, + "restore_donors": [ + 17, + 33, + 77, + 470 + ] + }, + "first_cut": 307, + "last_cut": 307 + }, + { + "conditions": { + "joint_rank": 7, + "lost_targets": [], + "restoration_rank": 4, + "restore_donors": [ + 17, + 22, + 33, + 77, + 470 + ] + }, + "first_cut": 308, + "last_cut": 312 + }, + { + "conditions": { + "joint_rank": 7, + "lost_targets": [], + "restoration_rank": 4, + "restore_donors": [ + 17, + 22, + 33, + 77, + 87, + 470 + ] + }, + "first_cut": 313, + "last_cut": 517 + }, + { + "conditions": { + "joint_rank": 8 + }, + "first_cut": 518, + "last_cut": 712 + } + ], + "windows": [ + [ + 0, + 517 + ] + ] + }, + { + "helper": 476, + "joint_rank_seven_cuts": 285, + "necessary_condition_pass_count": 0, + "runs": [ + { + "conditions": { + "joint_rank": 7, + "lost_targets": [ + 130, + 138, + 146, + 154, + 168, + 171, + 177, + 200, + 208 + ], + "restoration_rank": 7, + "restore_donors": [ + 67, + 328, + 331, + 385, + 476 + ] + }, + "first_cut": 0, + "last_cut": 284 + }, + { + "conditions": { + "joint_rank": 8 + }, + "first_cut": 285, + "last_cut": 712 + } + ], + "windows": [] + } + ], + "meaning": "Passing both necessary tests is not a legal suffix or new supplier.", + "no_new_kappa": true, + "schema_version": 1, + "source_sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f" +} diff --git a/research/r439-later-retirement-cuts/README.md b/research/r439-later-retirement-cuts/README.md new file mode 100644 index 0000000000..c2fec1d897 --- /dev/null +++ b/research/r439-later-retirement-cuts/README.md @@ -0,0 +1,187 @@ +# R439: complete later-cut retirement census + +**Scoped bit-supplier negative result and precise handoff; no new kappa.** +For PR1128's six width-seven candidates, this package checks every boundary +along the fixed PR589 B word: **713 cuts and 4,278 helper/cut pairs**. It supplies the complete +necessary-condition census for the later-cut first-restoration question left +explicitly open by Ross Richardson's concurrent PR1256. + +A cut numbered k is **after exactly the first k B records**. Thus cut 10 is +after zero-based B[9]. The D/A/scatter prefix and B chronology are fixed. + +| Helper | Cuts with joint restoration/erasure rank seven | Cuts also passing first-restoration target access | +|---:|---|---| +| 465 | 0–48 | **10–48** (39 cuts) | +| 466 | 0–78 | **none** | +| 468 | 0–88 | **31–88** (58 cuts) | +| 469 | 0–555 | **none** | +| 470 | 0–517 | **0–517** (518 cuts) | +| 476 | 0–284 | **none** | + +Every later cut outside the second column has joint rank eight. These are +**necessary-condition windows**, not feasible suffixes or constructions. +No B/C replacement, physical owner allocation or supplier invoice is supplied. + +The sharp chronology point is helper466: its blocking target208 is first +read at B[88], but the joint bound has already risen to eight after B[78]. +Simply waiting for that target read cannot save it. Helpers465 and468 do +escape their initial target-access obstruction after B[9] and B[30], +respectively, but only until the joint bound rises after B[48] and B[88]. +For helpers469 and476, at least one inaccessible required target dependency +remains at every cut with joint rank seven. + +## Exact contract and argument + +The sole mathematical input is the frozen PR589 tuned word. At each cut, +write the 661-register scalar state as `w=M u` over F2. All source, target +and helper inputs are independent. Each prefix gate is an invertible +transvection, including the already-consumed retained scatter; no new access +to its COPY channels is allowed. Current frames F_r are rational subspaces +of Q^8. Frame changes must be monotone. Scalar operations must use a common +frame, extra dirty workspace must start independently and be restored, and +there is no new COPY, descent, reset or other high-to-low transport. + +We test a suffix whose **first restoration block** operates at a single +rational frame J, with no lower-frame preprocessing after the chosen cut, +and restores the designated helper h to its original dirty input s_h. +After that block, arbitrary allowed multi-frame scalar work is permitted. +The ultimate endpoint for h must have dimension at most seven; other source, +target and helper endpoints and scalar values retain their original contract. +This is the first-restoration model of PR1256, not arbitrary suffix synthesis. + +Let R_h be the support of `e_h^T M^-1`, and D_h the support of the h-th column +of M. The restoration/erasure argument from PR1128 gives the necessary bound + +`U_h = span(F_h, {F_r : r in R_h union D_h}) <= final_frame(h)`. + +All these joins have rank seven or eight in the completed census. A rank-eight +join excludes every proper final frame in this interface, even with arbitrary +rational choices, target access and restored dirty scratch. For a rank-seven +join, a first restoration block must use a frame containing + +`J_h = span(F_h, {F_r : r in R_h})`. + +The required final target value `y_t + x_(t-111)` has the unique boundary row +`b_t = (e_t + e_(t-111))^T M^-1`. If b_t uses a coordinate forced into the +restoration block, but J_h is not contained in t's final frame V_t, no allowed +completion can supply that dependence to t. Every touched register has moved +to J_h or a larger frame; monotonicity prevents any of its information from +reaching V_t. Untouched boundary coordinates and fresh independent dirt cannot +encode the missing independent coordinate. Enlarging the first restoration +frame cannot cure a failed containment. + +This is PR1256's information-access implication. We apply it at **every** +later B boundary, where both inverse rows and frames change. The complete +certificate records contiguous runs with identical restoration donors, join +rank, restoration rank and lost-target sets. No cut, rational station or +support-size cutoff is sampled. The proof establishes the stated exclusions; +passing the two tests supplies no sufficiency claim. + +For helper466, the target-access witness is target208 at every eligible cut +0–78. At cut79 the joint rank is eight; at cut89, after target208's original +read, it is still eight. The 469/476 lost-target sets are likewise nonempty +through every rank-seven cut. Full sets and every transition are retained in +[LATER-CUTS.json](LATER-CUTS.json). + +## Predecessors and evidence-driven scope change + +Ali Romman's PR1128 (`df29b159239b79d7e451d6ddda826a73e0e50a67`) establishes the +boundary lemma and the six after-scatter candidates. Ross Richardson's +PR1256 (`d6d5a994fcdcd8d04ec439ff988daa8f37b17ece`) establishes the initial +six-case target-access obstruction and an explicit finite helper470 retirement +using rank two before rank seven. Its construction is predecessor evidence, +not implemented or repriced here. Its native/physical/H4 obligations remain. + +This session initially derived the same stationary stars and endpoint-cap +failures independently. The final overlap refresh found PR1256 before any +submission. That initial material is retained in [STATION-NOTE.md](STATION-NOTE.md) +and `CERTIFICATE.json` as corroboration only. It is not the novelty claim. +The one evidence-driven pivot is exactly PR1256's listed later-cut question; +its README says no search there was performed. In particular, our no-window +result for helper466 explains why its proposed target-read follow-up fails +in the fixed chronology, while the two other suggested candidates retain +precise finite windows. Earlier helper470 deletion belongs to Ali Romman's +PR1043; its savings are not combined with anything here. + +Fresh OS seed **17** selected the original user's bit-supplier track. The +three initial candidates, first scope, pivot and stopping rule are in +`TASK.json`. There was no pinned sprint issue, so the authorized local-claim +fallback was used. The initial snapshot covered 850 open PR bodies; the final +pre-pivot refresh covered 855 and all 12 returned discussions. PR1253 concerns +common-first-contact kernel entrances and PR1250 source-mask deletion; both +are distinct and neither is a mathematical dependency here. + +## Reproduce and negative controls + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 scripts/research_package.py --package research/r439-later-retirement-cuts +``` + +The principal commands also run on Python 3.10+: + +```sh +python3 -I -O -B research/r439-later-retirement-cuts/later_cuts.py +python3 -I -O -B research/r439-later-retirement-cuts/check_later_cuts.py +python3 -I -O -B research/r439-later-retirement-cuts/test_later_cuts.py +``` + +Expected markers include `PASS_LATER_BIT_CUTS pairs=4278` and +`PASS_INDEPENDENT_LATER_CUTS full_inverse_rebuilds=713 helper_cut_pairs=4278`, +followed by passing tests and `PASS_REGISTERED_RESEARCH_PACKAGE`. + +The primary engine incrementally updates inverse rows with each B +transvection, using packed binary rows and rational geometry. The separate +checker imports no primary engine, reconstructs the **entire inverse from +scratch at every one of the 713 boundaries**, and uses independently replayed +set-valued scalar states and fraction-free integer geometry. It checks each +restoration identity directly and agrees on every run and boundary, not just +the total counts. Both inherit only the exact raw word; no predecessor +executable code is imported. Separate code paths are not independent human +review. + +The test suite rejects wrong boundary indexing, shifted donor support, +missing target obligations, false pass windows, incomplete cut coverage and +changed source bytes. It checks optimized source-only relocation and parsed +certificate regeneration. The retained stationary suite adds all ten legal +witness-gate omissions, three endpoint-cap failures with relaxed positive +controls, six certificate mutations in both engines, a wrong station, damaged +original cleanup and source-corruption tests. + +Base `dadfea6e8a78ff6ba901705f87532a71c6f5bbb8`; input SHA256 +`e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f`. +`SOURCES.json` pins base Git blobs, historical context and both predecessor +heads/documents. See `VALIDATION.md` for actual local runs and omitted work. + +## Scope, cost and credit + +This is an exact finite census plus the cited necessary-condition arguments. +It is not a formal proof-assistant verification of the multiplication theorem. +Even optimistically free suffix work cannot repair a failed information-access +condition within this model. The surviving windows still require full source +access, target effects, restoration, frame transitions, copies, recursive +children, physical hosting, precision/tape and outer/all-size admission before +any new paid profile or exponent can be claimed. The selected complex supplier +remains binding. No native replay, complete cold supplier replay, production +adoption, remote CI or new kappa is claimed. `upstream/`, frozen predecessor +packages and the selected frontier are unchanged. + +Credit **Ali Romman** (PR1128 and earlier PR1043), **Ross Richardson** +(PR1256), **Sagar Thakrar** (PR1023 width-seven hosting incentive), +DreamingOfClouds (PR589/545), eumemic (PR555/543), and their retained +compiler/hosting lineage. Prepared for **Philipp (@mightyOil)** with substantial +**OpenAI Codex / GPT-6 Astra** assistance in proof, code, tests and writing. +New material is Apache-2.0. + +## Open next questions + +Can helper465 at cut10 or helper468 at cut31 be restored through a fully +priced legal suffix? Those are the earliest new necessary-condition windows; +start there and preserve all dirty columns, pending target reads and physical +frame paths. The census supplies no such suffix and does not justify a new +search outside the 39/58 windows without a changed assumption. For helper470, +PR1256 already gives a finite cut-zero continuation; native H4, owner-window +and precision admission are the more useful next checks. Changes to the prefix, +lower-frame preparation, target-read reordering or added transport are outside +this census and require a new explicit contract and complete cost. diff --git a/research/r439-later-retirement-cuts/SOURCES.json b/research/r439-later-retirement-cuts/SOURCES.json new file mode 100644 index 0000000000..fd76caad17 --- /dev/null +++ b/research/r439-later-retirement-cuts/SOURCES.json @@ -0,0 +1,85 @@ +{ + "schema_version": 1, + "base_commit": "dadfea6e8a78ff6ba901705f87532a71c6f5bbb8", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + }, + { + "path": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "usage": "input", + "git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a", + "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f" + }, + { + "path": "research/bit589-width-packing/README.md", + "usage": "provenance", + "git_blob": "a915381a7a38d3728205a2120aa034f94537ca0f", + "sha256": "671ca8a9d9e78348eae1e5c605ead1606df3d5e23d251600f0bdf60175479f1e" + }, + { + "path": "docs/research/community-batch1099-review.md", + "usage": "provenance", + "git_blob": "6cb6ec061a071a06a2d18cd4dc3e9a2b05d28099", + "sha256": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb" + }, + { + "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "usage": "provenance", + "git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8", + "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + } + ], + "predecessors": [ + { + "pr": 1128, + "head": "df29b159239b79d7e451d6ddda826a73e0e50a67", + "author": "Ali Romman (@aliromman)", + "role": "Boundary lemma and six-survivor premise; independently replayed, no executable code imported.", + "documents": [ + { + "path": "research/bit-width-seven-boundary/README.md", + "git_blob": "f1930385706e38cc3b9995b8ba01f3ac9d06034b", + "sha256": "29b61651091c0870f9762efb6f93ebfa358d7bb8206d04012b18192cf4dabfab" + }, + { + "path": "research/bit-width-seven-boundary/PROOF.md", + "git_blob": "b3bedffde3ee5f1914873ec7918039ab6614678c", + "sha256": "f9fb4706dd523229e8351646c5ef011d8bd16eebc3dd6c35a778b352c123b387" + }, + { + "path": "research/bit-width-seven-boundary/CERTIFICATE.json", + "git_blob": "6982d303d1ba1dfa0b33a2a7f1a1acc9b8a5b2ee", + "sha256": "06ea7280e8a0829b283e352d5590a7cc832ee0973335c24dbac02505d493fa36" + } + ] + }, + { + "pr": 1256, + "head": "d6d5a994fcdcd8d04ec439ff988daa8f37b17ece", + "author": "Ross Richardson", + "role": "First-restoration target-access lemma, after-scatter classification, finite470 continuation; later-cut question. No executable code imported.", + "documents": [ + { + "path": "research/bit-early-retirement-cut/README.md", + "git_blob": "4f3716685c7a22ec4c1b8a68c8beb69021acd0a9", + "sha256": "57b952674aefc3fb6287ceaab7c940c100916dba8ba97104e1838c785e3d8e9f" + }, + { + "path": "research/bit-early-retirement-cut/CERTIFICATE.json", + "git_blob": "b7a8d17755711ccb901742c59dd775c586be1c8d", + "sha256": "735c507caf32715f978e9c0ca67cb056184c751593cd8c58e9dd97232def7a46" + } + ] + } + ] +} diff --git a/research/r439-later-retirement-cuts/STATION-NOTE.md b/research/r439-later-retirement-cuts/STATION-NOTE.md new file mode 100644 index 0000000000..d56a412505 --- /dev/null +++ b/research/r439-later-retirement-cuts/STATION-NOTE.md @@ -0,0 +1,41 @@ +# Initial stationary fixtures: independent corroboration only + +The session began by replaying PR1128's 439-helper after-scatter boundary and +checking a single rank-seven station. Concurrent Ross Richardson PR1256 +subsumes this question and gives the stronger future-target-access argument +and finite two-frame helper470 continuation. This appendix claims no priority +or new supplier result. README.md describes the later-cut contribution. + +433 helpers have rank-eight restoration/erasure joins. The other six are +465/466/468/469/470/476. The first three cannot perform all isolation work at +their forced station while retaining their dirty-carrying targets' final +frames. The other three admit scalar/frame-local isolation: + +``` +station 517: 469 ^= 50; 413 ^= 469; 479 ^= 469 +station 513: 470 ^= 77; 444 ^= 470; 475 ^= 470 +station 514: 476 ^= 67; 476 ^= 328; 476 ^= 331; 476 ^= 385 +``` + +These programs restore the designated independent dirty input and remove it +from all other registers, preserving their other coefficients. Their counts +3/3/4 are minimal in binary ADDs: the first two change three required +destinations; the third computes the parity of five essential boundary +coordinates, whose dependency graph requires four edges. All participating +registers can reach the station and retain their final-frame cap. However, +future target information may already have become inaccessible; none is an +admitted suffix. In particular these stationary programs must not be confused +with PR1256's two-frame helper470 program, which leaves source77 at rank two. + +`CERTIFICATE.json`, `verify.py`, `independent.py` and `test_package.py` retain +this complete after-scatter replay and its controlled scalar fixtures. The +primary also checks the original B/C map on all661 columns. The six test +groups cover both complete engines, ten gate omissions, three target-cap +failures plus relaxed positive controls, six receipt mutations, a wrong +station, damaged original cleanup, exact regeneration, isolated relocation +and source corruption. These checks support the later-cut implementations; +they do not establish a complete physical supplier or new kappa. + +Credit Ali Romman's PR1128, Ross Richardson's PR1256 and the PR589/555 lineage. +Prepared for Philipp (@mightyOil), with substantial OpenAI Codex assistance. +Apache-2.0. diff --git a/research/r439-later-retirement-cuts/TASK.json b/research/r439-later-retirement-cuts/TASK.json new file mode 100644 index 0000000000..66355fa1d5 --- /dev/null +++ b/research/r439-later-retirement-cuts/TASK.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 2, + "base_commit": "dadfea6e8a78ff6ba901705f87532a71c6f5bbb8", + "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": "Source-bound all-713-B-boundary first-restoration/target-access census for the six PR1128 survivors; fill the later-cut gap explicitly left by PR1256.", + "scope_change_reason": "The final refresh found PR1256 had subsumed the initial stationary classification. One evidence-driven pivot to its explicitly unsearched later B cuts; initial material is corroborative only.", + "bottleneck_link": "A narrower helper changes hosted residual width; these blocks expose the exact later source-access obstruction. Side mechanism result with no complete supplier price and no selected kappa gain.", + "budget_minutes": 40, + "stop_rule": "Exactly713 cuts for each of6 helpers; stop after joint-rank and first-restoration target-access classification. No arbitrary suffix rewriting or cost search.", + "outcome": "completed", + "evidence": "LATER-CUTS.json; independent full inverse rebuild at every boundary; primary incremental updates; full boundary and mutation/relocation suites.", + "author": "Philipp (@mightyOil)", + "ai_assistance": "Substantial OpenAI Codex / GPT-6 Astra assistance in proof, code, testing and writing.", + "open_questions": [ + { + "question": "Can helper465 at cut10 or468 at cut31 be completed through a legal, fully priced suffix?", + "why_it_matters": "The census identifies the exact remaining necessary-condition windows, but passing them is not construction.", + "first_step": "Construct and replay all dirty columns starting from the stated earliest cut.", + "blocked_by": "Pending target dependencies, source access, frame schedules, H4 and physical hosting/precision costs." + } + ], + "seed": 17, + "assignment_track": "bit supplier, original user mapping 00-19", + "candidates": [ + { + "scope": "PR1128 six-survivor single-station exit feasibility", + "decision": "selected" + }, + { + "scope": "R439 fixed-profile scalar block optimization", + "decision": "overlaps PR1208/1221" + }, + { + "scope": "Arbitrary source-mask helper deletion", + "decision": "already classified in PR1250" + } + ], + "coordination": { + "pinned_issue_present": false, + "claim": "local claim before implementation", + "overlap_snapshot_open_prs": 850, + "predecessor": 1128, + "distinct_from": [ + 1179, + 1250, + 1253 + ], + "final_snapshot_open_prs": 855, + "final_snapshot_discussions": 12, + "concurrent_overlap": { + "pr": 1256, + "head": "d6d5a994fcdcd8d04ec439ff988daa8f37b17ece", + "treatment": "Credit initial stationary results and470 continuation; extend only explicitly unsearched later cuts." + }, + "submission_refresh": "Latest100 open PR bodies through1268; no additional later-cut overlap." + } +} diff --git a/research/r439-later-retirement-cuts/VALIDATION.md b/research/r439-later-retirement-cuts/VALIDATION.md new file mode 100644 index 0000000000..40bfe0921e --- /dev/null +++ b/research/r439-later-retirement-cuts/VALIDATION.md @@ -0,0 +1,42 @@ +# Local verification receipt + +Date: 2026-10-13. Environment: macOS arm64, CPython 3.12.13 and 3.14.7. +Base and refreshed main: `dadfea6e8a78ff6ba901705f87532a71c6f5bbb8`. + +Passed on Python 3.12.13: + +``` +python3.12 scripts/research_package.py --package research/r439-later-retirement-cuts +``` + +- Complete primary census: 4,278 pairs, 713 cuts per helper. +- Separate checker: 713 complete inverse reconstructions and equality at every boundary. +- Four later-cut test groups, including six corrupted census variants, boundary witnesses, source corruption, optimized relocation and exact regeneration. +- Six stationary fixture groups, including ten gate omissions, three target-cap failures/relaxed positives, six receipt faults in both engines, wrong station, damaged original cleanup, source corruption, relocation and overwrite rejection. +- Final marker: `PASS_REGISTERED_RESEARCH_PACKAGE research/r439-later-retirement-cuts outcome=completed`. + +The four later-cut groups also pass with CPython 3.14.7 under `-I -O -B`. +The six stationary groups passed on the same interpreter before the directory +was renamed; the complete registered replay after the rename passed on 3.12.13. + +Also passed: + +``` +python3 -B scripts/research_baseline.py +python3 -B scripts/verify_selected_result.py +python3 -m unittest discover -s tests -p test_selected_result.py +``` + +The baseline reports source bindings only, unchanged selected kappa +`836330098538459/500000000000000000`, and the complex side binding. The five +selected-result tests pass. No selected frontier file or upstream file changed. + +Overlap: initial complete850-PR snapshot; refreshed complete855-PR snapshot +and12 discussions exposed PR1256 and caused the documented one-scope pivot. +Final latest100-PR refresh through PR1268 found no additional later-cut census; +newer work concerns other circuits, packing and ledger verification. These +bounded live observations do not constitute a novelty guarantee. + +Not run or claimed: native 5/9/11-stage supplier replay, full selected cold +replay, new suffix construction, hosted admission, complete paid profile, +remote CI, proof-assistant verification or independent human review. diff --git a/research/r439-later-retirement-cuts/VERIFY.json b/research/r439-later-retirement-cuts/VERIFY.json new file mode 100644 index 0000000000..d0b8177ef4 --- /dev/null +++ b/research/r439-later-retirement-cuts/VERIFY.json @@ -0,0 +1,55 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/later_cuts.py" + ], + "timeout_seconds": 120, + "checks": "Complete4278 pair census using incremental inverse updates." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/check_later_cuts.py" + ], + "timeout_seconds": 120, + "checks": "Independent inverse rebuilt from scratch at all713 boundaries; compare every boundary." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/test_later_cuts.py" + ], + "timeout_seconds": 120, + "checks": "Boundary, donor, target-access, coverage, source corruption and relocation controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 120, + "checks": "Retained original439-helper stationary fixtures and their semantic controls." + } + ] +} diff --git a/research/r439-later-retirement-cuts/check_later_cuts.py b/research/r439-later-retirement-cuts/check_later_cuts.py new file mode 100644 index 0000000000..5c0f46de39 --- /dev/null +++ b/research/r439-later-retirement-cuts/check_later_cuts.py @@ -0,0 +1,82 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Independent every-boundary inverse replay; no later_cuts/verify imports.""" +import gzip +import hashlib +import importlib.util +import json +from pathlib import Path + +HERE=Path(__file__).resolve().parent +spec=importlib.util.spec_from_file_location('integer_geometry',HERE/'independent.py') +I=importlib.util.module_from_spec(spec);spec.loader.exec_module(I) + + +def check(cert): + raw=(I.ROOT/I.WORD).read_bytes();I.need(hashlib.sha256(raw).hexdigest()==I.SHA,'source hash') + w=json.loads(gzip.decompress(raw));n=2*w['v']+w['R'];v=w['v'] + state=[{r} for r in range(n)];current=w['start'][:] + prefix=w['D']+w['A']+[[0,v+t,[w['ret'][j]]] for t,js in enumerate(w['scatter']) for j in js] + for section in ['D','A']: + for f,t,ss in w[section]: + for r in [t]+ss:current[r]=f + for s in ss:state[t]^=state[s] + for t,js in enumerate(w['scatter']): + for j in js:state[v+t]^=state[w['ret'][j]] + frames=[I.reduce_rows([w['lines'][i] for i in f]) for f in w['frames']] + expanded={} + I.need([h['helper'] for h in cert['helpers']]==[465,466,468,469,470,476],'helper coverage') + for entry in cert['helpers']: + sequence=[] + for run in entry['runs']: + I.need(run['first_cut']==len(sequence) and run['last_cut']>=run['first_cut'],'run coverage') + sequence += [run['conditions']]*(run['last_cut']-run['first_cut']+1) + I.need(len(sequence)==713,'cut coverage') + passed=[k for k,r in enumerate(sequence) if r.get('lost_targets')==[]] + windows=[] + for k in passed: + if not windows or windows[-1][1]+1!=k:windows.append([k,k]) + else:windows[-1][1]=k + I.need(windows==entry['windows'] and len(passed)==entry['necessary_condition_pass_count'],'windows') + I.need(sum(r['joint_rank']==7 for r in sequence)==entry['joint_rank_seven_cuts'],'join counts') + expanded[entry['helper']]=sequence + geometry,subset_cache={},{} + def join(registers): + key=tuple(sorted({current[r] for r in registers})) + if key not in geometry:geometry[key]=I.reduce_rows([x for f in key for x in frames[f]]) + return geometry[key] + def subset(vecs,f): + key=(tuple(map(tuple,vecs)),f) + if key not in subset_cache:subset_cache[key]=len(I.reduce_rows(vecs+frames[f]))==len(frames[f]) + return subset_cache[key] + def support(value):return [r for r in range(n) if value & (1<= pivot and pivot in matrix[r]) + matrix[pivot], matrix[donor] = matrix[donor], matrix[pivot] + inverse[pivot], inverse[donor] = inverse[donor], inverse[pivot] + for r in z: + if r != pivot and pivot in matrix[r]: + matrix[r] ^= matrix[pivot] + inverse[r] ^= inverse[pivot] + need(all(matrix[r] == {r} for r in z), 'matrix inverse') + frames = [reduce_rows([w['lines'][i] for i in f]) for f in w['frames']] + def subset(a, b): + return len(reduce_rows(frames[a]+frames[b])) == len(frames[b]) + ranks = [] + cases = [] + for h in range(2*v, n): + restore = sorted(inverse[h]) + dirt = [r for r in range(n) if h in rows[r]] + involved = sorted(set(restore+dirt+[h])) + vectors = [x for r in involved for x in frames[current[r]]] + rank = len(reduce_rows(vectors)) + ranks.append([h, rank]) + if rank == 7: + candidates = [f for f in range(len(frames)) if len(frames[f]) == 7 + and len(reduce_rows(vectors+frames[f])) == 7] + station = min(candidates) + blocked = [r for r in involved if r != h and not subset(station, w['final'][r])] + gates = [[h, r] for r in restore if r != h]+[[r, h] for r in dirt if r != h] + case = {'helper':h, 'station':station, 'restore':restore, 'dirt':dirt, + 'endpoint_blockers':blocked, 'isolation_gates':gates, 'legal':not blocked} + if not blocked: + values, now = [set(row) for row in rows], current[:] + for dst, src in gates: + for r in (dst, src): + need(subset(now[r], station), 'arrival') + need(subset(station, station if r == h else w['final'][r]), 'cap') + now[r] = station + values[dst] ^= values[src] + need(values[h] == {h}, 'restoration') + need(all(values[r] == rows[r]-{h} for r in range(n) if r != h), 'clean columns') + case['minimum_adds'] = max(len(dirt)-1+int(rows[h] != {h}), len(restore)-1) + need(case['minimum_adds'] == len(gates), 'optimality') + case['promotions'] = [{'register':r, 'from_frame':current[r], 'to_frame':station, + 'rank_increment':7-len(frames[current[r]])} + for r in involved if not subset(station, current[r])] + for i, (f, dst, srcs) in enumerate(w['B']): + bad = [r for r in [dst]+srcs if not subset(now[r], f)] + if bad: + case['first_fixed_B_conflict'] = {'gate_index':i,'frame':f,'registers':bad} + break + for r in [dst]+srcs: + now[r] = f + need('first_fixed_B_conflict' in case, 'continuation conflict') + cases.append(case) + result = {'schema_version':1, 'status':'SCOPED_SINGLE_STATION_CLASSIFICATION', + 'seed':17, 'word_sha256':SHA, 'join_rank_counts':{str(k):sum(r==k for _,r in ranks) for k in [7,8]}, + 'all_helper_join_ranks':ranks, 'rank_seven_cases':cases, + 'legal_helpers':[r['helper'] for r in cases if r['legal']], 'no_new_kappa':True} + need(result == cert, 'independent certificate mismatch') + return result + + +if __name__ == '__main__': + check(json.loads((HERE/'CERTIFICATE.json').read_text())) + print('PASS_INDEPENDENT_SINGLE_STATION sets=661 Gaussian_inverse=550 helpers=439 legal=3') diff --git a/research/r439-later-retirement-cuts/later_cuts.py b/research/r439-later-retirement-cuts/later_cuts.py new file mode 100644 index 0000000000..f687873634 --- /dev/null +++ b/research/r439-later-retirement-cuts/later_cuts.py @@ -0,0 +1,84 @@ +# SPDX-License-Identifier: Apache-2.0 +"""All fixed-B-prefix cuts; exact necessary conditions, not suffix synthesis.""" +import argparse +import importlib.util +import json +from pathlib import Path + +HERE=Path(__file__).resolve().parent +spec=importlib.util.spec_from_file_location('station_verify',HERE/'verify.py') +V=importlib.util.module_from_spec(spec);spec.loader.exec_module(V) +HELPERS=[465,466,468,469,470,476] + + +def compute(): + w=V.load(); n=2*w['v']+w['R']; v=w['v']; rows,current,_=V.cut(w) + fb=[V.basis([w['lines'][i] for i in f]) for f in w['frames']] + gates=w['D']+w['A']+[[0,v+t,[w['ret'][j]]] for t,js in enumerate(w['scatter']) for j in js] + inv=[1<>h&1] + U=join(donors+dirt+[h]) + record={'joint_rank':len(U)} + if len(U)<=7: + J=join(donors+[h]);mask=sum(1<>t&1:restore[h]^=sm + for i in range(v): + if target[i]>>t&1:target[i]^=sm + result=[] + for h in HELPERS: + runs=[] + for cut,row in enumerate(all_rows[h]): + if not runs or runs[-1]['conditions']!=row: + runs.append({'first_cut':cut,'last_cut':cut,'conditions':row}) + else:runs[-1]['last_cut']=cut + passed=[i for i,row in enumerate(all_rows[h]) if row.get('lost_targets')==[]] + windows=[] + for i in passed: + if not windows or windows[-1][1]+1!=i:windows.append([i,i]) + else:windows[-1][1]=i + result.append({'helper':h,'joint_rank_seven_cuts':sum(r['joint_rank']==7 for r in all_rows[h]), + 'necessary_condition_pass_count':len(passed),'windows':windows,'runs':runs}) + return {'schema_version':1,'source_sha256':V.DIGEST,'B_gate_count':len(w['B']), + 'cuts_per_helper':len(w['B'])+1,'helper_cut_pairs':len(HELPERS)*(len(w['B'])+1), + 'cut_convention':'cut k is after exactly the first k B records, with D/A/scatter fixed', + 'meaning':'Passing both necessary tests is not a legal suffix or new supplier.', + 'helpers':result,'no_new_kappa':True} + + +def main(): + ap=argparse.ArgumentParser();ap.add_argument('--output',type=Path);args=ap.parse_args() + result=compute() + if args.output: + with args.output.open('x') as out:json.dump(result,out,indent=2,sort_keys=True);out.write('\n') + else:V.require(result==json.loads((HERE/'LATER-CUTS.json').read_text()),'later-cut certificate mismatch') + print('PASS_LATER_BIT_CUTS pairs=4278 windows=465:10-48,468:31-88,470:0-517 excluded=466,469,476 no_new_kappa') + +if __name__=='__main__':main() diff --git a/research/r439-later-retirement-cuts/test_later_cuts.py b/research/r439-later-retirement-cuts/test_later_cuts.py new file mode 100644 index 0000000000..8a1ecb1743 --- /dev/null +++ b/research/r439-later-retirement-cuts/test_later_cuts.py @@ -0,0 +1,75 @@ +# SPDX-License-Identifier: Apache-2.0 +import copy +import importlib.util +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +HERE=Path(__file__).resolve().parent + +def module(name): + s=importlib.util.spec_from_file_location(name,HERE/(name+'.py')) + m=importlib.util.module_from_spec(s);s.loader.exec_module(m);return m + +P,Q=module('later_cuts'),module('check_later_cuts') + +class LaterCutTests(unittest.TestCase): + @classmethod + def setUpClass(cls):cls.cert=json.loads((HERE/'LATER-CUTS.json').read_text()) + + def test_complete_both_engines(self): + self.assertEqual(P.compute(),self.cert) + Q.check(self.cert) + + def test_named_boundary_witnesses(self): + cases={e['helper']:e for e in self.cert['helpers']} + def row(h,k):return next(r['conditions'] for r in cases[h]['runs'] if r['first_cut']<=k<=r['last_cut']) + self.assertEqual(row(465,9)['lost_targets'],[122]) + self.assertEqual(row(465,10)['lost_targets'],[]) + self.assertEqual(row(465,48)['joint_rank'],7) + self.assertEqual(row(465,49)['joint_rank'],8) + self.assertEqual(row(468,30)['lost_targets'],[144]) + self.assertEqual(row(468,31)['lost_targets'],[]) + self.assertEqual(row(468,88)['joint_rank'],7) + self.assertEqual(row(468,89)['joint_rank'],8) + self.assertEqual(row(466,78)['lost_targets'],[208]) + self.assertEqual(row(466,79)['joint_rank'],8) + self.assertEqual(row(466,89)['joint_rank'],8) + + def test_mathematical_certificate_faults(self): + mutations=[lambda c:c['helpers'][0]['windows'][0].__setitem__(0,9), + lambda c:c['helpers'][0]['runs'][0]['conditions']['lost_targets'].clear(), + lambda c:c['helpers'][1]['runs'][0]['conditions']['restore_donors'].append(1), + lambda c:c['helpers'][3]['runs'][0]['conditions'].update({'joint_rank':8}), + lambda c:c['helpers'][4]['runs'][-1].update({'last_cut':711}), + lambda c:c['helpers'].pop()] + for mut in mutations: + bad=copy.deepcopy(self.cert);mut(bad) + self.assertNotEqual(P.compute(),bad) + with self.assertRaises(ValueError):Q.check(bad) + + def test_source_only_optimized_relocation_and_controls(self): + with tempfile.TemporaryDirectory(prefix='later bit cuts ') as tmp: + root=Path(tmp);pkg=root/'research/r439-later-retirement-cuts' + shutil.copytree(HERE,pkg) + raw=root/P.V.WORD;raw.parent.mkdir(parents=True,exist_ok=True) + shutil.copy2(P.V.ROOT/P.V.WORD,raw) + for script in ['later_cuts.py','check_later_cuts.py']: + run=subprocess.run([sys.executable,'-I','-O','-B',str(pkg/script)],cwd=root,capture_output=True,text=True) + self.assertEqual(run.returncode,0,run.stderr) + out=root/'later-regenerated.json' + cmd=[sys.executable,'-I','-O','-B',str(pkg/'later_cuts.py'),'--output',str(out)] + self.assertEqual(subprocess.run(cmd,capture_output=True).returncode,0) + self.assertEqual(json.loads(out.read_text()),self.cert) + self.assertNotEqual(subprocess.run(cmd,capture_output=True).returncode,0) + raw.write_bytes(raw.read_bytes()+b'corrupt') + for script in ['later_cuts.py','check_later_cuts.py']: + run=subprocess.run([sys.executable,'-I','-O','-B',str(pkg/script)],capture_output=True,text=True) + self.assertNotEqual(run.returncode,0) + self.assertIn('source hash',run.stderr) + +if __name__=='__main__':unittest.main(verbosity=2) diff --git a/research/r439-later-retirement-cuts/test_package.py b/research/r439-later-retirement-cuts/test_package.py new file mode 100644 index 0000000000..4ab08384f9 --- /dev/null +++ b/research/r439-later-retirement-cuts/test_package.py @@ -0,0 +1,110 @@ +# SPDX-License-Identifier: Apache-2.0 +import copy +import importlib.util +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent + +def module(name): + spec = importlib.util.spec_from_file_location(name, HERE/(name+'.py')) + mod = importlib.util.module_from_spec(spec) + spec.loader.exec_module(mod) + return mod + +V, I = module('verify'), module('independent') + +class PackageTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.cert = json.loads((HERE/'CERTIFICATE.json').read_text()) + cls.word = V.load() + cls.rows, cls.current, _ = V.cut(cls.word) + cls.fb = [V.basis([cls.word['lines'][i] for i in f]) for f in cls.word['frames']] + + def test_complete_separate_replays(self): + V.verify(self.cert, self.word) + I.check(self.cert) + + def test_all_ten_gate_omissions(self): + total = 0 + for row in self.cert['rank_seven_cases']: + if row['legal']: + for j in range(len(row['isolation_gates'])): + gates = row['isolation_gates'][:j]+row['isolation_gates'][j+1:] + with self.assertRaisesRegex(ValueError, 'restoration|another column'): + V.station_check(self.word, self.rows, self.current, self.fb, + row['helper'], row['station'], gates) + total += 1 + self.assertEqual(total, 10) + + def test_three_target_caps_and_relaxed_positive_controls(self): + count = 0 + for row in self.cert['rank_seven_cases']: + if not row['legal']: + with self.assertRaisesRegex(ValueError, 'final endpoint cap'): + V.station_check(self.word, self.rows, self.current, self.fb, + row['helper'], row['station'], row['isolation_gates']) + relaxed = copy.deepcopy(self.word) + for r in row['endpoint_blockers']: + relaxed['final'][r] = 1 + V.station_check(relaxed, self.rows, self.current, self.fb, + row['helper'], row['station'], row['isolation_gates']) + count += 1 + self.assertEqual(count, 3) + + def test_certificate_corruptions_both_engines(self): + mutations = [lambda c:c['join_rank_counts'].update({'8':432}), + lambda c:c['legal_helpers'].append(465), + lambda c:c['rank_seven_cases'][0]['endpoint_blockers'].clear(), + lambda c:c['rank_seven_cases'][3].update({'minimum_adds':2}), + lambda c:c['rank_seven_cases'][4]['isolation_gates'].pop(), + lambda c:c['rank_seven_cases'][5]['first_fixed_B_conflict'].update({'gate_index':285})] + for mutation in mutations: + bad = copy.deepcopy(self.cert) + mutation(bad) + with self.assertRaisesRegex(ValueError, 'certificate mismatch'): + V.verify(bad, self.word) + with self.assertRaisesRegex(ValueError, 'certificate mismatch'): + I.check(bad) + + def test_wrong_station_and_original_dirty_endpoint(self): + row = self.cert['rank_seven_cases'][3] + with self.assertRaisesRegex(ValueError, 'station arrival'): + V.station_check(self.word, self.rows, self.current, self.fb, 469, 513, row['isolation_gates']) + bad = copy.deepcopy(self.word) + bad['C'] = bad['C'][:-1] + with self.assertRaisesRegex(ValueError, 'baseline full endpoint'): + V.derive(bad) + + def test_relocation_source_pin_regeneration_and_overwrite(self): + with tempfile.TemporaryDirectory(prefix='station exits ') as tmp: + root = Path(tmp) + pkg = root/'research/r439-later-retirement-cuts' + shutil.copytree(HERE, pkg) + raw = root/V.WORD + raw.parent.mkdir(parents=True, exist_ok=True) + shutil.copy2(V.ROOT/V.WORD, raw) + for script in ['verify.py','independent.py']: + run = subprocess.run([sys.executable,'-I','-O','-B',str(pkg/script)], + cwd=root, capture_output=True, text=True) + self.assertEqual(run.returncode, 0, run.stderr) + out = root/'regenerated.json' + command = [sys.executable,'-I','-O','-B',str(pkg/'verify.py'),'--output',str(out)] + self.assertEqual(subprocess.run(command, capture_output=True).returncode, 0) + self.assertEqual(json.loads(out.read_text()), self.cert) + self.assertNotEqual(subprocess.run(command, capture_output=True).returncode, 0) + raw.write_bytes(raw.read_bytes()+b'corrupt') + for script in ['verify.py','independent.py']: + run = subprocess.run([sys.executable,'-I','-O','-B',str(pkg/script)], + capture_output=True,text=True) + self.assertNotEqual(run.returncode, 0) + self.assertIn('source hash', run.stderr) + +if __name__ == '__main__': + unittest.main(verbosity=2) diff --git a/research/r439-later-retirement-cuts/verify.py b/research/r439-later-retirement-cuts/verify.py new file mode 100644 index 0000000000..99f7c75177 --- /dev/null +++ b/research/r439-later-retirement-cuts/verify.py @@ -0,0 +1,182 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Exact single-station classification. Philipp, with OpenAI Codex assistance.""" +import argparse +import gzip +import hashlib +import json +from fractions import Fraction +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +WORD = "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz" +DIGEST = "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f" + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def basis(vectors): + pivots = {} + for vector in vectors: + row = list(map(Fraction, vector)) + for p in sorted(pivots): + q = row[p] + if q: + row = [a - q*b for a, b in zip(row, pivots[p])] + p = next((i for i, x in enumerate(row) if x), None) + if p is not None: + q = row[p] + pivots[p] = [x/q for x in row] + if len(pivots) == 8: + break + return [pivots[p] for p in sorted(pivots)] + + +def contained(left, right): + return len(basis(right + left)) == len(right) + + +def bits(n): + while n: + b = n & -n + yield b.bit_length()-1 + n ^= b + + +def load(root=ROOT): + raw = (root / WORD).read_bytes() + require(hashlib.sha256(raw).hexdigest() == DIGEST, "source hash") + return json.loads(gzip.decompress(raw)) + + +def cut(word): + n, v = 2*word['v'] + word['R'], word['v'] + rows, frames = [1 << r for r in range(n)], word['start'][:] + for section in ('D', 'A'): + for f, t, ss in word[section]: + for r in [t, *ss]: + frames[r] = f + for s in ss: + rows[t] ^= rows[s] + for t, totals in enumerate(word['scatter']): + for total in totals: + rows[v+t] ^= rows[word['ret'][total]] + inverse = [1 << r for r in range(n)] + for _, t, ss in reversed(word['A']): + if not v <= t < 2*v: + for s in ss: + inverse[t] ^= inverse[s] + return rows, frames, inverse + + +def station_check(word, rows, current, fb, h, u, gates): + state, actual = rows[:], current[:] + for t, s in gates: + require(t != s, "self addition") + for r in (t, s): + require(contained(fb[actual[r]], fb[u]), "station arrival") + cap = u if r == h else word['final'][r] + require(contained(fb[u], fb[cap]), "final endpoint cap") + actual[r] = u + state[t] ^= state[s] + require(state[h] == 1 << h, "helper restoration") + for r in range(len(state)): + if r != h: + require(state[r] == rows[r] ^ (((rows[r] >> h) & 1) << h), + "isolation changes another column") + return actual + + +def derive(word): + rows, current, inverse = cut(word) + fb = [basis([word['lines'][i] for i in frame]) for frame in word['frames']] + baseline, frame_path = rows[:], current[:] + for section in ('B', 'C'): + for f, t, ss in word[section]: + for r in [t, *ss]: + require(contained(fb[frame_path[r]], fb[f]), 'baseline monotone frame') + frame_path[r] = f + for s in ss: + baseline[t] ^= baseline[s] + for r, value in enumerate(baseline): + expected = (1 << r) ^ ((1 << (r-word['v'])) if word['v'] <= r < 2*word['v'] else 0) + require(value == expected, 'baseline full endpoint') + require(contained(fb[frame_path[r]], fb[word['final'][r]]), 'baseline final cap') + counts, rank_rows, survivors = {}, [], [] + for h in range(2*word['v'], len(rows)): + restore = list(bits(inverse[h])) + got = 0 + for r in restore: + got ^= rows[r] + require(got == 1 << h, "inverse row") + dirt = [r for r, value in enumerate(rows) if value >> h & 1] + donors = sorted(set(restore + dirt + [h])) + join = basis([line for r in donors for line in fb[current[r]]]) + rank = len(join) + counts[str(rank)] = counts.get(str(rank), 0) + 1 + rank_rows.append([h, rank]) + if rank != 7: + require(rank == 8, "unexpected join rank") + continue + require(h in restore, "missing pivot") + choices = [f for f, b in enumerate(fb) if len(b) == 7 and contained(join, b)] + require(bool(choices), "missing catalogued hyperplane") + u = min(choices) + blocked = [r for r in donors if r != h and not contained(fb[u], fb[word['final'][r]])] + gates = [[h, r] for r in restore if r != h] + [[r, h] for r in dirt if r != h] + row = {'helper': h, 'station': u, 'restore': restore, 'dirt': dirt, + 'endpoint_blockers': blocked, 'isolation_gates': gates, + 'legal': not blocked} + if not blocked: + actual = station_check(word, rows, current, fb, h, u, gates) + lower = max(len(dirt)-1 + int(rows[h] != 1 << h), len(restore)-1) + require(lower == len(gates), "non-sharp gate lower bound") + row['minimum_adds'] = lower + row['promotions'] = [{'register': r, 'from_frame': current[r], + 'to_frame': u, 'rank_increment': 7-len(fb[current[r]])} + for r in donors if not contained(fb[u], fb[current[r]])] + conflict = None + for i, (f, t, ss) in enumerate(word['B']): + bad = [r for r in [t, *ss] if not contained(fb[actual[r]], fb[f])] + if bad: + conflict = {'gate_index': i, 'frame': f, 'registers': bad} + break + for r in [t, *ss]: + actual[r] = f + require(conflict is not None, "unexpected unchanged-B continuation") + row['first_fixed_B_conflict'] = conflict + survivors.append(row) + return {'schema_version': 1, 'status': 'SCOPED_SINGLE_STATION_CLASSIFICATION', + 'seed': 17, 'word_sha256': DIGEST, 'join_rank_counts': counts, + 'all_helper_join_ranks': rank_rows, 'rank_seven_cases': survivors, + 'legal_helpers': [r['helper'] for r in survivors if r['legal']], + 'no_new_kappa': True} + + +def verify(expected, word): + actual = derive(word) + require(actual == expected, "certificate mismatch") + require(actual['legal_helpers'] == [469, 470, 476], "legal set") + return actual + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--root', type=Path, default=ROOT) + parser.add_argument('--output', type=Path) + args = parser.parse_args() + result = derive(load(args.root)) + if args.output: + with args.output.open('x') as stream: + json.dump(result, stream, indent=2, sort_keys=True) + stream.write('\n') + else: + require(result == json.loads((HERE/'CERTIFICATE.json').read_text()), 'certificate mismatch') + print('PASS_SINGLE_STATION_EXITS helpers=439 join8=433 endpoint_blocked=3 legal=469,470,476 adds=3,3,4 no_new_kappa') + + +if __name__ == '__main__': + main()