From a3d9c0aa0a16b68b1f4dd064671ad018013e6dd4 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar Date: Tue, 13 Oct 2026 10:14:48 +0530 Subject: [PATCH] Research: certify rank-two obstruction for CK cleanup pair fusion --- .../CERTIFICATE.json | 327 ++++++++++++++++++ research/complex-ck-cleanup-fusion/CLAIM.md | 37 ++ research/complex-ck-cleanup-fusion/README.md | 205 +++++++++++ .../complex-ck-cleanup-fusion/SOURCES.json | 13 + .../complex-ck-cleanup-fusion/VALIDATION.md | 61 ++++ .../check_columns.py | 116 +++++++ research/complex-ck-cleanup-fusion/verify.py | 192 ++++++++++ 7 files changed, 951 insertions(+) create mode 100644 research/complex-ck-cleanup-fusion/CERTIFICATE.json create mode 100644 research/complex-ck-cleanup-fusion/CLAIM.md create mode 100644 research/complex-ck-cleanup-fusion/README.md create mode 100644 research/complex-ck-cleanup-fusion/SOURCES.json create mode 100644 research/complex-ck-cleanup-fusion/VALIDATION.md create mode 100644 research/complex-ck-cleanup-fusion/check_columns.py create mode 100644 research/complex-ck-cleanup-fusion/verify.py diff --git a/research/complex-ck-cleanup-fusion/CERTIFICATE.json b/research/complex-ck-cleanup-fusion/CERTIFICATE.json new file mode 100644 index 0000000000..04e84538c3 --- /dev/null +++ b/research/complex-ck-cleanup-fusion/CERTIFICATE.json @@ -0,0 +1,327 @@ +{ + "assignment_seed": 20, + "cleanup_counts": { + "add": 8186, + "scale": 123 + }, + "cleanup_operations": 8309, + "rank_two_pairs": 78, + "registers": 716, + "same_endpoint_pairs": 78, + "schema": "ck-cleanup-rank-two-v1", + "word": "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/CANONICAL-WORD.json.gz", + "pairs": [ + { + "a":"-2","b":"1","columns":[236,230],"determinant":"-1","i":17,"j":24,"minor":[["-1","1"],["2","-1"]],"rows":[230,231],"s":236,"t":230,"u_r":"-1","u_support":2,"v_c":"-1/2","v_support":3, + "dual": {"a":"2","b":"-1","columns":[230,231],"determinant":"-1","minor":[["2","-3"],["-1","1"]],"rows":[236,230],"s":230,"t":236,"u_r":"-1/2","u_support":3,"v_c":"-1","v_support":2} + }, + { + "a":"-2","b":"1","columns":[444,438],"determinant":"-1","i":47,"j":54,"minor":[["-1","1"],["2","-1"]],"rows":[438,439],"s":444,"t":438,"u_r":"-1","u_support":2,"v_c":"-1/2","v_support":3, + "dual": {"a":"2","b":"-1","columns":[438,439],"determinant":"-1","minor":[["2","-3"],["-1","1"]],"rows":[444,438],"s":438,"t":444,"u_r":"-1/2","u_support":3,"v_c":"-1","v_support":2} + }, + { + "a":"2","b":"-3","columns":[536,512],"determinant":"-3","i":6,"j":247,"minor":[["-1","-2"],["-1","1"]],"rows":[512,536],"s":536,"t":512,"u_r":"1","u_support":2,"v_c":"1/2","v_support":2, + "dual": {"a":"-2","b":"3","columns":[512,536],"determinant":"-3","minor":[["1","-2"],["-1","-1"]],"rows":[536,512],"s":512,"t":536,"u_r":"1/2","u_support":2,"v_c":"1","v_support":2} + }, + { + "a":"-2","b":"1","columns":[248,242],"determinant":"-1","i":823,"j":838,"minor":[["1","1"],["0","-1"]],"rows":[242,244],"s":248,"t":242,"u_r":"-1","u_support":11,"v_c":"-1/2","v_support":2, + "dual": {"a":"2","b":"-1","columns":[242,244],"determinant":"-1","minor":[["0","-1"],["-1","1"]],"rows":[248,242],"s":242,"t":248,"u_r":"-1/2","u_support":2,"v_c":"-1","v_support":11} + }, + { + "a":"-2","b":"1","columns":[264,258],"determinant":"-1/4","i":841,"j":855,"minor":[["-1","1"],["1/2","-1/4"]],"rows":[258,60],"s":264,"t":258,"u_r":"-1/4","u_support":11,"v_c":"-1/2","v_support":3, + "dual": {"a":"2","b":"-1","columns":[258,60],"determinant":"-1/4","minor":[["2","-3/4"],["-1","1/4"]],"rows":[264,258],"s":258,"t":264,"u_r":"-1/2","u_support":3,"v_c":"-1/4","v_support":11} + }, + { + "a":"1/2","b":"-1/2","columns":[226,81],"determinant":"1/4","i":681,"j":955,"minor":[["1/2","-1"],["1/2","-1/2"]],"rows":[92,225],"s":226,"t":92,"u_r":"1","u_support":5,"v_c":"-1","v_support":3, + "dual": {"a":"-1/2","b":"1/2","columns":[92,225],"determinant":"1/4","minor":[["-1/2","-1"],["1/2","1/2"]],"rows":[226,81],"s":92,"t":226,"u_r":"-1","u_support":3,"v_c":"1","v_support":5} + }, + { + "a":"1/2","b":"-1/2","columns":[434,37],"determinant":"-2","i":764,"j":1013,"minor":[["1/2","2"],["2","4"]],"rows":[37,259],"s":434,"t":37,"u_r":"4","u_support":10,"v_c":"2","v_support":3, + "dual": {"a":"-1/2","b":"1/2","columns":[37,259],"determinant":"-2","minor":[["-1/2","-4"],["-1","-4"]],"rows":[434,37],"s":37,"t":434,"u_r":"2","u_support":3,"v_c":"4","v_support":10} + }, + { + "a":"-1","b":"-1/2","columns":[57,92],"determinant":"3/4","i":671,"j":1042,"minor":[["1/4","1/2"],["-9/4","-3/2"]],"rows":[225,7],"s":57,"t":225,"u_r":"3/2","u_support":12,"v_c":"1","v_support":5, + "dual": {"a":"1","b":"1/2","columns":[225,7],"determinant":"3/4","minor":[["1","3/2"],["1/2","3/2"]],"rows":[57,92],"s":225,"t":57,"u_r":"1","u_support":5,"v_c":"3/2","v_support":12} + }, + { + "a":"-2","b":"1","columns":[252,246],"determinant":"-1","i":1065,"j":1084,"minor":[["1","1"],["0","-1"]],"rows":[246,247],"s":252,"t":246,"u_r":"-1","u_support":14,"v_c":"-1/2","v_support":2, + "dual": {"a":"2","b":"-1","columns":[246,247],"determinant":"-1","minor":[["0","-1"],["-1","1"]],"rows":[252,246],"s":246,"t":252,"u_r":"-1/2","u_support":2,"v_c":"-1","v_support":14} + }, + { + "a":"-2","b":"1","columns":[296,290],"determinant":"-1/2","i":1089,"j":1113,"minor":[["-1","1"],["1","-1/2"]],"rows":[290,258],"s":296,"t":290,"u_r":"-1/2","u_support":15,"v_c":"-1/2","v_support":3, + "dual": {"a":"2","b":"-1","columns":[290,258],"determinant":"-1/2","minor":[["2","-3/2"],["-1","1/2"]],"rows":[296,290],"s":290,"t":296,"u_r":"-1/2","u_support":3,"v_c":"-1/2","v_support":15} + }, + { + "a":"-2","b":"1","columns":[412,406],"determinant":"-1/2","i":1138,"j":1155,"minor":[["-1","1"],["1","-1/2"]],"rows":[406,262],"s":412,"t":406,"u_r":"-1/2","u_support":15,"v_c":"-1/2","v_support":3, + "dual": {"a":"2","b":"-1","columns":[406,262],"determinant":"-1/2","minor":[["2","-3/2"],["-1","1/2"]],"rows":[412,406],"s":406,"t":412,"u_r":"-1/2","u_support":3,"v_c":"-1/2","v_support":15} + }, + { + "a":"1","b":"-1","columns":[436,36],"determinant":"-1/2","i":44,"j":1269,"minor":[["-5/2","1/4"],["-3","1/2"]],"rows":[435,20],"s":436,"t":435,"u_r":"1/2","u_support":13,"v_c":"1","v_support":7, + "dual": {"a":"-1","b":"1","columns":[435,20],"determinant":"-1/2","minor":[["9/4","5/2"],["-1/4","-1/2"]],"rows":[436,36],"s":435,"t":436,"u_r":"1","u_support":7,"v_c":"1/2","v_support":13} + }, + { + "a":"1/4","b":"-1","columns":[436,20],"determinant":"1/2","i":1164,"j":1277,"minor":[["-11/2","3/4"],["3","-1/2"]],"rows":[110,20],"s":436,"t":110,"u_r":"-1","u_support":15,"v_c":"2","v_support":4, + "dual": {"a":"-1/4","b":"1","columns":[110,20],"determinant":"1/2","minor":[["5","-2"],["-1","1/2"]],"rows":[436,20],"s":110,"t":436,"u_r":"2","u_support":4,"v_c":"-1","v_support":15} + }, + { + "a":"-1/2","b":"-10","columns":[228,0],"determinant":"-5","i":1037,"j":1315,"minor":[["-4","-3/2"],["-2","1/2"]],"rows":[57,7],"s":228,"t":57,"u_r":"1/2","u_support":14,"v_c":"-2","v_support":3, + "dual": {"a":"1/2","b":"10","columns":[57,7],"determinant":"-5","minor":[["4","-3"],["-1","-1/2"]],"rows":[228,0],"s":57,"t":228,"u_r":"-2","u_support":3,"v_c":"1/2","v_support":14} + }, + { + "a":"1","b":"2","columns":[228,0],"determinant":"1/2","i":14,"j":1321,"minor":[["7/2","1/4"],["3/2","1/4"]],"rows":[227,7],"s":228,"t":227,"u_r":"1/4","u_support":12,"v_c":"1","v_support":7, + "dual": {"a":"-1","b":"-2","columns":[227,7],"determinant":"1/2","minor":[["-3","-1"],["-1/4","-1/4"]],"rows":[228,0],"s":227,"t":228,"u_r":"1","u_support":7,"v_c":"1/4","v_support":12} + }, + { + "a":"2","b":"-3","columns":[238,0],"determinant":"-3/2","i":1022,"j":1340,"minor":[["-3","-3/2"],["0","1/2"]],"rows":[81,7],"s":238,"t":81,"u_r":"-1/2","u_support":15,"v_c":"-1/2","v_support":5, + "dual": {"a":"-2","b":"3","columns":[81,7],"determinant":"-3/2","minor":[["-3/2","3/2"],["3/2","-1/2"]],"rows":[238,0],"s":81,"t":238,"u_r":"-1/2","u_support":5,"v_c":"-1/2","v_support":15} + }, + { + "a":"-2","b":"1","columns":[428,422],"determinant":"-1/2","i":1352,"j":1377,"minor":[["-1","1"],["1","-1/2"]],"rows":[422,246],"s":428,"t":422,"u_r":"-1/2","u_support":19,"v_c":"-1/2","v_support":3, + "dual": {"a":"2","b":"-1","columns":[422,246],"determinant":"-1/2","minor":[["2","-3/2"],["-1","1/2"]],"rows":[428,422],"s":422,"t":428,"u_r":"-1/2","u_support":3,"v_c":"-1/2","v_support":19} + }, + { + "a":"-2","b":"1","columns":[344,337],"determinant":"-1/2","i":1390,"j":1419,"minor":[["-1","1"],["1","-1/2"]],"rows":[337,262],"s":344,"t":337,"u_r":"-1/2","u_support":21,"v_c":"-1/2","v_support":3, + "dual": {"a":"2","b":"-1","columns":[337,262],"determinant":"-1/2","minor":[["2","-3/2"],["-1","1/2"]],"rows":[344,337],"s":337,"t":344,"u_r":"-1/2","u_support":3,"v_c":"-1/2","v_support":21} + }, + { + "a":"-2","b":"-1","columns":[285,278],"determinant":"-1/2","i":1211,"j":1519,"minor":[["-1","0"],["-1","1/2"]],"rows":[278,275],"s":285,"t":278,"u_r":"1/2","u_support":9,"v_c":"-1/2","v_support":3, + "dual": {"a":"2","b":"1","columns":[278,275],"determinant":"-1/2","minor":[["3/2","1/2"],["-1/2","-1/2"]],"rows":[285,278],"s":278,"t":285,"u_r":"-1/2","u_support":3,"v_c":"1/2","v_support":9} + }, + { + "a":"-2","b":"-1","columns":[301,294],"determinant":"-1/2","i":980,"j":1559,"minor":[["-1","0"],["-1","1/2"]],"rows":[294,291],"s":301,"t":294,"u_r":"1/2","u_support":5,"v_c":"-1/2","v_support":3, + "dual": {"a":"2","b":"1","columns":[294,291],"determinant":"-1/2","minor":[["3/2","1/2"],["-1/2","-1/2"]],"rows":[301,294],"s":294,"t":301,"u_r":"-1/2","u_support":3,"v_c":"1/2","v_support":5} + }, + { + "a":"-2","b":"-1","columns":[317,310],"determinant":"1/2","i":862,"j":1659,"minor":[["-1","0"],["1","-1/2"]],"rows":[310,291],"s":317,"t":310,"u_r":"-1/2","u_support":12,"v_c":"-1/2","v_support":3, + "dual": {"a":"2","b":"1","columns":[310,291],"determinant":"1/2","minor":[["3/2","-1/2"],["-1/2","1/2"]],"rows":[317,310],"s":310,"t":317,"u_r":"-1/2","u_support":3,"v_c":"-1/2","v_support":12} + }, + { + "a":"1/2","b":"1/2","columns":[260,61],"determinant":"-1/8","i":853,"j":1704,"minor":[["1/2","0"],["1/4","-1/4"]],"rows":[264,38],"s":260,"t":264,"u_r":"1/2","u_support":14,"v_c":"-1","v_support":9, + "dual": {"a":"-1/2","b":"-1/2","columns":[264,38],"determinant":"-1/8","minor":[["-1/2","0"],["1/2","1/4"]],"rows":[260,61],"s":264,"t":260,"u_r":"-1","u_support":9,"v_c":"1/2","v_support":14} + }, + { + "a":"-2","b":"1","columns":[300,293],"determinant":"-1/2","i":1815,"j":1860,"minor":[["-1","1"],["1","-1/2"]],"rows":[293,242],"s":300,"t":293,"u_r":"-1/2","u_support":33,"v_c":"-1/2","v_support":3, + "dual": {"a":"2","b":"-1","columns":[293,242],"determinant":"-1/2","minor":[["2","-3/2"],["-1","1/2"]],"rows":[300,293],"s":293,"t":300,"u_r":"-1/2","u_support":3,"v_c":"-1/2","v_support":33} + }, + { + "a":"1/2","b":"1/2","columns":[292,18],"determinant":"1/4","i":1105,"j":1899,"minor":[["1/2","0"],["-1/2","1/2"]],"rows":[296,10],"s":292,"t":296,"u_r":"-1","u_support":20,"v_c":"-1","v_support":12, + "dual": {"a":"-1/2","b":"-1/2","columns":[296,10],"determinant":"1/4","minor":[["-1/2","0"],["1/2","-1/2"]],"rows":[292,18],"s":296,"t":292,"u_r":"-1","u_support":12,"v_c":"-1","v_support":20} + }, + { + "a":"1/2","b":"1/2","columns":[420,43],"determinant":"1/4","i":1476,"j":2153,"minor":[["1/2","0"],["-3/4","1/2"]],"rows":[419,242],"s":420,"t":419,"u_r":"-1","u_support":17,"v_c":"-1","v_support":5, + "dual": {"a":"-1/2","b":"-1/2","columns":[419,242],"determinant":"1/4","minor":[["-3/4","1/4"],["1/2","-1/2"]],"rows":[420,43],"s":419,"t":420,"u_r":"-1","u_support":5,"v_c":"-1","v_support":17} + }, + { + "a":"1/2","b":"1/2","columns":[276,31],"determinant":"-1/4","i":1306,"j":2274,"minor":[["1","-1/2"],["1/2","-1/2"]],"rows":[280,262],"s":276,"t":280,"u_r":"1","u_support":27,"v_c":"-1","v_support":12, + "dual": {"a":"-1/2","b":"-1/2","columns":[280,262],"determinant":"-1/4","minor":[["-1/2","0"],["1/2","1/2"]],"rows":[276,31],"s":280,"t":276,"u_r":"-1","u_support":12,"v_c":"1","v_support":27} + }, + { + "a":"-2","b":"1","columns":[316,85],"determinant":"-1/2","i":2396,"j":2451,"minor":[["-1","1"],["1","-1/2"]],"rows":[309,277],"s":316,"t":309,"u_r":"-1/2","u_support":33,"v_c":"-1/2","v_support":4, + "dual": {"a":"2","b":"-1","columns":[309,277],"determinant":"-1/2","minor":[["2","-3/2"],["-1","1/2"]],"rows":[316,85],"s":309,"t":316,"u_r":"-1/2","u_support":4,"v_c":"-1/2","v_support":33} + }, + { + "a":"1","b":"1/2","columns":[308,24],"determinant":"1/2","i":1115,"j":2498,"minor":[["1/2","0"],["1","1"]],"rows":[306,7],"s":308,"t":306,"u_r":"1","u_support":29,"v_c":"1","v_support":6, + "dual": {"a":"-1","b":"-1/2","columns":[306,7],"determinant":"1/2","minor":[["-3/4","-1/2"],["-1/2","-1"]],"rows":[308,24],"s":306,"t":308,"u_r":"1","u_support":6,"v_c":"1","v_support":29} + }, + { + "a":"-2","b":"1","columns":[364,356],"determinant":"-1/2","i":2545,"j":2604,"minor":[["-1","1"],["1","-1/2"]],"rows":[356,246],"s":364,"t":356,"u_r":"-1/2","u_support":34,"v_c":"-1/2","v_support":3, + "dual": {"a":"2","b":"-1","columns":[356,246],"determinant":"-1/2","minor":[["2","-3/2"],["-1","1/2"]],"rows":[364,356],"s":356,"t":364,"u_r":"-1/2","u_support":3,"v_c":"-1/2","v_support":34} + }, + { + "a":"1","b":"1/2","columns":[404,41],"determinant":"-1/4","i":1734,"j":2660,"minor":[["1/2","0"],["3/4","-1/2"]],"rows":[403,60],"s":404,"t":403,"u_r":"1/2","u_support":19,"v_c":"-1","v_support":6, + "dual": {"a":"-1","b":"-1/2","columns":[403,60],"determinant":"-1/4","minor":[["-1","-1/2"],["1/2","1/2"]],"rows":[404,41],"s":403,"t":404,"u_r":"-1","u_support":6,"v_c":"1/2","v_support":19} + }, + { + "a":"1","b":"1/2","columns":[61,25],"determinant":"1/8","i":1696,"j":2723,"minor":[["1/2","0"],["1/4","1/4"]],"rows":[260,28],"s":61,"t":260,"u_r":"1/4","u_support":17,"v_c":"1","v_support":4, + "dual": {"a":"-1","b":"-1/2","columns":[260,28],"determinant":"1/8","minor":[["-3/4","-1/8"],["-1/2","-1/4"]],"rows":[61,25],"s":260,"t":61,"u_r":"1","u_support":4,"v_c":"1/4","v_support":17} + }, + { + "a":"1/2","b":"5/4","columns":[244,10],"determinant":"5/8","i":835,"j":2792,"minor":[["-1/4","-3/4"],["1","1/2"]],"rows":[248,7],"s":244,"t":248,"u_r":"1","u_support":29,"v_c":"1","v_support":13, + "dual": {"a":"-1/2","b":"-5/4","columns":[248,7],"determinant":"5/8","minor":[["-1","1/4"],["-1/2","-1/2"]],"rows":[244,10],"s":248,"t":244,"u_r":"1","u_support":13,"v_c":"1","v_support":29} + }, + { + "a":"1","b":"1/2","columns":[18,102],"determinant":"-1/2","i":1886,"j":2876,"minor":[["1/2","0"],["-1/2","-1"]],"rows":[292,18],"s":18,"t":292,"u_r":"-1","u_support":23,"v_c":"1","v_support":4, + "dual": {"a":"-1","b":"-1/2","columns":[292,18],"determinant":"-1/2","minor":[["-1/2","0"],["-1/2","1"]],"rows":[18,102],"s":292,"t":18,"u_r":"1","u_support":4,"v_c":"-1","v_support":23} + }, + { + "a":"1","b":"-1","columns":[62,63],"determinant":"1/2","i":1595,"j":2978,"minor":[["-1","0"],["1/2","-1/2"]],"rows":[63,7],"s":62,"t":63,"u_r":"-1/2","u_support":20,"v_c":"1","v_support":2, + "dual": {"a":"-1","b":"1","columns":[63,7],"determinant":"1/2","minor":[["1","0"],["0","1/2"]],"rows":[62,63],"s":63,"t":62,"u_r":"1","u_support":2,"v_c":"-1/2","v_support":20} + }, + { + "a":"1/2","b":"-1","columns":[418,13],"determinant":"9/8","i":3137,"j":3252,"minor":[["1/2","27/8"],["-1/2","-9/8"]],"rows":[43,63],"s":418,"t":43,"u_r":"-1","u_support":19,"v_c":"9/4","v_support":5, + "dual": {"a":"-1/2","b":"1","columns":[43,63],"determinant":"9/8","minor":[["-1/2","3/2"],["-9/8","9/8"]],"rows":[418,13],"s":43,"t":418,"u_r":"9/4","u_support":5,"v_c":"-1","v_support":19} + }, + { + "a":"15/8","b":"-2","columns":[104,16],"determinant":"-15/2","i":3304,"j":3347,"minor":[["7/4","-15/4"],["-15/4","15/4"]],"rows":[16,43],"s":104,"t":16,"u_r":"1","u_support":39,"v_c":"2","v_support":2, + "dual": {"a":"-15/8","b":"2","columns":[16,43],"determinant":"-15/2","minor":[["-7/4","-15/4"],["-15/4","-15/4"]],"rows":[104,16],"s":16,"t":104,"u_r":"2","u_support":2,"v_c":"1","v_support":39} + }, + { + "a":"1","b":"-2","columns":[104,78],"determinant":"1/4","i":3251,"j":3359,"minor":[["-2","0"],["1/4","-1/8"]],"rows":[418,16],"s":104,"t":418,"u_r":"-1/8","u_support":40,"v_c":"1","v_support":3, + "dual": {"a":"-1","b":"2","columns":[418,16],"determinant":"1/4","minor":[["2","0"],["3/4","1/8"]],"rows":[104,78],"s":418,"t":104,"u_r":"1","u_support":3,"v_c":"-1/8","v_support":40} + }, + { + "a":"-2","b":"2","columns":[333,109],"determinant":"1","i":883,"j":3693,"minor":[["2","0"],["-1","1/2"]],"rows":[325,7],"s":333,"t":325,"u_r":"-1/2","u_support":46,"v_c":"1/2","v_support":4, + "dual": {"a":"2","b":"-2","columns":[325,7],"determinant":"1","minor":[["-2","0"],["1/2","-1/2"]],"rows":[333,109],"s":325,"t":333,"u_r":"1/2","u_support":4,"v_c":"-1/2","v_support":46} + }, + { + "a":"2","b":"-1","columns":[22,108],"determinant":"-1","i":3765,"j":3807,"minor":[["2","3/2"],["2","1"]],"rows":[108,10],"s":22,"t":108,"u_r":"1","u_support":41,"v_c":"1/2","v_support":3, + "dual": {"a":"-2","b":"1","columns":[108,10],"determinant":"-1","minor":[["-2","-3"],["-1","-1"]],"rows":[22,108],"s":108,"t":22,"u_r":"1/2","u_support":3,"v_c":"1","v_support":41} + }, + { + "a":"2","b":"1","columns":[22,23],"determinant":"-2","i":3450,"j":3809,"minor":[["1","0"],["-6","-2"]],"rows":[23,10],"s":22,"t":23,"u_r":"-2","u_support":17,"v_c":"1/2","v_support":5, + "dual": {"a":"-2","b":"-1","columns":[23,10],"determinant":"-2","minor":[["-1","4"],["0","2"]],"rows":[22,23],"s":23,"t":22,"u_r":"1/2","u_support":5,"v_c":"-2","v_support":17} + }, + { + "a":"-1/2","b":"1","columns":[331,23],"determinant":"-4","i":1774,"j":3884,"minor":[["7/2","5/2"],["-4","-4"]],"rows":[324,10],"s":331,"t":324,"u_r":"-4","u_support":33,"v_c":"-2","v_support":7, + "dual": {"a":"1/2","b":"-1","columns":[324,10],"determinant":"-4","minor":[["-1","0"],["-1/2","4"]],"rows":[331,23],"s":324,"t":331,"u_r":"-2","u_support":7,"v_c":"-4","v_support":33} + }, + { + "a":"1","b":"-2","columns":[45,48],"determinant":"4","i":4018,"j":4155,"minor":[["0","2"],["-2","-2"]],"rows":[107,7],"s":45,"t":107,"u_r":"-2","u_support":65,"v_c":"1","v_support":6, + "dual": {"a":"-1","b":"2","columns":[107,7],"determinant":"4","minor":[["-1","6"],["-1","2"]],"rows":[45,48],"s":107,"t":45,"u_r":"1","u_support":6,"v_c":"-2","v_support":65} + }, + { + "a":"1","b":"3","columns":[334,22],"determinant":"96","i":3805,"j":4261,"minor":[["-7/2","-13"],["16","32"]],"rows":[22,10],"s":334,"t":22,"u_r":"32","u_support":54,"v_c":"1","v_support":5, + "dual": {"a":"-1","b":"-3","columns":[22,10],"determinant":"96","minor":[["-41/2","80"],["7","-32"]],"rows":[334,22],"s":22,"t":334,"u_r":"1","u_support":5,"v_c":"32","v_support":54} + }, + { + "a":"1/4","b":"-7","columns":[323,331],"determinant":"-7/8","i":3866,"j":4347,"minor":[["-8","1/8"],["-1","1/8"]],"rows":[331,22],"s":323,"t":331,"u_r":"1/8","u_support":21,"v_c":"4","v_support":2, + "dual": {"a":"-1/4","b":"7","columns":[331,22],"determinant":"-7/8","minor":[["8","1/8"],["-1","-1/8"]],"rows":[323,331],"s":331,"t":323,"u_r":"4","u_support":2,"v_c":"1/8","v_support":21} + }, + { + "a":"1/4","b":"-1","columns":[323,331],"determinant":"1","i":3846,"j":4351,"minor":[["-1/2","1"],["-1/2","-1"]],"rows":[335,331],"s":323,"t":335,"u_r":"-1","u_support":4,"v_c":"4","v_support":4, + "dual": {"a":"-1/4","b":"1","columns":[335,331],"determinant":"1","minor":[["-1/2","3/2"],["-1","1"]],"rows":[323,331],"s":335,"t":323,"u_r":"4","u_support":4,"v_c":"-1","v_support":4} + }, + { + "a":"1/2","b":"1/2","columns":[407,14],"determinant":"-1/2","i":1154,"j":4582,"minor":[["1/2","-2"],["0","-1"]],"rows":[412,28],"s":407,"t":412,"u_r":"1","u_support":21,"v_c":"-2","v_support":8, + "dual": {"a":"-1/2","b":"-1/2","columns":[412,28],"determinant":"-1/2","minor":[["0","1/2"],["1","1"]],"rows":[407,14],"s":412,"t":407,"u_r":"-2","u_support":8,"v_c":"1","v_support":21} + }, + { + "a":"1","b":"-4","columns":[41,52],"determinant":"-1","i":2657,"j":4750,"minor":[["-4","0"],["-1","1/4"]],"rows":[404,10],"s":41,"t":404,"u_r":"1/4","u_support":27,"v_c":"1","v_support":4, + "dual": {"a":"-1","b":"4","columns":[404,10],"determinant":"-1","minor":[["4","0"],["-1","-1/4"]],"rows":[41,52],"s":404,"t":41,"u_r":"1","u_support":4,"v_c":"1/4","v_support":27} + }, + { + "a":"1","b":"-1/2","columns":[402,41],"determinant":"-1/2","i":4368,"j":4776,"minor":[["-5/4","-1"],["3/4","1"]],"rows":[42,41],"s":402,"t":42,"u_r":"1","u_support":8,"v_c":"1","v_support":4, + "dual": {"a":"-1","b":"1/2","columns":[42,41],"determinant":"-1/2","minor":[["7/4","-5/4"],["1","-1"]],"rows":[402,41],"s":42,"t":402,"u_r":"1","u_support":4,"v_c":"1","v_support":8} + }, + { + "a":"-2","b":"1/2","columns":[402,41],"determinant":"-1","i":4669,"j":4778,"minor":[["0","2"],["1/2","-2"]],"rows":[106,42],"s":402,"t":106,"u_r":"-1","u_support":26,"v_c":"-1","v_support":3, + "dual": {"a":"2","b":"-1/2","columns":[106,42],"determinant":"-1","minor":[["0","-1"],["-1","2"]],"rows":[402,41],"s":106,"t":402,"u_r":"-1","u_support":3,"v_c":"-1","v_support":26} + }, + { + "a":"2","b":"-2","columns":[9,94],"determinant":"-4","i":5277,"j":5305,"minor":[["2","-4"],["-2","2"]],"rows":[94,7],"s":9,"t":94,"u_r":"1/2","u_support":26,"v_c":"2","v_support":2, + "dual": {"a":"-2","b":"2","columns":[94,7],"determinant":"-4","minor":[["-2","-2"],["-4","-2"]],"rows":[9,94],"s":94,"t":9,"u_r":"2","u_support":2,"v_c":"1/2","v_support":26} + }, + { + "a":"1","b":"-2","columns":[9,2],"determinant":"1/2","i":5263,"j":5318,"minor":[["-2","0"],["1/2","-1/4"]],"rows":[256,7],"s":9,"t":256,"u_r":"-1/4","u_support":24,"v_c":"1","v_support":3, + "dual": {"a":"-1","b":"2","columns":[256,7],"determinant":"1/2","minor":[["2","0"],["1","1/4"]],"rows":[9,2],"s":256,"t":9,"u_r":"1","u_support":3,"v_c":"-1/4","v_support":24} + }, + { + "a":"2","b":"1/2","columns":[64,4],"determinant":"-1/16","i":5075,"j":5432,"minor":[["9/32","1/16"],["7/16","-1/8"]],"rows":[395,9],"s":64,"t":395,"u_r":"-1/8","u_support":42,"v_c":"1/2","v_support":5, + "dual": {"a":"-2","b":"-1/2","columns":[395,9],"determinant":"-1/16","minor":[["-1/2","-1/2"],["0","1/8"]],"rows":[64,4],"s":395,"t":64,"u_r":"1/2","u_support":5,"v_c":"-1/8","v_support":42} + }, + { + "a":"-1/2","b":"-1/2","columns":[69,64],"determinant":"9/4","i":5137,"j":5481,"minor":[["-1","9/4"],["1","-9/2"]],"rows":[96,5],"s":69,"t":96,"u_r":"-1","u_support":51,"v_c":"-9","v_support":4, + "dual": {"a":"1/2","b":"1/2","columns":[96,5],"determinant":"9/4","minor":[["1","-1/2"],["-9/2","9/2"]],"rows":[69,64],"s":96,"t":69,"u_r":"-9","u_support":4,"v_c":"-1","v_support":51} + }, + { + "a":"-1/4","b":"-1","columns":[387,65],"determinant":"1/2","i":5455,"j":5534,"minor":[["5","3/2"],["-2","-1/2"]],"rows":[65,5],"s":387,"t":65,"u_r":"-1/2","u_support":24,"v_c":"-4","v_support":3, + "dual": {"a":"1/4","b":"1","columns":[65,5],"determinant":"1/2","minor":[["-4","5/2"],["-1","1/2"]],"rows":[387,65],"s":65,"t":387,"u_r":"-4","u_support":3,"v_c":"-1/2","v_support":24} + }, + { + "a":"-2","b":"1","columns":[349,341],"determinant":"-1/4","i":549,"j":5803,"minor":[["1","0"],["-1/2","-1/4"]],"rows":[341,7],"s":349,"t":341,"u_r":"-1/4","u_support":42,"v_c":"-1/2","v_support":3, + "dual": {"a":"2","b":"-1","columns":[341,7],"determinant":"-1/4","minor":[["-3/2","1/4"],["-1/2","1/4"]],"rows":[349,341],"s":341,"t":349,"u_r":"-1/2","u_support":3,"v_c":"-1/4","v_support":42} + }, + { + "a":"2","b":"1/2","columns":[58,93],"determinant":"1/4","i":5596,"j":5885,"minor":[["3/8","-1/4"],["1/4","1/2"]],"rows":[347,9],"s":58,"t":347,"u_r":"1/2","u_support":62,"v_c":"1/2","v_support":5, + "dual": {"a":"-2","b":"-1/2","columns":[347,9],"determinant":"1/4","minor":[["-1/2","0"],["0","-1/2"]],"rows":[58,93],"s":347,"t":58,"u_r":"1/2","u_support":5,"v_c":"1/2","v_support":62} + }, + { + "a":"1","b":"-5/2","columns":[363,4],"determinant":"-5/4","i":2188,"j":6011,"minor":[["-21/8","-1/4"],["1/4","1/2"]],"rows":[277,7],"s":363,"t":277,"u_r":"-1/2","u_support":28,"v_c":"-1","v_support":28, + "dual": {"a":"-1","b":"5/2","columns":[277,7],"determinant":"-5/4","minor":[["2","1"],["1/4","-1/2"]],"rows":[363,4],"s":277,"t":363,"u_r":"-1","u_support":28,"v_c":"-1/2","v_support":28} + }, + { + "a":"2","b":"-1","columns":[60,29],"determinant":"1","i":6245,"j":6417,"minor":[["0","1/2"],["-2","-1"]],"rows":[29,9],"s":60,"t":29,"u_r":"-1","u_support":127,"v_c":"1/2","v_support":3, + "dual": {"a":"-2","b":"1","columns":[29,9],"determinant":"1","minor":[["-2","3"],["-1","1"]],"rows":[60,29],"s":29,"t":60,"u_r":"1/2","u_support":3,"v_c":"-1","v_support":127} + }, + { + "a":"-2","b":"-2","columns":[366,60],"determinant":"3/2","i":6411,"j":6508,"minor":[["-4","-1"],["-3/2","-3/4"]],"rows":[60,7],"s":366,"t":60,"u_r":"-3/4","u_support":70,"v_c":"-1/2","v_support":5, + "dual": {"a":"2","b":"2","columns":[60,7],"determinant":"3/2","minor":[["6","3"],["1","3/4"]],"rows":[366,60],"s":60,"t":366,"u_r":"-1/2","u_support":5,"v_c":"-3/4","v_support":70} + }, + { + "a":"1/2","b":"31/8","columns":[354,30],"determinant":"31/32","i":6091,"j":6777,"minor":[["31/8","0"],["33/8","1/4"]],"rows":[59,29],"s":354,"t":59,"u_r":"1","u_support":8,"v_c":"1/2","v_support":9, + "dual": {"a":"-1/2","b":"-31/8","columns":[59,29],"determinant":"31/32","minor":[["-31/8","-1/4"],["0","-1/4"]],"rows":[354,30],"s":59,"t":354,"u_r":"1/2","u_support":9,"v_c":"1","v_support":8} + }, + { + "a":"-1/2","b":"-7/2","columns":[354,84],"determinant":"7/4","i":6466,"j":6813,"minor":[["-7/2","0"],["7/4","-1/2"]],"rows":[355,10],"s":354,"t":355,"u_r":"-1/2","u_support":19,"v_c":"-2","v_support":4, + "dual": {"a":"1/2","b":"7/2","columns":[355,10],"determinant":"7/4","minor":[["7/2","0"],["0","1/2"]],"rows":[354,84],"s":355,"t":354,"u_r":"-2","u_support":4,"v_c":"-1/2","v_support":19} + }, + { + "a":"-1/8","b":"-3/4","columns":[354,83],"determinant":"9/32","i":6670,"j":6817,"minor":[["-1","1/4"],["3/8","-3/8"]],"rows":[352,7],"s":354,"t":352,"u_r":"-3/8","u_support":49,"v_c":"-8","v_support":3, + "dual": {"a":"1/8","b":"3/4","columns":[352,7],"determinant":"9/32","minor":[["1","-3/32"],["-1","3/8"]],"rows":[354,83],"s":352,"t":354,"u_r":"-8","u_support":3,"v_c":"-3/8","v_support":49} + }, + { + "a":"-1/2","b":"1","columns":[73,30],"determinant":"-4","i":6499,"j":6874,"minor":[["7/4","1"],["-3","-4"]],"rows":[366,29],"s":73,"t":366,"u_r":"-4","u_support":34,"v_c":"-2","v_support":5, + "dual": {"a":"1/2","b":"-1","columns":[366,29],"determinant":"-4","minor":[["-3/4","-1"],["-1","4"]],"rows":[73,30],"s":366,"t":73,"u_r":"-2","u_support":5,"v_c":"-4","v_support":34} + }, + { + "a":"1/2","b":"1","columns":[340,6],"determinant":"-1/2","i":5844,"j":7046,"minor":[["0","2"],["1/4","-1/2"]],"rows":[58,7],"s":340,"t":58,"u_r":"1/2","u_support":145,"v_c":"-2","v_support":5, + "dual": {"a":"-1/2","b":"-1","columns":[58,7],"determinant":"-1/2","minor":[["-1/8","1/4"],["7/4","1/2"]],"rows":[340,6],"s":58,"t":340,"u_r":"-2","u_support":5,"v_c":"1/2","v_support":145} + }, + { + "a":"-1/2","b":"3","columns":[28,86],"determinant":"6","i":6892,"j":7086,"minor":[["0","6"],["-1","2"]],"rows":[86,7],"s":28,"t":86,"u_r":"2","u_support":146,"v_c":"-2","v_support":5, + "dual": {"a":"1/2","b":"-3","columns":[86,7],"determinant":"6","minor":[["18","7"],["-6","-2"]],"rows":[28,86],"s":86,"t":28,"u_r":"-2","u_support":5,"v_c":"2","v_support":146} + }, + { + "a":"-1/16","b":"-1","columns":[339,1],"determinant":"1","i":7079,"j":7226,"minor":[["-4","-3/4"],["-4","-1"]],"rows":[28,7],"s":339,"t":28,"u_r":"1","u_support":140,"v_c":"16","v_support":3, + "dual": {"a":"1/16","b":"1","columns":[28,7],"determinant":"1","minor":[["4","3"],["1","1"]],"rows":[339,1],"s":28,"t":339,"u_r":"16","u_support":3,"v_c":"1","v_support":140} + }, + { + "a":"1/4","b":"16","columns":[339,1],"determinant":"2","i":7045,"j":7306,"minor":[["419/32","-3/32"],["31/8","1/8"]],"rows":[340,7],"s":339,"t":340,"u_r":"1/4","u_support":126,"v_c":"2","v_support":5, + "dual": {"a":"-1/4","b":"-16","columns":[340,7],"determinant":"2","minor":[["-515/32","1/8"],["3/32","-1/8"]],"rows":[339,1],"s":340,"t":339,"u_r":"2","u_support":5,"v_c":"1/4","v_support":126} + }, + { + "a":"1/2","b":"-1/2","columns":[299,18],"determinant":"-1/16","i":994,"j":7511,"minor":[["-1/2","0"],["-1/8","1/8"]],"rows":[295,293],"s":299,"t":295,"u_r":"1/4","u_support":16,"v_c":"1","v_support":23, + "dual": {"a":"-1/2","b":"1/2","columns":[295,293],"determinant":"-1/16","minor":[["1/2","0"],["0","-1/8"]],"rows":[299,18],"s":295,"t":299,"u_r":"1","u_support":23,"v_c":"1/4","v_support":16} + }, + { + "a":"1/2","b":"7","columns":[288,299],"determinant":"-7/4","i":7490,"j":7548,"minor":[["8","1/8"],["-2","-1/4"]],"rows":[299,7],"s":288,"t":299,"u_r":"-1/4","u_support":34,"v_c":"2","v_support":2, + "dual": {"a":"-1/2","b":"-7","columns":[299,7],"determinant":"-7/4","minor":[["-8","1/4"],["-1","1/4"]],"rows":[288,299],"s":299,"t":288,"u_r":"2","u_support":2,"v_c":"-1/4","v_support":34} + }, + { + "a":"1/2","b":"-2","columns":[288,299],"determinant":"2","i":7466,"j":7552,"minor":[["-1","1"],["-1","-1"]],"rows":[303,299],"s":288,"t":303,"u_r":"-1","u_support":4,"v_c":"2","v_support":3, + "dual": {"a":"-1/2","b":"2","columns":[303,299],"determinant":"2","minor":[["-1","3"],["-1","1"]],"rows":[288,299],"s":303,"t":288,"u_r":"2","u_support":3,"v_c":"-1","v_support":4} + }, + { + "a":"1/64","b":"4","columns":[379,3],"determinant":"2","i":6562,"j":8071,"minor":[["2","1"],["-1","1/2"]],"rows":[30,9],"s":379,"t":30,"u_r":"-1/2","u_support":112,"v_c":"-64","v_support":15, + "dual": {"a":"-1/64","b":"-4","columns":[30,9],"determinant":"2","minor":[["-2","-1"],["1","-1/2"]],"rows":[379,3],"s":30,"t":379,"u_r":"-64","u_support":15,"v_c":"-1/2","v_support":112} + }, + { + "a":"1/8","b":"18","columns":[379,6],"determinant":"9/4","i":5338,"j":8100,"minor":[["253/16","-1/16"],["35/8","1/8"]],"rows":[263,9],"s":379,"t":263,"u_r":"1/4","u_support":75,"v_c":"4","v_support":30, + "dual": {"a":"-1/8","b":"-18","columns":[263,9],"determinant":"9/4","minor":[["-289/16","1/8"],["1/16","-1/8"]],"rows":[379,6],"s":263,"t":379,"u_r":"4","u_support":30,"v_c":"1/4","v_support":75} + }, + { + "a":"-1/2","b":"-67","columns":[379,1],"determinant":"201/8","i":1229,"j":8114,"minor":[["-67","0"],["-539/32","-3/8"]],"rows":[279,277],"s":379,"t":279,"u_r":"1/4","u_support":17,"v_c":"3","v_support":56, + "dual": {"a":"1/2","b":"67","columns":[279,277],"determinant":"201/8","minor":[["67","3/32"],["0","3/8"]],"rows":[379,1],"s":279,"t":379,"u_r":"3","u_support":56,"v_c":"1/4","v_support":17} + }, + { + "a":"1/8","b":"1","columns":[379,1],"determinant":"-1/4","i":2580,"j":8130,"minor":[["-11/2","-1/4"],["-13/2","-1/4"]],"rows":[364,246],"s":379,"t":364,"u_r":"1","u_support":32,"v_c":"-2","v_support":82, + "dual": {"a":"-1/8","b":"-1","columns":[364,246],"determinant":"-1/4","minor":[["13/2","15/2"],["1/4","1/4"]],"rows":[379,1],"s":364,"t":379,"u_r":"-2","u_support":82,"v_c":"1","v_support":32} + }, + { + "a":"1","b":"-1","columns":[8,95],"determinant":"-1/2","i":7886,"j":8220,"minor":[["-1","0"],["-1/2","1/2"]],"rows":[95,3],"s":8,"t":95,"u_r":"1/2","u_support":21,"v_c":"1","v_support":5, + "dual": {"a":"-1","b":"1","columns":[95,3],"determinant":"-1/2","minor":[["1","0"],["-1","-1/2"]],"rows":[8,95],"s":95,"t":8,"u_r":"1","u_support":5,"v_c":"1/2","v_support":21} + }, + { + "a":"1","b":"-1/2","columns":[26,67],"determinant":"-1/4","i":7806,"j":8259,"minor":[["0","1/2"],["1/2","1/2"]],"rows":[67,3],"s":26,"t":67,"u_r":"1/2","u_support":15,"v_c":"1","v_support":3, + "dual": {"a":"-1","b":"1/2","columns":[67,3],"determinant":"-1/4","minor":[["-1/4","-3/4"],["-1/2","-1/2"]],"rows":[26,67],"s":67,"t":26,"u_r":"1","u_support":3,"v_c":"1/2","v_support":15} + }, + { + "a":"-2","b":"8","columns":[381,66],"determinant":"2","i":733,"j":8300,"minor":[["4","1/2"],["-2","1/4"]],"rows":[373,7],"s":381,"t":373,"u_r":"-1/4","u_support":27,"v_c":"1/2","v_support":5, + "dual": {"a":"2","b":"-8","columns":[373,7],"determinant":"2","minor":[["-8","0"],["3/2","-1/4"]],"rows":[381,66],"s":373,"t":381,"u_r":"1/2","u_support":5,"v_c":"-1/4","v_support":27} + }, + { + "a":"-1/2","b":"-3","columns":[381,374],"determinant":"3/2","i":7907,"j":8301,"minor":[["-2","1/2"],["-1","-1/2"]],"rows":[374,358],"s":381,"t":374,"u_r":"-1/2","u_support":11,"v_c":"-2","v_support":4, + "dual": {"a":"1/2","b":"3","columns":[374,358],"determinant":"3/2","minor":[["-7","5/2"],["-2","1/2"]],"rows":[381,374],"s":374,"t":381,"u_r":"-2","u_support":4,"v_c":"-1/2","v_support":11} + } + ] +} diff --git a/research/complex-ck-cleanup-fusion/CLAIM.md b/research/complex-ck-cleanup-fusion/CLAIM.md new file mode 100644 index 0000000000..2e4b97ff52 --- /dev/null +++ b/research/complex-ck-cleanup-fusion/CLAIM.md @@ -0,0 +1,37 @@ +# Sprint claim + +- Track: complex supplier. OS assignment seed: 20. +- Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +- Start: 2026-10-13 04:26:40 UTC. Expected finish: 05:16:40 UTC. +- Object: the selected #626 CK provider's full-frame scalar cleanup. +- Hypothesis: same-source, same-target additions separated only by commuting + operations can be combined at their later position without changing the + complete dirty-input map or increasing the absolute prefix envelope. +- Method: exhaust the pair domain in this one cleanup word, then apply a + deterministic fixed-point fusion pass and exactly replay both orientations. + Seed 20 selects CK by parity. Full-frame cleanup is selected after excluding + the already-claimed factory and B-frame tasks. +- Deliverable: exact local circuit evidence, a reproducible checker, source pins, + negative controls, and a scoped result. No new kappa is assumed. +- Candidates considered: raw factory resynthesis, selected B-frame reassignment, + and cleanup fusion. #681 and #698 cover the first two. #696 lowers individual + unchanged macros; this experiment changes the cleanup macro word. #687 changes + a raw K-triangle read order. No pending result is a dependency. +- Coordination: GitHub's pinned-issue query returned an empty list. No separate + issue was opened. Open PRs were inspected through #700 before this local claim. +- Scope: only this research package. Keep upstream, accepted supplier sources, + selected certificates, ownership, frame paths, and recursive profiles unchanged. +- Substantial OpenAI Codex assistance is used for research, code, and writing. + +Status: completed, 2026-10-13 04:44 UTC. The initial commuting search found no +candidate among all 78 pairs. One refinement computed the complete conjugated +shear: every pair has a certified rank-two defect in both orientations. No +single rank-one replacement can work anywhere among the unchanged middle gates +on arbitrary register inputs. This is a scoped negative result, with no kappa +claim and no fixed-point optimization run. + +Result: [research note](README.md), [exact certificate](CERTIFICATE.json), and +[review branch](https://github.com/thakrarsagar/integer-mult-bounds/tree/research/complex-ck-cleanup-fusion/research/complex-ck-cleanup-fusion). +Reproduce with `python3 -B research/complex-ck-cleanup-fusion/verify.py`. +Expected: `PASS_CK_CLEANUP_RANK_TWO pairs=78 rank=2 columns=312 controls=8`. +The final verification and overlap record is in [VALIDATION.md](VALIDATION.md). diff --git a/research/complex-ck-cleanup-fusion/README.md b/research/complex-ck-cleanup-fusion/README.md new file mode 100644 index 0000000000..0a1033e916 --- /dev/null +++ b/research/complex-ck-cleanup-fusion/README.md @@ -0,0 +1,205 @@ +# Rank-two obstruction to CK cleanup pair fusion + +**Status: scoped negative result. No new supplier or kappa.** + +The selected #626 CK provider has 8,309 full-frame cleanup operations, +including 8,186 additions and 123 nonzero scalings. Exactly 78 pairs of additions +have the same ordered target and source registers. For every such pair, removing +the two endpoints while retaining the intervening word creates a defect of rank +two. Consequently, **no single addition, scaling, or other rank-one update can +replace the pair at any position among the unchanged intervening gates**. + +This is a statement about the complete rational map on arbitrary register inputs. +It allows any coefficient and any target/source for the proposed replacement. +It does not rule out changing intermediate gates, using multiple replacement +gates, exploiting restricted inputs, or resynthesizing a larger circuit. + +## Reproduce + +From the repository root, with Python 3.11 or later: + +```sh +python3 -B research/complex-ck-cleanup-fusion/verify.py +``` + +Expected: + +```text +PASS_CK_CLEANUP_RANK_TWO pairs=78 rank=2 columns=312 controls=8 +``` + +The command needs only the standard library and committed files. It performs +no network access or file writes. It checks source pins, the binding to the +selected CK specification, every cleanup register's full-frame boundary, +complete pair coverage, all 156 forward/dual witnesses, and the committed +certificate. Checks stay enabled with `python3 -O`. + +`verify.py` is the authoritative entry point for source pins and all certificate +metadata. `check_columns.py` also runs separately, without checking those pins. +It checks all 624 minor entries by +replaying 312 basis columns. This is an independent arithmetic implementation, +not an independent human review. It uses dense vectors and literal inverse +and forward scalar operations; it imports no code from the sparse conjugation +checker. The main command additionally checks the recorded support sizes and +conjugation factors. Neither implementation replays all 716 columns of the +complete supplier. Two columns suffice for each nonzero minor. + +## Exact finite statement + +Use column vectors and let an addition be +`A(t,s,a) = I + a e_t e_s^T`, with `t != s` and `a != 0`. +For a repeated pair at cleanup indices `i < j`, put + +```text +E = e_t e_s^T +M = the product of cleanup gates strictly between i and j +P = (I + b E) M (I + a E) +u = M e_t +v^T = e_s^T M^-1 +D = P M^-1 - I + = a (u + b e_t u_s) v^T + b e_t e_s^T. +``` + +Every middle gate is invertible. All additions have distinct registers, and all +scalings have a nonzero coefficient. Thus the inverse used here exists. + +Choose `r != t` with `u_r != 0` and `c != s` with `v_c != 0`. The determinant +of the minor of `D` on ordered rows `[t,r]` and columns `[s,c]` is + +```text +det D[[t,r],[s,c]] = a b u_r v_c != 0. +``` + +The expression for `D` is a sum of two rank-one matrices, so its rank is +exactly two. Such `r,c` exist for every one of the 78 pairs. The certificate +records the four minor entries, their determinant, the two exterior factors, +and the support sizes. These are rational identities and remain nonzero over +the complex numbers. + +For a proposed insertion position, split the unchanged middle word as `M=Y X`. +A replacement `R` would have to satisfy `P=Y R X`, hence + +```text +R - I = Y^-1 (P - M) X^-1. +``` + +Multiplying by invertible matrices preserves rank. Therefore `rank(R-I)=2` at +every insertion position. A single addition or scaling has `rank(R-I) <= 1`, +so it cannot work. This also excludes arbitrary rank-one updates, which are +more permissive than the supplier's actual scalar gate set. + +The backward orientation replaces each chronological gate by its inverse +transpose, keeping the gate order. The checker recomputes the witnesses in that +orientation rather than assuming the forward minors also work. Independently, +`P^-T - M^-T = P^-T (M-P)^T M^-T` shows that the defect rank is preserved. + +For example, pair `[17,24]` consists of additions from register 236 to register +230 with coefficients `-2` and `1`. The forward minor on rows `[230,231]` and +columns `[236,230]` is + +```text +[-1 1] +[ 2 -1] +``` + +Its determinant is `-1`. The corresponding dual minor also has determinant +`-1`. All indices are zero-based within the pinned cleanup list. + +## Experiment and coverage + +OS randomness produced assignment seed **20**, selecting the complex-supplier +track and, by parity, CK rather than JP8. The three candidate tasks were factory +resynthesis, B-frame reassignment, and cleanup pair fusion. Concurrent #681 and +#698 already cover the first two, so this experiment uses the cleanup circuit. + +The initial test allowed moving an addition across individually commuting gates +to merge it with another addition on the same ordered registers. All 78 pairs +have blockers. That failed search alone says nothing about collective +cancellation within the middle word. The one refinement was to compute the +complete conjugated shear and an exact rank minor. It proves the stronger +fixed-middle obstruction above, including middle words whose individual gates +do not commute with the endpoint. + +The completed domain consists of **every pair of distinct additions with the +same ordered target and source in this one cleanup word**, with both +orientations checked. Pair generation stops after exhausting the list. There +is no sampling, timeout, or random search beyond the assignment choice. No +fixed-point fusion pass is needed because no first fusion in this class exists. +Pairs with different endpoint registers are outside this domain. + +Even granting a replacement arbitrary coefficients, an arbitrary rank-one map, +and free placement/source access does not overcome the rank defect. No proposed +circuit reaches the cost-accounting stage. Frame changes, wrappers, restoration, +recursive children, ownership, and the selected bit supplier therefore retain +their original costs. Cleanup arithmetic simplification alone would not change +the recursive rank histogram in any case. + +## Controls + +Five semantic controls check the distinction between a blocker and a proof: + +- A commuting middle addition permits a rank-one combined update. +- A noncommuting source scaling by two still permits a combined coefficient + `3/2`; it must not be classified as a rank-two obstruction. +- A reverse-direction middle addition has the exact minor determinant `-1`. +- Opposite endpoint coefficients around that middle addition do not cancel. +- Two inverse middle additions cancel collectively and permit fusion, despite + each being an individual commutation blocker. + +The direct-column checker also rejects three altered certificates: a changed +minor entry, a flipped dual endpoint coefficient, and an omitted pair. A +recomputed certificate must match every field of the committed evidence. + +## Provenance, relation to other work, and limits + +Base commit: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +The accepted result at this base is conditional +`kappa=51110230636731/31250000000000000`, from #626 with #543. +The actual construction and scope are identified by +[the selected record](../../certificates/selected-result.json) and +[the maintainer review](../../docs/research/community-k492-review.md). +[SOURCES.json](SOURCES.json) records exact dependency heads and file hashes. +The compressed word is bound by its decompressed-payload hash, so gzip metadata +and compression versions do not affect equality. + +Credit belongs to Jeremy Kothe's #622 K-triangle construction, Chafik Boukhalfa's +#626 selected owner package, DreamingOfClouds' cold-helper and native-verifier +work, icekylinx's scalar factory/direct-delivery lineage, Dugongue's coordinate +and rank-sector work, eumemic's retained #543 bit supplier, and the predecessors +credited in the selected review. The original source files and notices remain +unchanged. + +Related pending work is credited without treating its titles as accepted results: + +- Evan McKinney's [#271](https://github.com/CrocSwap/integer-mult-bounds/pull/271) + simplifies bit cleanup sandwiches and changes helper endpoints. Its field, + circuit, and allowed rewrite differ from this fixed complex cleanup test. +- eumemic's [#411](https://github.com/CrocSwap/integer-mult-bounds/pull/411) + resynthesizes complex target prefixes and recomputes dirty responses. +- [#681](https://github.com/CrocSwap/integer-mult-bounds/pull/681) resynthesizes an + eight-register raw factory window. This does not contradict the narrower + two-endpoint, unchanged-middle obstruction. +- [#687](https://github.com/CrocSwap/integer-mult-bounds/pull/687) examines raw + K-triangle read relocation; [#698](https://github.com/CrocSwap/integer-mult-bounds/pull/698) + optimizes B frames at fixed gate order; [#696](https://github.com/CrocSwap/integer-mult-bounds/pull/696) + lowers the primitives implementing unchanged complex macros. +- Concurrent [#710](https://github.com/CrocSwap/integer-mult-bounds/pull/710), + prepared for Sagar Thakrar with Codex assistance, uses exact conjugation to + shorten the bit supplier's R420 cleanup. It was discovered during the final + overlap refresh. Its joint two-sandwich rewrite over F2 changes five gates + to three; this rational CK census excludes only two endpoints becoming one + update with their middle fixed. The two results are compatible. + +None of those pending packages is imported or needed to reproduce this result. +The accepted providers, `upstream/`, selected frontier, and global accounting +are unchanged. No optimality claim is made for CK, JP8, the whole cleanup word, +or broader circuit synthesis. All-size compilation, common-label and +mutable-basis realization, hosting, residual, precision/tape, recovery, and +analytic-transfer assumptions of the selected construction remain inherited. +This finite certificate and written rank argument are not a Lean proof or a +verification of the complete multiplication theorem. + +Prepared for **@thakrarsagar**, with substantial **OpenAI Codex assistance** in +research, code, mathematical analysis, verification, and writing. A second Codex +agent supplied the independent column implementation and reviewed the rank +argument. New material is under the repository's [Apache-2.0 license](../../LICENSE). diff --git a/research/complex-ck-cleanup-fusion/SOURCES.json b/research/complex-ck-cleanup-fusion/SOURCES.json new file mode 100644 index 0000000000..1a06af3cc8 --- /dev/null +++ b/research/complex-ck-cleanup-fusion/SOURCES.json @@ -0,0 +1,13 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "selected_pr626_head": "660de893d27bb7abd1d5b01b1640207528a5c851", + "reviewed_pr622_head": "f69477f4f6d3c7eb1f740b166881bffed4ffa9f6", + "retained_pr543_head": "2065fe4f72a914d907f1046603f5a36f17018535", + "files": { + "certificates/selected-result.json": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53", + "research/complex-k492-owner-repair/data/SPEC.json": "2a2577ac526535826fed9d5f7f83f6e2e0ec058a146c64f7286720b995fa2323", + "research/complex-k492-owner-repair/code/hpe_emit_local.py": "7e4a6fbc38c8228157b6311457d1496bf460291393043932d2c365f004f77805", + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/CANONICAL-WORD.json.gz": "9bbc75dede090cfd7a0a0252424ea9d9f6211e2350d2a801d4e4f2f0784167c7" + }, + "hash_convention": "SHA256 of exact file bytes; for .gz, SHA256 of the decompressed payload." +} diff --git a/research/complex-ck-cleanup-fusion/VALIDATION.md b/research/complex-ck-cleanup-fusion/VALIDATION.md new file mode 100644 index 0000000000..ebaca30e07 --- /dev/null +++ b/research/complex-ck-cleanup-fusion/VALIDATION.md @@ -0,0 +1,61 @@ +# Validation receipt + +Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +Local environment: macOS 26.5.2 arm64; Python 3.14.8 and Python 3.11.15. +Verification started at approximately 2026-10-13 04:39 UTC, after the completed +bounded experiment and before submission. The original maximum work budget +was 50 minutes, with completion permitted earlier. + +Passed: + +- `python3 -B research/complex-ck-cleanup-fusion/verify.py`. +- `python3 -O -B research/complex-ck-cleanup-fusion/verify.py`, with all checks + still active. Both print `PASS_CK_CLEANUP_RANK_TWO pairs=78 rank=2 columns=312 controls=8`. +- Independent direct-column checker, including optimized Python execution: + 78 pairs, both orientations, 312 columns, 624 exact minor entries. +- Python 3.11.15 optimized replay from a minimal temporary checkout containing + only this package and the four pinned inputs, at a path containing spaces, + invoked while the working directory was `/`. +- Recompressing the input with gzip level 1 and a different timestamp preserves + acceptance. Changing the decompressed input, supplier SPEC bytes, or certificate + support metadata causes rejection in the temporary checkout. +- `make selected-record-check` passes with the unchanged accepted rational kappa, + source inventory, and proof-supplement checks. +- Staged whitespace checks and local documentation links pass. The diff contains + only this package; upstream main still has the recorded base commit. + +The package's five semantic controls and three certificate-mutation controls run +on every normal invocation. They distinguish individual commutation blockers +from complete-middle rank obstructions and detect bad minor entries, dual signs, +and coverage. Two additional Codex workers reviewed the same narrowly claimed +scope. One supplied the independent arithmetic implementation; another reported +no mathematical or code blocker for the full-register-space statement. This is +AI-assisted review, not independent human review. + +The full repository `make verify`, selected cold supplier regeneration, +global invoice/assembly replay, Lean, and remote Linux CI were not run for this +isolated research addition. No selected construction, generator, production +verifier, or source input changes. The result does not claim a faster +implementation, smaller recursive moment, or larger kappa. + +Final overlap review inspected 531 open PRs through #712 and refreshed the pinned +issue query, which remained empty. In particular, #710's new bit-cleanup +conjugation construction is credited in the README and does not establish the +CK rank-two census. #705 concerns determinant obstructions for Clifford register +paths and is a different search class. Exact inspected heads for related work: + +| PR | Head | +| --- | --- | +| #271 | `ebc1defe8c13f39f86e5901c3437c1be52886a2b` | +| #411 | `f58d95f2c5da03445e704ea9c72cc55df9e68190` | +| #681 | `80d4edbc2d53f058787cb5c43bd0fc22c7e7fdff` | +| #687 | `82bbb9c3ac34540f196410d137ebc59d9c2c43a9` | +| #696 | `5a3f983715027c4fd83f50bc9001d4b18463bed1` | +| #698 | `ab78f797cffcbeddbb17a7eb069741085ffe3351` | +| #705 | `eeb0cd605415a73b792915aaa9185000f293c84a` | +| #710 | `d97c8d20a8b885271a24c5a4e8446ac7f5697d5c` | + +An immediate pre-submission refresh covered 535 open PRs through #716. +#713/#716 concern R420 target-basis compensation; #714 concerns clean product-shear +checkpoints; #715 concerns mixed E8 ports. None studies this fixed CK cleanup +pair domain. diff --git a/research/complex-ck-cleanup-fusion/check_columns.py b/research/complex-ck-cleanup-fusion/check_columns.py new file mode 100644 index 0000000000..8056842e36 --- /dev/null +++ b/research/complex-ck-cleanup-fusion/check_columns.py @@ -0,0 +1,116 @@ +#!/usr/bin/env python3 +"""Independently replay the two columns of every recorded cleanup minor.""" + +import argparse +import gzip +import json +from fractions import Fraction +from itertools import combinations +from pathlib import Path + + +SOURCE = Path('research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/CANONICAL-WORD.json.gz') + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def apply(gate, column, inverse=False): + if gate[0] == 'add': + q = Fraction(gate[3], gate[4]) + column[gate[1]] += (-q if inverse else q) * column[gate[2]] + elif gate[0] == 'scale': + q = Fraction(gate[2], gate[3]) + require(q != 0, 'noninvertible middle scale') + column[gate[1]] *= 1 / q if inverse else q + else: + raise ValueError('unexpected cleanup gate') + + +def difference_column(word, i, j, column_index, n): + column = [Fraction(0) for _ in range(n)] + column[column_index] = Fraction(1) + for gate in reversed(word[i + 1:j]): + apply(gate, column, inverse=True) + for gate in word[i:j + 1]: + apply(gate, column) + column[column_index] -= 1 + return column + + +def dual_gate(gate): + if gate[0] == 'add': + return ['add', gate[2], gate[1], -gate[3], gate[4], gate[5]] + return ['scale', gate[1], gate[3], gate[2], gate[4]] + + +def self_check(): + add = ['add', 0, 1, 1, 1, 1] + middle = ['add', 1, 0, 1, 1, 1] + word = [add, middle, add] + require(difference_column(word, 0, 2, 0, 2) == [-2, -1], 'rank-two control column 0') + require(difference_column(word, 0, 2, 1, 2) == [3, 1], 'rank-two control column 1') + dual = [dual_gate(gate) for gate in word] + require(difference_column(dual, 0, 2, 0, 2) == [1, -3], 'dual control column 0') + require(difference_column(dual, 0, 2, 1, 2) == [1, -2], 'dual control column 1') + word = [add, ['scale', 1, 2, 1, 1], add] + require(difference_column(word, 0, 2, 0, 2) == [0, 0], 'scale control column 0') + require(difference_column(word, 0, 2, 1, 2) == [Fraction(3, 2), 0], 'scale control column 1') + + +def verify(root, certificate): + self_check() + with gzip.open(Path(root) / SOURCE, 'rt') as stream: + source = json.load(stream) + word = source['cleanup'] + n = 2 * source['v'] + source['R'] + groups = {} + for index, gate in enumerate(word): + require(gate[0] in ('add', 'scale'), 'unexpected cleanup gate') + require(len(gate) == (6 if gate[0] == 'add' else 5), 'unexpected gate shape') + registers = gate[1:3] if gate[0] == 'add' else gate[1:2] + require(all(type(r) is int and 0 <= r < n for r in registers), 'invalid register') + require(gate[-1] == 1, 'cleanup gate outside full frame') + if gate[0] == 'add': + require(gate[1] != gate[2] and Fraction(gate[3], gate[4]) != 0, 'invalid addition') + groups.setdefault(tuple(gate[1:3]), []).append(index) + else: + require(Fraction(gate[2], gate[3]) != 0, 'noninvertible scale') + expected = sorted(pair for group in groups.values() for pair in combinations(group, 2)) + pairs = certificate['pairs'] + require(sorted((p['i'], p['j']) for p in pairs) == expected, 'incomplete or duplicated pair coverage') + words = (word, [dual_gate(gate) for gate in word]) + for pair in pairs: + i, j = pair['i'], pair['j'] + for record, oriented_word in zip((pair, pair['dual']), words): + first, last = oriented_word[i], oriented_word[j] + t, s = record['t'], record['s'] + require(first[1:3] == last[1:3] == [t, s], 'endpoint registers differ') + require(Fraction(record['a']) == Fraction(first[3], first[4]), 'first coefficient differs') + require(Fraction(record['b']) == Fraction(last[3], last[4]), 'last coefficient differs') + rows, columns = record['rows'], record['columns'] + require(len(rows) == len(columns) == 2, 'minor must be two by two') + require(rows[0] == t and columns[0] == s, 'minor anchor differs') + require(rows[1] != t and columns[1] != s, 'minor indices repeat') + require(all(type(r) is int and 0 <= r < n for r in rows + columns), 'invalid minor index') + replayed = [difference_column(oriented_word, i, j, c, n) for c in columns] + minor = [[replayed[c][r] for c in range(2)] for r in rows] + declared = [[Fraction(value) for value in row] for row in record['minor']] + require(minor == declared, f'minor entries differ for pair {i}, {j}') + determinant = minor[0][0] * minor[1][1] - minor[0][1] * minor[1][0] + require(determinant != 0, f'zero minor for pair {i}, {j}') + require(determinant == Fraction(record['determinant']), f'determinant differs for pair {i}, {j}') + # Direct columns check the minor, not the conjugation-vector support counts. + return 4 * len(pairs) + + +if __name__ == '__main__': + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('certificate', nargs='?', type=Path, default=Path(__file__).with_name('CERTIFICATE.json')) + arguments = parser.parse_args() + with arguments.certificate.open() as stream: + certificate = json.load(stream) + count = verify(Path(__file__).resolve().parents[2], certificate) + print(f'PASS independent direct-column replay: {count // 4} pairs, {count} columns, {2 * count} minor entries in both orientations') diff --git a/research/complex-ck-cleanup-fusion/verify.py b/research/complex-ck-cleanup-fusion/verify.py new file mode 100644 index 0000000000..498d7f5079 --- /dev/null +++ b/research/complex-ck-cleanup-fusion/verify.py @@ -0,0 +1,192 @@ +"""Exact rank-two obstructions to fusing repeated CK cleanup additions. + +Apache-2.0. Prepared for @thakrarsagar with substantial OpenAI Codex assistance. +The supplier sources and contributors are credited in README.md. +""" + +import argparse +import copy +import gzip +import hashlib +import json +from collections import Counter +from fractions import Fraction as Q +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +WORD = "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/CANONICAL-WORD.json.gz" + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def load_word(): + pins = json.loads((HERE / "SOURCES.json").read_text()) + for name, expected in pins["files"].items(): + data = (ROOT / name).read_bytes() + if name.endswith(".gz"): + data = gzip.decompress(data) + require(hashlib.sha256(data).hexdigest() == expected, "source pin: " + name) + word = json.loads(gzip.decompress((ROOT / WORD).read_bytes())) + selected = json.loads((ROOT / "certificates/selected-result.json").read_text()) + require(selected["audited_source_head"] == pins["selected_pr626_head"], "selected head binding") + require(selected["reviewed_dependency_heads"]["622"] == pins["reviewed_pr622_head"], "PR622 head binding") + require(selected["reviewed_dependency_heads"]["543"] == pins["retained_pr543_head"], "PR543 head binding") + spec = json.loads((ROOT / "research/complex-k492-owner-repair/data/SPEC.json").read_text()) + require(spec["providers"]["ck"]["artifact_semantic_sha256"]["CANONICAL-WORD.json.gz"] + == pins["files"][WORD], "CK SPEC binding") + n = 2 * word["v"] + word["R"] + for op in word["cleanup"]: + require(op[0] in ("add", "scale"), "unexpected cleanup operation") + require(len(op) == (6 if op[0] == "add" else 5), "operation shape") + regs = op[1:3] if op[0] == "add" else op[1:2] + require(all(isinstance(r, int) and 0 <= r < n for r in regs), "register range") + require(op[-1] == 1 and all(word["final"][r] == 1 for r in regs), "full-frame cleanup") + require(op[0] != "add" or op[1] != op[2], "aliased addition") + q = Q(*op[3:5]) if op[0] == "add" else Q(*op[2:4]) + require(q != 0, "zero addition or singular scale") + return word + + +def put(vector, index, value): + if value: + vector[index] = value + else: + vector.pop(index, None) + + +def conjugate(middle, target, source): + """Return M e_target and e_source^T M^-1 without constructing M.""" + u, v = {target: Q(1)}, {source: Q(1)} + for op in middle: + x = op[1] + if op[0] == "add": + y, q = op[2], Q(*op[3:5]) + put(u, x, u.get(x, 0) + q * u.get(y, 0)) + put(v, y, v.get(y, 0) - q * v.get(x, 0)) + else: + q = Q(*op[2:4]) + put(u, x, q * u.get(x, 0)) + put(v, x, v.get(x, 0) / q) + return u, v + + +def dual(op): + if op[0] == "add": + return ["add", op[2], op[1], -op[3], op[4], op[5]] + return ["scale", op[1], op[3], op[2], op[4]] + + +def rank_two_witness(middle, t, s, a, b): + u, v = conjugate(middle, t, s) + rows = sorted(set(u) - {t}) + columns = sorted(set(v) - {s}) + if not rows or not columns: + return None + r, c = rows[0], columns[0] + + def entry(x, y): + shifted = u.get(x, 0) + (b * u.get(s, 0) if x == t else 0) + return a * shifted * v.get(y, 0) + (b if (x, y) == (t, s) else 0) + + minor = [[entry(x, y) for y in (s, c)] for x in (t, r)] + determinant = minor[0][0] * minor[1][1] - minor[0][1] * minor[1][0] + require(determinant == a * b * u[r] * v[c] != 0, "rank-two determinant") + return { + "rows": [t, r], "columns": [s, c], + "minor": [[str(x) for x in row] for row in minor], + "determinant": str(determinant), + "u_support": len(u), "v_support": len(v), + "u_r": str(u[r]), "v_c": str(v[c]), + } + + +def census(word): + ops = word["cleanup"] + seen, pairs = {}, [] + for j, last in enumerate(ops): + if last[0] != "add": + continue + t, s = last[1:3] + for i in seen.get((t, s), []): + a, b = Q(*ops[i][3:5]), Q(*last[3:5]) + witness = rank_two_witness(ops[i + 1:j], t, s, a, b) + require(witness is not None, f"unresolved pair: {i},{j}") + reflected = rank_two_witness([dual(op) for op in ops[i + 1:j]], s, t, -a, -b) + require(reflected is not None, f"unresolved dual pair: {i},{j}") + pairs.append({"i": i, "j": j, "t": t, "s": s, + "a": str(a), "b": str(b), **witness, + "dual": {"t": s, "s": t, "a": str(-a), "b": str(-b), **reflected}}) + seen.setdefault((t, s), []).append(j) + return { + "schema": "ck-cleanup-rank-two-v1", + "assignment_seed": 20, + "word": WORD, + "registers": 2 * word["v"] + word["R"], + "cleanup_operations": len(ops), + "cleanup_counts": dict(sorted(Counter(op[0] for op in ops).items())), + "same_endpoint_pairs": len(pairs), + "rank_two_pairs": len(pairs), + "pairs": pairs, + } + + +def controls(): + # A noncommuting middle gate alone does not imply a rank-two obstruction. + require(rank_two_witness([["add", 0, 2, 3, 1, 1]], 0, 1, Q(1), Q(1)) is None, + "commuting positive control") + scaled = [["scale", 1, 2, 1, 1]] + require(rank_two_witness(scaled, 0, 1, Q(1), Q(1)) is None, + "scaled-conjugation positive control") + u, v = conjugate(scaled, 0, 1) + require(u[0] * v[1] + 1 == Q(3, 2), "transported coefficient") + middle = [["add", 1, 0, 1, 1, 1]] + witness = rank_two_witness(middle, 0, 1, Q(1), Q(1)) + require(witness["minor"] == [["3", "-2"], ["1", "-1"]] + and witness["determinant"] == "-1", "rank-two control") + # Opposite endpoint coefficients do not suffice for cancellation. + require(rank_two_witness(middle, 0, 1, Q(1), Q(-1)) is not None, + "false cancellation control") + # If the whole middle is identity, local blockers must cancel collectively. + identity_middle = middle + [["add", 1, 0, -1, 1, 1]] + require(rank_two_witness(identity_middle, 0, 1, Q(1), Q(1)) is None, + "collective cancellation positive control") + return 5 + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", action="store_true", help="print regenerated certificate without writing files") + args = parser.parse_args() + result = census(load_word()) + count = controls() + if args.emit: + print(json.dumps(result, indent=2, sort_keys=True)) + return + expected = json.loads((HERE / "CERTIFICATE.json").read_text()) + require(result == expected, "certificate differs from exact recomputation") + from check_columns import verify + checked = verify(ROOT, result) + for label in ("minor", "dual coefficient", "coverage"): + mutant = copy.deepcopy(result) + if label == "minor": + mutant["pairs"][0]["minor"][0][0] = str(Q(mutant["pairs"][0]["minor"][0][0]) + 1) + elif label == "dual coefficient": + mutant["pairs"][0]["dual"]["a"] = str(-Q(mutant["pairs"][0]["dual"]["a"])) + else: + mutant["pairs"].pop() + try: + verify(ROOT, mutant) + except ValueError: + count += 1 + else: + raise ValueError("accepted invalid certificate: " + label) + print(f"PASS_CK_CLEANUP_RANK_TWO pairs={len(result['pairs'])} " + f"rank=2 columns={checked} controls={count}") + + +if __name__ == "__main__": + main()