diff --git a/research/p112-rank6-hall-obstruction/CERTIFICATE.json b/research/p112-rank6-hall-obstruction/CERTIFICATE.json new file mode 100644 index 0000000000..ce6227f3d0 --- /dev/null +++ b/research/p112-rank6-hall-obstruction/CERTIFICATE.json @@ -0,0 +1,2056 @@ +{ + "schema_version": 1, + "copy_profile": [ + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 8 + ], + "total_copy_rank": 62, + "support_sha256": "553f17ddef29c997a3f8c6b282bf40be665a73833f2a6a89e04804f3648b668a", + "frames": { + "frame_hit_histogram": { + "8": 305, + "9": 650, + "10": 305 + }, + "minimum_frame_hits": 8, + "diagonal_hit_histogram": { + "1": 51, + "2": 40, + "3": 15, + "4": 6 + }, + "uncovered_diagonals": [], + "saturated_frames": 305, + "empty_trace_constraints": [ + [ + 4, + 1 + ], + [ + 6, + 0 + ], + [ + 7, + 2 + ], + [ + 37, + 7 + ], + [ + 39, + 0 + ], + [ + 43, + 1 + ], + [ + 43, + 7 + ], + [ + 44, + 4 + ], + [ + 48, + 4 + ], + [ + 49, + 6 + ], + [ + 52, + 7 + ], + [ + 56, + 7 + ], + [ + 62, + 2 + ], + [ + 67, + 0 + ], + [ + 67, + 4 + ], + [ + 69, + 7 + ], + [ + 72, + 7 + ], + [ + 73, + 2 + ], + [ + 73, + 7 + ], + [ + 81, + 6 + ], + [ + 83, + 0 + ], + [ + 83, + 4 + ], + [ + 88, + 7 + ], + [ + 98, + 8 + ], + [ + 99, + 8 + ], + [ + 101, + 0 + ], + [ + 101, + 1 + ], + [ + 102, + 2 + ], + [ + 102, + 8 + ], + [ + 103, + 2 + ], + [ + 103, + 8 + ], + [ + 105, + 0 + ], + [ + 105, + 1 + ], + [ + 115, + 0 + ], + [ + 117, + 0 + ], + [ + 117, + 1 + ], + [ + 119, + 0 + ], + [ + 119, + 2 + ], + [ + 121, + 0 + ], + [ + 122, + 0 + ], + [ + 122, + 1 + ], + [ + 123, + 1 + ], + [ + 124, + 1 + ], + [ + 124, + 5 + ], + [ + 125, + 1 + ], + [ + 126, + 0 + ], + [ + 126, + 1 + ], + [ + 126, + 5 + ], + [ + 127, + 1 + ], + [ + 130, + 2 + ], + [ + 133, + 1 + ], + [ + 140, + 5 + ], + [ + 140, + 8 + ], + [ + 141, + 0 + ], + [ + 141, + 8 + ], + [ + 144, + 2 + ], + [ + 144, + 5 + ], + [ + 144, + 8 + ], + [ + 145, + 2 + ], + [ + 145, + 8 + ], + [ + 147, + 0 + ], + [ + 148, + 1 + ], + [ + 149, + 0 + ], + [ + 149, + 1 + ], + [ + 150, + 2 + ], + [ + 152, + 1 + ], + [ + 152, + 2 + ], + [ + 153, + 1 + ], + [ + 156, + 8 + ], + [ + 157, + 0 + ], + [ + 157, + 8 + ], + [ + 160, + 8 + ], + [ + 161, + 8 + ], + [ + 165, + 0 + ], + [ + 165, + 1 + ], + [ + 169, + 1 + ], + [ + 182, + 4 + ], + [ + 183, + 3 + ], + [ + 183, + 6 + ], + [ + 186, + 4 + ], + [ + 198, + 4 + ], + [ + 198, + 5 + ], + [ + 199, + 4 + ], + [ + 199, + 6 + ], + [ + 202, + 2 + ], + [ + 202, + 4 + ], + [ + 203, + 4 + ], + [ + 203, + 6 + ], + [ + 204, + 1 + ], + [ + 204, + 3 + ], + [ + 207, + 5 + ], + [ + 207, + 6 + ], + [ + 213, + 1 + ], + [ + 213, + 5 + ], + [ + 214, + 4 + ], + [ + 214, + 5 + ], + [ + 218, + 4 + ], + [ + 219, + 6 + ], + [ + 222, + 6 + ], + [ + 223, + 5 + ], + [ + 223, + 6 + ], + [ + 226, + 6 + ], + [ + 236, + 3 + ], + [ + 237, + 4 + ], + [ + 243, + 2 + ], + [ + 243, + 5 + ], + [ + 243, + 6 + ], + [ + 251, + 6 + ], + [ + 253, + 4 + ], + [ + 285, + 5 + ], + [ + 285, + 7 + ], + [ + 289, + 2 + ], + [ + 289, + 7 + ], + [ + 293, + 1 + ], + [ + 297, + 1 + ], + [ + 342, + 5 + ], + [ + 343, + 2 + ], + [ + 344, + 5 + ], + [ + 353, + 0 + ], + [ + 353, + 4 + ], + [ + 353, + 6 + ], + [ + 357, + 0 + ], + [ + 357, + 4 + ], + [ + 357, + 6 + ], + [ + 361, + 0 + ], + [ + 363, + 0 + ], + [ + 363, + 2 + ], + [ + 367, + 5 + ], + [ + 368, + 4 + ], + [ + 368, + 5 + ], + [ + 369, + 4 + ], + [ + 369, + 6 + ], + [ + 371, + 2 + ], + [ + 372, + 2 + ], + [ + 372, + 4 + ], + [ + 373, + 4 + ], + [ + 373, + 6 + ], + [ + 374, + 0 + ], + [ + 374, + 1 + ], + [ + 377, + 5 + ], + [ + 377, + 6 + ], + [ + 378, + 0 + ], + [ + 378, + 1 + ], + [ + 379, + 2 + ], + [ + 382, + 1 + ], + [ + 383, + 0 + ], + [ + 383, + 1 + ], + [ + 383, + 5 + ], + [ + 384, + 4 + ], + [ + 384, + 5 + ], + [ + 385, + 4 + ], + [ + 385, + 6 + ], + [ + 386, + 1 + ], + [ + 387, + 0 + ], + [ + 387, + 1 + ], + [ + 388, + 4 + ], + [ + 389, + 4 + ], + [ + 389, + 6 + ], + [ + 393, + 5 + ], + [ + 393, + 6 + ], + [ + 406, + 0 + ], + [ + 406, + 4 + ], + [ + 409, + 0 + ], + [ + 409, + 2 + ], + [ + 409, + 5 + ], + [ + 409, + 6 + ], + [ + 410, + 1 + ], + [ + 411, + 2 + ], + [ + 417, + 0 + ], + [ + 417, + 4 + ], + [ + 417, + 6 + ], + [ + 421, + 4 + ], + [ + 421, + 6 + ], + [ + 422, + 0 + ], + [ + 422, + 4 + ], + [ + 426, + 1 + ], + [ + 431, + 0 + ], + [ + 435, + 0 + ], + [ + 455, + 5 + ], + [ + 455, + 8 + ], + [ + 456, + 5 + ], + [ + 457, + 7 + ], + [ + 459, + 2 + ], + [ + 459, + 8 + ], + [ + 460, + 2 + ], + [ + 461, + 7 + ], + [ + 462, + 5 + ], + [ + 465, + 5 + ], + [ + 468, + 7 + ], + [ + 481, + 0 + ], + [ + 481, + 2 + ], + [ + 481, + 5 + ], + [ + 485, + 2 + ], + [ + 497, + 0 + ], + [ + 505, + 4 + ], + [ + 509, + 4 + ], + [ + 527, + 3 + ], + [ + 527, + 6 + ], + [ + 547, + 5 + ], + [ + 547, + 6 + ], + [ + 560, + 3 + ], + [ + 560, + 7 + ], + [ + 563, + 5 + ], + [ + 563, + 6 + ], + [ + 565, + 7 + ], + [ + 569, + 0 + ], + [ + 569, + 5 + ], + [ + 575, + 6 + ], + [ + 576, + 7 + ], + [ + 577, + 4 + ], + [ + 577, + 7 + ], + [ + 581, + 7 + ], + [ + 591, + 6 + ], + [ + 593, + 4 + ], + [ + 593, + 7 + ], + [ + 601, + 3 + ], + [ + 605, + 3 + ], + [ + 635, + 3 + ], + [ + 635, + 5 + ], + [ + 639, + 2 + ], + [ + 639, + 3 + ], + [ + 651, + 5 + ], + [ + 655, + 2 + ], + [ + 657, + 3 + ], + [ + 657, + 5 + ], + [ + 680, + 0 + ], + [ + 686, + 5 + ], + [ + 690, + 6 + ], + [ + 692, + 7 + ], + [ + 693, + 0 + ], + [ + 693, + 6 + ], + [ + 694, + 2 + ], + [ + 694, + 6 + ], + [ + 704, + 2 + ], + [ + 704, + 7 + ], + [ + 714, + 0 + ], + [ + 729, + 2 + ], + [ + 729, + 6 + ], + [ + 738, + 7 + ], + [ + 739, + 0 + ], + [ + 739, + 5 + ], + [ + 740, + 5 + ], + [ + 741, + 6 + ], + [ + 743, + 0 + ], + [ + 744, + 7 + ], + [ + 745, + 6 + ], + [ + 747, + 2 + ], + [ + 747, + 7 + ], + [ + 753, + 2 + ], + [ + 753, + 6 + ], + [ + 763, + 2 + ], + [ + 763, + 7 + ], + [ + 771, + 0 + ], + [ + 771, + 4 + ], + [ + 772, + 5 + ], + [ + 772, + 8 + ], + [ + 773, + 8 + ], + [ + 775, + 3 + ], + [ + 775, + 4 + ], + [ + 779, + 0 + ], + [ + 794, + 8 + ], + [ + 795, + 5 + ], + [ + 795, + 8 + ], + [ + 818, + 5 + ], + [ + 819, + 4 + ], + [ + 821, + 1 + ], + [ + 821, + 5 + ], + [ + 823, + 1 + ], + [ + 825, + 4 + ], + [ + 827, + 3 + ], + [ + 827, + 5 + ], + [ + 863, + 0 + ], + [ + 863, + 6 + ], + [ + 867, + 3 + ], + [ + 867, + 6 + ], + [ + 874, + 7 + ], + [ + 884, + 0 + ], + [ + 899, + 4 + ], + [ + 899, + 6 + ], + [ + 904, + 3 + ], + [ + 904, + 7 + ], + [ + 908, + 7 + ], + [ + 917, + 7 + ], + [ + 923, + 6 + ], + [ + 932, + 7 + ], + [ + 933, + 7 + ], + [ + 941, + 0 + ], + [ + 941, + 4 + ], + [ + 942, + 8 + ], + [ + 943, + 8 + ], + [ + 945, + 3 + ], + [ + 945, + 4 + ], + [ + 964, + 8 + ], + [ + 965, + 2 + ], + [ + 965, + 8 + ], + [ + 983, + 4 + ], + [ + 987, + 4 + ], + [ + 989, + 4 + ], + [ + 991, + 1 + ], + [ + 993, + 1 + ], + [ + 995, + 4 + ], + [ + 1038, + 2 + ], + [ + 1039, + 2 + ], + [ + 1044, + 5 + ], + [ + 1045, + 1 + ], + [ + 1045, + 5 + ], + [ + 1052, + 7 + ], + [ + 1066, + 3 + ], + [ + 1069, + 4 + ], + [ + 1069, + 7 + ], + [ + 1072, + 4 + ], + [ + 1075, + 4 + ], + [ + 1075, + 7 + ], + [ + 1078, + 4 + ], + [ + 1092, + 2 + ], + [ + 1093, + 2 + ], + [ + 1099, + 7 + ], + [ + 1102, + 0 + ], + [ + 1105, + 7 + ], + [ + 1114, + 7 + ], + [ + 1122, + 5 + ], + [ + 1123, + 5 + ], + [ + 1124, + 3 + ], + [ + 1125, + 5 + ], + [ + 1125, + 6 + ], + [ + 1129, + 7 + ], + [ + 1131, + 7 + ], + [ + 1132, + 0 + ], + [ + 1132, + 4 + ], + [ + 1133, + 0 + ], + [ + 1133, + 4 + ], + [ + 1135, + 7 + ], + [ + 1138, + 4 + ], + [ + 1139, + 4 + ], + [ + 1140, + 4 + ], + [ + 1142, + 1 + ], + [ + 1144, + 1 + ], + [ + 1146, + 4 + ], + [ + 1154, + 8 + ], + [ + 1178, + 8 + ], + [ + 1179, + 7 + ], + [ + 1185, + 7 + ], + [ + 1190, + 0 + ], + [ + 1196, + 0 + ], + [ + 1196, + 1 + ], + [ + 1198, + 1 + ], + [ + 1199, + 5 + ], + [ + 1199, + 6 + ], + [ + 1209, + 7 + ], + [ + 1211, + 0 + ], + [ + 1220, + 4 + ], + [ + 1221, + 4 + ], + [ + 1223, + 2 + ], + [ + 1233, + 2 + ], + [ + 1244, + 4 + ], + [ + 1245, + 4 + ] + ] + }, + "all_clique_rank_counts": { + "cliques_by_size": { + "1": 112, + "2": 3304, + "3": 31024, + "4": 94892, + "5": 82656, + "6": 39088, + "7": 10592, + "8": 1260 + }, + "failed_cliques": 375, + "first_failure": [ + [ + 10, + 11 + ], + 1 + ] + }, + "separator": { + "frame": [ + 2, + 3, + 20, + 21, + 40, + 41, + 48, + 49 + ], + "term": 1, + "active_terms": [ + 0, + 1, + 2, + 3, + 4, + 5, + 7, + 9 + ], + "left_on_frame": [ + 20, + 49 + ], + "right_on_frame": [ + 2, + 3, + 40, + 41 + ] + }, + "census": { + "parent_rank_histogram": { + "7": 7616, + "8": 37440, + "9": 12544 + }, + "maximal_row_cuts": 967232, + "tagged_matches": [ + 4, + 4, + 4, + 4, + 4, + 4, + 4, + 4, + 4 + ], + "distinct_support_choices": [ + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2 + ], + "enumeration_sha256": "693e54d7a0e81dc9e116079508b3d85b0da7353a30c96e69bf35e04f81016167", + "representatives": [ + [ + { + "parent": [ + 149, + 54 + ], + "cut": "4400220400b200d28001a40050050", + "left": "200db0040dd0044001458021609608", + "right": "ffff0000ffff00000ffff003c03c", + "diagonal": "db00000d0040000058020008008", + "hits": 1120 + }, + { + "parent": [ + 149, + 90 + ], + "cut": "4400220400b200d28001a40050050", + "left": "200db0040dd0044001458021609608", + "right": "3c3c3c3c3c3c3c3c3fc0f0f03c03c0", + "diagonal": "200c30040c10040001408020200200", + "hits": 1120 + } + ], + [ + { + "parent": [ + 239, + 88 + ], + "cut": "5440400140010115044101004012a8", + "left": "2aa8a880a880800222085852154800", + "right": "c3c3c3c3c3c3c3c33fc0f0f03c03c0", + "diagonal": "28080808080800222005050140000", + "hits": 1120 + }, + { + "parent": [ + 239, + 52 + ], + "cut": "5440400140010115044101004012a8", + "left": "2aa8a880a880800222085852154800", + "right": "ff0000ffff0000ff000ffff003c03c", + "diagonal": "2a000080a800000200085850014000", + "hits": 1120 + } + ], + [ + { + "parent": [ + 161, + 108 + ], + "cut": "60000601811118105082820500500", + "left": "118181886606060010428281069068", + "right": "3cc3c33cc33c3cc33fcf0f03c03c00", + "diagonal": "108181084204040010420201001000", + "hits": 1120 + }, + { + "parent": [ + 161, + 88 + ], + "cut": "60000601811118105082820500500", + "left": "118181886606060010428281069068", + "right": "c3c3c3c3c3c3c3c33fc0f0f03c03c0", + "diagonal": "18181804202020010408080040040", + "hits": 1120 + } + ], + [ + { + "parent": [ + 231, + 90 + ], + "cut": "78080088008087014002020096a00", + "left": "e00e0e100e10100102854541500068", + "right": "3c3c3c3c3c3c3c3c3fc0f0f03c03c0", + "diagonal": "200c0c100c10100002804040100040", + "hits": 1120 + }, + { + "parent": [ + 231, + 2 + ], + "cut": "78080088008087014002020096a00", + "left": "e00e0e100e10100102854541500068", + "right": "ffffffff0000000000000003fffffc", + "diagonal": "e00e0e100000000000000001500068", + "hits": 1120 + } + ], + [ + { + "parent": [ + 165, + 0 + ], + "cut": "90000909909090010424240600600", + "left": "44242422424444240a04242206a068", + "right": "ffffffff00000003fffffc", + "diagonal": "424444240000000206a068", + "hits": 1120 + }, + { + "parent": [ + 165, + 52 + ], + "cut": "90000909909090010424240600600", + "left": "44242422424444240a04242206a068", + "right": "ff0000ffff0000ff000ffff003c03c", + "diagonal": "440000224200002400042420028028", + "hits": 1120 + } + ], + [ + { + "parent": [ + 207, + 54 + ], + "cut": "40012aa88002400111045200408804", + "left": "a88054400115a880044108a11522a0", + "right": "ffff0000ffff00000ffff003c03c", + "diagonal": "8054000015a800000108a0010020", + "hits": 1120 + }, + { + "parent": [ + 207, + 108 + ], + "cut": "40012aa88002400111045200408804", + "left": "a88054400115a880044108a11522a0", + "right": "3cc3c33cc33c3cc33fcf0f03c03c00", + "diagonal": "288040000114288004410801002000", + "hits": 1120 + } + ], + [ + { + "parent": [ + 7, + 54 + ], + "cut": "1781000081e8000000000aa0006a90", + "left": "e87e00007e17000000000550009560", + "right": "ffff0000ffff00000ffff003c03c", + "diagonal": "7e00000017000000000550008020", + "hits": 1120 + }, + { + "parent": [ + 7, + 2 + ], + "cut": "1781000081e8000000000aa0006a90", + "left": "e87e00007e17000000000550009560", + "right": "ffffffff0000000000000003fffffc", + "diagonal": "e87e00000000000000000000009560", + "hits": 1120 + } + ], + [ + { + "parent": [ + 13, + 88 + ], + "cut": "4020d04020b040201402010082918", + "left": "b0d020b0d040b0d02801020041624", + "right": "c3c3c3c3c3c3c3c33fc0f0f03c03c0", + "diagonal": "30102030100030102801020040200", + "hits": 1120 + }, + { + "parent": [ + 13, + 2 + ], + "cut": "4020d04020b040201402010082918", + "left": "b0d020b0d040b0d02801020041624", + "right": "ffffffff0000000000000003fffffc", + "diagonal": "b0d020b0000000000000000041624", + "hits": 1120 + } + ], + [ + { + "parent": [ + 41, + 88 + ], + "cut": "88c40080223100214008042858200", + "left": "c4408cc431102331280040814a4100", + "right": "c3c3c3c3c3c3c3c33fc0f0f03c03c0", + "diagonal": "c04080c00100030128004080080100", + "hits": 1120 + }, + { + "parent": [ + 41, + 2 + ], + "cut": "88c40080223100214008042858200", + "left": "c4408cc431102331280040814a4100", + "right": "ffffffff0000000000000003fffffc", + "diagonal": "c4408cc400000000000000014a4100", + "hits": 1120 + } + ] + ] + }, + "quotient": { + "totals": { + "families": 4096, + "diagonal_rejected": 4093, + "rank2_rejected": 3 + }, + "per_coordinate": { + "0": { + "families": 512, + "diagonal_rejected": 509, + "rank2_rejected": 3 + }, + "1": { + "families": 512, + "diagonal_rejected": 512 + }, + "26": { + "families": 512, + "diagonal_rejected": 512 + }, + "27": { + "families": 512, + "diagonal_rejected": 512 + }, + "44": { + "families": 512, + "diagonal_rejected": 512 + }, + "45": { + "families": 512, + "diagonal_rejected": 512 + }, + "54": { + "families": 512, + "diagonal_rejected": 512 + }, + "55": { + "families": 512, + "diagonal_rejected": 512 + } + }, + "diagonal_survivors": [ + { + "coordinate_root": 0, + "choices": [ + 1, + 1, + 0, + 0, + 1, + 1, + 0, + 0, + 0 + ], + "terms": [ + [ + 149, + 90, + "4400220400b200d28001a40050050" + ], + [ + 239, + 52, + "5440400140010115044101004012a8" + ], + [ + 161, + 108, + "60000601811118105082820500500" + ], + [ + 231, + 90, + "78080088008087014002020096a00" + ], + [ + 165, + 52, + "90000909909090010424240600600" + ], + [ + 207, + 108, + "40012aa88002400111045200408804" + ], + [ + 7, + 54, + "1781000081e8000000000aa0006a90" + ], + [ + 13, + 88, + "4020d04020b040201402010082918" + ], + [ + 41, + 88, + "88c40080223100214008042858200" + ] + ], + "rank_cut": { + "roots": [ + 2, + 22 + ], + "active_terms": [ + 9 + ] + } + }, + { + "coordinate_root": 0, + "choices": [ + 1, + 1, + 0, + 0, + 1, + 1, + 0, + 1, + 0 + ], + "terms": [ + [ + 149, + 90, + "4400220400b200d28001a40050050" + ], + [ + 239, + 52, + "5440400140010115044101004012a8" + ], + [ + 161, + 108, + "60000601811118105082820500500" + ], + [ + 231, + 90, + "78080088008087014002020096a00" + ], + [ + 165, + 52, + "90000909909090010424240600600" + ], + [ + 207, + 108, + "40012aa88002400111045200408804" + ], + [ + 7, + 54, + "1781000081e8000000000aa0006a90" + ], + [ + 13, + 2, + "4020d04020b040201402010082918" + ], + [ + 41, + 88, + "88c40080223100214008042858200" + ] + ], + "rank_cut": { + "roots": [ + 4, + 22 + ], + "active_terms": [ + 9 + ] + } + }, + { + "coordinate_root": 0, + "choices": [ + 1, + 1, + 0, + 1, + 1, + 1, + 0, + 0, + 0 + ], + "terms": [ + [ + 149, + 90, + "4400220400b200d28001a40050050" + ], + [ + 239, + 52, + "5440400140010115044101004012a8" + ], + [ + 161, + 108, + "60000601811118105082820500500" + ], + [ + 231, + 2, + "78080088008087014002020096a00" + ], + [ + 165, + 52, + "90000909909090010424240600600" + ], + [ + 207, + 108, + "40012aa88002400111045200408804" + ], + [ + 7, + 54, + "1781000081e8000000000aa0006a90" + ], + [ + 13, + 88, + "4020d04020b040201402010082918" + ], + [ + 41, + 88, + "88c40080223100214008042858200" + ] + ], + "rank_cut": { + "roots": [ + 2, + 23 + ], + "active_terms": [ + 9 + ] + } + } + ] + }, + "original_choices": [ + 1, + 1, + 0, + 1, + 1, + 1, + 0, + 0, + 0 + ], + "controls": [ + "missing_active_term", + "nonempty_trace_claimed_empty", + "duplicate_frame_root", + "uncut_parent_priced_six", + "unsaturated_frame_cannot_use_square_duality", + "support_enlargement_invalidates_certificate", + "nonorthogonal_pair_is_not_an_identity_minor", + "false_rank_cut_incidence", + "enlarged_support_can_erase_rank_cut" + ], + "positive_controls": { + "coordinate_identity_entries": 12544, + "coordinate_trace_checks": 10080, + "rational_square_fixtures": 48, + "ordinary_transpose_complex_fixture": true + }, + "optimistic_budget": { + "baseline_ceiling": [ + "52814190909/31250000000000", + "1690054109089/1000000000000000" + ], + "mixed62_ceiling": [ + "44596655473/25000000000000", + "1783866218921/1000000000000000" + ], + "strict_five_percent_screen": true, + "physical_extra_costs": "Optimistically omitted only for screening; no realization or kappa claim." + }, + "scope": "No masked decoder in the declared nine retained-hit rank-at-most-six star-descendant family plus any one coordinate-star rectangle, over C with ordinary transpose. Other COPY62 supports remain open." +} diff --git a/research/p112-rank6-hall-obstruction/OVERLAP.json b/research/p112-rank6-hall-obstruction/OVERLAP.json new file mode 100644 index 0000000000..e6854e0836 --- /dev/null +++ b/research/p112-rank6-hall-obstruction/OVERLAP.json @@ -0,0 +1,53 @@ +{ + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1929#discussioncomment-18925869", + "coverage": { + "open_prs": {"fetched_at": "2026-10-14T14:27:47.108625+00:00", "records": 584, "complete_pagination": true}, + "discussions": {"fetched_at": "2026-10-14T14:29:09.251198+00:00", "records": 565, "complete_pagination": true}, + "method": "Parent-shared snapshot, targeted offline overlap searches, local READMEs/TASK/ledger, and targeted live GraphQL head queries. No independent full refresh.", + "limitations": "Open PR metadata includes drafts; closed/merged work is searched only through retained local packages and targeted known-head queries. Arbitrary diffs and all historical closed PRs are not exhausted. No matches is not a novelty certificate." + }, + "queries": [ + "complex-rank-shape-decoder", + "block climb; block decoder; rank shape; ten-term", + "rank-six diagonal; rank6; simultaneous frame; star trim", + "saturated frame; frame trace; diagonal products; support Hall", + "saturated; dual frame; COPY62; all-clique" + ], + "nearest_sources": [ + { + "pr": 1347, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1347", + "head": "64fd5f9e91961dedc16118fcc7ad71ee82efe28f", + "live_state": "MERGED", + "credit": "Cinna Davis / 1337isnot1337", + "distinction": "Homogeneous COPY6 frame-demand relaxation, complete maximal-slice capacity census, and a COPY60 witness with missing diagonals. Mixed ranks are explicitly excluded. The new COPY62 witness covers all diagonals and its complete new retained-hit quotient needs proper-clique rank cuts." + }, + { + "pr": 1402, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1402", + "head": "e5917254b781e9f327436ac682baab1c93941aed", + "live_state": "MERGED", + "credit": "Cinna Davis / 1337isnot1337", + "distinction": "Complete representative union for PR1347's original ten patterns. This package uses nine different patterns and a coordinate COPY8 term." + }, + { + "path": "research/p112-rank6-cover-representatives/README.md", + "credit": "woklerx with OpenAI Codex assistance", + "distinction": "Sharp one-choice-per-term diagonal cap99 for the original ten COPY6 patterns; domination and quotient method credited, not claimed anew. Live source bytes pinned in SOURCES.json." + }, + { + "pr": 1633, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1633", + "head": "652264fa1f70820139b2730363a0056b7fadc689", + "live_state": "OPEN", + "distinction": "All-pairs factor excess-rank theorem; not this masked mixed-support family. No source code imported." + }, + { + "pr": 1909, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1909", + "head": "64922f413dc6cb3ae3d843cd53b4aa7d985b55d0", + "distinction": "Previous-round tetrad-local COPY112 theorem. Neither this support alphabet nor its COPY62 counterexample is tetrad-local; no source reused or resubmitted." + } + ] +} diff --git a/research/p112-rank6-hall-obstruction/README.md b/research/p112-rank6-hall-obstruction/README.md new file mode 100644 index 0000000000..52f98eb46d --- /dev/null +++ b/research/p112-rank6-hall-obstruction/README.md @@ -0,0 +1,237 @@ +# A COPY62 P112 cover passes frame and diagonal screens but cannot decode + +**Scoped negative result and exact support certificate. No supplier, new kappa, +or selected-frontier change.** + +The concrete ten-rectangle proposal in [SUPPORT.json](SUPPORT.json) has nine +COPY6 maximal star slices and one retained coordinate COPY8 rectangle. It +meets every one of the 1,260 live orthogonal eight-frames at least eight times +and covers every one of the 112 diagonals. Its frame-hit histogram is +`{8:305, 9:650, 10:305}`. Thus the diagonal failure of PR1347's COPY60 witness +is genuinely repaired at the level of these necessary conditions. + +Nevertheless, the proposal is not a masked decoder. Moreover, **none of the +4,096 representative/coordinate choices in the precisely defined family +below is a masked decoder**, for any complex coefficients under ordinary +transpose, independent transposition of the nine rectangles, arbitrary +further support restrictions, or any additional cost-zero terms. + +## Result and complete bounded family + +Let `H_k`, for `k=0..8`, be the complete eight-frame hit set of rank-six +rectangle `k` in SUPPORT.json. Each contains 1,120 frames; the nine sets are +distinct. A permitted paid term `k`: + +1. starts from **any** of the 7,616 tagged C/N root-star parent pairs of binary + pairing rank seven on the fixed P112 model; +2. restricts both supports arbitrarily to pairing rank at most six; +3. retains every hit in `H_k`, but is allowed additional hits; +4. may transpose its two support factors. + +The tenth term has arbitrary coefficients supported inside the square of +**any one of the eight punctured-frame coordinate stars**. Its full support +has pairing rank eight. The theorem does not prescribe its coefficients to +be those of the coordinate decoder. This is a generous support model, not a +physical helper program. + +The complete maximal-slice census gives four tagged matches for each `H_k`, +which reduce to **two distinct support rectangles** per pattern. No strict +hit-superset appears. Each pair of choices also has different diagonal +support. Transposition does not change the screens used below. + +| Exact quotient | Number | +|---|---:| +| Tagged rank-seven parents | 7,616 | +| Nonzero-codeword maximal row slices traversed | 967,232 | +| Independent representative choices | `2^9 = 512` | +| Coordinate-star choices | 8 | +| Complete representative/coordinate quotient | 4,096 | +| Rejected by an uncovered diagonal | 4,093 | +| Diagonal survivors | 3 | +| Survivors rejected by a two-root rank cut | 3 | + +All three diagonal survivors use coordinate root 0. For that coordinate the +partition is 509 diagonal failures plus three rank-cut failures among 512 +choices. Each of the other seven coordinates has 512 diagonal failures. +[CERTIFICATE.json](CERTIFICATE.json) gives all 18 maximal representatives, +the complete source-census digest, all three explicit survivor words, and a +compact orthogonal-pair separator for each survivor. This is a complete +bounded quotient, **not** an exhaustion of all COPY62 decoders. + +The three certificates are short enough to inspect directly. Bits choose the +ordered representatives in `CERTIFICATE.json`; root and term IDs are zero-based. + +| Representative bits | Orthogonal pair | Only active term on the pair | +|---|---|---| +| `110011000` | `(2,22)` | 9, the coordinate rectangle | +| `110011010` | `(4,22)` | 9, the coordinate rectangle | +| `110111000` (the supplied proposal) | `(2,23)` | 9, the coordinate rectangle | + +In each row, a single rank-one contribution cannot equal `4 I_2`. + +## Why these are coefficient-independent obstructions + +### Proper-clique rank cuts + +For any orthogonal live root set `S`, the constrained masked target is +`(2G)[S,S] = 4 I_|S|`. Each paid outer product has rank at most one on this +submatrix and vanishes unless both support factors meet `S`. Therefore at +least `|S|` paid rectangles must meet `S` on both sides. A cost-zero term +cannot contribute: the binary label pairing is one everywhere on `S x S`, +whereas a zero-cost support rectangle has identically zero pairing. + +For each of the three diagonal-surviving representatives, the certificate +exhibits an orthogonal **pair** met on both sides by fewer than two terms. +No choice of coefficients can give the required rank-two matrix. This is +stronger here than checking full eight-frames and diagonals alone. + +The replay also enumerates **all 262,928 nonempty orthogonal cliques**, with +counts by size +`112, 3304, 31024, 94892, 82656, 39088, 10592, 1260`. +It does not mistake subsets of live eight-frames for this full set: some +proper cliques have no live eight-frame extension. The complete scan is +supplementary; the short two-root certificates already prove rejection. + +### Additional saturated-frame duality certificate + +The supplied proposal also has a separate eight-frame obstruction. On a +frame `F` with exactly eight potentially active rectangles, write their +restricted factors as square matrices `D_F,T_F`. An exact decoder would give +`D_F T_F^t = 4I`. Both matrices are invertible, hence `T_F^t D_F = 4I` as well. +Consequently every active term must satisfy + +`sum(i in F) d_k(i) t_k(i) = 4`. + +The certificate identifies an active term whose allowed left and right +supports are disjoint on such a frame. Its left-hand side is identically +zero. This reasoning uses **ordinary transpose**, not conjugate transpose +or positivity, and is valid over the complex numbers. It does not apply to +an unsaturated frame with nine or ten potentially active terms; a negative +control enforces that boundary. We do not claim priority for square-matrix +duality itself; the contribution is its exact source-bound application. + +### Why the quotient covers arbitrary joint trims + +Write a binary rank-seven parent matrix as `M = A B`, with `A` of column +rank seven and `B` of row rank seven. If a joint restriction `A_L B_R` has +rank at most six, at least one of `A_L,B_R` loses rank: if both retained rank +seven, one has a left inverse and the other a right inverse, forcing their +product to retain rank seven. + +A nonzero functional annihilating the deficient factor supplies a nonzero +parent codeword. Expand that side to the codeword's entire zero set and +restore the other parent support. This dominates the original rectangle. +The row-oriented case is enumerated directly, and the column-oriented case +is a transpose of an enumerated row slice. This is the domination argument +of PR1347 and its representative successors, applied to the new patterns. + +Expansion preserves the required hits and only adds diagonal and clique +hits. The census includes every expanded rectangle retaining `H_k`. +Every expanded nine-tuple, even with the full coordinate rectangle, has an +uncovered diagonal or a deficient orthogonal pair. Shrinking any rectangle +cannot repair either defect. Independent transposition preserves both +screens. This proves the stated family theorem without assuming that actual +nonzero supports equal the maximal caps. + +## Complete optimistic budget, not a construction + +Keep every non-centre rank count of the selected local profile and replace +its eight COPY8 children by nine COPY6 and one COPY8 child: + +- baseline: `{1:2412, 2:418, 3:432, 4:142, 5:82, 8:8}`, centre charge 64; +- proposed relaxation: `{1:2412, 2:418, 3:432, 4:142, 5:82, 6:9, 8:1}`, + centre charge 62; +- both use `m=73`, `families=896`, `stages=9`, and the inherited coverage law. + +The pinned rational-interval ceiling engine gives + +- baseline `a` ceiling in `[0.001690054109088, 0.001690054109089]`; +- COPY62 ceiling in `[0.001783866218920, 0.001783866218921]`. + +The latter lower endpoint is strictly greater than 1.05 times the former +upper endpoint: about **5.55%** ideal headroom. This is why rejecting false +positives at COPY62 matters. New frame transitions, source access, restoration, +hosting and precision costs are **optimistically omitted for this rejection +screen only**. There is no paid physical realization, supplier admission, +scalar-operation saving, or improved multiplication exponent. + +## Reproduce and verification coverage + +From the repository root, standard-library CPython 3.12: + +```sh +uv run --python 3.12 --no-project python -I -B research/p112-rank6-hall-obstruction/verify.py +uv run --python 3.12 --no-project python -I -O -B research/p112-rank6-hall-obstruction/verify.py +uv run --python 3.12 --no-project python scripts/research_package.py --package research/p112-rank6-hall-obstruction +``` + +The verifier compares the complete deterministic certificate. `--write` +regenerates it. It independently checks the ten displayed copy ranks with +least-pivot binary elimination, traverses the complete parent/codeword +quotient, checks all three short separators, and checks the extra duality +separator. A known exact eight-coordinate decoder supplies 12,544 all-pairs +identity checks, all 10,080 saturated-frame term traces, and a positive +all-clique screen. Small rational duals and a genuinely complex ordinary- +transpose fixture supplement nine semantic negative controls. + +Actual command outputs and environment are in [VALIDATION.json](VALIDATION.json). +No full selected-frontier cold replay, native compiler run, hosted CI result, +Lean proof or independent human proof review is claimed. + +## Search history, limits and overlap + +The independently drawn seed is `5130d276c01dfff62d214a1fd73e9011`, track +`complex-mechanisms`, emitted card `complex-rank-shape-decoder`. +[SELECTION.json](SELECTION.json) preserves the full chooser output. The exact +base is `0b1cccf86e2f5132ed286a26ef0a681a495740ea`. + +The original COPY60 search retained the full maximum-hit representative +catalogue rather than PR1347's single diagonal representative. A 180-second +MILP run and a 300-second native-cardinality attempt produced no witness; +neither is an exclusion proof. The one declared pivot introduced a retained +coordinate COPY8 term. The resulting COPY62 support witness passes the +predecessor screens but fails exact necessary rank conditions. An additional +600-second lazy proper-subframe search stopped after three incumbents; no +UNSAT or global negative claim follows. We therefore prove only the complete +source-bound representative family above, not the broader searched class. + +`search.py` and `search_sat.py` retain optional proposal mechanisms; acceptance +requires neither SciPy nor PySAT. Their optional solver outcomes are never +proof inputs. Current `--all-cliques` separation enumerates the full clique +set, not merely subsets of eight-frames. Different solver runs may find +other supports or time out. The fixed certificate, not rerunning a heuristic, +is the reproducible result. + +This changes PR1347's homogeneous COPY6 alphabet and its ten fixed patterns; +it is not the earlier COPY60/99-diagonal result with a larger seed. It is also +distinct from prior-round PR1909's tetrad-local COPY112 theorem. The rank-eight +all-pairs and rank-eight masked-rigidity results do not cover these ten paid +terms. [OVERLAP.json](OVERLAP.json) records exact heads and coverage limitations. + +## Open next questions + +Can a different mixed COPY62 support choice survive all proper-clique cuts +and saturated-frame duality? The first step is to add these cheap exact +separators to support synthesis before solving for complex coefficients. +This matters because its optimistic profile clears the five-percent screen. +The fixed nine retained-hit patterns must change to escape this theorem. +Even a surviving support proposal still needs exact coefficients and a fully +charged physical construction; neither follows from a feasible support +relaxation. + +## Credit and license + +Cinna Davis (@1337isnot1337), PR1347 and PR1323, supplies the rank-six support +model, census and frame-cover question; PR1402 supplies the representative +warning and union obstruction. The retained `p112-rank6-cover-representatives` +package by @woklerx with Codex supplies the sharp one-choice-per-term cap 99 +and the joint-trim domination argument. We reuse their pinned geometry, not +claim independent priority for those facts. Navinor/PR1226, David Arias/PR1236, +Hanson Sun/PR1242, DreamingOfClouds/PR717 and themilkman216/PR968 retain the +underlying star, label, frame and decoder credits. Douglas Colkitt's PR1240 +supplies the exact optimistic ceiling engine; the selected supplier and its +full credited lineage remain unchanged. + +New work by **Adam Gall**, with substantial **OpenAI Codex GPT-6 Astra** +assistance in reasoning, experiments, implementation and documentation. +Apache-2.0. All predecessor files and their notices are unchanged. diff --git a/research/p112-rank6-hall-obstruction/SEARCH-HISTORY.json b/research/p112-rank6-hall-obstruction/SEARCH-HISTORY.json new file mode 100644 index 0000000000..206d8d0425 --- /dev/null +++ b/research/p112-rank6-hall-obstruction/SEARCH-HISTORY.json @@ -0,0 +1,33 @@ +{ + "scope": "Proposal history only. No solver infeasibility result is used in the theorem.", + "census": {"tagged_rank7_parents": 7616, "maximal_row_slices": 967232, "distinct_maximum_hit_and_diagonal_representatives": 10752}, + "attempts": [ + { + "hypothesis": "Ten COPY6 maximum-hit rectangles, all full-frame demands and all diagonals; first canonical representative forced.", + "command": "uv run --python 3.12 --no-project --with scipy==1.17.0 python research/p112-rank6-hall-obstruction/search.py --seconds 180 --force-first --output /tmp/imb-round2-06-search1120.json", + "environment": {"numpy": "2.5.4", "scipy": "1.17.0"}, + "solver_elapsed_seconds": 180.1860056250007, + "result": "Time limit reached. HiGHS model_status Time limit reached; primal_status None. No feasible incumbent and no infeasibility conclusion." + }, + { + "hypothesis": "Same homogeneous maximum-hit support family using native cardinality constraints.", + "command": "uv run --python 3.12 --no-project --with python-sat==1.8.dev24 python research/p112-rank6-hall-obstruction/search_sat.py --output /tmp/imb-round2-06-sat1120.json", + "external_timeout_seconds": 300, + "result": "Timed out after printing the full10752-candidate census. No SAT/UNSAT result." + }, + { + "hypothesis": "Declared mixed COPY62 pivot: nine maximum-hit COPY6 rectangles plus punctured coordinate root0, all full-frame and diagonal conditions.", + "command": "uv run --python 3.12 --no-project --with python-sat==1.8.dev24 python research/p112-rank6-hall-obstruction/search_sat.py --coordinate --output /tmp/imb-round2-06-sat62.json", + "solver_elapsed_seconds": 48.897238708999794, + "result": "SAT proposal retained verbatim in SUPPORT.json. Exact acceptance is independent of the native solver and uses only standard-library replay." + }, + { + "hypothesis": "Broader mixed COPY62 search with lazy proper-subframe rank constraints.", + "command_at_time": "uv run --python 3.12 --no-project --with python-sat==1.8.dev24 python research/p112-rank6-hall-obstruction/search_sat.py --coordinate --all-cliques --output /tmp/imb-round2-06-sat62cliques.json", + "external_timeout_seconds": 600, + "incumbent_subframe_failure_counts": [169, 131, 239], + "result": "Timed out after three incumbents. At that experiment the generator enumerated subsets of live eight-frames; current search_sat.py enumerates all262928 orthogonal cliques. No completed broad search or infeasibility theorem is claimed." + } + ], + "delivered_result": "Exact finite retained-hit quotient for the new nine patterns and all eight coordinate choices:4096 cases,4093 diagonal failures,3 explicit rank-two failures. General joint-support and transpose coverage follows the README domination proof, not solver status." +} diff --git a/research/p112-rank6-hall-obstruction/SELECTION.json b/research/p112-rank6-hall-obstruction/SELECTION.json new file mode 100644 index 0000000000..b0a8abf805 --- /dev/null +++ b/research/p112-rank6-hall-obstruction/SELECTION.json @@ -0,0 +1,71 @@ +{ + "seed": "5130d276c01dfff62d214a1fd73e9011", + "track": "complex-mechanisms", + "suggestions": [ + { + "task_id": "complex-rank-shape-decoder", + "scope_key": "02b31ebd160542c86299", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "method": "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "starting_points": [ + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md" + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound.", + "first_step": { + "command": ["python3", "-B", "research/complex-local-word-ceiling/verify.py"], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope." + ], + "overlap_terms": ["rank shape", "block climb", "masked decoder", "overcomplete", "effective rank"], + "scope_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance." + }, + { + "task_id": "complex-new-helper-inventory", + "scope_key": "f3b0895a4f9f1cc62e75", + "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?", + "method": "Design a small completed instance and independently verify its endpoint and rank bill.", + "starting_points": ["research/complex-local-word-ceiling/README.md", "research/heterogeneous-owner-assembly/README.md", "certificates/selected-result.json"], + "acceptance_gate": "A new physically realizable contract outside the frozen catalogue whose per-call profile, screened with ceiling.ceiling(), beats the selected word's packing ceiling; a lower cap does not establish identical circuitry or order attainable optima, and is insufficient to pass the stronger-budget target under this model.", + "first_step": { + "command": ["python3", "-B", "research/complex-local-word-ceiling/verify.py"], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin.", + "bottleneck_link": "Packing of the selected word is capped at +0.87% (ceiling model); only a lower local excess spend or a changed coverage law raises the cap.", + "allowed_variations": ["Narrow to one changed boundary or helper type with explicit counts.", "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope."], + "scope_change_triggers": ["Mixing only providers already inside the pinned catalogue."], + "overlap_terms": ["helper inventory", "heterogeneous-owner", "mutable leaver"], + "scope_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance." + } + ], + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "catalog_assessed_on": "2026-10-13", + "priority_revision": 3, + "priority_log": "docs/research/research-priority-log.md", + "catalog_sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "selected": { + "kappa": "836330098538459/500000000000000000", + "review": "docs/research/community-batch1099-review.md", + "source_manifest": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "reproduce": "make frontier1094-verify" + }, + "status": "SUGGESTIONS_ONLY_NOT_RESERVED", + "next_step": "Check live overlap, refine one question's object and domain, and record a bounded task card. A different seed or scope key is not evidence of novelty." +} diff --git a/research/p112-rank6-hall-obstruction/SOURCES.json b/research/p112-rank6-hall-obstruction/SOURCES.json new file mode 100644 index 0000000000..5e5eeb15c1 --- /dev/null +++ b/research/p112-rank6-hall-obstruction/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "research/complex-local-word-ceiling/ceiling.py", + "usage": "input", + "git_blob": "6c0f54527d879396f689523bfde19928a9b6157c", + "sha256": "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc" + }, + { + "path": "research/p112-rank6-cover-representatives/README.md", + "usage": "input", + "git_blob": "8d9ce1efd8539238e722fb1a8a338c49e43fc7be", + "sha256": "bcd8f858f6e65589960dc867939a1f2328d08a0d068214762819190012ce7a4a" + }, + { + "path": "research/p112-rank6-frame-coverage/COVERING.json", + "usage": "input", + "git_blob": "b762571ef996a80ed8a16d392fc56782091ac58f", + "sha256": "27d567a56500f857962ddc69a9baed691a945e5a2979a26632e84c23133f1c95" + }, + { + "path": "research/p112-rank6-frame-coverage/README.md", + "usage": "input", + "git_blob": "2c4118013e9da8e98c5f9194b4e694b53773f01f", + "sha256": "481b9e21f33b0ac611c16862f43e5f063818189c02a816ed5aa0de5e5f113d8f" + }, + { + "path": "research/p112-rank6-frame-coverage/engine.py", + "usage": "input", + "git_blob": "6afabd3777975310683e4cdc8a4e4b95f0a330ac", + "sha256": "b59101564855a89de04f39fd28b0a853aa3c46ce0ce99951d93d7dd018543536" + } + ] +} diff --git a/research/p112-rank6-hall-obstruction/SUPPORT.json b/research/p112-rank6-hall-obstruction/SUPPORT.json new file mode 100644 index 0000000000..16f7efbbca --- /dev/null +++ b/research/p112-rank6-hall-obstruction/SUPPORT.json @@ -0,0 +1,60 @@ +{ + "census": { + "parents": 7616, + "slices": 967232, + "candidates": 10752 + }, + "forced_first": false, + "min_hits": 1120, + "coordinate_root": 0, + "elapsed_seconds": 48.897238708999794, + "satisfiable": true, + "solver": "PySAT Minicard; no UNSAT certificate claimed", + "terms": [ + [ + 149, + 90, + "4400220400b200d28001a40050050" + ], + [ + 239, + 52, + "5440400140010115044101004012a8" + ], + [ + 161, + 108, + "60000601811118105082820500500" + ], + [ + 231, + 2, + "78080088008087014002020096a00" + ], + [ + 165, + 52, + "90000909909090010424240600600" + ], + [ + 207, + 108, + "40012aa88002400111045200408804" + ], + [ + 7, + 54, + "1781000081e8000000000aa0006a90" + ], + [ + 13, + 88, + "4020d04020b040201402010082918" + ], + [ + 41, + 88, + "88c40080223100214008042858200" + ] + ] +} diff --git a/research/p112-rank6-hall-obstruction/TASK.json b/research/p112-rank6-hall-obstruction/TASK.json new file mode 100644 index 0000000000..ccd735b7e8 --- /dev/null +++ b/research/p112-rank6-hall-obstruction/TASK.json @@ -0,0 +1,83 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "Complete source-bound COPY62 family: each of nine new 1120-hit patterns from SUPPORT.json may use any joint rank-at-most-six descendant of any rank-seven C/N parent retaining those hits, independently transposed, plus one arbitrary rectangle inside any of the eight coordinate-star squares. Full maximal-slice census reduces to 4096 representative/coordinate cases; 4093 fail diagonal coverage and the remaining three fail a rank-two orthogonal-pair cut.", + "scope_change_reason": "PR1347 excludes mixed copy ranks. Bounded COPY60 searches produced no witness, not an exclusion. The single declared COPY62 pivot produced a new support witness passing all predecessor full-frame and diagonal screens. A broader proper-subframe search did not finish; the delivered negative theorem is explicitly the complete retained-hit quotient of this source-bound witness, not a global COPY62 floor.", + "bottleneck_link": "The COPY62 optimistic profile exceeds the selected-word packing cap by 5.55%, so source-bound coefficient obstructions at this budget close a consequential false-positive path before physical synthesis.", + "budget_minutes": 120, + "stop_rule": "Retain the original search failure as such. Screen mixed COPY62 before searching. Accept only exact support witnesses and explicit rational infeasibility certificates, never floating/native solver UNSAT status alone. State the finite candidate family exactly, without promoting it to an unrestricted decoder lower bound.", + "outcome": "negative-result", + "evidence": "SUPPORT.json; CERTIFICATE.json with full 967232-slice census, all 18 representatives, all three explicit diagonal survivors and rank-two separators; README proof of joint-trim and transpose completeness; additional saturated-frame duality certificate.", + "author": "Adam Gall", + "ai_assistance": "Substantial OpenAI Codex GPT-6 Astra assistance in research, mathematical reasoning, implementation and writing.", + "selection_seed": "5130d276c01dfff62d214a1fd73e9011", + "track": "complex-mechanisms", + "scope_key": "02b31ebd160542c86299", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1929#discussioncomment-18925869", + "predecessors": { + "PR1347": "64fd5f9e91961dedc16118fcc7ad71ee82efe28f", + "PR1402": "e5917254b781e9f327436ac682baab1c93941aed" + }, + "optimistic_budget": { + "baseline_local_profile": {"1": 2412, "2": 418, "3": 432, "4": 142, "5": 82, "8": 8}, + "candidate_local_profile": {"1": 2412, "2": 418, "3": 432, "4": 142, "5": 82, "6": 9, "8": 1}, + "candidate_centre_charge": 62, + "m": 73, + "families": 896, + "stages": 9, + "additional_cost": "Optimistically zero for a rejection screen only. Physical copies, frames, restoration, hosting and precision remain unpaid obligations." + }, + "open_questions": [ + { + "question": "Can different mixed COPY62 supports survive every proper-clique rank cut and saturated-frame duality?", + "why_it_matters": "The fully optimistic mixed profile clears the five-percent selected-word ceiling screen.", + "first_step": "Change the retained hit patterns and add exact clique and saturated-duality separators to support synthesis before solving for coefficients.", + "blocked_by": "The current nine-pattern family is excluded; surviving supports would still need exact coefficients and a fully charged physical realization." + } + ] +} diff --git a/research/p112-rank6-hall-obstruction/VALIDATION.json b/research/p112-rank6-hall-obstruction/VALIDATION.json new file mode 100644 index 0000000000..22981b59bf --- /dev/null +++ b/research/p112-rank6-hall-obstruction/VALIDATION.json @@ -0,0 +1,63 @@ +{ + "environment": { + "python": "CPython3.12.12", + "interpreter_command": "uv run --python 3.12 --no-project python --version", + "observed_version_output": "Python 3.12.12", + "host": "darwin27.0.0 arm64", + "verification_dependencies": "Python standard library only" + }, + "final_phase": { + "combined_wall_seconds": 12.30, + "commands": [ + { + "command": "uv run --python 3.12 --no-project python -I -B research/p112-rank6-hall-obstruction/verify.py --write", + "exit_status": 0, + "output": "PASS_P112_MIXED62_QUOTIENT parents=7616 slices=967232 families=4096 diagonal_survivors=3 rank2_rejections=3 controls=9", + "scope": "Generate exact certificate while executing the complete mathematical replay and semantic controls." + }, + { + "command": "uv run --python 3.12 --no-project python -I -O -B research/p112-rank6-hall-obstruction/verify.py", + "exit_status": 0, + "output": "PASS_P112_MIXED62_QUOTIENT parents=7616 slices=967232 families=4096 diagonal_survivors=3 rank2_rejections=3 controls=9", + "scope": "Optimized-interpreter replay compares the complete stored certificate; checks do not rely on assertions." + }, + { + "command": "uv run --python 3.12 --no-project python scripts/research_package.py --package research/p112-rank6-hall-obstruction", + "exit_status": 0, + "output": [ + "CHECK Complete 967232-slice representative quotient, all 4096 mixed choices, three exact rank-two separators, saturated duality, coordinate-decoder positive fixture and nine semantic negative controls.", + "PASS_P112_MIXED62_QUOTIENT parents=7616 slices=967232 families=4096 diagonal_survivors=3 rank2_rejections=3 controls=9", + "PASS_REGISTERED_RESEARCH_PACKAGE research/p112-rank6-hall-obstruction outcome=negative-result" + ], + "scope": "Registered Python3.12 replay, task metadata and exact source/provenance pins." + } + ] + }, + "positive_evidence": { + "coordinate_decoder_all_pair_entries": 12544, + "coordinate_decoder_saturated_term_traces": 10080, + "nonsingular_rational_two_by_two_dual_fixtures": 48, + "complex_ordinary_transpose_fixture": true, + "complete_orthogonal_cliques": 262928, + "source_proposal_failed_proper_cliques": 375 + }, + "negative_controls": [ + "missing_active_term", + "nonempty_trace_claimed_empty", + "duplicate_frame_root", + "uncut_parent_priced_six", + "unsaturated_frame_cannot_use_square_duality", + "support_enlargement_invalidates_certificate", + "nonorthogonal_pair_is_not_an_identity_minor", + "false_rank_cut_incidence", + "enlarged_support_can_erase_rank_cut" + ], + "unrun": [ + "Full selected-frontier cold replay", + "Native compiler or hosted supplier admission", + "Hosted CI", + "Lean or other proof-assistant verification", + "Independent human proof review" + ], + "post_verification_changes": "Documentation only: added the three explicit separator rows and removed an internal coordination sentence. Executable sources, certificate and replay manifest are unchanged." +} diff --git a/research/p112-rank6-hall-obstruction/VERIFY.json b/research/p112-rank6-hall-obstruction/VERIFY.json new file mode 100644 index 0000000000..0627e1d5ad --- /dev/null +++ b/research/p112-rank6-hall-obstruction/VERIFY.json @@ -0,0 +1,25 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/complex-local-word-ceiling/ceiling.py", + "research/p112-rank6-cover-representatives/README.md", + "research/p112-rank6-frame-coverage/COVERING.json", + "research/p112-rank6-frame-coverage/README.md", + "research/p112-rank6-frame-coverage/engine.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Complete 967232-slice representative quotient, all 4096 mixed choices, three exact rank-two separators, saturated duality, coordinate-decoder positive fixture and nine semantic negative controls." + } + ] +} diff --git a/research/p112-rank6-hall-obstruction/family.py b/research/p112-rank6-hall-obstruction/family.py new file mode 100644 index 0000000000..3acdf21a2c --- /dev/null +++ b/research/p112-rank6-hall-obstruction/family.py @@ -0,0 +1,131 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Complete retained-hit quotient for the nine new COPY6 patterns. + +The full parent/codeword traversal follows the credited PR1347 and +p112-rank6-cover-representatives patterns. New work is the mixed COPY62 +family, all eight coordinate choices, and exact proper-clique separators. +""" +from collections import Counter +import hashlib +import itertools +import screen + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def representatives(data, pairing, supports, frames, original): + incidence = [0] * 120 + for j, frame in enumerate(frames): + for root in frame: + incidence[root] |= 1 << j + cache = {} + + def hits(mask): + if mask not in cache: + value = 0 + for root in screen.engine.bits(mask): + value |= incidence[root] + cache[mask] = value + return cache[mask] + + patterns = [hits(left) & hits(right) for left, right in original[:9]] + require(len(set(patterns)) == 9 and all(p.bit_count() == 1120 for p in patterns), + "nine distinct new maximum-hit patterns") + tagged_counts = [0] * 9 + found = [{} for _ in patterns] + parent_counts = Counter() + cases = 0 + digest = hashlib.sha256() + for a, left in enumerate(supports): + for b, right in enumerate(supports): + rank = screen.engine.rank(pairing, left, right) + parent_counts[rank] += 1 + if rank != 7: + continue + words = screen.engine.column_code(pairing, left, right) + require(len(words) == 127 and len(set(words)) == 127, "complete nonzero rank-seven code") + right_hits = hits(right) + for cut in words: + cases += 1 + digest.update(f"{a},{b},{cut:x}\n".encode()) + row = left ^ cut + met = hits(row) & right_hits + for k, target in enumerate(patterns): + if target & ~met: + continue + tagged_counts[k] += 1 + require(screen.engine.rank(pairing, row, right) == 6, "representative rank") + found[k].setdefault((row, right), dict(parent=[a, b], cut=format(cut, "x"), + left=format(row, "x"), right=format(right, "x"), + diagonal=format(row & right, "x"), + hits=met.bit_count())) + require(dict(parent_counts) == {7: 7616, 8: 37440, 9: 12544}, "complete parent-rank census") + require(cases == 967232, "complete maximal row-cut census") + choices = [[table[key] for key in sorted(table)] for table in found] + require(tagged_counts == [4] * 9 and [len(c) for c in choices] == [2] * 9, + "complete representative quotient changed") + require(all(record["hits"] == 1120 for group in choices for record in group), + "a strict hit-superset appeared") + require(all(len({record["diagonal"] for record in group}) == 2 for group in choices), + "two genuinely different diagonal choices per pattern") + require(all(hits(supports[2*c]) == (1 << len(frames)) - 1 for c in data["punctured_frame"]), + "each coordinate star meets every live frame") + census = dict(parent_rank_histogram=dict(sorted(parent_counts.items())), maximal_row_cuts=cases, + tagged_matches=tagged_counts, distinct_support_choices=[len(c) for c in choices], + enumeration_sha256=digest.hexdigest(), representatives=choices) + return choices, census + + +def check_rank_cut(data, terms, cut): + roots = cut["roots"] + require(len(roots) == 2 and len(set(roots)) == 2 and set(roots) <= set(data["live"]), "rank-cut roots") + a, b = roots + require(sum(x*y for x, y in zip(data["lines"][a], data["lines"][b])) == 0, + "rank-cut roots must be orthogonal") + mask = (1 << a) | (1 << b) + active = [j for j, (left, right) in enumerate(terms) if left & mask and right & mask] + require(active == cut["active_terms"], "rank-cut incidence") + require(len(active) < 2, "rank-two target is not excluded") + return True + + +def quotient(data, ip, supports, choices): + live_mask = sum(1 << i for i in data["live"]) + pairs = [(a, b) for a, b in itertools.combinations(data["live"], 2) if ip[a][b] == 0] + per_coordinate = {c: Counter() for c in data["punctured_frame"]} + survivors = [] + for indices in itertools.product(range(2), repeat=9): + selected = [choices[k][choice] for k, choice in enumerate(indices)] + terms = [(int(record["left"], 16), int(record["right"], 16)) for record in selected] + union = 0 + for left, right in terms: + union |= left & right + for coordinate in data["punctured_frame"]: + star = supports[2 * coordinate] + totals = per_coordinate[coordinate] + totals["families"] += 1 + if union | star != live_mask: + totals["diagonal_rejected"] += 1 + continue + completed = terms + [(star, star)] + cut = None + for a, b in pairs: + mask = (1 << a) | (1 << b) + active = [j for j, (left, right) in enumerate(completed) if left & mask and right & mask] + if len(active) < 2: + cut = dict(roots=[a, b], active_terms=active) + break + require(cut is not None, "a diagonal survivor needs a new coefficient investigation") + check_rank_cut(data, completed, cut) + totals["rank2_rejected"] += 1 + survivors.append(dict(coordinate_root=coordinate, choices=list(indices), + terms=[[record["parent"][0], record["parent"][1], record["cut"]] + for record in selected], rank_cut=cut)) + totals = sum(per_coordinate.values(), Counter()) + require(totals == {"families": 4096, "diagonal_rejected": 4093, "rank2_rejected": 3}, + "complete quotient result changed") + return dict(totals=dict(totals), per_coordinate={str(c): dict(v) for c, v in per_coordinate.items()}, + diagonal_survivors=survivors) diff --git a/research/p112-rank6-hall-obstruction/screen.py b/research/p112-rank6-hall-obstruction/screen.py new file mode 100644 index 0000000000..b4f449107d --- /dev/null +++ b/research/p112-rank6-hall-obstruction/screen.py @@ -0,0 +1,69 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Exact necessary coefficient equations on saturated orthogonal frames.""" +from collections import Counter +import importlib.util +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +SPEC = importlib.util.spec_from_file_location( + "credited_rank6_geometry", ROOT / "research/p112-rank6-frame-coverage/engine.py") +engine = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(engine) + + +def frame_screen(data, frames, terms): + """Terms are support upper bounds, not claimed nonzero coefficients.""" + masks = [sum(1 << root for root in frame) for frame in frames] + diagonal = {i: sum(bool(left & right & (1 << i)) for left, right in terms) + for i in data["live"]} + counts, trace_empty, saturated = [], [], [] + for index, mask in enumerate(masks): + active = [k for k, (left, right) in enumerate(terms) if left & mask and right & mask] + counts.append(len(active)) + if len(active) == 8: + saturated.append((index, active)) + for k in active: + if not terms[k][0] & terms[k][1] & mask: + trace_empty.append([index, k]) + return dict(frame_hit_histogram=dict(sorted(Counter(counts).items())), + minimum_frame_hits=min(counts), + diagonal_hit_histogram=dict(sorted(Counter(diagonal.values()).items())), + uncovered_diagonals=[i for i, value in diagonal.items() if not value], + saturated_frames=len(saturated), empty_trace_constraints=trace_empty), saturated + + +def clique_masks(data): + """Every nonempty orthogonal clique, including ones with no live 8-frame.""" + roots = data["lines"] + adjacency = [sum(1 << j for j in data["live"] + if i != j and sum(x*y for x, y in zip(roots[i], roots[j])) == 0) + for i in range(len(roots))] + cliques = [] + + def visit(chosen, possible): + while possible: + bit = possible & -possible + possible ^= bit + i = bit.bit_length() - 1 + cliques.append(chosen | bit) + visit(chosen | bit, possible & adjacency[i]) + + visit(0, sum(1 << i for i in data["live"])) + return sorted(cliques, key=lambda value: (value.bit_count(), value)) + + +def all_clique_screen(data, terms): + """Every principal orthogonal-clique rank count, not just eight-frames.""" + counts, failures = Counter(), [] + for mask in clique_masks(data): + size = mask.bit_count() + counts[size] += 1 + active = sum(bool(left & mask and right & mask) for left, right in terms) + if active < size: + failures.append([list(engine.bits(mask)), active]) + return dict(cliques_by_size=dict(sorted(counts.items())), + failed_cliques=len(failures), first_failure=failures[0] if failures else None) + + + + diff --git a/research/p112-rank6-hall-obstruction/search.py b/research/p112-rank6-hall-obstruction/search.py new file mode 100755 index 0000000000..503ff78aa4 --- /dev/null +++ b/research/p112-rank6-hall-obstruction/search.py @@ -0,0 +1,104 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Optional floating MILP proposal search; not an exclusion certificate.""" +import argparse +import importlib.util +import json +from pathlib import Path +import time + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SPEC = importlib.util.spec_from_file_location( + "rank6_predecessor", ROOT / "research/p112-rank6-frame-coverage/engine.py") +engine = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(engine) + + +def candidates(min_hits=1120): + data = engine.model() + _, pairing, supports, frames = engine.geometry(data) + frame_masks = [sum(1 << i for i in frame) for frame in frames] + hit_cache = {} + + def hits(support): + if support not in hit_cache: + hit_cache[support] = sum(1 << i for i, f in enumerate(frame_masks) if f & support) + return hit_cache[support] + + dictionary = {} + parents = slices = 0 + for a, left in enumerate(supports): + for b, right in enumerate(supports): + if engine.rank(pairing, left, right) != 7: + continue + parents += 1 + right_hits = hits(right) + for cut in engine.column_code(pairing, left, right): + slices += 1 + row = left ^ cut + met = hits(row) & right_hits + if met.bit_count() >= min_hits: + key = (met, row & right) + dictionary.setdefault(key, (a, b, cut, row, right)) + records = [(met, diag, *dictionary[(met, diag)]) for met, diag in sorted(dictionary)] + return data, frames, records, dict(parents=parents, slices=slices, candidates=len(records)) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--min-hits", type=int, default=1120) + parser.add_argument("--seconds", type=int, default=180) + parser.add_argument("--force-first", action="store_true") + parser.add_argument("--output", type=Path, required=True) + args = parser.parse_args() + if args.output.exists(): + raise ValueError("refusing to overwrite an experiment") + import numpy as np + import scipy + from scipy.optimize import Bounds, LinearConstraint, milp + from scipy.sparse import coo_matrix + data, frames, records, census = candidates(args.min_hits) + print("SEARCH_CENSUS", census, flush=True) + all_frames = (1 << len(frames)) - 1 + live_index = {root: index for index, root in enumerate(data["live"])} + rr, cc = [], [] + for j, (met, diag, *_) in enumerate(records): + for i in engine.bits(all_frames ^ met): + rr.append(i) + cc.append(j) + rr.append(1260) + cc.append(j) + for root in engine.bits(diag): + rr.append(1261 + live_index[root]) + cc.append(j) + matrix = coo_matrix((np.ones(len(rr)), (rr, cc)), shape=(1373, len(records))).tocsc() + lower, upper = np.zeros(len(records)), np.full(len(records), 10.) + if args.force_first: + lower[0] = 1 + low, high = np.full(1373, -np.inf), np.full(1373, 2.) + low[1260] = high[1260] = 10 + low[1261:], high[1261:] = 1, np.inf + start = time.monotonic() + result = milp(np.zeros(len(records)), integrality=np.ones(len(records)), + bounds=Bounds(lower, upper), constraints=LinearConstraint(matrix, low, high), + options={"time_limit": args.seconds, "mip_rel_gap": 0.}) + receipt = dict(census=census, min_hits=args.min_hits, forced_first=args.force_first, + seconds_limit=args.seconds, elapsed_seconds=time.monotonic()-start, + numpy=np.__version__, scipy=scipy.__version__, status=int(result.status), + message=result.message, feasible=False, + scope="Necessary frame-count and diagonal-cover constraints only; floating solver is not proof.") + if result.x is not None: + chosen = [j for j, value in enumerate(result.x) for _ in range(round(float(value)))] + terms = [records[j] for j in chosen] + counts = [sum(bool(term[0] >> i & 1) for term in terms) for i in range(1260)] + diagonal = [sum(bool(term[1] >> root & 1) for term in terms) for root in data["live"]] + receipt.update(terms=[[a, b, format(cut, "x")] for _, _, a, b, cut, _, _ in terms], + minimum_frame_hits=min(counts), minimum_diagonal_hits=min(diagonal), + feasible=len(terms)==10 and min(counts)>=8 and min(diagonal)>=1) + args.output.write_text(json.dumps(receipt, indent=2)+"\n") + print("SEARCH_RESULT", receipt["feasible"], receipt["status"], receipt["message"]) + + +if __name__ == "__main__": + main() diff --git a/research/p112-rank6-hall-obstruction/search_sat.py b/research/p112-rank6-hall-obstruction/search_sat.py new file mode 100755 index 0000000000..75b3a223c7 --- /dev/null +++ b/research/p112-rank6-hall-obstruction/search_sat.py @@ -0,0 +1,82 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Optional native-cardinality proposal search; acceptance uses exact replay.""" +import argparse +import json +from pathlib import Path +import time +import search + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--min-hits", type=int, default=1120) + parser.add_argument("--coordinate", action="store_true") + parser.add_argument("--all-cliques", action="store_true") + parser.add_argument("--output", type=Path, required=True) + args = parser.parse_args() + if args.output.exists(): + raise ValueError("refusing to overwrite an experiment") + from pysat.solvers import Minicard + data, frames, records, census = search.candidates(args.min_hits) + print("SAT_CENSUS", census, flush=True) + size = len(records) + misses = [[] for _ in frames] + diagonals = {i: [] for i in data["live"]} + full = (1 << len(frames)) - 1 + for j, (met, diag, *_) in enumerate(records, 1): + for i in search.engine.bits(full ^ met): + misses[i].append(j) + for i in search.engine.bits(diag): + diagonals[i].append(j) + coordinate_root = data["punctured_frame"][0] + _, _, supports, _ = search.engine.geometry(data) + coordinate_support = supports[2 * coordinate_root] if args.coordinate else 0 + count = 9 if args.coordinate else 10 + from screen import clique_masks + cliques = clique_masks(data) if args.all_cliques else [] + start = time.monotonic() + with Minicard() as solver: + solver.add_atmost(list(range(1, size + 1)), count) + solver.add_atmost(list(range(-size, 0)), size - count) + for row in misses: + solver.add_atmost(row, 2) + for root, row in diagonals.items(): + if not coordinate_support >> root & 1: + solver.add_clause(row) + if not args.coordinate: + solver.add_clause([1]) + rounds = 0 + while True: + result = solver.solve() + if not result: + break + ids = [j-1 for j in solver.get_model() if 0 < j <= size] + terms = [(records[j][5], records[j][6]) for j in ids] + if args.coordinate: + terms.append((coordinate_support, coordinate_support)) + failures = [mask for mask in cliques + if sum(bool(left & mask and right & mask) for left, right in terms) < mask.bit_count()] + print("SAT_CLIQUE_ROUND", rounds, "failures", len(failures), flush=True) + if not failures: + break + for mask in failures: + missed = [j for j, record in enumerate(records, 1) + if not (record[5] & mask and record[6] & mask)] + bound = count - mask.bit_count() + bool(coordinate_support & mask) + solver.add_atmost(missed, bound) + rounds += 1 + receipt = dict(census=census, forced_first=not args.coordinate, min_hits=args.min_hits, + coordinate_root=coordinate_root if args.coordinate else None, + all_cliques=args.all_cliques, separation_rounds=rounds, + elapsed_seconds=time.monotonic()-start, satisfiable=result, + solver="PySAT Minicard; no UNSAT certificate claimed") + if result: + ids = [j-1 for j in solver.get_model() if 0 < j <= size] + receipt["terms"] = [[records[j][2], records[j][3], format(records[j][4], "x")] for j in ids] + args.output.write_text(json.dumps(receipt, indent=2)+"\n") + print("SAT_RESULT", result, receipt.get("terms"), flush=True) + + +if __name__ == "__main__": + main() diff --git a/research/p112-rank6-hall-obstruction/verify.py b/research/p112-rank6-hall-obstruction/verify.py new file mode 100755 index 0000000000..d18043adc6 --- /dev/null +++ b/research/p112-rank6-hall-obstruction/verify.py @@ -0,0 +1,249 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Replay a mixed COPY62 support witness and its exact coefficient obstruction.""" +import argparse +from fractions import Fraction +import hashlib +import importlib.util +import itertools +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(HERE)) +import screen +import family + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def rank_low(rows): + """Second F2 elimination, using least rather than greatest pivots.""" + pivots = {} + for row in rows: + while row: + bit = row & -row + if bit in pivots: + row ^= pivots[bit] + else: + pivots[bit] = row + break + return len(pivots) + + +def decode(data, pairing, supports, witness): + require(witness["coordinate_root"] in data["punctured_frame"], "coordinate must be punctured") + require(len(witness["terms"]) == 9, "nine rank-six rectangles required") + terms, invoices = [], [] + for a, b, encoded in witness["terms"]: + require(type(a) is int and type(b) is int and 0 <= a < 240 and 0 <= b < 240, "parent tag") + left, right = supports[a], supports[b] + cut = int(encoded, 16) + require(screen.engine.rank(pairing, left, right) == 7, "rank-seven parent") + require(cut in screen.engine.column_code(pairing, left, right), "maximal slice codeword") + left ^= cut + ranks = (screen.engine.rank(pairing, left, right), + rank_low(pairing[i] & right for i in screen.engine.bits(left))) + require(ranks == (6, 6), "independent COPY6 ranks") + terms.append((left, right)) + invoices.append(6) + coordinate = supports[2 * witness["coordinate_root"]] + require(screen.engine.rank(pairing, coordinate, coordinate) == 8, "coordinate COPY8") + require(rank_low(pairing[i] & coordinate for i in screen.engine.bits(coordinate)) == 8, + "independent coordinate COPY8") + terms.append((coordinate, coordinate)) + invoices.append(8) + return terms, invoices + + +def check_separator(data, terms, certificate): + """Reject malformed or unsaturated trace certificates, not just bad hashes.""" + frame = certificate["frame"] + require(len(frame) == 8 and len(set(frame)) == 8 and set(frame) <= set(data["live"]), "separator frame") + roots = data["lines"] + require(all(sum(x*y for x, y in zip(roots[i], roots[j])) == 0 + for i, j in itertools.combinations(frame, 2)), "separator orthogonality") + mask = sum(1 << i for i in frame) + active = [k for k, (left, right) in enumerate(terms) if left & mask and right & mask] + require(active == certificate["active_terms"] and len(active) == 8, "separator saturation") + k = certificate["term"] + require(k in active, "separator term is not active") + left, right = terms[k] + require(list(screen.engine.bits(left & mask)) == certificate["left_on_frame"], "separator left support") + require(list(screen.engine.bits(right & mask)) == certificate["right_on_frame"], "separator right support") + require(not left & right & mask, "separator is not an empty diagonal product") + return True + + +def positive_controls(data, ip, pairing, supports, frames): + coordinates = data["punctured_frame"] + live = data["live"] + columns = [[ip[root][c] for c in coordinates] for root in live] + for i, root in enumerate(live): + for j, other in enumerate(live): + require(sum(x*y for x, y in zip(columns[i], columns[j])) == 2 * ip[root][other], + "coordinate exact identity") + terms = [(supports[2*c], supports[2*c]) for c in coordinates] + summary, saturated = screen.frame_screen(data, frames, terms) + require(summary["minimum_frame_hits"] == 8 and not summary["empty_trace_constraints"], + "true coordinate decoder falsely rejected") + for index, active in saturated: + for k in active: + require(sum(ip[root][coordinates[k]] ** 2 for root in frames[index]) == 4, + "positive saturated trace") + clique = screen.all_clique_screen(data, terms) + require(not clique["failed_cliques"], "true decoder fails a principal rank cut") + # Independently exercise square-factor duality over Q, including negative entries. + invertible = 0 + for a, b, c, d in itertools.product((-1, 0, 1), repeat=4): + det = a*d-b*c + if not det: + continue + D = [[Fraction(a), Fraction(b)], [Fraction(c), Fraction(d)]] + T = [[Fraction(d, det), Fraction(-c, det)], [Fraction(-b, det), Fraction(a, det)]] + require(all(sum(D[i][k]*T[j][k] for k in range(2)) == (i == j) + for i in range(2) for j in range(2)), "small exact dual") + require(all(sum(D[i][k]*T[i][k] for i in range(2)) == 1 for k in range(2)), "small term trace") + invertible += 1 + # A genuinely complex ordinary-transpose fixture: i * (-i) = 1, + # whereas a mistaken Hermitian product gives -1. Gaussian pairs are exact. + def mul(x, y): + return x[0]*y[0]-x[1]*y[1], x[0]*y[1]+x[1]*y[0] + require(mul((0, 1), (0, -1)) == (1, 0), "complex ordinary transpose") + require(mul((0, 1), (0, 1)) != (1, 0), "Hermitian mutation must fail") + return dict(coordinate_identity_entries=len(live)**2, + coordinate_trace_checks=8*len(frames), rational_square_fixtures=invertible, + ordinary_transpose_complex_fixture=True) + + +def budget(): + spec = importlib.util.spec_from_file_location( + "credited_ceiling", ROOT / "research/complex-local-word-ceiling/ceiling.py") + ceiling = importlib.util.module_from_spec(spec) + spec.loader.exec_module(ceiling) + baseline = {1: 2412, 2: 418, 3: 432, 4: 142, 5: 82, 8: 8} + mixed = {1: 2412, 2: 418, 3: 432, 4: 142, 5: 82, 6: 9, 8: 1} + low, high = ceiling.ceiling(baseline, 73, 896, 9, 64) + candidate_low, candidate_high = ceiling.ceiling(mixed, 73, 896, 9, 62) + require(candidate_low > Fraction(21, 20)*high, "optimistic five-percent screen") + return dict(baseline_ceiling=[str(low), str(high)], mixed62_ceiling=[str(candidate_low), str(candidate_high)], + strict_five_percent_screen=True, + physical_extra_costs="Optimistically omitted only for screening; no realization or kappa claim.") + + +def compute(): + pins = json.loads((HERE / "SOURCES.json").read_text()) + for record in pins["files"]: + if record["usage"] == "input": + require(hashlib.sha256((ROOT / record["path"]).read_bytes()).hexdigest() == record["sha256"], + "source bytes: " + record["path"]) + data = screen.engine.model() + ip, pairing, supports, frames = screen.engine.geometry(data) + witness = json.loads((HERE / "SUPPORT.json").read_text()) + terms, invoice = decode(data, pairing, supports, witness) + summary, _ = screen.frame_screen(data, frames, terms) + require(summary["minimum_frame_hits"] >= 8 and not summary["uncovered_diagonals"], + "proposal must survive old frame and diagonal conditions") + choices, census = family.representatives(data, pairing, supports, frames, terms) + quotient = family.quotient(data, ip, supports, choices) + original_choices = [next(i for i, record in enumerate(group) + if (int(record["left"], 16), int(record["right"], 16)) == terms[k]) + for k, group in enumerate(choices)] + original_case = next(case for case in quotient["diagonal_survivors"] + if case["coordinate_root"] == witness["coordinate_root"] and case["choices"] == original_choices) + for case in quotient["diagonal_survivors"]: + survivor_terms, survivor_invoice = decode(data, pairing, supports, case) + survivor_summary, _ = screen.frame_screen(data, frames, survivor_terms) + require(sum(survivor_invoice) == 62 and survivor_summary["minimum_frame_hits"] >= 8 + and not survivor_summary["uncovered_diagonals"], "survivor must pass predecessor screens") + family.check_rank_cut(data, survivor_terms, case["rank_cut"]) + cliques = screen.all_clique_screen(data, terms) + require(cliques["failed_cliques"] > 0, "the complete clique scan must detect the source counterexample") + require(summary["empty_trace_constraints"], "missing additional saturated-duality obstruction") + f, k = summary["empty_trace_constraints"][0] + mask = sum(1 << i for i in frames[f]) + separator = dict(frame=list(frames[f]), term=k, + active_terms=[j for j, (left, right) in enumerate(terms) if left & mask and right & mask], + left_on_frame=list(screen.engine.bits(terms[k][0] & mask)), + right_on_frame=list(screen.engine.bits(terms[k][1] & mask))) + check_separator(data, terms, separator) + controls = [] + def reject(name, function): + try: + function() + except (ValueError, KeyError): + controls.append(name) + else: + raise ValueError("negative control accepted: " + name) + bad = dict(separator, active_terms=separator["active_terms"][:-1]) + reject("missing_active_term", lambda: check_separator(data, terms, bad)) + bad_term = next(j for j in separator["active_terms"] if terms[j][0] & terms[j][1] & mask) + bad = dict(separator, term=bad_term, + left_on_frame=list(screen.engine.bits(terms[bad_term][0] & mask)), + right_on_frame=list(screen.engine.bits(terms[bad_term][1] & mask))) + reject("nonempty_trace_claimed_empty", lambda: check_separator(data, terms, bad)) + bad = dict(separator, frame=separator["frame"][:-1] + [separator["frame"][0]]) + reject("duplicate_frame_root", lambda: check_separator(data, terms, bad)) + bad_witness = json.loads(json.dumps(witness)) + bad_witness["terms"][0][2] = "0" + reject("uncut_parent_priced_six", lambda: decode(data, pairing, supports, bad_witness)) + for other in frames: + other_mask = sum(1 << i for i in other) + active = [j for j, (left, right) in enumerate(terms) if left & other_mask and right & other_mask] + if len(active) > 8: + bad = dict(separator, frame=list(other), active_terms=active) + reject("unsaturated_frame_cannot_use_square_duality", lambda: check_separator(data, terms, bad)) + break + else: + raise ValueError("missing unsaturated negative fixture") + # Enlarging the obstructed rectangle by its right support erases the + # empty-diagonal premise. The verifier must not preserve the old rejection. + enlarged = list(terms) + left, right = enlarged[k] + enlarged[k] = (left | right, right) + bad = dict(separator, left_on_frame=list(screen.engine.bits((left | right) & mask))) + reject("support_enlargement_invalidates_certificate", lambda: check_separator(data, enlarged, bad)) + rank_cut = original_case["rank_cut"] + a = rank_cut["roots"][0] + b = next(i for i in data["live"] if i != a and ip[a][i] != 0) + bad_cut = dict(rank_cut, roots=[a, b]) + reject("nonorthogonal_pair_is_not_an_identity_minor", lambda: family.check_rank_cut(data, terms, bad_cut)) + bad_cut = dict(rank_cut, active_terms=[]) + reject("false_rank_cut_incidence", lambda: family.check_rank_cut(data, terms, bad_cut)) + cut_mask = sum(1 << i for i in rank_cut["roots"]) + enlarged = list(terms) + inactive = next(j for j in range(10) if j not in rank_cut["active_terms"]) + left, right = enlarged[inactive] + enlarged[inactive] = (left | cut_mask, right | cut_mask) + active = [j for j, (left, right) in enumerate(enlarged) if left & cut_mask and right & cut_mask] + bad_cut = dict(rank_cut, active_terms=active) + reject("enlarged_support_can_erase_rank_cut", lambda: family.check_rank_cut(data, enlarged, bad_cut)) + positive = positive_controls(data, ip, pairing, supports, frames) + return dict(schema_version=1, copy_profile=invoice, total_copy_rank=sum(invoice), + support_sha256=hashlib.sha256((HERE / "SUPPORT.json").read_bytes()).hexdigest(), + frames=summary, all_clique_rank_counts=cliques, separator=separator, + census=census, quotient=quotient, original_choices=original_choices, + controls=controls, positive_controls=positive, optimistic_budget=budget(), + scope="No masked decoder in the declared nine retained-hit rank-at-most-six star-descendant family plus any one coordinate-star rectangle, over C with ordinary transpose. Other COPY62 supports remain open.") + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", action="store_true") + args = parser.parse_args() + result = json.loads(json.dumps(compute())) + if args.write: + (HERE / "CERTIFICATE.json").write_text(json.dumps(result, indent=2)+"\n") + else: + require(result == json.loads((HERE / "CERTIFICATE.json").read_text()), "complete certificate mismatch") + print("PASS_P112_MIXED62_QUOTIENT parents=7616 slices=967232 families=4096 " + "diagonal_survivors=3 rank2_rejections=3 controls=" + str(len(result["controls"]))) + + +if __name__ == "__main__": + main()