diff --git a/research/r439-helper-triples/CERTIFICATE.json b/research/r439-helper-triples/CERTIFICATE.json new file mode 100644 index 0000000000..d26948359e --- /dev/null +++ b/research/r439-helper-triples/CERTIFICATE.json @@ -0,0 +1,8530 @@ +{ + "format": "r439-helper-triples/1", + "seed": 12, + "group": [ + { + "matrix": [ + 1, + 2, + 4 + ], + "word": [] + }, + { + "matrix": [ + 1, + 2, + 5 + ], + "word": [ + [ + 2, + 0 + ] + ] + }, + { + "matrix": [ + 1, + 2, + 6 + ], + "word": [ + [ + 2, + 1 + ] + ] + }, + { + "matrix": [ + 1, + 2, + 7 + ], + "word": [ + [ + 2, + 1 + ], + [ + 2, + 0 + ] + ] + }, + { + "matrix": [ + 1, + 3, + 4 + ], + "word": [ + [ + 1, + 0 + ] + ] + }, + { + "matrix": [ + 1, + 3, + 5 + ], + "word": [ + [ + 2, + 0 + ], + [ + 1, + 0 + ] + ] + }, + { + "matrix": [ + 1, + 3, + 6 + ], + "word": [ + [ + 2, + 1 + ], + [ + 1, + 0 + ] + ] + }, + { + "matrix": [ + 1, + 3, + 7 + ], + "word": [ + [ + 1, + 0 + ], + [ + 2, + 1 + ] + ] + }, + { + "matrix": [ + 1, + 4, + 2 + ], + "word": [ + [ + 2, + 1 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ] + ] + }, + { + "matrix": [ + 1, + 4, + 3 + ], + "word": [ + [ + 2, + 1 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ], + [ + 2, + 0 + ] + ] + }, + { + "matrix": [ + 1, + 4, + 6 + ], + "word": [ + [ + 2, + 1 + ], + [ + 1, + 2 + ] + ] + }, + { + "matrix": [ + 1, + 4, + 7 + ], + "word": [ + [ + 2, + 1 + ], + [ + 1, + 2 + ], + [ + 2, + 0 + ] + ] + }, + { + "matrix": [ + 1, + 5, + 2 + ], + "word": [ + [ + 2, + 1 + ], + [ + 2, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ] + ] + }, + { + "matrix": [ + 1, + 5, + 3 + ], + "word": [ + [ + 2, + 1 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ] + ] + }, + { + "matrix": [ + 1, + 5, + 6 + ], + "word": [ + [ + 2, + 1 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ] + ] + }, + { + "matrix": [ + 1, + 5, + 7 + ], + "word": [ + [ + 2, + 1 + ], + [ + 2, + 0 + ], + [ + 1, + 2 + ] + ] + }, + { + "matrix": [ + 1, + 6, + 2 + ], + "word": [ + [ + 1, + 2 + ], + [ + 2, + 1 + ] + ] + }, + { + "matrix": [ + 1, + 6, + 3 + ], + "word": [ + [ + 1, + 2 + ], + [ + 2, + 1 + ], + [ + 2, + 0 + ] + ] + }, + { + "matrix": [ + 1, + 6, + 4 + ], + "word": [ + [ + 1, + 2 + ] + ] + }, + { + "matrix": [ + 1, + 6, + 5 + ], + "word": [ + [ + 1, + 2 + ], + [ + 2, + 0 + ] + ] + }, + { + "matrix": [ + 1, + 7, + 2 + ], + "word": [ + [ + 2, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ] + ] + }, + { + "matrix": [ + 1, + 7, + 3 + ], + "word": [ + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ] + ] + }, + { + "matrix": [ + 1, + 7, + 4 + ], + "word": [ + [ + 1, + 0 + ], + [ + 1, + 2 + ] + ] + }, + { + "matrix": [ + 1, + 7, + 5 + ], + "word": [ + [ + 2, + 0 + ], + [ + 1, + 2 + ] + ] + }, + { + "matrix": [ + 2, + 1, + 4 + ], + "word": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 2, + 1, + 5 + ], + "word": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 2, + 1 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 2, + 1, + 6 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 2, + 1, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 2, + 0 + ], + [ + 1, + 0 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 2, + 3, + 4 + ], + "word": [ + [ + 1, + 0 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 2, + 3, + 5 + ], + "word": [ + [ + 2, + 0 + ], + [ + 1, + 0 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 2, + 3, + 6 + ], + "word": [ + [ + 2, + 1 + ], + [ + 1, + 0 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 2, + 3, + 7 + ], + "word": [ + [ + 1, + 0 + ], + [ + 2, + 1 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 2, + 4, + 1 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 2 + ], + [ + 2, + 0 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 2, + 4, + 3 + ], + "word": [ + [ + 2, + 1 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ], + [ + 2, + 0 + ], + [ + 0, + 2 + ] + ] + }, + { + "matrix": [ + 2, + 4, + 5 + ], + "word": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 2, + 1 + ], + [ + 0, + 1 + ], + [ + 1, + 2 + ] + ] + }, + { + "matrix": [ + 2, + 4, + 7 + ], + "word": [ + [ + 1, + 0 + ], + [ + 2, + 1 + ], + [ + 0, + 1 + ], + [ + 1, + 2 + ] + ] + }, + { + "matrix": [ + 2, + 5, + 1 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 2 + ], + [ + 2, + 0 + ], + [ + 1, + 0 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 2, + 5, + 3 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 2, + 1 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 2, + 5, + 4 + ], + "word": [ + [ + 0, + 2 + ], + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 2, + 5, + 6 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 2, + 6, + 1 + ], + "word": [ + [ + 0, + 2 + ], + [ + 2, + 0 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 2, + 6, + 3 + ], + "word": [ + [ + 1, + 2 + ], + [ + 2, + 1 + ], + [ + 2, + 0 + ], + [ + 0, + 2 + ] + ] + }, + { + "matrix": [ + 2, + 6, + 5 + ], + "word": [ + [ + 2, + 0 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 2, + 6, + 7 + ], + "word": [ + [ + 0, + 2 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ], + [ + 2, + 0 + ], + [ + 0, + 2 + ] + ] + }, + { + "matrix": [ + 2, + 7, + 1 + ], + "word": [ + [ + 0, + 2 + ], + [ + 2, + 0 + ], + [ + 1, + 0 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 2, + 7, + 3 + ], + "word": [ + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 2, + 1 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 2, + 7, + 4 + ], + "word": [ + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 2, + 7, + 6 + ], + "word": [ + [ + 0, + 2 + ], + [ + 2, + 1 + ], + [ + 1, + 0 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 3, + 1, + 4 + ], + "word": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ] + }, + { + "matrix": [ + 3, + 1, + 5 + ], + "word": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 2, + 1 + ] + ] + }, + { + "matrix": [ + 3, + 1, + 6 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ] + }, + { + "matrix": [ + 3, + 1, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 2, + 0 + ], + [ + 1, + 0 + ] + ] + }, + { + "matrix": [ + 3, + 2, + 4 + ], + "word": [ + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 3, + 2, + 5 + ], + "word": [ + [ + 2, + 0 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 3, + 2, + 6 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 3, + 2, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 2, + 0 + ] + ] + }, + { + "matrix": [ + 3, + 4, + 1 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 2 + ], + [ + 2, + 0 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 3, + 4, + 2 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 1 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ] + ] + }, + { + "matrix": [ + 3, + 4, + 5 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 1 + ], + [ + 1, + 2 + ], + [ + 2, + 0 + ] + ] + }, + { + "matrix": [ + 3, + 4, + 6 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 1 + ], + [ + 1, + 2 + ] + ] + }, + { + "matrix": [ + 3, + 5, + 1 + ], + "word": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ] + ] + }, + { + "matrix": [ + 3, + 5, + 2 + ], + "word": [ + [ + 0, + 1 + ], + [ + 2, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ] + ] + }, + { + "matrix": [ + 3, + 5, + 4 + ], + "word": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ] + ] + }, + { + "matrix": [ + 3, + 5, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 2, + 0 + ], + [ + 1, + 2 + ] + ] + }, + { + "matrix": [ + 3, + 6, + 1 + ], + "word": [ + [ + 0, + 2 + ], + [ + 1, + 2 + ], + [ + 2, + 0 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 3, + 6, + 2 + ], + "word": [ + [ + 0, + 1 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ] + ] + }, + { + "matrix": [ + 3, + 6, + 4 + ], + "word": [ + [ + 0, + 1 + ], + [ + 1, + 2 + ] + ] + }, + { + "matrix": [ + 3, + 6, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 1, + 2 + ], + [ + 2, + 0 + ] + ] + }, + { + "matrix": [ + 3, + 7, + 1 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ] + ] + }, + { + "matrix": [ + 3, + 7, + 2 + ], + "word": [ + [ + 2, + 0 + ], + [ + 0, + 1 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ] + ] + }, + { + "matrix": [ + 3, + 7, + 5 + ], + "word": [ + [ + 2, + 0 + ], + [ + 0, + 1 + ], + [ + 1, + 2 + ] + ] + }, + { + "matrix": [ + 3, + 7, + 6 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ] + ] + }, + { + "matrix": [ + 4, + 1, + 2 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 0, + 2 + ], + [ + 0, + 1 + ], + [ + 2, + 0 + ] + ] + }, + { + "matrix": [ + 4, + 1, + 3 + ], + "word": [ + [ + 0, + 2 + ], + [ + 2, + 1 + ], + [ + 2, + 0 + ], + [ + 1, + 2 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 4, + 1, + 6 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 4, + 1, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 2, + 0 + ], + [ + 1, + 0 + ], + [ + 0, + 2 + ] + ] + }, + { + "matrix": [ + 4, + 2, + 1 + ], + "word": [ + [ + 0, + 2 + ], + [ + 2, + 0 + ], + [ + 0, + 2 + ] + ] + }, + { + "matrix": [ + 4, + 2, + 3 + ], + "word": [ + [ + 0, + 2 + ], + [ + 0, + 1 + ], + [ + 2, + 0 + ], + [ + 0, + 2 + ] + ] + }, + { + "matrix": [ + 4, + 2, + 5 + ], + "word": [ + [ + 2, + 0 + ], + [ + 0, + 2 + ] + ] + }, + { + "matrix": [ + 4, + 2, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 2, + 0 + ], + [ + 0, + 2 + ] + ] + }, + { + "matrix": [ + 4, + 3, + 1 + ], + "word": [ + [ + 0, + 2 + ], + [ + 2, + 0 + ], + [ + 0, + 2 + ], + [ + 1, + 2 + ] + ] + }, + { + "matrix": [ + 4, + 3, + 2 + ], + "word": [ + [ + 2, + 1 + ], + [ + 1, + 0 + ], + [ + 0, + 2 + ], + [ + 0, + 1 + ], + [ + 2, + 0 + ] + ] + }, + { + "matrix": [ + 4, + 3, + 5 + ], + "word": [ + [ + 2, + 0 + ], + [ + 1, + 0 + ], + [ + 0, + 2 + ] + ] + }, + { + "matrix": [ + 4, + 3, + 6 + ], + "word": [ + [ + 2, + 1 + ], + [ + 1, + 0 + ], + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 4, + 5, + 2 + ], + "word": [ + [ + 2, + 1 + ], + [ + 2, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 4, + 5, + 3 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 2, + 1 + ], + [ + 0, + 2 + ] + ] + }, + { + "matrix": [ + 4, + 5, + 6 + ], + "word": [ + [ + 2, + 1 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 4, + 5, + 7 + ], + "word": [ + [ + 2, + 1 + ], + [ + 2, + 0 + ], + [ + 1, + 2 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 4, + 6, + 1 + ], + "word": [ + [ + 0, + 2 + ], + [ + 2, + 0 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ] + ] + }, + { + "matrix": [ + 4, + 6, + 3 + ], + "word": [ + [ + 2, + 0 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 2, + 1 + ] + ] + }, + { + "matrix": [ + 4, + 6, + 5 + ], + "word": [ + [ + 2, + 0 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ] + ] + }, + { + "matrix": [ + 4, + 6, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 2, + 0 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ] + ] + }, + { + "matrix": [ + 4, + 7, + 1 + ], + "word": [ + [ + 0, + 2 + ], + [ + 2, + 0 + ], + [ + 1, + 0 + ], + [ + 0, + 2 + ] + ] + }, + { + "matrix": [ + 4, + 7, + 2 + ], + "word": [ + [ + 2, + 0 + ], + [ + 0, + 2 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ] + ] + }, + { + "matrix": [ + 4, + 7, + 5 + ], + "word": [ + [ + 2, + 0 + ], + [ + 0, + 2 + ], + [ + 1, + 2 + ] + ] + }, + { + "matrix": [ + 4, + 7, + 6 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 5, + 1, + 2 + ], + "word": [ + [ + 2, + 1 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ], + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ] + }, + { + "matrix": [ + 5, + 1, + 3 + ], + "word": [ + [ + 0, + 2 + ], + [ + 2, + 1 + ], + [ + 2, + 0 + ], + [ + 1, + 2 + ] + ] + }, + { + "matrix": [ + 5, + 1, + 6 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 0, + 2 + ] + ] + }, + { + "matrix": [ + 5, + 1, + 7 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 0, + 2 + ], + [ + 2, + 1 + ] + ] + }, + { + "matrix": [ + 5, + 2, + 1 + ], + "word": [ + [ + 0, + 2 + ], + [ + 2, + 0 + ] + ] + }, + { + "matrix": [ + 5, + 2, + 3 + ], + "word": [ + [ + 0, + 2 + ], + [ + 2, + 1 + ], + [ + 2, + 0 + ] + ] + }, + { + "matrix": [ + 5, + 2, + 4 + ], + "word": [ + [ + 0, + 2 + ] + ] + }, + { + "matrix": [ + 5, + 2, + 6 + ], + "word": [ + [ + 0, + 2 + ], + [ + 2, + 1 + ] + ] + }, + { + "matrix": [ + 5, + 3, + 1 + ], + "word": [ + [ + 0, + 2 + ], + [ + 2, + 0 + ], + [ + 1, + 2 + ] + ] + }, + { + "matrix": [ + 5, + 3, + 2 + ], + "word": [ + [ + 0, + 2 + ], + [ + 2, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ] + ] + }, + { + "matrix": [ + 5, + 3, + 4 + ], + "word": [ + [ + 1, + 0 + ], + [ + 0, + 2 + ] + ] + }, + { + "matrix": [ + 5, + 3, + 7 + ], + "word": [ + [ + 1, + 0 + ], + [ + 0, + 2 + ], + [ + 2, + 1 + ] + ] + }, + { + "matrix": [ + 5, + 4, + 2 + ], + "word": [ + [ + 2, + 1 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 5, + 4, + 3 + ], + "word": [ + [ + 2, + 1 + ], + [ + 1, + 2 + ], + [ + 0, + 1 + ], + [ + 2, + 0 + ] + ] + }, + { + "matrix": [ + 5, + 4, + 6 + ], + "word": [ + [ + 2, + 1 + ], + [ + 1, + 2 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 5, + 4, + 7 + ], + "word": [ + [ + 2, + 1 + ], + [ + 1, + 2 + ], + [ + 2, + 0 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 5, + 6, + 1 + ], + "word": [ + [ + 0, + 2 + ], + [ + 1, + 2 + ], + [ + 2, + 0 + ] + ] + }, + { + "matrix": [ + 5, + 6, + 2 + ], + "word": [ + [ + 0, + 2 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ] + ] + }, + { + "matrix": [ + 5, + 6, + 4 + ], + "word": [ + [ + 0, + 2 + ], + [ + 1, + 2 + ] + ] + }, + { + "matrix": [ + 5, + 6, + 7 + ], + "word": [ + [ + 0, + 2 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ], + [ + 2, + 0 + ] + ] + }, + { + "matrix": [ + 5, + 7, + 1 + ], + "word": [ + [ + 0, + 2 + ], + [ + 2, + 0 + ], + [ + 1, + 0 + ] + ] + }, + { + "matrix": [ + 5, + 7, + 3 + ], + "word": [ + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 2, + 1 + ] + ] + }, + { + "matrix": [ + 5, + 7, + 4 + ], + "word": [ + [ + 0, + 2 + ], + [ + 1, + 0 + ] + ] + }, + { + "matrix": [ + 5, + 7, + 6 + ], + "word": [ + [ + 0, + 2 + ], + [ + 2, + 1 + ], + [ + 1, + 0 + ] + ] + }, + { + "matrix": [ + 6, + 1, + 2 + ], + "word": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 0, + 2 + ], + [ + 0, + 1 + ], + [ + 2, + 0 + ] + ] + }, + { + "matrix": [ + 6, + 1, + 3 + ], + "word": [ + [ + 0, + 2 + ], + [ + 2, + 1 + ], + [ + 2, + 0 + ], + [ + 0, + 2 + ], + [ + 1, + 2 + ] + ] + }, + { + "matrix": [ + 6, + 1, + 4 + ], + "word": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 6, + 1, + 5 + ], + "word": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 2, + 1 + ], + [ + 0, + 2 + ] + ] + }, + { + "matrix": [ + 6, + 2, + 1 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 2 + ], + [ + 2, + 0 + ], + [ + 0, + 2 + ] + ] + }, + { + "matrix": [ + 6, + 2, + 3 + ], + "word": [ + [ + 0, + 2 + ], + [ + 2, + 1 + ], + [ + 2, + 0 + ], + [ + 0, + 2 + ] + ] + }, + { + "matrix": [ + 6, + 2, + 5 + ], + "word": [ + [ + 2, + 0 + ], + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 6, + 2, + 7 + ], + "word": [ + [ + 2, + 1 + ], + [ + 2, + 0 + ], + [ + 0, + 2 + ] + ] + }, + { + "matrix": [ + 6, + 3, + 1 + ], + "word": [ + [ + 0, + 2 + ], + [ + 2, + 0 + ], + [ + 1, + 2 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 6, + 3, + 2 + ], + "word": [ + [ + 1, + 0 + ], + [ + 0, + 2 + ], + [ + 0, + 1 + ], + [ + 2, + 0 + ] + ] + }, + { + "matrix": [ + 6, + 3, + 4 + ], + "word": [ + [ + 1, + 0 + ], + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 6, + 3, + 7 + ], + "word": [ + [ + 1, + 0 + ], + [ + 2, + 1 + ], + [ + 0, + 2 + ] + ] + }, + { + "matrix": [ + 6, + 4, + 1 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 2 + ], + [ + 2, + 0 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ] + ] + }, + { + "matrix": [ + 6, + 4, + 3 + ], + "word": [ + [ + 2, + 1 + ], + [ + 2, + 0 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 2, + 1 + ] + ] + }, + { + "matrix": [ + 6, + 4, + 5 + ], + "word": [ + [ + 2, + 0 + ], + [ + 0, + 2 + ], + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ] + }, + { + "matrix": [ + 6, + 4, + 7 + ], + "word": [ + [ + 2, + 1 + ], + [ + 2, + 0 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ] + ] + }, + { + "matrix": [ + 6, + 5, + 1 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 2 + ], + [ + 2, + 0 + ], + [ + 1, + 0 + ], + [ + 0, + 2 + ] + ] + }, + { + "matrix": [ + 6, + 5, + 2 + ], + "word": [ + [ + 2, + 1 + ], + [ + 2, + 0 + ], + [ + 0, + 2 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ] + ] + }, + { + "matrix": [ + 6, + 5, + 4 + ], + "word": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 6, + 5, + 7 + ], + "word": [ + [ + 2, + 1 + ], + [ + 2, + 0 + ], + [ + 0, + 2 + ], + [ + 1, + 2 + ] + ] + }, + { + "matrix": [ + 6, + 7, + 2 + ], + "word": [ + [ + 2, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 6, + 7, + 3 + ], + "word": [ + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 2, + 1 + ], + [ + 0, + 2 + ] + ] + }, + { + "matrix": [ + 6, + 7, + 4 + ], + "word": [ + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 6, + 7, + 5 + ], + "word": [ + [ + 2, + 0 + ], + [ + 1, + 2 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 7, + 1, + 2 + ], + "word": [ + [ + 1, + 2 + ], + [ + 2, + 1 + ], + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ] + }, + { + "matrix": [ + 7, + 1, + 3 + ], + "word": [ + [ + 0, + 2 + ], + [ + 0, + 1 + ], + [ + 2, + 0 + ], + [ + 1, + 2 + ] + ] + }, + { + "matrix": [ + 7, + 1, + 4 + ], + "word": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 0, + 2 + ] + ] + }, + { + "matrix": [ + 7, + 1, + 5 + ], + "word": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 0, + 2 + ], + [ + 2, + 1 + ] + ] + }, + { + "matrix": [ + 7, + 2, + 1 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 2 + ], + [ + 2, + 0 + ] + ] + }, + { + "matrix": [ + 7, + 2, + 3 + ], + "word": [ + [ + 0, + 2 + ], + [ + 0, + 1 + ], + [ + 2, + 0 + ] + ] + }, + { + "matrix": [ + 7, + 2, + 4 + ], + "word": [ + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 7, + 2, + 6 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 2 + ] + ] + }, + { + "matrix": [ + 7, + 3, + 1 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 2 + ], + [ + 2, + 0 + ], + [ + 1, + 2 + ] + ] + }, + { + "matrix": [ + 7, + 3, + 2 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 2 + ], + [ + 2, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ] + ] + }, + { + "matrix": [ + 7, + 3, + 5 + ], + "word": [ + [ + 2, + 1 + ], + [ + 1, + 0 + ], + [ + 0, + 2 + ], + [ + 2, + 1 + ] + ] + }, + { + "matrix": [ + 7, + 3, + 6 + ], + "word": [ + [ + 2, + 1 + ], + [ + 1, + 0 + ], + [ + 0, + 2 + ] + ] + }, + { + "matrix": [ + 7, + 4, + 1 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 2 + ], + [ + 2, + 0 + ] + ] + }, + { + "matrix": [ + 7, + 4, + 2 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ] + ] + }, + { + "matrix": [ + 7, + 4, + 5 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ], + [ + 2, + 0 + ] + ] + }, + { + "matrix": [ + 7, + 4, + 6 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 2 + ] + ] + }, + { + "matrix": [ + 7, + 5, + 1 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 2 + ], + [ + 2, + 0 + ], + [ + 1, + 0 + ] + ] + }, + { + "matrix": [ + 7, + 5, + 3 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 2, + 1 + ] + ] + }, + { + "matrix": [ + 7, + 5, + 4 + ], + "word": [ + [ + 0, + 2 + ], + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ] + }, + { + "matrix": [ + 7, + 5, + 6 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ] + ] + }, + { + "matrix": [ + 7, + 6, + 2 + ], + "word": [ + [ + 1, + 2 + ], + [ + 2, + 1 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 7, + 6, + 3 + ], + "word": [ + [ + 1, + 2 + ], + [ + 0, + 1 + ], + [ + 2, + 0 + ] + ] + }, + { + "matrix": [ + 7, + 6, + 4 + ], + "word": [ + [ + 1, + 2 + ], + [ + 0, + 1 + ] + ] + }, + { + "matrix": [ + 7, + 6, + 5 + ], + "word": [ + [ + 1, + 2 + ], + [ + 2, + 0 + ], + [ + 0, + 1 + ] + ] + } + ], + "pair_count": 192, + "singleton_count": 55, + "scores": 1774080, + "positive_nominees": 935, + "census_sha256": "7984264fa942879b6d295282aecf01e4e0d075ade2529622e5e74191495fc08f", + "conflicts": 780, + "rejected": [ + { + "pair_index": 53, + "singleton": 166, + "matrix": [ + 3, + 6, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 1, + 2 + ], + [ + 2, + 0 + ] + ], + "gain": 9, + "bill": { + "F": 74945, + "B": 10562318, + "D_adds": 5742, + "native_ADDs": 11962, + "local_expression": 3005567203716542662076735648000, + "nine_stage_expression": 7714187601942952263245616771710898445938599932579020800000 + } + }, + { + "pair_index": 53, + "singleton": 166, + "matrix": [ + 6, + 3, + 7 + ], + "word": [ + [ + 1, + 0 + ], + [ + 2, + 1 + ], + [ + 0, + 2 + ] + ], + "gain": 9, + "bill": { + "F": 74723, + "B": 10609340, + "D_adds": 5742, + "native_ADDs": 11962, + "local_expression": 3005519903652462546190616652800, + "nine_stage_expression": 7736862720180813079990144068390251077523638411455365120000 + } + }, + { + "pair_index": 16, + "singleton": 272, + "matrix": [ + 1, + 3, + 7 + ], + "word": [ + [ + 1, + 0 + ], + [ + 2, + 1 + ] + ], + "gain": 9, + "bill": { + "F": 71915, + "B": 10584738, + "D_adds": 5742, + "native_ADDs": 11962, + "local_expression": 2666850395968941903100345824000, + "nine_stage_expression": 6329330823982492415741264666187111710293002953726361600000 + } + }, + { + "pair_index": 53, + "singleton": 166, + "matrix": [ + 7, + 6, + 3 + ], + "word": [ + [ + 1, + 2 + ], + [ + 0, + 1 + ], + [ + 2, + 0 + ] + ], + "gain": 9, + "bill": { + "F": 75227, + "B": 10562318, + "D_adds": 5742, + "native_ADDs": 11962, + "local_expression": 3039622703881186025346737746688, + "nine_stage_expression": 7860417079569811737761851518125096364989071124253384900608 + } + }, + { + "pair_index": 53, + "singleton": 166, + "matrix": [ + 7, + 3, + 6 + ], + "word": [ + [ + 2, + 1 + ], + [ + 1, + 0 + ], + [ + 0, + 2 + ] + ], + "gain": 9, + "bill": { + "F": 75953, + "B": 10562318, + "D_adds": 5742, + "native_ADDs": 11962, + "local_expression": 3128479030628835952853204156672, + "nine_stage_expression": 8247105274122125911776447350769171779196373232035920084992 + } + }, + { + "pair_index": 48, + "singleton": 56, + "matrix": [ + 7, + 2, + 4 + ], + "word": [ + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ], + "gain": 9, + "bill": { + "F": 71983, + "B": 10562318, + "D_adds": 5733, + "native_ADDs": 11953, + "local_expression": 2663104932766740964819477618432, + "nine_stage_expression": 6305602496524166352204066295877237706178843572738658926592 + } + }, + { + "pair_index": 83, + "singleton": 204, + "matrix": [ + 5, + 3, + 7 + ], + "word": [ + [ + 1, + 0 + ], + [ + 0, + 2 + ], + [ + 2, + 1 + ] + ], + "gain": 7, + "bill": { + "F": 72587, + "B": 10555708, + "D_adds": 5719, + "native_ADDs": 11939, + "local_expression": 2727289574747690083046141938688, + "nine_stage_expression": 6558184511961589783478729448216484742897501616070216122368 + } + }, + { + "pair_index": 55, + "singleton": 177, + "matrix": [ + 3, + 2, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 2, + 0 + ] + ], + "gain": 7, + "bill": { + "F": 72027, + "B": 10562318, + "D_adds": 5719, + "native_ADDs": 11939, + "local_expression": 2667991430543138995365761004288, + "nine_stage_expression": 6324897739749038795042365884370323490799511190750372036608 + } + }, + { + "pair_index": 53, + "singleton": 166, + "matrix": [ + 6, + 7, + 3 + ], + "word": [ + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 2, + 1 + ], + [ + 0, + 2 + ] + ], + "gain": 7, + "bill": { + "F": 77471, + "B": 10639598, + "D_adds": 5719, + "native_ADDs": 11939, + "local_expression": 3368588006019785124594023042816, + "nine_stage_expression": 9374251653847536778663231182798543058655182652617370107904 + } + }, + { + "pair_index": 16, + "singleton": 272, + "matrix": [ + 1, + 7, + 3 + ], + "word": [ + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ] + ], + "gain": 7, + "bill": { + "F": 73499, + "B": 10621428, + "D_adds": 5719, + "native_ADDs": 11939, + "local_expression": 2866751733328356512472020020224, + "nine_stage_expression": 7156138070376913093413356492585516046075530472517571444736 + } + }, + { + "pair_index": 83, + "singleton": 204, + "matrix": [ + 5, + 7, + 3 + ], + "word": [ + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 2, + 1 + ] + ], + "gain": 7, + "bill": { + "F": 72539, + "B": 10555708, + "D_adds": 5712, + "native_ADDs": 11932, + "local_expression": 2721882682969461975805985229824, + "nine_stage_expression": 6536529339394509789699872256784452573793513624831394840576 + } + }, + { + "pair_index": 83, + "singleton": 204, + "matrix": [ + 3, + 7, + 5 + ], + "word": [ + [ + 2, + 0 + ], + [ + 0, + 1 + ], + [ + 1, + 2 + ] + ], + "gain": 7, + "bill": { + "F": 72491, + "B": 10555708, + "D_adds": 5712, + "native_ADDs": 11932, + "local_expression": 2716482942079616092990821026816, + "nine_stage_expression": 6514931409071605032165949106932932546222850773375751553024 + } + }, + { + "pair_index": 83, + "singleton": 204, + "matrix": [ + 3, + 5, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 2, + 0 + ], + [ + 1, + 2 + ] + ], + "gain": 7, + "bill": { + "F": 72587, + "B": 10562318, + "D_adds": 5712, + "native_ADDs": 11932, + "local_expression": 2730706309745741309193931735808, + "nine_stage_expression": 6574626927761900706056309403026532393441522876325516279808 + } + }, + { + "pair_index": 16, + "singleton": 272, + "matrix": [ + 3, + 1, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 2, + 0 + ], + [ + 1, + 0 + ] + ], + "gain": 7, + "bill": { + "F": 73499, + "B": 10595326, + "D_adds": 5712, + "native_ADDs": 11932, + "local_expression": 2852679047535759874285299950336, + "nine_stage_expression": 7086052543408344729136317766292544738016105185204456390656 + } + }, + { + "pair_index": 16, + "singleton": 272, + "matrix": [ + 7, + 3, + 6 + ], + "word": [ + [ + 2, + 1 + ], + [ + 1, + 0 + ], + [ + 0, + 2 + ] + ], + "gain": 6, + "bill": { + "F": 73499, + "B": 10591052, + "D_adds": 5713, + "native_ADDs": 11933, + "local_expression": 2850378053467050475678320978944, + "nine_stage_expression": 7074625818745059745793791118245854841767655938524809527296 + } + }, + { + "pair_index": 16, + "singleton": 272, + "matrix": [ + 6, + 3, + 7 + ], + "word": [ + [ + 1, + 0 + ], + [ + 2, + 1 + ], + [ + 0, + 2 + ] + ], + "gain": 6, + "bill": { + "F": 74315, + "B": 10583878, + "D_adds": 5707, + "native_ADDs": 11927, + "local_expression": 2942382104890905447343119584000, + "nine_stage_expression": 7455926756047407112776247133175434079329280297048473600000 + } + }, + { + "pair_index": 16, + "singleton": 272, + "matrix": [ + 7, + 6, + 3 + ], + "word": [ + [ + 1, + 2 + ], + [ + 0, + 1 + ], + [ + 2, + 0 + ] + ], + "gain": 6, + "bill": { + "F": 74015, + "B": 10591538, + "D_adds": 5695, + "native_ADDs": 11915, + "local_expression": 2911100921995471434494475104000, + "nine_stage_expression": 7327819347358570116058056267492960815797328779712921600000 + } + }, + { + "pair_index": 16, + "singleton": 272, + "matrix": [ + 3, + 6, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 1, + 2 + ], + [ + 2, + 0 + ] + ], + "gain": 6, + "bill": { + "F": 74411, + "B": 10554848, + "D_adds": 5695, + "native_ADDs": 11915, + "local_expression": 2937618292388787057102163214336, + "nine_stage_expression": 7422215516976544397294792839274676002724452778792351432704 + } + }, + { + "pair_index": 55, + "singleton": 177, + "matrix": [ + 1, + 3, + 7 + ], + "word": [ + [ + 1, + 0 + ], + [ + 2, + 1 + ] + ], + "gain": 6, + "bill": { + "F": 72163, + "B": 10523472, + "D_adds": 5695, + "native_ADDs": 11915, + "local_expression": 2663433222392521958095855337472, + "nine_stage_expression": 6291424939778413497237584397761997258939419849905460477952 + } + }, + { + "pair_index": 54, + "singleton": 164, + "matrix": [ + 7, + 2, + 4 + ], + "word": [ + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ], + "gain": 6, + "bill": { + "F": 72079, + "B": 10545944, + "D_adds": 5695, + "native_ADDs": 11915, + "local_expression": 2665490591788864528111926931456, + "nine_stage_expression": 6308491600529375811437383719586958102669863209885736370176 + } + }, + { + "pair_index": 16, + "singleton": 272, + "matrix": [ + 3, + 2, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 2, + 0 + ] + ], + "gain": 6, + "bill": { + "F": 72035, + "B": 10542618, + "D_adds": 5695, + "native_ADDs": 11915, + "local_expression": 2658934240889331381844633056000, + "nine_stage_expression": 6281329951161496427749691626483489997673233885783654400000 + } + }, + { + "pair_index": 81, + "singleton": 265, + "matrix": [ + 3, + 2, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 2, + 0 + ] + ], + "gain": 6, + "bill": { + "F": 72035, + "B": 10545630, + "D_adds": 5695, + "native_ADDs": 11915, + "local_expression": 2660453759849026481849253600000, + "nine_stage_expression": 6288511269950282143490141172316688945265291485184000000000 + } + }, + { + "pair_index": 55, + "singleton": 177, + "matrix": [ + 1, + 2, + 7 + ], + "word": [ + [ + 2, + 1 + ], + [ + 2, + 0 + ] + ], + "gain": 6, + "bill": { + "F": 72147, + "B": 10523472, + "D_adds": 5695, + "native_ADDs": 11915, + "local_expression": 2661662003748797110421463810048, + "nine_stage_expression": 6284453349699972904733465344046373124499874503546527285248 + } + }, + { + "pair_index": 162, + "singleton": 13, + "matrix": [ + 3, + 6, + 4 + ], + "word": [ + [ + 0, + 1 + ], + [ + 1, + 2 + ] + ], + "gain": 5, + "bill": { + "F": 72035, + "B": 10574036, + "D_adds": 5696, + "native_ADDs": 11916, + "local_expression": 2674805606454452292091850624000, + "nine_stage_expression": 6356541154556686333743487953593343684780162490459750400000 + } + }, + { + "pair_index": 43, + "singleton": 210, + "matrix": [ + 7, + 6, + 4 + ], + "word": [ + [ + 1, + 2 + ], + [ + 0, + 1 + ] + ], + "gain": 5, + "bill": { + "F": 72431, + "B": 10535254, + "D_adds": 5696, + "native_ADDs": 11916, + "local_expression": 2699252044830188584346043094784, + "nine_stage_expression": 6437872492403488586349831018779545851326782678276153278464 + } + }, + { + "pair_index": 43, + "singleton": 210, + "matrix": [ + 1, + 7, + 4 + ], + "word": [ + [ + 1, + 0 + ], + [ + 1, + 2 + ] + ], + "gain": 5, + "bill": { + "F": 72827, + "B": 10542896, + "D_adds": 5696, + "native_ADDs": 11916, + "local_expression": 2747749133094132501700843323392, + "nine_stage_expression": 6635012002400917627917195512490585093500608634250170728448 + } + }, + { + "pair_index": 77, + "singleton": 13, + "matrix": [ + 7, + 2, + 4 + ], + "word": [ + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ], + "gain": 5, + "bill": { + "F": 72035, + "B": 10574036, + "D_adds": 5696, + "native_ADDs": 11916, + "local_expression": 2674805606454452292091850624000, + "nine_stage_expression": 6356541154556686333743487953593343684780162490459750400000 + } + }, + { + "pair_index": 81, + "singleton": 265, + "matrix": [ + 1, + 2, + 7 + ], + "word": [ + [ + 2, + 1 + ], + [ + 2, + 0 + ] + ], + "gain": 5, + "bill": { + "F": 72035, + "B": 10545630, + "D_adds": 5696, + "native_ADDs": 11916, + "local_expression": 2660453759849026481849253600000, + "nine_stage_expression": 6288511269950282143490141172316688945265291485184000000000 + } + }, + { + "pair_index": 55, + "singleton": 177, + "matrix": [ + 2, + 3, + 7 + ], + "word": [ + [ + 1, + 0 + ], + [ + 2, + 1 + ], + [ + 0, + 1 + ] + ], + "gain": 5, + "bill": { + "F": 72195, + "B": 10534524, + "D_adds": 5696, + "native_ADDs": 11916, + "local_expression": 2672582805456248139694791552000, + "nine_stage_expression": 6331916705163861112714166301683061483299245660097740800000 + } + }, + { + "pair_index": 55, + "singleton": 177, + "matrix": [ + 7, + 2, + 3 + ], + "word": [ + [ + 0, + 2 + ], + [ + 0, + 1 + ], + [ + 2, + 0 + ] + ], + "gain": 5, + "bill": { + "F": 72203, + "B": 10533326, + "D_adds": 5696, + "native_ADDs": 11916, + "local_expression": 2672863331792341085667596534528, + "nine_stage_expression": 6332544312399256034173960647726693892277713534273131118592 + } + }, + { + "pair_index": 52, + "singleton": 13, + "matrix": [ + 3, + 6, + 4 + ], + "word": [ + [ + 0, + 1 + ], + [ + 1, + 2 + ] + ], + "gain": 5, + "bill": { + "F": 72035, + "B": 10574036, + "D_adds": 5696, + "native_ADDs": 11916, + "local_expression": 2674805606454452292091850624000, + "nine_stage_expression": 6356541154556686333743487953593343684780162490459750400000 + } + }, + { + "pair_index": 16, + "singleton": 272, + "matrix": [ + 7, + 3, + 1 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 2 + ], + [ + 2, + 0 + ], + [ + 1, + 2 + ] + ], + "gain": 5, + "bill": { + "F": 75599, + "B": 10636154, + "D_adds": 5696, + "native_ADDs": 11916, + "local_expression": 3128220517044143323711231813376, + "nine_stage_expression": 8284353901617473154593934431446012626936390730462879809536 + } + }, + { + "pair_index": 16, + "singleton": 272, + "matrix": [ + 7, + 1, + 3 + ], + "word": [ + [ + 0, + 2 + ], + [ + 0, + 1 + ], + [ + 2, + 0 + ], + [ + 1, + 2 + ] + ], + "gain": 5, + "bill": { + "F": 76787, + "B": 10620272, + "D_adds": 5696, + "native_ADDs": 11916, + "local_expression": 3268243113829393814309789155328, + "nine_stage_expression": 8902684507403181903481314376636451504652090382168094670848 + } + }, + { + "pair_index": 53, + "singleton": 228, + "matrix": [ + 1, + 3, + 7 + ], + "word": [ + [ + 1, + 0 + ], + [ + 2, + 1 + ] + ], + "gain": 4, + "bill": { + "F": 71929, + "B": 10584346, + "D_adds": 5688, + "native_ADDs": 11908, + "local_expression": 2668210558216629052591399342336, + "nine_stage_expression": 6334555538247945804009839584574335629050287231517260251136 + } + }, + { + "pair_index": 81, + "singleton": 265, + "matrix": [ + 2, + 3, + 7 + ], + "word": [ + [ + 1, + 0 + ], + [ + 2, + 1 + ], + [ + 0, + 1 + ] + ], + "gain": 4, + "bill": { + "F": 71927, + "B": 10602138, + "D_adds": 5672, + "native_ADDs": 11892, + "local_expression": 2676965164541526337178738704128, + "nine_stage_expression": 6376369367536611220888070519211123717741886312622837465088 + } + }, + { + "pair_index": 10, + "singleton": 228, + "matrix": [ + 3, + 2, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 2, + 0 + ] + ], + "gain": 4, + "bill": { + "F": 72439, + "B": 10570070, + "D_adds": 5672, + "native_ADDs": 11892, + "local_expression": 2718022452441556519730223558400, + "nine_stage_expression": 6526999921678798104316120886958535551477868763018690560000 + } + }, + { + "pair_index": 126, + "singleton": 307, + "matrix": [ + 7, + 2, + 4 + ], + "word": [ + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ], + "gain": 4, + "bill": { + "F": 71999, + "B": 10555986, + "D_adds": 5668, + "native_ADDs": 11888, + "local_expression": 2661686970648218188820601843456, + "nine_stage_expression": 6297489713773570156671534223653098614265112207393445380096 + } + }, + { + "pair_index": 65, + "singleton": 218, + "matrix": [ + 7, + 2, + 4 + ], + "word": [ + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ], + "gain": 4, + "bill": { + "F": 71975, + "B": 10571988, + "D_adds": 5664, + "native_ADDs": 11884, + "local_expression": 2667093970849063845039216000000, + "nine_stage_expression": 6325209808374065015436248010299414230378950819840000000000 + } + }, + { + "pair_index": 53, + "singleton": 228, + "matrix": [ + 3, + 2, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 2, + 0 + ] + ], + "gain": 4, + "bill": { + "F": 72439, + "B": 10670354, + "D_adds": 5664, + "native_ADDs": 11884, + "local_expression": 2769841824167892954209620416256, + "nine_stage_expression": 6778248164362044383011480581051466998486273649815674945536 + } + }, + { + "pair_index": 54, + "singleton": 164, + "matrix": [ + 2, + 7, + 4 + ], + "word": [ + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 0, + 1 + ] + ], + "gain": 4, + "bill": { + "F": 72059, + "B": 10620440, + "D_adds": 5660, + "native_ADDs": 11880, + "local_expression": 2701031730818669357235799961600, + "nine_stage_expression": 6479643546217890758375594303917082160734282744342773760000 + } + }, + { + "pair_index": 54, + "singleton": 164, + "matrix": [ + 4, + 2, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 2, + 0 + ], + [ + 0, + 2 + ] + ], + "gain": 4, + "bill": { + "F": 72279, + "B": 10867136, + "D_adds": 5660, + "native_ADDs": 11880, + "local_expression": 2853951473559768596251735228416, + "nine_stage_expression": 7212087838234817459178487759254938208086064609060030775296 + } + }, + { + "pair_index": 123, + "singleton": 412, + "matrix": [ + 7, + 2, + 4 + ], + "word": [ + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ], + "gain": 4, + "bill": { + "F": 71963, + "B": 10555986, + "D_adds": 5660, + "native_ADDs": 11880, + "local_expression": 2657696380727620016932477440768, + "nine_stage_expression": 6281761507114658873533031262454205453173006441303215439872 + } + }, + { + "pair_index": 144, + "singleton": 358, + "matrix": [ + 3, + 2, + 5 + ], + "word": [ + [ + 2, + 0 + ], + [ + 0, + 1 + ] + ], + "gain": 4, + "bill": { + "F": 72719, + "B": 10426798, + "D_adds": 5660, + "native_ADDs": 11880, + "local_expression": 2675627112058924472301058498304, + "nine_stage_expression": 6300619485117038793428056937774246661296432270302559338496 + } + }, + { + "pair_index": 81, + "singleton": 265, + "matrix": [ + 7, + 2, + 3 + ], + "word": [ + [ + 0, + 2 + ], + [ + 0, + 1 + ], + [ + 2, + 0 + ] + ], + "gain": 4, + "bill": { + "F": 71927, + "B": 10585244, + "D_adds": 5656, + "native_ADDs": 11876, + "local_expression": 2668440729596157704978664184832, + "nine_stage_expression": 6335824646537894870610365449720089445217945597623264083968 + } + }, + { + "pair_index": 43, + "singleton": 210, + "matrix": [ + 1, + 3, + 7 + ], + "word": [ + [ + 1, + 0 + ], + [ + 2, + 1 + ] + ], + "gain": 4, + "bill": { + "F": 72371, + "B": 10615872, + "D_adds": 5656, + "native_ADDs": 11876, + "local_expression": 2733915213059286567002208731136, + "nine_stage_expression": 6609756851509696879832002901790104194538885490568083800064 + } + }, + { + "pair_index": 43, + "singleton": 210, + "matrix": [ + 7, + 4, + 6 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 2 + ] + ], + "gain": 3, + "bill": { + "F": 73259, + "B": 10439118, + "D_adds": 5654, + "native_ADDs": 11874, + "local_expression": 2742145821404689729474075878144, + "nine_stage_expression": 6569012369459326972737658266759415566994526448192854163456 + } + }, + { + "pair_index": 43, + "singleton": 210, + "matrix": [ + 1, + 4, + 7 + ], + "word": [ + [ + 2, + 1 + ], + [ + 1, + 2 + ], + [ + 2, + 0 + ] + ], + "gain": 3, + "bill": { + "F": 73703, + "B": 10446760, + "D_adds": 5654, + "native_ADDs": 11874, + "local_expression": 2796396217943404633825387212800, + "nine_stage_expression": 6790350944935801159268244394060617026524482623158353920000 + } + }, + { + "pair_index": 81, + "singleton": 265, + "matrix": [ + 1, + 7, + 2 + ], + "word": [ + [ + 2, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ] + ], + "gain": 3, + "bill": { + "F": 72395, + "B": 10515494, + "D_adds": 5654, + "native_ADDs": 11874, + "local_expression": 2685128357513877449924548832000, + "nine_stage_expression": 6373845085500533042243980113110410599965606180539596800000 + } + }, + { + "pair_index": 10, + "singleton": 228, + "matrix": [ + 7, + 2, + 4 + ], + "word": [ + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ], + "gain": 3, + "bill": { + "F": 72571, + "B": 10460294, + "D_adds": 5648, + "native_ADDs": 11868, + "local_expression": 2676437330958388840688109132544, + "nine_stage_expression": 6317293055615197687816601570425525799277833842133485748224 + } + }, + { + "pair_index": 52, + "singleton": 13, + "matrix": [ + 3, + 4, + 6 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 1 + ], + [ + 1, + 2 + ] + ], + "gain": 3, + "bill": { + "F": 72563, + "B": 10641716, + "D_adds": 5648, + "native_ADDs": 11868, + "local_expression": 2769166008110749708457848245248, + "nine_stage_expression": 6763363482084059122254180159960236830884440205256936128512 + } + }, + { + "pair_index": 52, + "singleton": 13, + "matrix": [ + 6, + 3, + 4 + ], + "word": [ + [ + 1, + 0 + ], + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ], + "gain": 3, + "bill": { + "F": 72539, + "B": 10506994, + "D_adds": 5648, + "native_ADDs": 11868, + "local_expression": 2696817981186961319873329246976, + "nine_stage_expression": 6416699186834838227739982913498039455561525505506647474176 + } + }, + { + "pair_index": 22, + "singleton": 218, + "matrix": [ + 7, + 2, + 4 + ], + "word": [ + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ], + "gain": 3, + "bill": { + "F": 72587, + "B": 10460854, + "D_adds": 5648, + "native_ADDs": 11868, + "local_expression": 2678494741332255904748395772672, + "nine_stage_expression": 6325614518826389049878303495065368360030902673837966491648 + } + }, + { + "pair_index": 162, + "singleton": 13, + "matrix": [ + 6, + 3, + 4 + ], + "word": [ + [ + 1, + 0 + ], + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ], + "gain": 3, + "bill": { + "F": 72539, + "B": 10481578, + "D_adds": 5648, + "native_ADDs": 11868, + "local_expression": 2683786770693878993619499698944, + "nine_stage_expression": 6354837143540642734282257848496342145926830328535618420736 + } + }, + { + "pair_index": 43, + "singleton": 210, + "matrix": [ + 6, + 7, + 4 + ], + "word": [ + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 0, + 1 + ] + ], + "gain": 3, + "bill": { + "F": 74519, + "B": 10497876, + "D_adds": 5645, + "native_ADDs": 11865, + "local_expression": 2918662687578737796122945534976, + "nine_stage_expression": 7316119118175469486417152119891380917441591356072977760256 + } + }, + { + "pair_index": 77, + "singleton": 13, + "matrix": [ + 4, + 2, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 2, + 0 + ], + [ + 0, + 2 + ] + ], + "gain": 3, + "bill": { + "F": 72579, + "B": 10567684, + "D_adds": 5642, + "native_ADDs": 11862, + "local_expression": 2732577896707766160603053976576, + "nine_stage_expression": 6584368006459908589318510834102643881544601086250625007616 + } + }, + { + "pair_index": 77, + "singleton": 13, + "matrix": [ + 2, + 7, + 4 + ], + "word": [ + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 0, + 1 + ] + ], + "gain": 3, + "bill": { + "F": 72699, + "B": 10476772, + "D_adds": 5642, + "native_ADDs": 11862, + "local_expression": 2699108050139359106091832986624, + "nine_stage_expression": 6413455385148818504975055496096926743525292611976755675136 + } + }, + { + "pair_index": 43, + "singleton": 210, + "matrix": [ + 7, + 1, + 4 + ], + "word": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 0, + 2 + ] + ], + "gain": 3, + "bill": { + "F": 73727, + "B": 10450402, + "D_adds": 5642, + "native_ADDs": 11862, + "local_expression": 2801080921487917370027109064448, + "nine_stage_expression": 6810903428029221588750219174107353027313406247281128112128 + } + }, + { + "pair_index": 54, + "singleton": 164, + "matrix": [ + 3, + 2, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 2, + 0 + ] + ], + "gain": 3, + "bill": { + "F": 72627, + "B": 10632774, + "D_adds": 5642, + "native_ADDs": 11862, + "local_expression": 2771835518169611641651177734912, + "nine_stage_expression": 6770438224714532694865601681625487326670869677561566199808 + } + }, + { + "pair_index": 162, + "singleton": 13, + "matrix": [ + 3, + 4, + 6 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 1 + ], + [ + 1, + 2 + ] + ], + "gain": 3, + "bill": { + "F": 72563, + "B": 10482644, + "D_adds": 5642, + "native_ADDs": 11862, + "local_expression": 2686997961149581690652951333888, + "nine_stage_expression": 6367946677593381897967570838257221015169748166633567813632 + } + }, + { + "pair_index": 53, + "singleton": 228, + "matrix": [ + 1, + 7, + 3 + ], + "word": [ + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ] + ], + "gain": 2, + "bill": { + "F": 73541, + "B": 10538760, + "D_adds": 5643, + "native_ADDs": 11863, + "local_expression": 2827141826900057725859489894400, + "nine_stage_expression": 6955776753132251962410053945500427146820005261675069440000 + } + }, + { + "pair_index": 123, + "singleton": 412, + "matrix": [ + 4, + 2, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 2, + 0 + ], + [ + 0, + 2 + ] + ], + "gain": 2, + "bill": { + "F": 72767, + "B": 10428850, + "D_adds": 5643, + "native_ADDs": 11863, + "local_expression": 2681984275136622249349908320000, + "nine_stage_expression": 6326419087404005067142485412678397206968529530060800000000 + } + }, + { + "pair_index": 12, + "singleton": 218, + "matrix": [ + 3, + 2, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 2, + 0 + ] + ], + "gain": 2, + "bill": { + "F": 72731, + "B": 10446066, + "D_adds": 5643, + "native_ADDs": 11863, + "local_expression": 2686854701321683044848508236544, + "nine_stage_expression": 6352560034990905647315083896756158577279285606285085507584 + } + }, + { + "pair_index": 96, + "singleton": 210, + "matrix": [ + 7, + 2, + 4 + ], + "word": [ + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ], + "gain": 2, + "bill": { + "F": 72935, + "B": 10428850, + "D_adds": 5641, + "native_ADDs": 11861, + "local_expression": 2700603199168139434695740000000, + "nine_stage_expression": 6399787330072806211745147271050067498879933440000000000000 + } + }, + { + "pair_index": 10, + "singleton": 228, + "matrix": [ + 7, + 2, + 3 + ], + "word": [ + [ + 0, + 2 + ], + [ + 0, + 1 + ], + [ + 2, + 0 + ] + ], + "gain": 2, + "bill": { + "F": 73459, + "B": 10492000, + "D_adds": 5639, + "native_ADDs": 11859, + "local_expression": 2792746870163193941699584000000, + "nine_stage_expression": 6795135315912334784667873969609480964591845376000000000000 + } + }, + { + "pair_index": 43, + "singleton": 210, + "matrix": [ + 1, + 7, + 3 + ], + "word": [ + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ] + ], + "gain": 2, + "bill": { + "F": 74615, + "B": 10499776, + "D_adds": 5639, + "native_ADDs": 11859, + "local_expression": 2931017908581864223461441536000, + "nine_stage_expression": 7368698287842481330407935136745321232950638962907545600000 + } + }, + { + "pair_index": 53, + "singleton": 228, + "matrix": [ + 3, + 1, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 2, + 0 + ], + [ + 1, + 0 + ] + ], + "gain": 2, + "bill": { + "F": 73975, + "B": 10773854, + "D_adds": 5639, + "native_ADDs": 11859, + "local_expression": 3007302168510790198011964000000, + "nine_stage_expression": 7824365600469089212526362803140308821614123376640000000000 + } + }, + { + "pair_index": 86, + "singleton": 383, + "matrix": [ + 3, + 2, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 2, + 0 + ] + ], + "gain": 2, + "bill": { + "F": 72659, + "B": 10430750, + "D_adds": 5635, + "native_ADDs": 11855, + "local_expression": 2671033262061633717541964000000, + "nine_stage_expression": 6284187725822474463548925178492346859401071616000000000000 + } + }, + { + "pair_index": 70, + "singleton": 164, + "matrix": [ + 3, + 6, + 4 + ], + "word": [ + [ + 0, + 1 + ], + [ + 1, + 2 + ] + ], + "gain": 2, + "bill": { + "F": 73403, + "B": 10450580, + "D_adds": 5635, + "native_ADDs": 11855, + "local_expression": 2764408326008290950613542579200, + "nine_stage_expression": 6663011282179931760228335141357439921939295975579320320000 + } + }, + { + "pair_index": 156, + "singleton": 185, + "matrix": [ + 7, + 2, + 4 + ], + "word": [ + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ], + "gain": 2, + "bill": { + "F": 72635, + "B": 10437394, + "D_adds": 5635, + "native_ADDs": 11855, + "local_expression": 2671787738303774038648577504000, + "nine_stage_expression": 6289815956318928249805999729467333919449508436600422400000 + } + }, + { + "pair_index": 3, + "singleton": 228, + "matrix": [ + 3, + 2, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 2, + 0 + ] + ], + "gain": 2, + "bill": { + "F": 73123, + "B": 10471910, + "D_adds": 5633, + "native_ADDs": 11853, + "local_expression": 2744061107500261173338483372800, + "nine_stage_expression": 6590426639340779701008675360372693231120534623546245120000 + } + }, + { + "pair_index": 53, + "singleton": 228, + "matrix": [ + 7, + 2, + 3 + ], + "word": [ + [ + 0, + 2 + ], + [ + 0, + 1 + ], + [ + 2, + 0 + ] + ], + "gain": 2, + "bill": { + "F": 74723, + "B": 10592284, + "D_adds": 5633, + "native_ADDs": 11853, + "local_expression": 2995864083038595951135765244928, + "nine_stage_expression": 7687230205674343770150739305814218911380256467035946483712 + } + }, + { + "pair_index": 3, + "singleton": 228, + "matrix": [ + 1, + 3, + 7 + ], + "word": [ + [ + 1, + 0 + ], + [ + 2, + 1 + ] + ], + "gain": 2, + "bill": { + "F": 73123, + "B": 10471910, + "D_adds": 5633, + "native_ADDs": 11853, + "local_expression": 2744061107500261173338483372800, + "nine_stage_expression": 6590426639340779701008675360372693231120534623546245120000 + } + }, + { + "pair_index": 54, + "singleton": 164, + "matrix": [ + 7, + 4, + 2 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ] + ], + "gain": 2, + "bill": { + "F": 73183, + "B": 10624960, + "D_adds": 5633, + "native_ADDs": 11853, + "local_expression": 2831817147773038910936075468800, + "nine_stage_expression": 7012940914405961424852488976676258167702570749415915520000 + } + }, + { + "pair_index": 54, + "singleton": 164, + "matrix": [ + 4, + 7, + 2 + ], + "word": [ + [ + 2, + 0 + ], + [ + 0, + 2 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ] + ], + "gain": 2, + "bill": { + "F": 73183, + "B": 10652224, + "D_adds": 5633, + "native_ADDs": 11853, + "local_expression": 2846368867524715277109230829568, + "nine_stage_expression": 7085200206617541360704041894083330537779632707967796641792 + } + }, + { + "pair_index": 43, + "singleton": 210, + "matrix": [ + 3, + 1, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 2, + 0 + ], + [ + 1, + 0 + ] + ], + "gain": 2, + "bill": { + "F": 73451, + "B": 10495406, + "D_adds": 5633, + "native_ADDs": 11853, + "local_expression": 2793647454359736144939755995904, + "nine_stage_expression": 6800259089080347156694816396588097264516402687126508929024 + } + }, + { + "pair_index": 10, + "singleton": 228, + "matrix": [ + 2, + 3, + 7 + ], + "word": [ + [ + 1, + 0 + ], + [ + 2, + 1 + ], + [ + 0, + 1 + ] + ], + "gain": 2, + "bill": { + "F": 73251, + "B": 10444834, + "D_adds": 5633, + "native_ADDs": 11853, + "local_expression": 2744250373471858536376381987584, + "nine_stage_expression": 6579817984563048200302754008206966744880567896903027523584 + } + }, + { + "pair_index": 26, + "singleton": 218, + "matrix": [ + 3, + 6, + 4 + ], + "word": [ + [ + 0, + 1 + ], + [ + 1, + 2 + ] + ], + "gain": 2, + "bill": { + "F": 72815, + "B": 10430750, + "D_adds": 5633, + "native_ADDs": 11853, + "local_expression": 2688274475818177726881500000000, + "nine_stage_expression": 6351939271708739769814488018954317353481600000000000000000 + } + }, + { + "pair_index": 53, + "singleton": 228, + "matrix": [ + 2, + 3, + 7 + ], + "word": [ + [ + 1, + 0 + ], + [ + 2, + 1 + ], + [ + 0, + 1 + ] + ], + "gain": 2, + "bill": { + "F": 73801, + "B": 10592140, + "D_adds": 5631, + "native_ADDs": 11851, + "local_expression": 2886251278427173453549134054400, + "nine_stage_expression": 7224137509007189072581846433541214659796955723506647040000 + } + }, + { + "pair_index": 111, + "singleton": 210, + "matrix": [ + 3, + 6, + 4 + ], + "word": [ + [ + 0, + 1 + ], + [ + 1, + 2 + ] + ], + "gain": 2, + "bill": { + "F": 73339, + "B": 10430750, + "D_adds": 5627, + "native_ADDs": 11847, + "local_expression": 2746730176401344172258604000000, + "nine_stage_expression": 6583805429103759166801817540549657454247177216000000000000 + } + }, + { + "pair_index": 166, + "singleton": 425, + "matrix": [ + 7, + 2, + 4 + ], + "word": [ + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ], + "gain": 2, + "bill": { + "F": 72731, + "B": 10430750, + "D_adds": 5627, + "native_ADDs": 11847, + "local_expression": 2678981555926027331498156000000, + "nine_stage_expression": 6315385452248389980064742681679508944203869184000000000000 + } + }, + { + "pair_index": 32, + "singleton": 425, + "matrix": [ + 3, + 2, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 2, + 0 + ] + ], + "gain": 2, + "bill": { + "F": 73091, + "B": 10430750, + "D_adds": 5627, + "native_ADDs": 11847, + "local_expression": 2718959623193740598609036000000, + "nine_stage_expression": 6473238178212122737033165222273598535137168384000000000000 + } + }, + { + "pair_index": 54, + "singleton": 164, + "matrix": [ + 2, + 4, + 7 + ], + "word": [ + [ + 1, + 0 + ], + [ + 2, + 1 + ], + [ + 0, + 1 + ], + [ + 1, + 2 + ] + ], + "gain": 2, + "bill": { + "F": 73007, + "B": 10773304, + "D_adds": 5627, + "native_ADDs": 11847, + "local_expression": 2890488941479611408530387628032, + "nine_stage_expression": 7324164594247389473030532726544632764869320795282785435648 + } + }, + { + "pair_index": 93, + "singleton": 358, + "matrix": [ + 1, + 3, + 7 + ], + "word": [ + [ + 1, + 0 + ], + [ + 2, + 1 + ] + ], + "gain": 1, + "bill": { + "F": 73535, + "B": 10448794, + "D_adds": 5628, + "native_ADDs": 11848, + "local_expression": 2778398900107076217483711584000, + "nine_stage_expression": 6718542580804208838573000944557087038108392337794662400000 + } + }, + { + "pair_index": 77, + "singleton": 13, + "matrix": [ + 7, + 4, + 2 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ] + ], + "gain": 1, + "bill": { + "F": 72843, + "B": 10554272, + "D_adds": 5628, + "native_ADDs": 11848, + "local_expression": 2755497427276774986229310226432, + "nine_stage_expression": 6671018884321777722632843932150899130591616876713189834752 + } + }, + { + "pair_index": 93, + "singleton": 358, + "matrix": [ + 5, + 7, + 3 + ], + "word": [ + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 2, + 1 + ] + ], + "gain": 1, + "bill": { + "F": 76043, + "B": 10442516, + "D_adds": 5628, + "native_ADDs": 11848, + "local_expression": 3068795854566797936682537970688, + "nine_stage_expression": 7926048575258830825814248446435746661336376003149286080512 + } + }, + { + "pair_index": 54, + "singleton": 164, + "matrix": [ + 7, + 2, + 6 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 2 + ] + ], + "gain": 1, + "bill": { + "F": 72699, + "B": 10571450, + "D_adds": 5628, + "native_ADDs": 11848, + "local_expression": 2748111852089185055560009440000, + "nine_stage_expression": 6648449085984061113727064066555640308209971722649600000000 + } + }, + { + "pair_index": 80, + "singleton": 65, + "matrix": [ + 3, + 6, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 1, + 2 + ], + [ + 2, + 0 + ] + ], + "gain": 1, + "bill": { + "F": 73523, + "B": 10644306, + "D_adds": 5628, + "native_ADDs": 11848, + "local_expression": 2881936016666920174409987021568, + "nine_stage_expression": 7229785687014507936664668254893906717728348611253142290432 + } + }, + { + "pair_index": 93, + "singleton": 358, + "matrix": [ + 5, + 3, + 7 + ], + "word": [ + [ + 1, + 0 + ], + [ + 0, + 2 + ], + [ + 2, + 1 + ] + ], + "gain": 1, + "bill": { + "F": 76307, + "B": 10435338, + "D_adds": 5627, + "native_ADDs": 11847, + "local_expression": 3096607446124739175082397061888, + "nine_stage_expression": 8042441338609714491411089769519058870423907972255462719488 + } + }, + { + "pair_index": 93, + "singleton": 358, + "matrix": [ + 3, + 5, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 2, + 0 + ], + [ + 1, + 2 + ] + ], + "gain": 1, + "bill": { + "F": 76203, + "B": 10444206, + "D_adds": 5626, + "native_ADDs": 11846, + "local_expression": 3089207211626146297581170443008, + "nine_stage_expression": 8014971543997366895602087154948011107043556031402954719232 + } + }, + { + "pair_index": 80, + "singleton": 65, + "matrix": [ + 6, + 3, + 7 + ], + "word": [ + [ + 1, + 0 + ], + [ + 2, + 1 + ], + [ + 0, + 2 + ] + ], + "gain": 1, + "bill": { + "F": 73599, + "B": 10665716, + "D_adds": 5626, + "native_ADDs": 11846, + "local_expression": 2902523505123179730273239817216, + "nine_stage_expression": 7325875795305957222184388835624723542921609227144701935616 + } + }, + { + "pair_index": 80, + "singleton": 65, + "matrix": [ + 7, + 6, + 3 + ], + "word": [ + [ + 1, + 2 + ], + [ + 0, + 1 + ], + [ + 2, + 0 + ] + ], + "gain": 1, + "bill": { + "F": 73647, + "B": 10797846, + "D_adds": 5626, + "native_ADDs": 11846, + "local_expression": 2980707870203251164072933725952, + "nine_stage_expression": 7720825588000359847353148425381923530245215230176157237248 + } + }, + { + "pair_index": 93, + "singleton": 358, + "matrix": [ + 3, + 7, + 5 + ], + "word": [ + [ + 2, + 0 + ], + [ + 0, + 1 + ], + [ + 1, + 2 + ] + ], + "gain": 1, + "bill": { + "F": 76071, + "B": 10435338, + "D_adds": 5626, + "native_ADDs": 11846, + "local_expression": 3067964929984096574771056402176, + "nine_stage_expression": 7918841134508401970379630028401803557276219081970977603584 + } + }, + { + "pair_index": 52, + "singleton": 13, + "matrix": [ + 4, + 3, + 6 + ], + "word": [ + [ + 2, + 1 + ], + [ + 1, + 0 + ], + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ], + "gain": 1, + "bill": { + "F": 72687, + "B": 10724208, + "D_adds": 5626, + "native_ADDs": 11846, + "local_expression": 2826706160068404672973370277888, + "nine_stage_expression": 7035331404289550909241345944308885177746253109005142458368 + } + }, + { + "pair_index": 187, + "singleton": 65, + "matrix": [ + 7, + 6, + 4 + ], + "word": [ + [ + 1, + 2 + ], + [ + 0, + 1 + ] + ], + "gain": 1, + "bill": { + "F": 72903, + "B": 10446104, + "D_adds": 5626, + "native_ADDs": 11846, + "local_expression": 2705981761122306951783142453248, + "nine_stage_expression": 6428124859850777615233250803472888942187977300928890929152 + } + }, + { + "pair_index": 10, + "singleton": 228, + "matrix": [ + 2, + 7, + 4 + ], + "word": [ + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 0, + 1 + ] + ], + "gain": 1, + "bill": { + "F": 72895, + "B": 10462194, + "D_adds": 5626, + "native_ADDs": 11846, + "local_expression": 2713430689179750770984046432000, + "nine_stage_expression": 6464273142449822665698425385026780902682578644094156800000 + } + }, + { + "pair_index": 10, + "singleton": 228, + "matrix": [ + 4, + 2, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 2, + 0 + ], + [ + 0, + 2 + ] + ], + "gain": 1, + "bill": { + "F": 74015, + "B": 10504446, + "D_adds": 5626, + "native_ADDs": 11846, + "local_expression": 2863423006922110758984802656000, + "nine_stage_expression": 7089755377430726082714864617998956262750184382962073600000 + } + }, + { + "pair_index": 52, + "singleton": 13, + "matrix": [ + 4, + 6, + 3 + ], + "word": [ + [ + 2, + 0 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 2, + 1 + ] + ], + "gain": 1, + "bill": { + "F": 72727, + "B": 10589486, + "D_adds": 5626, + "native_ADDs": 11846, + "local_expression": 2760684359025062477906409617152, + "nine_stage_expression": 6706837905187890109595517984472313893940884682782359420928 + } + }, + { + "pair_index": 77, + "singleton": 13, + "matrix": [ + 4, + 7, + 2 + ], + "word": [ + [ + 2, + 0 + ], + [ + 0, + 2 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ] + ], + "gain": 1, + "bill": { + "F": 72871, + "B": 10493984, + "D_adds": 5626, + "native_ADDs": 11846, + "local_expression": 2727250043778451551553739751424, + "nine_stage_expression": 6532435938611137735013549950684580794412800465089366851584 + } + }, + { + "pair_index": 152, + "singleton": 357, + "matrix": [ + 3, + 6, + 4 + ], + "word": [ + [ + 0, + 1 + ], + [ + 1, + 2 + ] + ], + "gain": 1, + "bill": { + "F": 72695, + "B": 10430750, + "D_adds": 5626, + "native_ADDs": 11846, + "local_expression": 2675005440917926218525500000000, + "nine_stage_expression": 6299771139310716924787693106901128477628800000000000000000 + } + }, + { + "pair_index": 93, + "singleton": 358, + "matrix": [ + 7, + 6, + 3 + ], + "word": [ + [ + 1, + 2 + ], + [ + 0, + 1 + ], + [ + 2, + 0 + ] + ], + "gain": 1, + "bill": { + "F": 76335, + "B": 10437928, + "D_adds": 5626, + "native_ADDs": 11846, + "local_expression": 3101556502889541385074279936000, + "nine_stage_expression": 8065209607643279114967841228435925746920658867480166400000 + } + }, + { + "pair_index": 10, + "singleton": 228, + "matrix": [ + 1, + 3, + 7 + ], + "word": [ + [ + 1, + 0 + ], + [ + 2, + 1 + ] + ], + "gain": 1, + "bill": { + "F": 73151, + "B": 10444834, + "D_adds": 5626, + "native_ADDs": 11846, + "local_expression": 2733026612516244713850507632384, + "nine_stage_expression": 6535027624259535154872115642532525882436615464955448131584 + } + }, + { + "pair_index": 54, + "singleton": 164, + "matrix": [ + 7, + 2, + 3 + ], + "word": [ + [ + 0, + 2 + ], + [ + 0, + 1 + ], + [ + 2, + 0 + ] + ], + "gain": 1, + "bill": { + "F": 72947, + "B": 10700774, + "D_adds": 5626, + "native_ADDs": 11846, + "local_expression": 2844675061611780874168330134272, + "nine_stage_expression": 7099665197938000411223387093384376729882908357298338398208 + } + }, + { + "pair_index": 77, + "singleton": 13, + "matrix": [ + 2, + 4, + 7 + ], + "word": [ + [ + 1, + 0 + ], + [ + 2, + 1 + ], + [ + 0, + 1 + ], + [ + 1, + 2 + ] + ], + "gain": 1, + "bill": { + "F": 72967, + "B": 10569584, + "D_adds": 5626, + "native_ADDs": 11846, + "local_expression": 2777635381971681026980240801792, + "nine_stage_expression": 6767121194123122056704102530608442947405373652577695039488 + } + }, + { + "pair_index": 145, + "singleton": 13, + "matrix": [ + 3, + 6, + 4 + ], + "word": [ + [ + 0, + 1 + ], + [ + 1, + 2 + ] + ], + "gain": 1, + "bill": { + "F": 72671, + "B": 10446724, + "D_adds": 5626, + "native_ADDs": 11846, + "local_expression": 2680548225622369977092324424704, + "nine_stage_expression": 6327994420783849271517792733972941838118782764415339986944 + } + }, + { + "pair_index": 162, + "singleton": 13, + "matrix": [ + 4, + 6, + 3 + ], + "word": [ + [ + 2, + 0 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 2, + 1 + ] + ], + "gain": 1, + "bill": { + "F": 72727, + "B": 10513870, + "D_adds": 5626, + "native_ADDs": 11846, + "local_expression": 2721398864999534865633493292800, + "nine_stage_expression": 6517314808460797529589468580194574669299332084995194880000 + } + }, + { + "pair_index": 80, + "singleton": 65, + "matrix": [ + 7, + 3, + 6 + ], + "word": [ + [ + 2, + 1 + ], + [ + 1, + 0 + ], + [ + 0, + 2 + ] + ], + "gain": 1, + "bill": { + "F": 73647, + "B": 10644306, + "D_adds": 5626, + "native_ADDs": 11846, + "local_expression": 2896542185191102833457938792192, + "nine_stage_expression": 7290958550353246432396197917021298620115251964439028563968 + } + }, + { + "pair_index": 111, + "singleton": 228, + "matrix": [ + 7, + 6, + 4 + ], + "word": [ + [ + 1, + 2 + ], + [ + 0, + 1 + ] + ], + "gain": 1, + "bill": { + "F": 73367, + "B": 10462194, + "D_adds": 5626, + "native_ADDs": 11846, + "local_expression": 2766481655231682983583972087552, + "nine_stage_expression": 6676283995787474999081441515119719587870594641642670522368 + } + }, + { + "pair_index": 54, + "singleton": 164, + "matrix": [ + 2, + 3, + 7 + ], + "word": [ + [ + 1, + 0 + ], + [ + 2, + 1 + ], + [ + 0, + 1 + ] + ], + "gain": 1, + "bill": { + "F": 72771, + "B": 10666078, + "D_adds": 5626, + "native_ADDs": 11846, + "local_expression": 2805850409180004328020659387136, + "nine_stage_expression": 6923897942814009066978418248409186313840440271640371134464 + } + }, + { + "pair_index": 80, + "singleton": 65, + "matrix": [ + 7, + 6, + 4 + ], + "word": [ + [ + 1, + 2 + ], + [ + 0, + 1 + ] + ], + "gain": 1, + "bill": { + "F": 72855, + "B": 10476812, + "D_adds": 5626, + "native_ADDs": 11846, + "local_expression": 2716541620046285535258867072000, + "nine_stage_expression": 6482661394556264418581805153618797321285133880472371200000 + } + }, + { + "pair_index": 93, + "singleton": 358, + "matrix": [ + 7, + 3, + 6 + ], + "word": [ + [ + 2, + 1 + ], + [ + 1, + 0 + ], + [ + 0, + 2 + ] + ], + "gain": 1, + "bill": { + "F": 75811, + "B": 10448682, + "D_adds": 5624, + "native_ADDs": 11844, + "local_expression": 3044385702528537114437664105216, + "nine_stage_expression": 7824328864790744961122856557056486671833956627712619577344 + } + }, + { + "pair_index": 162, + "singleton": 13, + "matrix": [ + 7, + 6, + 4 + ], + "word": [ + [ + 1, + 2 + ], + [ + 0, + 1 + ] + ], + "gain": 1, + "bill": { + "F": 72247, + "B": 10512578, + "D_adds": 5624, + "native_ADDs": 11844, + "local_expression": 2667214174434885233525827118848, + "nine_stage_expression": 6301964274608045305940695526640552097621864106930049384448 + } + }, + { + "pair_index": 93, + "singleton": 358, + "matrix": [ + 3, + 2, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 2, + 0 + ] + ], + "gain": 1, + "bill": { + "F": 73167, + "B": 10462138, + "D_adds": 5623, + "native_ADDs": 11843, + "local_expression": 2743889436582856884141195863808, + "nine_stage_expression": 6585639309691844938208343038679286811176907430290037669888 + } + }, + { + "pair_index": 93, + "singleton": 358, + "matrix": [ + 3, + 6, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 1, + 2 + ], + [ + 2, + 0 + ] + ], + "gain": 1, + "bill": { + "F": 75963, + "B": 10464656, + "D_adds": 5620, + "native_ADDs": 11840, + "local_expression": 3072106101939793672956482469888, + "nine_stage_expression": 7951522421453150785197913008565945507955361099630124204032 + } + }, + { + "pair_index": 93, + "singleton": 358, + "matrix": [ + 6, + 3, + 7 + ], + "word": [ + [ + 1, + 0 + ], + [ + 2, + 1 + ], + [ + 0, + 2 + ] + ], + "gain": 1, + "bill": { + "F": 76095, + "B": 10482700, + "D_adds": 5620, + "native_ADDs": 11840, + "local_expression": 3098807884273348572752880000000, + "nine_stage_expression": 8076313285138559437106365420182983086166753280000000000000 + } + }, + { + "pair_index": 104, + "singleton": 289, + "matrix": [ + 3, + 6, + 4 + ], + "word": [ + [ + 0, + 1 + ], + [ + 1, + 2 + ] + ], + "gain": 1, + "bill": { + "F": 72479, + "B": 10464656, + "D_adds": 5620, + "native_ADDs": 11840, + "local_expression": 2668495441069720057742815379456, + "nine_stage_expression": 6287828844446423195437711948668345760563868782684406808576 + } + } + ], + "accepted": [ + { + "pair_index": 42, + "singleton": 201, + "matrix": [ + 7, + 2, + 4 + ], + "word": [ + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ], + "gain": 9, + "bill": { + "F": 71915, + "B": 10562318, + "D_adds": 5751, + "native_ADDs": 11971, + "local_expression": 2655564814194801277805095904000, + "nine_stage_expression": 6275875225932365205955565278298294920001907345627545600000 + } + }, + { + "pair_index": 148, + "singleton": 255, + "matrix": [ + 3, + 2, + 6 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 1 + ] + ], + "gain": 9, + "bill": { + "F": 71915, + "B": 10562318, + "D_adds": 5742, + "native_ADDs": 11962, + "local_expression": 2655564814194801277805095904000, + "nine_stage_expression": 6275875225932365205955565278298294920001907345627545600000 + } + }, + { + "pair_index": 48, + "singleton": 56, + "matrix": [ + 5, + 7, + 4 + ], + "word": [ + [ + 0, + 2 + ], + [ + 1, + 0 + ] + ], + "gain": 8, + "bill": { + "F": 71915, + "B": 10562318, + "D_adds": 5734, + "native_ADDs": 11954, + "local_expression": 2655564814194801277805095904000, + "nine_stage_expression": 6275875225932365205955565278298294920001907345627545600000 + } + }, + { + "pair_index": 2, + "singleton": 215, + "matrix": [ + 3, + 2, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 2, + 0 + ] + ], + "gain": 8, + "bill": { + "F": 71915, + "B": 10562318, + "D_adds": 5726, + "native_ADDs": 11946, + "local_expression": 2655564814194801277805095904000, + "nine_stage_expression": 6275875225932365205955565278298294920001907345627545600000 + } + }, + { + "pair_index": 72, + "singleton": 166, + "matrix": [ + 3, + 6, + 4 + ], + "word": [ + [ + 0, + 1 + ], + [ + 1, + 2 + ] + ], + "gain": 7, + "bill": { + "F": 71915, + "B": 10562318, + "D_adds": 5719, + "native_ADDs": 11939, + "local_expression": 2655564814194801277805095904000, + "nine_stage_expression": 6275875225932365205955565278298294920001907345627545600000 + } + }, + { + "pair_index": 125, + "singleton": 363, + "matrix": [ + 3, + 2, + 5 + ], + "word": [ + [ + 2, + 0 + ], + [ + 0, + 1 + ] + ], + "gain": 6, + "bill": { + "F": 71939, + "B": 10532724, + "D_adds": 5713, + "native_ADDs": 11933, + "local_expression": 2643349396468942157702907350016, + "nine_stage_expression": 6216196305703639587864821499982878212211027935761589600256 + } + }, + { + "pair_index": 28, + "singleton": 249, + "matrix": [ + 1, + 3, + 6 + ], + "word": [ + [ + 2, + 1 + ], + [ + 1, + 0 + ] + ], + "gain": 6, + "bill": { + "F": 71939, + "B": 10532724, + "D_adds": 5707, + "native_ADDs": 11927, + "local_expression": 2643349396468942157702907350016, + "nine_stage_expression": 6216196305703639587864821499982878212211027935761589600256 + } + }, + { + "pair_index": 83, + "singleton": 204, + "matrix": [ + 3, + 2, + 5 + ], + "word": [ + [ + 2, + 0 + ], + [ + 0, + 1 + ] + ], + "gain": 6, + "bill": { + "F": 72035, + "B": 10526114, + "D_adds": 5701, + "native_ADDs": 11921, + "local_expression": 2650615870209733268430835424000, + "nine_stage_expression": 6242089643230275557900218761046125801803670261687910400000 + } + }, + { + "pair_index": 140, + "singleton": 344, + "matrix": [ + 3, + 6, + 4 + ], + "word": [ + [ + 0, + 1 + ], + [ + 1, + 2 + ] + ], + "gain": 5, + "bill": { + "F": 72035, + "B": 10526114, + "D_adds": 5696, + "native_ADDs": 11916, + "local_expression": 2650615870209733268430835424000, + "nine_stage_expression": 6242089643230275557900218761046125801803670261687910400000 + } + }, + { + "pair_index": 16, + "singleton": 272, + "matrix": [ + 1, + 2, + 7 + ], + "word": [ + [ + 2, + 1 + ], + [ + 2, + 0 + ] + ], + "gain": 4, + "bill": { + "F": 71639, + "B": 10537324, + "D_adds": 5692, + "native_ADDs": 11912, + "local_expression": 2612697842266605740033003273216, + "nine_stage_expression": 6098300659682755993685370207436110073140216416843759353856 + } + }, + { + "pair_index": 55, + "singleton": 177, + "matrix": [ + 3, + 5, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 2, + 0 + ], + [ + 1, + 2 + ] + ], + "gain": 4, + "bill": { + "F": 71799, + "B": 10551982, + "D_adds": 5688, + "native_ADDs": 11908, + "local_expression": 2637565442209837519682021201664, + "nine_stage_expression": 6201090454799270848666411229221007513679063191633270931456 + } + }, + { + "pair_index": 39, + "singleton": 137, + "matrix": [ + 3, + 2, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 2, + 0 + ] + ], + "gain": 4, + "bill": { + "F": 71863, + "B": 10551982, + "D_adds": 5684, + "native_ADDs": 11904, + "local_expression": 2644624929162326669588953192192, + "nine_stage_expression": 6228777326588061265551916096198621390014893182406876987392 + } + }, + { + "pair_index": 155, + "singleton": 334, + "matrix": [ + 6, + 3, + 7 + ], + "word": [ + [ + 1, + 0 + ], + [ + 2, + 1 + ], + [ + 0, + 2 + ] + ], + "gain": 4, + "bill": { + "F": 71863, + "B": 10551982, + "D_adds": 5680, + "native_ADDs": 11900, + "local_expression": 2644624929162326669588953192192, + "nine_stage_expression": 6228777326588061265551916096198621390014893182406876987392 + } + }, + { + "pair_index": 24, + "singleton": 59, + "matrix": [ + 1, + 3, + 7 + ], + "word": [ + [ + 1, + 0 + ], + [ + 2, + 1 + ] + ], + "gain": 4, + "bill": { + "F": 71927, + "B": 10555986, + "D_adds": 5676, + "native_ADDs": 11896, + "local_expression": 2653709781452035343669052970752, + "nine_stage_expression": 6266064741573392300000932539188345942578207752677310332928 + } + }, + { + "pair_index": 130, + "singleton": 292, + "matrix": [ + 3, + 2, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 2, + 0 + ] + ], + "gain": 4, + "bill": { + "F": 71927, + "B": 10555986, + "D_adds": 5672, + "native_ADDs": 11892, + "local_expression": 2653709781452035343669052970752, + "nine_stage_expression": 6266064741573392300000932539188345942578207752677310332928 + } + }, + { + "pair_index": 19, + "singleton": 93, + "matrix": [ + 7, + 2, + 4 + ], + "word": [ + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ], + "gain": 4, + "bill": { + "F": 71927, + "B": 10555986, + "D_adds": 5668, + "native_ADDs": 11888, + "local_expression": 2653709781452035343669052970752, + "nine_stage_expression": 6266064741573392300000932539188345942578207752677310332928 + } + }, + { + "pair_index": 17, + "singleton": 342, + "matrix": [ + 3, + 2, + 5 + ], + "word": [ + [ + 2, + 0 + ], + [ + 0, + 1 + ] + ], + "gain": 4, + "bill": { + "F": 71927, + "B": 10555986, + "D_adds": 5664, + "native_ADDs": 11884, + "local_expression": 2653709781452035343669052970752, + "nine_stage_expression": 6266064741573392300000932539188345942578207752677310332928 + } + }, + { + "pair_index": 9, + "singleton": 269, + "matrix": [ + 3, + 6, + 4 + ], + "word": [ + [ + 0, + 1 + ], + [ + 1, + 2 + ] + ], + "gain": 4, + "bill": { + "F": 71927, + "B": 10555986, + "D_adds": 5660, + "native_ADDs": 11880, + "local_expression": 2653709781452035343669052970752, + "nine_stage_expression": 6266064741573392300000932539188345942578207752677310332928 + } + }, + { + "pair_index": 144, + "singleton": 343, + "matrix": [ + 1, + 3, + 6 + ], + "word": [ + [ + 2, + 1 + ], + [ + 1, + 0 + ] + ], + "gain": 3, + "bill": { + "F": 72395, + "B": 10426798, + "D_adds": 5657, + "native_ADDs": 11877, + "local_expression": 2640022396879241886017889248000, + "nine_stage_expression": 6161502429526032335227641720550638128535156057689292800000 + } + }, + { + "pair_index": 126, + "singleton": 307, + "matrix": [ + 5, + 7, + 4 + ], + "word": [ + [ + 0, + 2 + ], + [ + 1, + 0 + ] + ], + "gain": 3, + "bill": { + "F": 72539, + "B": 10426798, + "D_adds": 5654, + "native_ADDs": 11874, + "local_expression": 2655807460951040308986986910464, + "nine_stage_expression": 6223025534638822367568269695503582951840809607853449936896 + } + }, + { + "pair_index": 150, + "singleton": 148, + "matrix": [ + 7, + 2, + 4 + ], + "word": [ + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ], + "gain": 3, + "bill": { + "F": 72539, + "B": 10428850, + "D_adds": 5651, + "native_ADDs": 11871, + "local_expression": 2656852892763112164628936160000, + "nine_stage_expression": 6227925761344351314564030681835402201449889233305600000000 + } + }, + { + "pair_index": 109, + "singleton": 8, + "matrix": [ + 7, + 2, + 4 + ], + "word": [ + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ], + "gain": 3, + "bill": { + "F": 72539, + "B": 10428850, + "D_adds": 5648, + "native_ADDs": 11868, + "local_expression": 2656852892763112164628936160000, + "nine_stage_expression": 6227925761344351314564030681835402201449889233305600000000 + } + }, + { + "pair_index": 81, + "singleton": 265, + "matrix": [ + 7, + 2, + 4 + ], + "word": [ + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ], + "gain": 3, + "bill": { + "F": 72539, + "B": 10428850, + "D_adds": 5645, + "native_ADDs": 11865, + "local_expression": 2656852892763112164628936160000, + "nine_stage_expression": 6227925761344351314564030681835402201449889233305600000000 + } + }, + { + "pair_index": 18, + "singleton": 299, + "matrix": [ + 3, + 2, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 2, + 0 + ] + ], + "gain": 2, + "bill": { + "F": 72539, + "B": 10428850, + "D_adds": 5643, + "native_ADDs": 11863, + "local_expression": 2656852892763112164628936160000, + "nine_stage_expression": 6227925761344351314564030681835402201449889233305600000000 + } + }, + { + "pair_index": 75, + "singleton": 328, + "matrix": [ + 3, + 2, + 5 + ], + "word": [ + [ + 2, + 0 + ], + [ + 0, + 1 + ] + ], + "gain": 2, + "bill": { + "F": 72563, + "B": 10430750, + "D_adds": 5641, + "native_ADDs": 11861, + "local_expression": 2660460013696359524911052000000, + "nine_stage_expression": 6242782671699667112665113884232304001498074112000000000000 + } + }, + { + "pair_index": 123, + "singleton": 412, + "matrix": [ + 3, + 2, + 7 + ], + "word": [ + [ + 0, + 1 + ], + [ + 2, + 0 + ] + ], + "gain": 2, + "bill": { + "F": 72611, + "B": 10430750, + "D_adds": 5639, + "native_ADDs": 11859, + "local_expression": 2665743143120298864233996000000, + "nine_stage_expression": 6263457827683752770373103698967788705967606784000000000000 + } + }, + { + "pair_index": 143, + "singleton": 278, + "matrix": [ + 1, + 3, + 6 + ], + "word": [ + [ + 2, + 1 + ], + [ + 1, + 0 + ] + ], + "gain": 2, + "bill": { + "F": 72611, + "B": 10430750, + "D_adds": 5637, + "native_ADDs": 11857, + "local_expression": 2665743143120298864233996000000, + "nine_stage_expression": 6263457827683752770373103698967788705967606784000000000000 + } + }, + { + "pair_index": 134, + "singleton": 243, + "matrix": [ + 7, + 2, + 4 + ], + "word": [ + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ], + "gain": 2, + "bill": { + "F": 72611, + "B": 10430750, + "D_adds": 5635, + "native_ADDs": 11855, + "local_expression": 2665743143120298864233996000000, + "nine_stage_expression": 6263457827683752770373103698967788705967606784000000000000 + } + }, + { + "pair_index": 61, + "singleton": 135, + "matrix": [ + 7, + 2, + 4 + ], + "word": [ + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ], + "gain": 2, + "bill": { + "F": 72611, + "B": 10430750, + "D_adds": 5633, + "native_ADDs": 11853, + "local_expression": 2665743143120298864233996000000, + "nine_stage_expression": 6263457827683752770373103698967788705967606784000000000000 + } + }, + { + "pair_index": 34, + "singleton": 218, + "matrix": [ + 3, + 6, + 4 + ], + "word": [ + [ + 0, + 1 + ], + [ + 1, + 2 + ] + ], + "gain": 2, + "bill": { + "F": 72611, + "B": 10430750, + "D_adds": 5631, + "native_ADDs": 11851, + "local_expression": 2665743143120298864233996000000, + "nine_stage_expression": 6263457827683752770373103698967788705967606784000000000000 + } + }, + { + "pair_index": 170, + "singleton": 279, + "matrix": [ + 3, + 6, + 4 + ], + "word": [ + [ + 0, + 1 + ], + [ + 1, + 2 + ] + ], + "gain": 2, + "bill": { + "F": 72611, + "B": 10430750, + "D_adds": 5629, + "native_ADDs": 11849, + "local_expression": 2665743143120298864233996000000, + "nine_stage_expression": 6263457827683752770373103698967788705967606784000000000000 + } + }, + { + "pair_index": 146, + "singleton": 210, + "matrix": [ + 7, + 2, + 4 + ], + "word": [ + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ], + "gain": 1, + "bill": { + "F": 72611, + "B": 10430750, + "D_adds": 5628, + "native_ADDs": 11848, + "local_expression": 2665743143120298864233996000000, + "nine_stage_expression": 6263457827683752770373103698967788705967606784000000000000 + } + }, + { + "pair_index": 182, + "singleton": 10, + "matrix": [ + 7, + 2, + 4 + ], + "word": [ + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ], + "gain": 1, + "bill": { + "F": 72639, + "B": 10430750, + "D_adds": 5627, + "native_ADDs": 11847, + "local_expression": 2668828196119205434703004000000, + "nine_stage_expression": 6275543608607732654044543880055000889630473216000000000000 + } + }, + { + "pair_index": 90, + "singleton": 311, + "matrix": [ + 1, + 3, + 7 + ], + "word": [ + [ + 1, + 0 + ], + [ + 2, + 1 + ] + ], + "gain": 1, + "bill": { + "F": 72163, + "B": 10448682, + "D_adds": 5626, + "native_ADDs": 11846, + "local_expression": 2625709869683601804264271848192, + "nine_stage_expression": 6114470690856091609772871907065128670687655700773252104192 + } + }, + { + "pair_index": 80, + "singleton": 184, + "matrix": [ + 7, + 2, + 4 + ], + "word": [ + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ], + "gain": 1, + "bill": { + "F": 72247, + "B": 10448682, + "D_adds": 5625, + "native_ADDs": 11845, + "local_expression": 2634889773526737825321945001728, + "nine_stage_expression": 6150140816818555231703292867340576323380673086351116075008 + } + }, + { + "pair_index": 106, + "singleton": 228, + "matrix": [ + 7, + 2, + 4 + ], + "word": [ + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ], + "gain": 1, + "bill": { + "F": 72375, + "B": 10448682, + "D_adds": 5624, + "native_ADDs": 11844, + "local_expression": 2648919301859868925729500000000, + "nine_stage_expression": 6204815225381825559990065678673976936440192000000000000000 + } + }, + { + "pair_index": 82, + "singleton": 136, + "matrix": [ + 3, + 6, + 4 + ], + "word": [ + [ + 0, + 1 + ], + [ + 1, + 2 + ] + ], + "gain": 1, + "bill": { + "F": 72375, + "B": 10448682, + "D_adds": 5623, + "native_ADDs": 11843, + "local_expression": 2648919301859868925729500000000, + "nine_stage_expression": 6204815225381825559990065678673976936440192000000000000000 + } + }, + { + "pair_index": 118, + "singleton": 13, + "matrix": [ + 7, + 2, + 4 + ], + "word": [ + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ], + "gain": 1, + "bill": { + "F": 72399, + "B": 10464656, + "D_adds": 5622, + "native_ADDs": 11842, + "local_expression": 2659668991063825342552531255296, + "nine_stage_expression": 6253203843833393632383133699318586751438846446425369214976 + } + }, + { + "pair_index": 124, + "singleton": 388, + "matrix": [ + 3, + 2, + 6 + ], + "word": [ + [ + 2, + 1 + ], + [ + 0, + 1 + ] + ], + "gain": 1, + "bill": { + "F": 72399, + "B": 10464656, + "D_adds": 5621, + "native_ADDs": 11841, + "local_expression": 2659668991063825342552531255296, + "nine_stage_expression": 6253203843833393632383133699318586751438846446425369214976 + } + }, + { + "pair_index": 119, + "singleton": 138, + "matrix": [ + 7, + 2, + 4 + ], + "word": [ + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ], + "gain": 1, + "bill": { + "F": 72399, + "B": 10464656, + "D_adds": 5620, + "native_ADDs": 11840, + "local_expression": 2659668991063825342552531255296, + "nine_stage_expression": 6253203843833393632383133699318586751438846446425369214976 + } + } + ], + "baseline": { + "F": 71907, + "B": 10562318, + "D_adds": 5760, + "native_ADDs": 11980, + "local_expression": 2654678678257550221373682862848, + "nine_stage_expression": 6272385284143355252940491378432965655169900286360795742208 + }, + "result": { + "F": 72399, + "B": 10464656, + "D_adds": 5620, + "native_ADDs": 11840, + "local_expression": 2659668991063825342552531255296, + "nine_stage_expression": 6253203843833393632383133699318586751438846446425369214976 + }, + "saved_ADDs": 140, + "candidate_sha256": "03016658f28ad8d53eba99c6a6bf4db8f6812200e978b4dfa15e74577ef612ee", + "stopping_rule": "one sorted pass through every strict-gain representative; no restart" +} diff --git a/research/r439-helper-triples/CLAIM.json b/research/r439-helper-triples/CLAIM.json new file mode 100644 index 0000000000..c5eef03d6e --- /dev/null +++ b/research/r439-helper-triples/CLAIM.json @@ -0,0 +1,50 @@ +{ + "track": "Bit supplier", + "assignment_seed": 12, + "random_source": "Python secrets.randbelow(100), operating system randomness", + "draw_note": "Earlier unsaved draw output was truncated before inspection; 12 is the recorded assignment draw.", + "base_commit": "007664306fff84fbb1c9a1b4053b69f439764034", + "claimed_at_utc": "2026-10-13T14:48:47.842229+00:00", + "expected_finish_utc": "2026-10-13T15:24:37Z", + "expected_verification_start_utc": "2026-10-13T15:14:37Z", + "coordination": "GitHub GraphQL pinnedIssues returned an empty list; local claim. Open issues 650 and 913 are not sprint coordination issues.", + "candidates": [ + { + "task": "Replace a PR926 helper pair plus an unmatched helper by a coupled GL(3,2) basis", + "decision": "chosen; overlapping helper changes are outside the PR941 disjoint-pair floor" + }, + { + "task": "Full hosted adoption of PR926 semantic compensation", + "decision": "too broad for this bounded run" + }, + { + "task": "R439 phase-B frame factorization", + "decision": "overlaps PRs 884, 891, 904, 908, 914, 923, 925, 936, 952" + } + ], + "object": "Frozen PR915 target basis inside PR926 R439 D compensation, keeping the remaining word fixed", + "method": "BFS all 168 GL(3,2) maps under six directed CNOT generators. For each of 192 PR926 helper pairs and 55 unmatched helpers, score every shortest representative with both preparation and restoration. One seed-12 ordered greedy disjoint pass, with literal positive-envelope guards. No restart or general optimum claim.", + "deliverable": "One finite circuit candidate or scoped negative result, reproducible census, exact all-column boundaries and negative controls", + "overlap": "713 open PRs scanned; PR941 certifies disjoint helper matching, excluding overlapping bases. PR952 synthesizes phase-A six-wire prefixes. No helper-triple compensation claim found.", + "selected_kappa": "1661957774647029/1000000000000000000", + "selected_source": "PR890, with unchanged PR589 bit supplier", + "result": { + "status": "finite bit construction, no new kappa", + "completed_at_utc": "2026-10-13T15:05:08.697112+00:00", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/965", + "implementation_commit": "82f2b20fff8ecc869dd0994721b77652c6c5063a", + "complete_ADDs": 11840, + "saved_beyond_PR926": 140, + "accepted_triples": 40, + "scores": 1774080, + "verification": "Full receipt equality, independent group/census, arbitrary-input restoration, owning checks, native legality and 5/9/11-stage replay passed; 144 bridge controls rejected. Selected-record check passed.", + "remaining": "Semantic D supplier admission, complete hosted emission/audit and invoices, outer assembly; inherited theorem assumptions remain.", + "overlap_refresh": "Queue through PR962 plus exact helper-triples search with zero matches before submission; no pinned coordination issue.", + "labels": "codex and codex-automation are not available in the upstream label catalog." + }, + "verification_began_utc": "2026-10-13T14:55:12Z", + "negative_result_review": [ + "research/experiment-log/negative-searches/factored-retiming/README.md: different word and retiming objective", + "research/experiment-log/campaign-100/algebraic-word-construction.md entry 45: proposal not evidenced" + ] +} diff --git a/research/r439-helper-triples/EXPECTED.json b/research/r439-helper-triples/EXPECTED.json new file mode 100644 index 0000000000..b48774171e --- /dev/null +++ b/research/r439-helper-triples/EXPECTED.json @@ -0,0 +1,1897 @@ +{ + "D_boundary_columns": 661, + "D_words_times_directions": 8, + "base_commit": "007664306fff84fbb1c9a1b4053b69f439764034", + "bill": { + "B": 10464656, + "D_adds": 5620, + "F": 72399, + "local_expression": 2659668991063825342552531255296, + "native_ADDs": 11840, + "nine_stage_expression": 6253203843833393632383133699318586751438846446425369214976 + }, + "candidate_sha256": "03016658f28ad8d53eba99c6a6bf4db8f6812200e978b4dfa15e74577ef612ee", + "controls": { + "neutral_pair_extra_ADDs": 2, + "rejected": [ + "omit helper preparation; clean-helper inputs alone miss it", + "omit target preparation; helper-only tests miss it", + "restore helper words in forward order", + "restore target word in forward order", + "omit helper restoration operation", + "omit target restoration operation", + "omit transformed middle coefficient", + "transpose helper entrance directions", + "all rejected nominees violate an exact integer cap", + "corrupt shortest-word certificate" + ] + }, + "native": { + "baseline": { + "common_frame_ADDs": 24305, + "copies": 9, + "erasures": 9, + "paid_histogram": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "rank_mass": 5129, + "records": 27234, + "staged": { + "11": { + "bridge_additions": 2664, + "controls_rejected": 24, + "formal_columns_checked": 1549, + "fresh_center_copies": 99, + "local_raw_H": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "payload_prefix_bits": 93, + "payload_prefix_upper": "9528119495320518471870892800", + "reverse_fresh_center_copies": 45, + "signed_lift_prefix": [ + { + "bits": 16, + "cancellation_free_signed_row_l1_upper": "49347", + "reverse": false + }, + { + "bits": 21, + "cancellation_free_signed_row_l1_upper": "1113070", + "reverse": true + } + ], + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 4 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 5 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 6 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 7 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 8 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 9 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 10 + } + ] + }, + "5": { + "bridge_additions": 666, + "controls_rejected": 6, + "formal_columns_checked": 883, + "fresh_center_copies": 45, + "local_raw_H": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "payload_prefix_bits": 93, + "payload_prefix_upper": "9528119495320518471870892800", + "reverse_fresh_center_copies": 18, + "signed_lift_prefix": [ + { + "bits": 16, + "cancellation_free_signed_row_l1_upper": "49347", + "reverse": false + }, + { + "bits": 21, + "cancellation_free_signed_row_l1_upper": "1113070", + "reverse": true + } + ], + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 4 + } + ] + }, + "9": { + "bridge_additions": 1998, + "controls_rejected": 18, + "formal_columns_checked": 1327, + "fresh_center_copies": 81, + "local_raw_H": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "payload_prefix_bits": 93, + "payload_prefix_upper": "9528119495320518471870892800", + "reverse_fresh_center_copies": 36, + "signed_lift_prefix": [ + { + "bits": 16, + "cancellation_free_signed_row_l1_upper": "49347", + "reverse": false + }, + { + "bits": 21, + "cancellation_free_signed_row_l1_upper": "1113070", + "reverse": true + } + ], + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 4 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 5 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 6 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 7 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 8 + } + ] + } + } + }, + "candidate": { + "common_frame_ADDs": 11840, + "copies": 9, + "erasures": 9, + "paid_histogram": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "rank_mass": 5129, + "records": 14769, + "staged": { + "11": { + "bridge_additions": 2664, + "controls_rejected": 24, + "formal_columns_checked": 1549, + "fresh_center_copies": 99, + "local_raw_H": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "payload_prefix_bits": 102, + "payload_prefix_upper": "2659668991063825342552531255296", + "reverse_fresh_center_copies": 45, + "signed_lift_prefix": [ + { + "bits": 17, + "cancellation_free_signed_row_l1_upper": "72399", + "reverse": false + }, + { + "bits": 24, + "cancellation_free_signed_row_l1_upper": "10464656", + "reverse": true + } + ], + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 11840, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 11840, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 11840, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 11840, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 11840, + "signed_inverse": false, + "stage": 4 + }, + { + "fresh_copies": 9, + "scalar_additions": 11840, + "signed_inverse": true, + "stage": 5 + }, + { + "fresh_copies": 9, + "scalar_additions": 11840, + "signed_inverse": false, + "stage": 6 + }, + { + "fresh_copies": 9, + "scalar_additions": 11840, + "signed_inverse": true, + "stage": 7 + }, + { + "fresh_copies": 9, + "scalar_additions": 11840, + "signed_inverse": false, + "stage": 8 + }, + { + "fresh_copies": 9, + "scalar_additions": 11840, + "signed_inverse": true, + "stage": 9 + }, + { + "fresh_copies": 9, + "scalar_additions": 11840, + "signed_inverse": false, + "stage": 10 + } + ] + }, + "5": { + "bridge_additions": 666, + "controls_rejected": 6, + "formal_columns_checked": 883, + "fresh_center_copies": 45, + "local_raw_H": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "payload_prefix_bits": 102, + "payload_prefix_upper": "2659668991063825342552531255296", + "reverse_fresh_center_copies": 18, + "signed_lift_prefix": [ + { + "bits": 17, + "cancellation_free_signed_row_l1_upper": "72399", + "reverse": false + }, + { + "bits": 24, + "cancellation_free_signed_row_l1_upper": "10464656", + "reverse": true + } + ], + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 11840, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 11840, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 11840, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 11840, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 11840, + "signed_inverse": false, + "stage": 4 + } + ] + }, + "9": { + "bridge_additions": 1998, + "controls_rejected": 18, + "formal_columns_checked": 1327, + "fresh_center_copies": 81, + "local_raw_H": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "payload_prefix_bits": 102, + "payload_prefix_upper": "2659668991063825342552531255296", + "reverse_fresh_center_copies": 36, + "signed_lift_prefix": [ + { + "bits": 17, + "cancellation_free_signed_row_l1_upper": "72399", + "reverse": false + }, + { + "bits": 24, + "cancellation_free_signed_row_l1_upper": "10464656", + "reverse": true + } + ], + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 11840, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 11840, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 11840, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 11840, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 11840, + "signed_inverse": false, + "stage": 4 + }, + { + "fresh_copies": 9, + "scalar_additions": 11840, + "signed_inverse": true, + "stage": 5 + }, + { + "fresh_copies": 9, + "scalar_additions": 11840, + "signed_inverse": false, + "stage": 6 + }, + { + "fresh_copies": 9, + "scalar_additions": 11840, + "signed_inverse": true, + "stage": 7 + }, + { + "fresh_copies": 9, + "scalar_additions": 11840, + "signed_inverse": false, + "stage": 8 + } + ] + } + } + }, + "parent": { + "common_frame_ADDs": 13208, + "copies": 9, + "erasures": 9, + "paid_histogram": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "rank_mass": 5129, + "records": 16137, + "staged": { + "11": { + "bridge_additions": 2664, + "controls_rejected": 24, + "formal_columns_checked": 1549, + "fresh_center_copies": 99, + "local_raw_H": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "payload_prefix_bits": 100, + "payload_prefix_upper": "699147249763640764132165496832", + "reverse_fresh_center_copies": 45, + "signed_lift_prefix": [ + { + "bits": 16, + "cancellation_free_signed_row_l1_upper": "49347", + "reverse": false + }, + { + "bits": 24, + "cancellation_free_signed_row_l1_upper": "9534616", + "reverse": true + } + ], + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 13208, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 13208, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 13208, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 13208, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 13208, + "signed_inverse": false, + "stage": 4 + }, + { + "fresh_copies": 9, + "scalar_additions": 13208, + "signed_inverse": true, + "stage": 5 + }, + { + "fresh_copies": 9, + "scalar_additions": 13208, + "signed_inverse": false, + "stage": 6 + }, + { + "fresh_copies": 9, + "scalar_additions": 13208, + "signed_inverse": true, + "stage": 7 + }, + { + "fresh_copies": 9, + "scalar_additions": 13208, + "signed_inverse": false, + "stage": 8 + }, + { + "fresh_copies": 9, + "scalar_additions": 13208, + "signed_inverse": true, + "stage": 9 + }, + { + "fresh_copies": 9, + "scalar_additions": 13208, + "signed_inverse": false, + "stage": 10 + } + ] + }, + "5": { + "bridge_additions": 666, + "controls_rejected": 6, + "formal_columns_checked": 883, + "fresh_center_copies": 45, + "local_raw_H": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "payload_prefix_bits": 100, + "payload_prefix_upper": "699147249763640764132165496832", + "reverse_fresh_center_copies": 18, + "signed_lift_prefix": [ + { + "bits": 16, + "cancellation_free_signed_row_l1_upper": "49347", + "reverse": false + }, + { + "bits": 24, + "cancellation_free_signed_row_l1_upper": "9534616", + "reverse": true + } + ], + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 13208, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 13208, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 13208, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 13208, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 13208, + "signed_inverse": false, + "stage": 4 + } + ] + }, + "9": { + "bridge_additions": 1998, + "controls_rejected": 18, + "formal_columns_checked": 1327, + "fresh_center_copies": 81, + "local_raw_H": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "payload_prefix_bits": 100, + "payload_prefix_upper": "699147249763640764132165496832", + "reverse_fresh_center_copies": 36, + "signed_lift_prefix": [ + { + "bits": 16, + "cancellation_free_signed_row_l1_upper": "49347", + "reverse": false + }, + { + "bits": 24, + "cancellation_free_signed_row_l1_upper": "9534616", + "reverse": true + } + ], + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 13208, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 13208, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 13208, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 13208, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 13208, + "signed_inverse": false, + "stage": 4 + }, + { + "fresh_copies": 9, + "scalar_additions": 13208, + "signed_inverse": true, + "stage": 5 + }, + { + "fresh_copies": 9, + "scalar_additions": 13208, + "signed_inverse": false, + "stage": 6 + }, + { + "fresh_copies": 9, + "scalar_additions": 13208, + "signed_inverse": true, + "stage": 7 + }, + { + "fresh_copies": 9, + "scalar_additions": 13208, + "signed_inverse": false, + "stage": 8 + } + ] + } + } + } + }, + "saved_ADDs": 140, + "search": { + "accepted": 40, + "distance_edges": 1008, + "group_matrices": 168, + "guarded_words": 155, + "helper_preparations": 234, + "literal_positive_instructions": 3688220, + "rejected": 115, + "scores": 1774080 + }, + "source_bound_precision": { + "baseline": { + "bits": 177, + "bound": "117742596540718658156527847560864213734191286190080000" + }, + "candidate": { + "bits": 192, + "bound": "6253203843833393632383133699318586751438846446425369214976" + }, + "formula": "2^18 * F^5 * B^4", + "parent": { + "bits": 189, + "bound": "633952218342189222305933054575935669674977721489175871488" + }, + "source_charge_bits": 192 + }, + "source_checks": { + "baseline": { + "conclusions": { + "C_is_U_inverse": true, + "J_identity": true, + "K_equals_D": true, + "U_block_form": true + }, + "full": { + "columns": 661, + "gates": { + "A": 2075, + "B": 712, + "C": 2574, + "D": 111 + }, + "scatter_terms": 527, + "totals": [ + { + "frame": 510, + "hyperplane_of_punctured_line": [ + 0, + 1, + 1, + 0, + -1, + 0, + 0, + 1 + ], + "rank": 7, + "register": 472 + }, + { + "frame": 511, + "hyperplane_of_punctured_line": [ + 0, + 1, + -1, + 0, + -1, + 0, + 0, + -1 + ], + "rank": 7, + "register": 473 + }, + { + "frame": 512, + "hyperplane_of_punctured_line": [ + 0, + 1, + 1, + 0, + 0, + -1, + -1, + 0 + ], + "rank": 7, + "register": 474 + }, + { + "frame": 513, + "hyperplane_of_punctured_line": [ + 0, + 1, + -1, + 0, + 0, + 1, + -1, + 0 + ], + "rank": 7, + "register": 475 + }, + { + "frame": 514, + "hyperplane_of_punctured_line": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1 + ], + "rank": 7, + "register": 476 + }, + { + "frame": 515, + "hyperplane_of_punctured_line": [ + 1, + 1, + -1, + 1, + 0, + 0, + 0, + 0 + ], + "rank": 7, + "register": 477 + }, + { + "frame": 516, + "hyperplane_of_punctured_line": [ + 1, + 0, + 0, + 1, + 1, + 0, + 0, + 1 + ], + "rank": 7, + "register": 478 + }, + { + "frame": 517, + "hyperplane_of_punctured_line": [ + 0, + 0, + 1, + 1, + 0, + 0, + 1, + -1 + ], + "rank": 7, + "register": 479 + }, + { + "frame": 518, + "hyperplane_of_punctured_line": [ + 0, + 1, + 0, + -1, + 0, + -1, + 0, + -1 + ], + "rank": 7, + "register": 480 + } + ] + }, + "hypotheses": { + "H1_no_target_feeds_z": true, + "H2_D_frame0_targets_from_helpers": true, + "H3_A_z_only_scatter_targets_B_split": true, + "H4_C_literal_reverse_at_full": true, + "H5_V_identity": true + }, + "info": { + "B_target_reads_of_registers_rewritten_earlier_in_B": 111, + "B_z_operand_kinds": { + "helper<-helper": 3, + "helper<-source": 13, + "source<-helper": 108, + "source<-source": 375 + }, + "B_z_operand_kinds_by_dim": { + "dim4:helper<-source": 13, + "dim4:source<-source": 375, + "dim6:helper<-helper": 3, + "dim6:source<-helper": 108 + }, + "B_z_write_frame_dims": { + "4": 388, + "6": 111 + }, + "B_z_writes_after_a_target_read_of_the_same_register": 454, + "cleanup_gates": 2574, + "helper_writes_B": 16, + "source_writes_A": 0, + "source_writes_B": 483, + "sources_rewritten_B": 108, + "target_reads_of_targets": 0, + "z_gates_A": 2075, + "z_gates_B": 499 + }, + "labels": { + "frames": 636, + "gram_det": 1, + "labels": 111, + "lattice_rank": 8, + "punctured": 9, + "root_lines": 120 + } + }, + "candidate": { + "conclusions": { + "C_is_U_inverse": true, + "J_identity": true, + "K_equals_D": false, + "U_block_form": true + }, + "full": { + "columns": 661, + "gates": { + "A": 2075, + "B": 712, + "C": 2574, + "D": 1191 + }, + "scatter_terms": 527, + "totals": [ + { + "frame": 510, + "hyperplane_of_punctured_line": [ + 0, + 1, + 1, + 0, + -1, + 0, + 0, + 1 + ], + "rank": 7, + "register": 472 + }, + { + "frame": 511, + "hyperplane_of_punctured_line": [ + 0, + 1, + -1, + 0, + -1, + 0, + 0, + -1 + ], + "rank": 7, + "register": 473 + }, + { + "frame": 512, + "hyperplane_of_punctured_line": [ + 0, + 1, + 1, + 0, + 0, + -1, + -1, + 0 + ], + "rank": 7, + "register": 474 + }, + { + "frame": 513, + "hyperplane_of_punctured_line": [ + 0, + 1, + -1, + 0, + 0, + 1, + -1, + 0 + ], + "rank": 7, + "register": 475 + }, + { + "frame": 514, + "hyperplane_of_punctured_line": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1 + ], + "rank": 7, + "register": 476 + }, + { + "frame": 515, + "hyperplane_of_punctured_line": [ + 1, + 1, + -1, + 1, + 0, + 0, + 0, + 0 + ], + "rank": 7, + "register": 477 + }, + { + "frame": 516, + "hyperplane_of_punctured_line": [ + 1, + 0, + 0, + 1, + 1, + 0, + 0, + 1 + ], + "rank": 7, + "register": 478 + }, + { + "frame": 517, + "hyperplane_of_punctured_line": [ + 0, + 0, + 1, + 1, + 0, + 0, + 1, + -1 + ], + "rank": 7, + "register": 479 + }, + { + "frame": 518, + "hyperplane_of_punctured_line": [ + 0, + 1, + 0, + -1, + 0, + -1, + 0, + -1 + ], + "rank": 7, + "register": 480 + } + ] + }, + "hypotheses": { + "H1_no_target_feeds_z": true, + "H2_D_frame0_targets_from_helpers": false, + "H3_A_z_only_scatter_targets_B_split": true, + "H4_C_literal_reverse_at_full": true, + "H5_V_identity": true + }, + "info": { + "B_target_reads_of_registers_rewritten_earlier_in_B": 111, + "B_z_operand_kinds": { + "helper<-helper": 3, + "helper<-source": 13, + "source<-helper": 108, + "source<-source": 375 + }, + "B_z_operand_kinds_by_dim": { + "dim4:helper<-source": 13, + "dim4:source<-source": 375, + "dim6:helper<-helper": 3, + "dim6:source<-helper": 108 + }, + "B_z_write_frame_dims": { + "4": 388, + "6": 111 + }, + "B_z_writes_after_a_target_read_of_the_same_register": 454, + "cleanup_gates": 2574, + "helper_writes_B": 16, + "source_writes_A": 0, + "source_writes_B": 483, + "sources_rewritten_B": 108, + "target_reads_of_targets": 0, + "z_gates_A": 2075, + "z_gates_B": 499 + }, + "labels": { + "frames": 636, + "gram_det": 1, + "labels": 111, + "lattice_rank": 8, + "punctured": 9, + "root_lines": 120 + } + }, + "parent": { + "conclusions": { + "C_is_U_inverse": true, + "J_identity": true, + "K_equals_D": false, + "U_block_form": true + }, + "full": { + "columns": 661, + "gates": { + "A": 2075, + "B": 712, + "C": 2574, + "D": 723 + }, + "scatter_terms": 527, + "totals": [ + { + "frame": 510, + "hyperplane_of_punctured_line": [ + 0, + 1, + 1, + 0, + -1, + 0, + 0, + 1 + ], + "rank": 7, + "register": 472 + }, + { + "frame": 511, + "hyperplane_of_punctured_line": [ + 0, + 1, + -1, + 0, + -1, + 0, + 0, + -1 + ], + "rank": 7, + "register": 473 + }, + { + "frame": 512, + "hyperplane_of_punctured_line": [ + 0, + 1, + 1, + 0, + 0, + -1, + -1, + 0 + ], + "rank": 7, + "register": 474 + }, + { + "frame": 513, + "hyperplane_of_punctured_line": [ + 0, + 1, + -1, + 0, + 0, + 1, + -1, + 0 + ], + "rank": 7, + "register": 475 + }, + { + "frame": 514, + "hyperplane_of_punctured_line": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1 + ], + "rank": 7, + "register": 476 + }, + { + "frame": 515, + "hyperplane_of_punctured_line": [ + 1, + 1, + -1, + 1, + 0, + 0, + 0, + 0 + ], + "rank": 7, + "register": 477 + }, + { + "frame": 516, + "hyperplane_of_punctured_line": [ + 1, + 0, + 0, + 1, + 1, + 0, + 0, + 1 + ], + "rank": 7, + "register": 478 + }, + { + "frame": 517, + "hyperplane_of_punctured_line": [ + 0, + 0, + 1, + 1, + 0, + 0, + 1, + -1 + ], + "rank": 7, + "register": 479 + }, + { + "frame": 518, + "hyperplane_of_punctured_line": [ + 0, + 1, + 0, + -1, + 0, + -1, + 0, + -1 + ], + "rank": 7, + "register": 480 + } + ] + }, + "hypotheses": { + "H1_no_target_feeds_z": true, + "H2_D_frame0_targets_from_helpers": false, + "H3_A_z_only_scatter_targets_B_split": true, + "H4_C_literal_reverse_at_full": true, + "H5_V_identity": true + }, + "info": { + "B_target_reads_of_registers_rewritten_earlier_in_B": 111, + "B_z_operand_kinds": { + "helper<-helper": 3, + "helper<-source": 13, + "source<-helper": 108, + "source<-source": 375 + }, + "B_z_operand_kinds_by_dim": { + "dim4:helper<-source": 13, + "dim4:source<-source": 375, + "dim6:helper<-helper": 3, + "dim6:source<-helper": 108 + }, + "B_z_write_frame_dims": { + "4": 388, + "6": 111 + }, + "B_z_writes_after_a_target_read_of_the_same_register": 454, + "cleanup_gates": 2574, + "helper_writes_B": 16, + "source_writes_A": 0, + "source_writes_B": 483, + "sources_rewritten_B": 108, + "target_reads_of_targets": 0, + "z_gates_A": 2075, + "z_gates_B": 499 + }, + "labels": { + "frames": 636, + "gram_det": 1, + "labels": 111, + "lattice_rank": 8, + "punctured": 9, + "root_lines": 120 + } + }, + "previous": { + "conclusions": { + "C_is_U_inverse": true, + "J_identity": true, + "K_equals_D": false, + "U_block_form": true + }, + "full": { + "columns": 661, + "gates": { + "A": 2075, + "B": 712, + "C": 2574, + "D": 1107 + }, + "scatter_terms": 527, + "totals": [ + { + "frame": 510, + "hyperplane_of_punctured_line": [ + 0, + 1, + 1, + 0, + -1, + 0, + 0, + 1 + ], + "rank": 7, + "register": 472 + }, + { + "frame": 511, + "hyperplane_of_punctured_line": [ + 0, + 1, + -1, + 0, + -1, + 0, + 0, + -1 + ], + "rank": 7, + "register": 473 + }, + { + "frame": 512, + "hyperplane_of_punctured_line": [ + 0, + 1, + 1, + 0, + 0, + -1, + -1, + 0 + ], + "rank": 7, + "register": 474 + }, + { + "frame": 513, + "hyperplane_of_punctured_line": [ + 0, + 1, + -1, + 0, + 0, + 1, + -1, + 0 + ], + "rank": 7, + "register": 475 + }, + { + "frame": 514, + "hyperplane_of_punctured_line": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1 + ], + "rank": 7, + "register": 476 + }, + { + "frame": 515, + "hyperplane_of_punctured_line": [ + 1, + 1, + -1, + 1, + 0, + 0, + 0, + 0 + ], + "rank": 7, + "register": 477 + }, + { + "frame": 516, + "hyperplane_of_punctured_line": [ + 1, + 0, + 0, + 1, + 1, + 0, + 0, + 1 + ], + "rank": 7, + "register": 478 + }, + { + "frame": 517, + "hyperplane_of_punctured_line": [ + 0, + 0, + 1, + 1, + 0, + 0, + 1, + -1 + ], + "rank": 7, + "register": 479 + }, + { + "frame": 518, + "hyperplane_of_punctured_line": [ + 0, + 1, + 0, + -1, + 0, + -1, + 0, + -1 + ], + "rank": 7, + "register": 480 + } + ] + }, + "hypotheses": { + "H1_no_target_feeds_z": true, + "H2_D_frame0_targets_from_helpers": false, + "H3_A_z_only_scatter_targets_B_split": true, + "H4_C_literal_reverse_at_full": true, + "H5_V_identity": true + }, + "info": { + "B_target_reads_of_registers_rewritten_earlier_in_B": 111, + "B_z_operand_kinds": { + "helper<-helper": 3, + "helper<-source": 13, + "source<-helper": 108, + "source<-source": 375 + }, + "B_z_operand_kinds_by_dim": { + "dim4:helper<-source": 13, + "dim4:source<-source": 375, + "dim6:helper<-helper": 3, + "dim6:source<-helper": 108 + }, + "B_z_write_frame_dims": { + "4": 388, + "6": 111 + }, + "B_z_writes_after_a_target_read_of_the_same_register": 454, + "cleanup_gates": 2574, + "helper_writes_B": 16, + "source_writes_A": 0, + "source_writes_B": 483, + "sources_rewritten_B": 108, + "target_reads_of_targets": 0, + "z_gates_A": 2075, + "z_gates_B": 499 + }, + "labels": { + "frames": 636, + "gram_det": 1, + "labels": 111, + "lattice_rank": 8, + "punctured": 9, + "root_lines": 120 + } + } + }, + "status": "PASS_R439_HELPER_TRIPLES_FINITE" +} diff --git a/research/r439-helper-triples/NOTICE.md b/research/r439-helper-triples/NOTICE.md new file mode 100644 index 0000000000..222ac661f3 --- /dev/null +++ b/research/r439-helper-triples/NOTICE.md @@ -0,0 +1,45 @@ +# Attribution and license + +New research, implementation and documentation: Ross Richardson +(@RossRichardson), with substantial OpenAI Codex assistance throughout. +Apache-2.0 under the repository license. One AI agent performed the work; +algorithmic independence does not mean independent human review. + +Gareth Davidson (@bitplane), PR915 at +`e9daefe320a0043000bd9746664ed02c3287d056`, supplies the frozen target basis; +PR926 at `0f216a345c37bc71cc0e22030ef11ec31b26a69e` supplies the disjoint +helper-pair comparator, source manifest and checking harness. `native.py` +is adapted from his PR926 runner; its original attribution is retained. +The new verifier calls the pinned predecessor's I/O, literal interpreter, +arbitrary-input boundary checker and unmodified owning tools. Its GL(3,2) +enumeration, Gaussian inverse and set-valued search check are independent +implementations of this contribution's packed BFS/column search. The native +harness lineage includes Sagar Thakrar's R420 decoder-sharing harness. + +Scott Woolsey Biggart's PR733 at +`dfe84e09298abc5c5e0074afda59a821e10abfb4` supplies the prior two-sided +binary compensation mechanism. PR926 preserves its original README and +notice. Mikhail R. Gadelha's semantic helper restoration, Greer Guthrie's +helper bases, Scott Woolsey Biggart's and Sagar Thakrar's target bases, +commdata2338's guarded search and Dugongue's reversible factoring precedents +remain credited through that manifest and notice. + +The bit word is DreamingOfClouds' PR589 at +`a5afc8c6169ea61ba7c51dfd3cade02cc7b13b46`, on eumemic's PR555/543, +with Jacob Sussman's E8 construction and the retained community lineage. +Owning geometry/interface tools are eumemic's; native exporter, staging and +checker lineage includes Dylan Crow, DaysSky, Zhihao Chen, DreamingOfClouds, +Chafik Boukhalfa and the contributors named in the unchanged source notices. +Niels Lohmann and contributors retain their MIT JSON-header license. Boost +is used only as a build dependency and is not redistributed here. + +Concurrent PR941 by Gareth Davidson gives distinct matching evidence in +the disjoint-pair class. We read its exact-head description and credit it +as context; we do not import its proof, executable or numerical certificate. +PR952's separate six-wire synthesis and other concurrent local-frame +improvements are not included in our reported saving. + +Original contributor notices, licenses and AI disclosures are retained at +their source paths. The original `upstream/` inputs are untouched. No +priority is claimed for Gaussian elimination, breadth-first search, +conjugation, shortest-path certificates or semantic D substitution. diff --git a/research/r439-helper-triples/PROOF.md b/research/r439-helper-triples/PROOF.md new file mode 100644 index 0000000000..8d92cdbdbd --- /dev/null +++ b/research/r439-helper-triples/PROOF.md @@ -0,0 +1,116 @@ +# Semantic boundary, complete cost and the finite search class + +All circuit identities here are over F2. Positive integer envelopes are a +separate calculation; cancellation in F2 cannot lower their invoice. + +## Boundary identity on arbitrary inputs + +Let `x` be the 111 source registers, `y` the 111 arbitrary target registers, +and `s` the 439 arbitrary dirty helpers. PR589's D has matrix K and endpoint +`(x,y,s) -> (x,y+Ks,s)`. PR915 supplies a fixed chronological word of 306 +target transvections, with matrix E. It directly injects EK between E and +its inverse. Both K and E are reconstructed from pinned inputs. + +Partition the helper coordinates into 152 unchanged pairs, 40 triples and +15 untouched singletons. Each triple joins exactly one original PR926 pair +to a distinct originally unmatched helper. Let H be the invertible map on +helpers obtained by the concatenation of the chosen component words. Each +component acts on disjoint coordinates, so no hidden connection between +components is needed. Inside a component the operations can fail to commute. + +Perform these five steps: + +1. Apply H to the helpers. +2. Apply E to the targets. +3. Inject `M = E K H^-1` from helpers to targets, once per nonzero coefficient. +4. Apply E^-1 to the targets. +5. Apply H^-1 to the helpers. + +After step 3 the target is `Ey + E K H^-1 Hs = Ey + EKs`. +Steps 4 and 5 produce `y+Ks` and `s`. No step reads or writes x. This proves +the D boundary for arbitrary target and helper dirt. Chronological reversal +implements each inverse because each individual CNOT is self-inverse; +applying the component's original order is generally incorrect. A control +detects that mistake in the actual candidate. + +For a chronological helper operation `s_d <- s_d + s_q`, write its matrix +as S. Extending H on the left changes the middle on the right by S: +`E K (S H)^-1 = (E K H^-1) S`. Thus column q, not column d, changes by XOR +with column d. The search uses this packed-column rule. The independent +verifier obtains H^-1 by Gaussian elimination and derives the columns from +that inverse. Full arbitrary-input column checks additionally test the +complete emitted D and its inverse against the original K. + +## Complete finite bill + +For a chosen helper component Q with preparation length l, its contribution +is `2l + wt((EK H^-1)|Q)`. The factor two pays both preparation and undo. +The target preparation and undo add 612, regardless of Q. Because the helper +components are disjoint, their column weights and costs add exactly. + +The chosen schedule has helper preparation length +`152 + 38*2 + 2*3 = 234`, middle weight 4,540, and D cost +`2*234 + 2*306 + 4540 = 5620`. The unchanged A/scatter/B/C suffix costs +6,220, giving 11,840 complete ADDs and saving 140 relative to PR926. + +The old and new D gates are at frame zero. They use only existing targets +and helpers already at that frame. The candidate changes no source access, +copied-total role, child profile or frame schedule. The literal exported +MOVE sequence of every register and all COPY/ERASE records are compared +with PR589, not inferred only from the endpoint identity. At 5/9/11 stages +the 140 local savings correspond to 700/1,260/1,540 ADDs; the unchanged +bridge and copy operations remain fully charged by the native checker. + +These counts are finite compiler evidence, not a complete asymptotic +recurrence or a replacement global supplier invoice. + +## Exhaustive small group and bounded larger search + +There are `(8-1)(8-2)(8-4)=168` invertible 3 by 3 Boolean matrices. The +six directed CNOTs generate the group: row addition plus row swapping +(three additions) gives Gaussian elimination. BFS therefore reaches all +168 maps and gives a shortest representative for each, for its declared +generator order. No claim depends on an unstated synthesis heuristic. + +The independent distance certificate consists of the 168 realizing words +and their lengths. Direct enumeration checks that every invertible matrix +appears once. For every directed generator edge, the two endpoint lengths +differ by at most one. Starting at distance zero for identity, these +inequalities show every identity-to-matrix path has length at least its +recorded length. Its realizing word supplies equality. This certifies the +unweighted shortest CNOT length, not a precision optimum. + +For each original pair and unmatched helper the search evaluates all 168 +maps using one such representative, totaling 1,774,080 scored alternatives. +It then performs one seed-12 tie-broken greedy pass over all positive-gain +alternatives, rejecting coordinate conflicts and failing integer guards. +The verifier independently repeats every score and the full pass. The 40 +accepted changes are compatible by construction. + +Different shortest representatives can have different positive envelopes; +longer representatives can also have different envelopes. Neither family +is exhausted here. Nor are alternate E, components of size four or more, +changes to an already accepted triple, or other greedy orders. No optimality +claim is made for the 11,840-ADD complete word. + +## Precision and interfaces + +Literal noncancelling execution in both directions gives F=72,399 and +B=10,464,656. The integer expressions in the README satisfy strict 104-bit +local and 192-bit nine-stage inequalities. Every admitted intermediate word +passes the same two inequalities. The staged native replay independently +agrees with both maxima, includes all bridge operations and rejects omitted +bridges. The 115 rejected alternatives are not evidence of a universal +obstruction; they fail these specific complete-word bounds at their turn. + +Replacing D preserves the full finite endpoint because the new D agrees +with the original D before the unchanged suffix begins. Original gate-local +H2 and the literal K extractor still reject its internal form. Consequently +the construction relies on the same semantic D-substitution obligation as +PR915/926. Whole-hosted emission, precision allocation, supplier admission, +outer assembly and the selected theorem's inherited assumptions remain +outside this result. + +The identity and exact finite checks do not formalize the full integer +multiplication theorem. Basis conjugation and semantic substitution are +predecessor mechanisms credited in NOTICE.md, not new claims of priority. diff --git a/research/r439-helper-triples/README.md b/research/r439-helper-triples/README.md new file mode 100644 index 0000000000..3ae21b85e0 --- /dev/null +++ b/research/r439-helper-triples/README.md @@ -0,0 +1,143 @@ +# R439 compensation with coupled helper triples + +**Finite bit-circuit construction; no new kappa.** Replacing 40 disjoint +PR926 helper pairs and 40 unused helpers by coupled three-helper bases saves +**140 further ADDs**, including every preparation and restoration operation. +The complete local word has **11,840 ADDs**, versus 11,980 in PR926, +13,208 in PR915 and 24,305 in selected bit source PR589. + +The selected conditional bound at this contribution's base remains +`1661957774647029/10^18 = 0.001661957774647029`, from PR890 with PR589. +This package does not replace that selection or claim a multiplication +runtime improvement. + +| Exact quantity | PR926 | Helper triples | +|---|---:|---:| +| Helper preparation / restoration, each | 192 | 234 | +| Target preparation / restoration, each | 306 | 306 | +| Middle injections | 4,764 | 4,540 | +| Complete D ADDs | 5,760 | 5,620 | +| Complete local ADDs | 11,980 | 11,840 | +| Forward positive maximum F | 71,907 | 72,399 | +| Reverse positive maximum B | 10,562,318 | 10,464,656 | +| Local expression bit length | 102 | 102 | +| Nine-stage expression bit length | 192 | 192 | + +Thus the complete prefix bill is **234 + 306 + 4,540 + 306 + 234 = 5,620**. +The unchanged suffix costs 6,220 ADDs. The 40 replacements consist of 38 +two-ADD preparations and two three-ADD preparations. The other 152 helper +pairs remain in place. No scratch helper, source access, MOVE path, +COPY/ERASE, frame, copied total or recursive child is added. All non-D +fields of the word remain identical to PR589; native replay checks the +exported resource equality separately. + +## Reproduce + +From the repository root, with Python 3.12+, a C++17 compiler and Boost: + +```sh +python3 -I -B research/r439-helper-triples/verify.py +``` + +For a nonstandard Boost installation, set `BOOST_INCLUDE` to its include +root. Set `CXX` if needed. The final line is: + +```text +PASS_R439_HELPER_TRIPLES_FINITE: 11,980 -> 11,840 ADDs; 40 helper triples; no new kappa +``` + +The command regenerates the complete search certificate and canonical word, +checks them independently, runs the owning E8/frame/interface checks, +compiles unchanged native checkers and tests the original, PR915 and new +words at 5, 9 and 11 stages. The complete report must equal `EXPECTED.json`. +Use `--output NEW_DIRECTORY` to retain logs and all generated evidence. +`--python-only` explicitly produces partial evidence with a different status. +`--record` creates a previously absent expected receipt and never overwrites +one; it is for initial artifact generation, not ordinary verification. + +The isolated standard-library discovery command is: + +```sh +python3 -I -B research/r439-helper-triples/search.py --output /tmp/new-r439-triple-search +``` + +It reproduces `CERTIFICATE.json` and `candidate.json.gz`; gzip payloads are +compared canonically, not by regenerated compression bytes. + +## Bounded experiment and independent evidence + +Assignment seed **12** came from operating-system randomness. The claim and +three considered tasks are in `CLAIM.json`. With the PR915 target basis +fixed, the domain is every one of PR926's **192 pairs**, each of its **55 +unused helpers**, and all **168 elements of GL(3,2)**: **1,774,080 scores**. +Breadth-first search nominates one shortest chronological CNOT word for +each matrix; seed 12 orders generators and ties. Both copies of that word +are charged. This is a new overlapping-helper search class, beyond the +disjoint-pair restriction; merely changing the matching seed is not its +mechanism. + +One sorted greedy pass considers all **935 strict-gain nominees**: **40** +are accepted, **115** fail an exact prefix guard, and **780** conflict with +an already used pair or singleton. It stops after that pass, without a +restart. Each successful replacement consumes a distinct original pair and +singleton. Search coverage is complete for this declared domain and these +representatives; it is not a global circuit optimum or an optimum over all +shortest words, longer words, alternate target bases or overlapping triples. + +The independent verifier enumerates invertible matrices directly and uses +Boolean Gaussian elimination, set-valued supports and literal scalar +instructions. It checks **1,008 neighbor inequalities** plus realizing +paths to certify all 168 shortest lengths, all search scores/ties, every +guard decision and the final word. Each of the 661 source, target and dirty +helper columns is replayed separately in both D directions for four words. +Controls remove preparation, restoration and middle coefficients, reverse +the required undo order, transpose helper directions and corrupt a group +certificate. A cancelling helper pair is accepted at the boundary but +charged two ADDs. Every over-budget nominee remains rejected. + +The owning checker is imported unchanged. It confirms the full endpoint, +geometry and H1/H3/H4/H5 predicates. As in PR915/926, **original syntactic +H2 and literal `K_equals_D` are false**; the complete semantic boundary is +checked independently instead. No predicate is rewritten to hide this. + +The exact numerical checks are: + +```text +64 F^3 B^2 = 2659668991063825342552531255296 < 2^104 +2^18 F^5 B^4 = 6253203843833393632383133699318586751438846446425369214976 < 2^192 +``` + +The second uses about **99.6193%** of its ceiling. Exact integers, not rounded +bit counts, decide admission. The expression and 192-bit charge are checked +against the unchanged supplier source. These are finite local/staged bounds, +not a complete hosted precision invoice. + +## Predecessors, pins and remaining obligations + +Exact research base: `007664306fff84fbb1c9a1b4053b69f439764034`. +`SOURCES.json` pins executable/data dependencies and records the selected +context at that base separately from runtime dependencies. The full consumed +predecessor closure is also checked through PR926's existing manifest. + +Credit Gareth Davidson's **PR915** target basis and **PR926** disjoint helper +construction, and Scott Woolsey Biggart's **PR733** two-sided mechanism. +The new contribution is the bounded coupled-triple replacement and its +independent evidence. Concurrent **PR941** reports a disjoint-pair floor of +11,948 ADDs with this target basis; the present 11,840-ADD word is outside +that class. This package does not import or independently certify PR941's +matching proof. PR952's six-wire phase-A synthesis concerns another section; +its savings are not composed here. The earlier factored-retiming negative +searches and unevidenced campaign triple proposal concern different objects +and do not establish an obstruction to this search class. + +Before using this word as the bit supplier, accept the semantic D interface, +emit and audit the complete hosted supplier, recompute the entire finite and +precision invoice and rebuild the outer assembly. Inherited all-size/compiler, +common-label/mutable-source realization, whole-call hosting, precision/tape +and analytic obligations remain. This is neither a formal proof of the full +multiplication theorem nor independent human peer review. It does not compose +other circuit savings or alter `upstream/`. + +Prepared by **Ross Richardson (@RossRichardson)** with substantial +**OpenAI Codex assistance** in research, implementation, proof checking and +packaging. Apache-2.0; cumulative attribution is in `NOTICE.md`. diff --git a/research/r439-helper-triples/SOURCES.json b/research/r439-helper-triples/SOURCES.json new file mode 100644 index 0000000000..28a8cea8f6 --- /dev/null +++ b/research/r439-helper-triples/SOURCES.json @@ -0,0 +1,26 @@ +{ + "base_commit": "007664306fff84fbb1c9a1b4053b69f439764034", + "files": { + "research/r439-two-sided-compensation/CERTIFICATE.json": "3abb601be609f117361e17ce5ada5477d4493ee6aec9070c749089ec923e1848", + "research/r439-two-sided-compensation/candidate.json.gz": "6ac771545e823c054e005429c405dbb2c01ff80fce181b714e1af5e28b6b7cb2", + "research/r439-two-sided-compensation/vendor/pr915/CERTIFICATE.json": "a9958d9a933b57dcb9f7e5cf8e9694c0762f055a1cdab9f8ab42b2c6561fc4d7", + "research/r439-two-sided-compensation/vendor/pr915/candidate.json.gz": "ac30266144f8772ec8cd629153993aa9eb692fe745a9f95015a1b7fa88977a2e", + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f", + "research/r439-two-sided-compensation/build.py": "df6d146c8cfb60046fe01ba4b02e673179c4317c66c16618ccb5675debda3a3b", + "research/r439-two-sided-compensation/verify.py": "4bf608cab413d40ec4ade21f05bd9ea38dedaf688c2df306f1024095b3142617", + "research/r439-two-sided-compensation/common.py": "885d19538d04ae22387ead8e0445a0bd0d36af30c0bb4e38e439b04e535ff190", + "research/r439-two-sided-compensation/native.py": "297c5a20e7f422509e63eb0a97abf7556c3347e03a83bb3b5e7a1cfc256250de", + "research/r439-two-sided-compensation/SOURCES.json": "6334cb185db0568919f5fcce85edaad1ceec1ffaf3e4ac08e6e9e819a8017eb1" + }, + "predecessors": { + "PR589": "a5afc8c6169ea61ba7c51dfd3cade02cc7b13b46", + "PR915": "e9daefe320a0043000bd9746664ed02c3287d056", + "PR926": "0f216a345c37bc71cc0e22030ef11ec31b26a69e", + "PR733": "dfe84e09298abc5c5e0074afda59a821e10abfb4", + "PR941_context_only": "8af78333709a2eafd84463a7dc91467be5618b49" + }, + "context_at_base_not_runtime_dependencies": { + "certificates/selected-result.json": "41fb066ff0f43ce472323195e9088d6d888715c13c54eae7b42e357ed5bfc726", + "docs/research/community-frontier890-review.md": "cd03b7c2c6c09db2cfa89ae40133ae44e1deb6e32ec5ddd23aacecc9c50f2fea" + } +} diff --git a/research/r439-helper-triples/VALIDATION.md b/research/r439-helper-triples/VALIDATION.md new file mode 100644 index 0000000000..577524e2f4 --- /dev/null +++ b/research/r439-helper-triples/VALIDATION.md @@ -0,0 +1,59 @@ +# Validation receipt and limits + +Research base: `007664306fff84fbb1c9a1b4053b69f439764034`. +Assignment seed: 12. Local run date: 2026-10-13 UTC / 2026-10-14 Melbourne. + +The initial complete receipt was generated with: + +```sh +BOOST_INCLUDE=/private/tmp/boost_1_87_0 python3 -I -B research/r439-helper-triples/verify.py --record --output /private/tmp/r439-helper-triples-verification-seed12-v2 +``` + +Environment: CPython 3.14.6, macOS 26.5.2 arm64, Apple clang 17.0.0 +(`clang-1700.6.4.2`), Boost 1.87 headers. The Boost path is local build +configuration, not a required fixed path. No network is needed for replay. + +`EXPECTED.json` records the complete deterministic receipt. It includes: + +- 168 independently enumerated GL(3,2) maps and 1,008 distance edges; +- 1,774,080 independently rescored choices with an identical census digest; +- 155 guarded complete words and 3,688,220 literal positive instructions; +- 40 accepted replacements, 115 exact guard rejections, 780 conflicts; +- 661 separate arbitrary input columns, four words, both D directions; +- ten local control categories and a charged cancelling-pair control; +- unchanged owning E8/frame/endpoint checks on all four words; +- original, PR915 and candidate native legality plus 5/9/11-stage replays, + covering 883/1,327/1,549 columns per word and 144 rejected omitted bridges; +- unchanged rank mass 5,129, all paid rank counts, nine COPY/ERASE pairs, + and every register's MOVE path; +- exact source-bound 104-bit local and 192-bit nine-stage inequalities. + +The ordinary verification command was then rerun into a fresh directory, +without `--record`, and passed exact comparison of the full committed receipt: + +```sh +BOOST_INCLUDE=/private/tmp/boost_1_87_0 python3 -I -B research/r439-helper-triples/verify.py --output /private/tmp/r439-helper-triples-final-seed12 +``` + +Final status: `PASS_R439_HELPER_TRIPLES_FINITE`. This fresh run rebuilt all +four C++ binaries and reran the complete checks listed above. Both the +certificate and regenerated gzip payload compare canonically and completely. + +The independent census and group check passed on the first implementation +run; its reporting layer then tried to serialize byte-valued boundary columns +as JSON and raised TypeError. That comparison was changed to direct byte +equality. The completed fresh run above passes every stage. This was a +verifier implementation error, not a circuit counterexample or failed search. + +`make selected-record-check` passes for PR890 at the exact base. Repository +wide `make verify`, complete cold supplier reconstruction, whole-hosted +adoption, outer assembly and Lean multiplication formalization were not run: +this isolated research package changes none of their inputs or selected +artifacts. The native checks are scoped evidence, not substitutes for those +remaining admission obligations. Hosted CI status is separate from these +local checks and is reported in the PR. + +The open queue was refreshed through PR962 before packaging. PR941's +disjoint-pair result and PR952's phase-A synthesis remain distinct. Main +still matched the exact base at that refresh. No coordination issue was +pinned; the claim and final result are recorded locally in CLAIM.json. diff --git a/research/r439-helper-triples/candidate.json.gz b/research/r439-helper-triples/candidate.json.gz new file mode 100644 index 0000000000..e74d3a8ede Binary files /dev/null and b/research/r439-helper-triples/candidate.json.gz differ diff --git a/research/r439-helper-triples/native.py b/research/r439-helper-triples/native.py new file mode 100644 index 0000000000..090ecca175 --- /dev/null +++ b/research/r439-helper-triples/native.py @@ -0,0 +1,112 @@ +#!/usr/bin/env python3 +"""Unmodified native legality and 5/9/11-stage checks, R439 helper triples. + +Harness adapted from Sagar Thakrar's research/r420-decoder-sharing/native.py. +Gareth Davidson / PR926 harness, adapted by Ross Richardson with +substantial OpenAI Codex assistance. Apache-2.0. +""" +import os +from pathlib import Path +import runpy +import shlex +import struct +import subprocess +import sys + +C = runpy.run_path(str(Path(__file__).resolve().parents[1] / "r439-two-sided-compensation/common.py")) +need = C["need"] + + +def run(root, baseline, parent, candidate, output): + C["pins"](root) + output = Path(output).resolve() + output.mkdir(parents=True, exist_ok=False) + hub = Path(root).resolve() / C["HUB"] + checker = hub / "code/bit/checkers" + compiler = shlex.split(os.environ.get("CXX", "c++")) + includes = ["-I" + str(hub / "portable-include"), "-I" + str(checker), + "-I" + os.environ.get("BOOST_INCLUDE", "/usr/include")] + commands = [] + + def execute(args, log): + args = [str(x) for x in args] + commands.append(args) + with log.open("x") as stream: + subprocess.run(args, stdout=stream, stderr=subprocess.STDOUT, check=True) + + common = compiler + ["-O2", "-std=c++17", "-DHDIM=8", "-DNCOPY=9"] + includes + execute(common + ["-o", output / "legality", checker / "legality_h.cpp"], + output / "compile-legality.log") + for k in (2, 4, 5): + execute(common + ["-DVPORTS=111", "-DRHELP=439", "-DKPAIRS=" + str(k), + "-o", output / ("columns-" + str(k)), checker / "columns_k.cpp"], + output / ("compile-columns-" + str(k) + ".log")) + python = [sys.executable, "-I", "-B"] + result, nonadd = {}, {} + for label, word in (("baseline", baseline), ("parent", parent), ("candidate", candidate)): + print("native", label, flush=True) + folder = output / label + folder.mkdir() + records, cin, cout = (folder / name for name in ("records", "cin", "cout")) + execute(python + [hub / "code/bit/export_records.py", Path(word).resolve(), records], + folder / "export.log") + execute(python + [hub / "code/bit/regression/stage_cohort.py", records, records, cin, cout], + folder / "stage.log") + execute([output / "legality", cin, cout, cout / "legality.json"], folder / "legality.log") + legality = C["load"](cout / "legality.json") + need(legality["status"] == "PASS_INDEPENDENT_COHORT_LEGALITY_SOURCE_OWNERS_AND_LIFECYCLE", + "native legality") + need(legality["copies"] == legality["erasures"] == 9, "native copy lifecycle") + # Per-register MOVE sequences, including ranks, and unchanged COPY/ERASE blocks. + record_rows = list(struct.iter_unpack("<6i", (records / "249-records.bin").read_bytes())) + movements = {} + for row in record_rows: + if row[0] == 0: + movements.setdefault(str(row[1]), []).append(list(row)) + nonadd[label] = {"moves": movements, "copy_erase": [list(x) for x in record_rows if x[0] in (2, 3)]} + columns_receipts = {} + for k in (2, 4, 5): + name = "columns-" + str(k) + execute([output / name, cout / "COHORT249-RECORDS.bin", cout / (name + ".json")], + folder / (name + ".log")) + columns = C["load"](cout / (name + ".json")) + expected_status = ("PASS_NEW_COHORT249_ALL_FIVE_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL" if k == 2 + else "PASS_NEW_COHORT249_ALL_BRIDGED_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL") + need(columns["status"] == expected_status, "native columns") + need(columns["formal_columns_checked"] == 2 * k * 111 + 439, "column coverage") + need(len(columns["stages"]) == 2 * k + 1, "stage coverage") + need(columns["bridge_additions"] == 6 * (k - 1) * 111, "bridge cost") + need(columns["fresh_center_copies"] == 9 * (2 * k + 1), "stage COPY cost") + need(columns["payload_prefix_bits"] <= 104, "inherited prefix cap") + controls = columns["negative_controls"] + need(len(controls) == 6 * (k - 1) and all(x["rejected"] is True for x in controls), + "omitted bridge controls") + need(legality["common_frame_ADDs"] == columns["local_scalar_additions"], "ADD agreement") + columns_receipts[str(2 * k + 1)] = {key: columns[key] for key in ( + "formal_columns_checked", "bridge_additions", "fresh_center_copies", "reverse_fresh_center_copies", + "signed_lift_prefix", "payload_prefix_bits", "payload_prefix_upper", "local_raw_H", "stages")} + columns_receipts[str(2 * k + 1)]["controls_rejected"] = len(controls) + result[label] = {key: legality[key] for key in ("records", "common_frame_ADDs", "rank_mass", "paid_histogram", + "copies", "erasures")} + result[label]["staged"] = columns_receipts + expected = {"baseline": (24305, 49347, 1113070, 177), + "parent": (13208, 49347, 9534616, 189), + "candidate": (11840, 72399, 10464656, 192)} + before = result["baseline"] + for label, (adds, forward, backward, nine_bits) in expected.items(): + after = result[label] + need(C["canonical"](nonadd["baseline"]) == C["canonical"](nonadd[label]), "frame paths changed") + need(after["common_frame_ADDs"] == adds, "native ADD cost") + need(before["records"] - after["records"] == 24305 - adds, "unexpected record changes") + for key in ("rank_mass", "paid_histogram", "copies", "erasures"): + need(before[key] == after[key], "paid resources changed: " + key) + for stage in ("5", "9", "11"): + old, new = before["staged"][stage], after["staged"][stage] + need(old["local_raw_H"] == new["local_raw_H"], "local raw ranks changed") + bounds = [int(x["cancellation_free_signed_row_l1_upper"]) for x in new["signed_lift_prefix"]] + need(bounds == [forward, backward], "literal/native positive bound agreement") + value = (1 << 18) * bounds[0] ** 5 * bounds[1] ** 4 + need(value.bit_length() == nine_bits and value < 1 << 192, "nine-stage prefix bound") + C["write"](output / "commands.json", commands) + C["write"](output / "native-report.json", result) + return result diff --git a/research/r439-helper-triples/search.py b/research/r439-helper-triples/search.py new file mode 100644 index 0000000000..3075181210 --- /dev/null +++ b/research/r439-helper-triples/search.py @@ -0,0 +1,202 @@ +#!/usr/bin/env python3 +"""Bounded, fully charged GL(3,2) replacements of R439 helper pairs. + +Ross Richardson, with substantial OpenAI Codex assistance. Apache-2.0. +The frozen target basis and disjoint-pair predecessor are Gareth Davidson's +PR915 and PR926, extending Scott Woolsey Biggart's PR733 mechanism. +""" +import argparse +from collections import deque +import copy +import gzip +import hashlib +import json +from pathlib import Path +import random +import runpy + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PRE = ROOT / "research/r439-two-sided-compensation" +SEED = 12 + + +def load(path): + path = Path(path) + data = path.read_bytes() + return json.loads(gzip.decompress(data) if path.suffix == ".gz" else data) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def digest(value): + return hashlib.sha256(canonical(value)).hexdigest() + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def pins(): + for path, expected in load(HERE / "SOURCES.json")["files"].items(): + require(hashlib.sha256((ROOT / path).read_bytes()).hexdigest() == expected, + "source pin: " + path) + + +def group(): + """All maps, with one seed-determined shortest chronological helper word.""" + generators = [(d, s) for d in range(3) for s in range(3) if d != s] + random.Random(SEED).shuffle(generators) + words = {(1, 2, 4): []} + queue = deque(words) + while queue: + matrix = queue.popleft() + for d, s in generators: + nxt = list(matrix) + nxt[d] ^= nxt[s] + nxt = tuple(nxt) + if nxt not in words: + words[nxt] = words[matrix] + [(d, s)] + queue.append(nxt) + require(len(words) == 168, "GL(3,2) order") + return words + + +def input_data(): + parent = load(PRE / "vendor/pr915/candidate.json.gz") + target_count = len(load(PRE / "vendor/pr915/CERTIFICATE.json")["steps"]) + previous = load(PRE / "CERTIFICATE.json") + pairs = [(step["a"], step["b"]) for step in previous["steps"]] + used = {j for pair in pairs for j in pair} + unused = sorted(set(range(parent["R"])) - used) + columns = [0] * parent["R"] + for _, destination, sources in parent["D"][target_count:target_count + parent["v"]]: + for source in sources: + columns[source - 2 * parent["v"]] ^= 1 << (destination - parent["v"]) + require((len(pairs), len(unused), target_count) == (192, 55, 306), "input dimensions") + return parent, target_count, pairs, unused, columns + + +def inverse_columns(word): + masks = [1, 2, 4] + for d, s in word: + masks[s] ^= masks[d] + return masks + + +def candidate(parent, target_count, columns, pairs, replacements): + operations = [] + for index, pair in enumerate(pairs): + if index not in replacements: + operations.append(pair) + else: + singleton, word = replacements[index] + labels = (*pair, singleton) + operations.extend((labels[d], labels[s]) for d, s in word) + transformed = list(columns) + for d, s in operations: + transformed[s] ^= transformed[d] + v = parent["v"] + helpers = [[0, 2 * v + d, [2 * v + s]] for d, s in operations] + middle = [[0, v + i, [2 * v + j for j, col in enumerate(transformed) if col >> i & 1]] + for i in range(v)] + result = copy.deepcopy(parent) + result["D"] = helpers + parent["D"][:target_count] + middle + parent["D"][target_count + v:] + helpers[::-1] + return result + + +def charges(word): + # Frozen predecessor's macro interpreter. verify.py uses literal events. + helpers = runpy.run_path(str(PRE / "build.py")) + forward = helpers["bounds"](word) + backward = helpers["bounds"](word, True) + return {"F": forward, "B": backward, + "D_adds": sum(len(g[2]) for g in word["D"]), + "native_ADDs": sum(len(g[2]) for sec in "DABC" for g in word[sec]) + sum(map(len, word["scatter"])), + "local_expression": 64 * forward ** 3 * backward ** 2, + "nine_stage_expression": (1 << 18) * forward ** 5 * backward ** 4} + + +def admitted(bill): + return bill["local_expression"] < 1 << 104 and bill["nine_stage_expression"] < 1 << 192 + + +def nominate(): + pins() + parent, target_count, pairs, unused, columns = input_data() + words = group() + representatives = [(matrix, word, inverse_columns(word)) for matrix, word in sorted(words.items())] + rng = random.Random(SEED) + census_hash = hashlib.sha256() + nominees = [] + scores = 0 + for index, (a, b) in enumerate(pairs): + for c in unused: + local = [columns[a], columns[b], columns[c]] + sums = [0] * 8 + for mask in range(1, 8): + low = mask & -mask + sums[mask] = sums[mask ^ low] ^ local[low.bit_length() - 1] + baseline_cost = 2 + sums[1].bit_count() + sums[3].bit_count() + sums[4].bit_count() + for matrix, word, masks in representatives: + cost = 2 * len(word) + sum(sums[mask].bit_count() for mask in masks) + gain = baseline_cost - cost + tie = rng.getrandbits(64) + row = [index, c, list(matrix), gain, tie] + census_hash.update(canonical(row) + b"\n") + scores += 1 + if gain > 0: + nominees.append((-gain, tie, index, c, matrix, word)) + nominees.sort() + baseline = candidate(parent, target_count, columns, pairs, {}) + require(digest(baseline) == digest(load(PRE / "candidate.json.gz")), "reconstruct PR926") + baseline_bill = charges(baseline) + replacements, taken_singletons, history, rejected = {}, set(), [], [] + conflicts = 0 + for negative_gain, tie, index, c, matrix, word in nominees: + if index in replacements or c in taken_singletons: + conflicts += 1 + continue + trial_replacements = {**replacements, index: (c, word)} + trial = candidate(parent, target_count, columns, pairs, trial_replacements) + bill = charges(trial) + entry = {"pair_index": index, "singleton": c, "matrix": list(matrix), + "word": word, "gain": -negative_gain, "bill": bill} + if not admitted(bill): + rejected.append(entry) + continue + replacements = trial_replacements + taken_singletons.add(c) + history.append(entry) + result = candidate(parent, target_count, columns, pairs, replacements) + result_bill = charges(result) + certificate = {"format": "r439-helper-triples/1", "seed": SEED, + "group": [{"matrix": list(m), "word": w} for m, w in sorted(words.items())], + "pair_count": len(pairs), "singleton_count": len(unused), "scores": scores, + "positive_nominees": len(nominees), "census_sha256": census_hash.hexdigest(), + "conflicts": conflicts, "rejected": rejected, "accepted": history, + "baseline": baseline_bill, "result": result_bill, + "saved_ADDs": baseline_bill["native_ADDs"] - result_bill["native_ADDs"], + "candidate_sha256": digest(result), + "stopping_rule": "one sorted pass through every strict-gain representative; no restart"} + require(certificate["saved_ADDs"] == sum(x["gain"] for x in history), "disjoint gain accounting") + return result, certificate + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, required=True, help="new directory") + args = parser.parse_args() + args.output.mkdir(parents=True, exist_ok=False) + result, certificate = nominate() + (args.output / "CERTIFICATE.json").write_text(json.dumps(certificate, indent=2) + "\n") + (args.output / "candidate.json.gz").write_bytes(gzip.compress(canonical(result), mtime=0)) + print(json.dumps({k: certificate[k] for k in ("scores", "positive_nominees", "conflicts", "saved_ADDs", "result")})) + print("accepted", len(certificate["accepted"]), "rejected", len(certificate["rejected"])) + + +if __name__ == "__main__": + main() diff --git a/research/r439-helper-triples/verify.py b/research/r439-helper-triples/verify.py new file mode 100644 index 0000000000..f09dfa4f71 --- /dev/null +++ b/research/r439-helper-triples/verify.py @@ -0,0 +1,312 @@ +#!/usr/bin/env python3 +"""Independent finite verification of the bounded R439 helper-triple search. + +Ross Richardson, with substantial OpenAI Codex assistance. Apache-2.0. +Reuses the pinned PR926 owning/native checkers with their credit intact. +""" +import argparse +import copy +import gzip +import hashlib +import itertools +import json +from pathlib import Path +import random +import runpy +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PRE = ROOT / "research/r439-two-sided-compensation" +C = runpy.run_path(str(PRE / "common.py")) +V = runpy.run_path(str(PRE / "verify.py")) +need = C["need"] +load = C["load"] + + +def same(a, b, message): + need(C["canonical"](a) == C["canonical"](b), message) + + +def check_pins(): + manifest = load(HERE / "SOURCES.json") + for name, expected in manifest["files"].items(): + need(hashlib.sha256((ROOT / name).read_bytes()).hexdigest() == expected, + "source pin: " + name) + C["pins"](ROOT) + return manifest + + +def invert(matrix): + """Ordinary Boolean Gaussian elimination; no builder or word reversal.""" + rows = [[(matrix[i] >> j) & 1 for j in range(3)] + [int(i == j) for j in range(3)] + for i in range(3)] + for j in range(3): + pivot = next((i for i in range(j, 3) if rows[i][j]), None) + need(pivot is not None, "singular triple matrix") + rows[j], rows[pivot] = rows[pivot], rows[j] + for i in range(3): + if i != j and rows[i][j]: + rows[i] = [a ^ b for a, b in zip(rows[i], rows[j])] + return [[rows[i][3 + j] for j in range(3)] for i in range(3)] + + +def check_group(entries): + # Enumerate every independent ordered triple directly, independently of BFS. + domain = set() + for rows in itertools.product(range(1, 8), repeat=3): + span = {0} + for row in rows: + span |= {x ^ row for x in tuple(span)} + if len(span) == 8: + domain.add(rows) + need(len(domain) == 168, "direct GL(3,2) domain") + words = {} + for entry in entries: + matrix, word = tuple(entry["matrix"]), entry["word"] + need(matrix in domain and matrix not in words, "group domain or duplicate") + current = [[int(i == j) for j in range(3)] for i in range(3)] + for operation in word: + need(len(operation) == 2 and all(type(x) is int and 0 <= x < 3 for x in operation), + "typed triple operation") + d, s = operation + need(d != s, "self operation") + current[d] = [a ^ b for a, b in zip(current[d], current[s])] + same([sum(b << j for j, b in enumerate(row)) for row in current], list(matrix), "word matrix") + words[matrix] = word + need(set(words) == domain and words[(1, 2, 4)] == [], "complete group") + # Realizing paths give upper bounds; all neighbor inequalities give lower bounds. + # Therefore these lengths are exact distances for all six directed generators. + edges = 0 + for matrix, word in words.items(): + for d in range(3): + for s in range(3): + if d == s: + continue + nxt = list(matrix) + nxt[d] ^= nxt[s] + need(abs(len(word) - len(words[tuple(nxt)])) <= 1, "group distance edge") + edges += 1 + return words, edges + + +def literal_bill(word): + bill = V["bill"](word) + f, b = bill["F"], bill["B"] + return {k: bill[k] for k in ("F", "B", "D_adds", "native_ADDs")} | { + "local_expression": 64 * f ** 3 * b ** 2, + "nine_stage_expression": (1 << 18) * f ** 5 * b ** 4} + + +def assemble(parent, rows, target, pairs, replacements): + transformed = [set(row) for row in rows] + operations = [] + for index, pair in enumerate(pairs): + if index in replacements: + c, word = replacements[index] + labels = [*pair, c] + operations.extend((labels[d], labels[s]) for d, s in word) + else: + operations.append(pair) + for d, s in operations: + for row in transformed: + if d in row: + row.symmetric_difference_update({s}) + v = parent["v"] + preparation = [[0, 2 * v + d, [2 * v + s]] for d, s in operations] + middle = [[0, v + i, [2 * v + j for j in sorted(row)]] for i, row in enumerate(transformed)] + result = copy.deepcopy(parent) + result["D"] = preparation + target + middle + target[::-1] + preparation[::-1] + return result, len(preparation) + + +def independent_search(original, parent, previous, candidate, certificate): + words, edges = check_group(certificate["group"]) + rows, _, target = V["frozen_parent"](original, parent) + pairs = V["helper_pairs"](load(PRE / "CERTIFICATE.json"), original["R"]) + columns = [{i for i, row in enumerate(rows) if j in row} for j in range(original["R"])] + singletons = sorted(set(range(original["R"])) - {j for pair in pairs for j in pair}) + inverse = {matrix: invert(matrix) for matrix in words} + rng = random.Random(12) + census_hash, nominees, scores = hashlib.sha256(), [], 0 + for index, (a, b) in enumerate(pairs): + for c in singletons: + local = [columns[a], columns[b], columns[c]] + sums = {} + for bits in itertools.product((0, 1), repeat=3): + support = set() + for bit, column in zip(bits, local): + if bit: + support.symmetric_difference_update(column) + sums[bits] = len(support) + old_cost = 2 + len(columns[a]) + len(columns[a] ^ columns[b]) + len(columns[c]) + for matrix in sorted(words): + word = words[matrix] + new_cost = 2 * len(word) + sum(sums[tuple(inverse[matrix][i][j] for i in range(3))] + for j in range(3)) + gain, tie = old_cost - new_cost, rng.getrandbits(64) + census_hash.update(C["canonical"]([index, c, list(matrix), gain, tie]) + b"\n") + scores += 1 + if gain > 0: + nominees.append((-gain, tie, index, c, matrix, word)) + same(scores, certificate["scores"], "complete search count") + same(scores, 192 * 55 * 168, "declared search domain") + same(census_hash.hexdigest(), certificate["census_sha256"], "independent entire census") + same(len(nominees), certificate["positive_nominees"], "positive census") + same((len(pairs), len(singletons)), (certificate["pair_count"], certificate["singleton_count"]), "domain dimensions") + baseline, _ = assemble(parent, rows, target, pairs, {}) + same(baseline, previous, "PR926 reconstruction") + same(literal_bill(baseline), certificate["baseline"], "baseline literal bill") + replacements, used, accepted, rejected, conflicts = {}, set(), [], [], 0 + instructions = 0 + for neg_gain, tie, index, c, matrix, word in sorted(nominees): + if index in replacements or c in used: + conflicts += 1 + continue + trial_replacements = {**replacements, index: (c, word)} + trial, _ = assemble(parent, rows, target, pairs, trial_replacements) + bill = literal_bill(trial) + instructions += 2 * len(V["stream"](trial)) + entry = {"pair_index": index, "singleton": c, "matrix": list(matrix), "word": word, + "gain": -neg_gain, "bill": bill} + if bill["local_expression"] >= 1 << 104 or bill["nine_stage_expression"] >= 1 << 192: + rejected.append(entry) + else: + replacements, used = trial_replacements, used | {c} + accepted.append(entry) + for name, value in (("accepted", accepted), ("rejected", rejected), ("conflicts", conflicts)): + same(value, certificate[name], "guarded pass: " + name) + rebuilt, h = assemble(parent, rows, target, pairs, replacements) + same(rebuilt, candidate, "independently rebuilt word") + same(literal_bill(candidate), certificate["result"], "candidate literal bill") + same(C["digest"](candidate), certificate["candidate_sha256"], "candidate canonical digest") + same(sum(x["gain"] for x in accepted), certificate["saved_ADDs"], "all restoration costs") + need(certificate["baseline"]["native_ADDs"] - certificate["result"]["native_ADDs"] == certificate["saved_ADDs"], "total saving") + return {"group_matrices": len(words), "distance_edges": edges, "scores": scores, + "guarded_words": len(accepted) + len(rejected), "literal_positive_instructions": instructions, + "accepted": len(accepted), "rejected": len(rejected), "helper_preparations": h}, h + + +def controls(original, candidate, certificate, reference, h): + names = [] + + def bad_boundary(name, changed): + need(V["boundary_columns"](changed) != reference, "control incorrectly accepted: " + name) + names.append(name) + + changed = copy.deepcopy(candidate) + del changed["D"][:h] + observed = V["boundary_columns"](changed) + need(observed[:222] == reference[:222] and observed[222:] != reference[222:], "dirty-helper control separation") + bad_boundary("omit helper preparation; clean-helper inputs alone miss it", changed) + changed = copy.deepcopy(candidate) + del changed["D"][h:h + 306] + observed = V["boundary_columns"](changed) + need(observed[222:] == reference[222:] and observed[111:222] != reference[111:222], "dirty-target control separation") + bad_boundary("omit target preparation; helper-only tests miss it", changed) + changed = copy.deepcopy(candidate) + changed["D"][-h:] = changed["D"][:h] + bad_boundary("restore helper words in forward order", changed) + changed = copy.deepcopy(candidate) + changed["D"][-h - 306:-h] = changed["D"][h:h + 306] + bad_boundary("restore target word in forward order", changed) + changed = copy.deepcopy(candidate) + changed["D"].pop() + bad_boundary("omit helper restoration operation", changed) + changed = copy.deepcopy(candidate) + changed["D"].pop(-h - 1) + bad_boundary("omit target restoration operation", changed) + changed = copy.deepcopy(candidate) + changed["D"][h + 306][2].pop() + bad_boundary("omit transformed middle coefficient", changed) + changed = copy.deepcopy(candidate) + for operation in changed["D"][:h]: + operation[1], operation[2][0] = operation[2][0], operation[1] + bad_boundary("transpose helper entrance directions", changed) + # This accepted control ensures restoration work cannot disappear from the bill. + neutral = copy.deepcopy(candidate) + neutral["D"][:0] = [[0, 222, [223]], [0, 222, [223]]] + need(V["boundary_columns"](neutral) == reference, "neutral-pair endpoint") + need(literal_bill(neutral)["native_ADDs"] == literal_bill(candidate)["native_ADDs"] + 2, "charge cancelling pair") + # Exact boundary equality is deliberately insufficient to certify the envelope. + rejected = certificate["rejected"] + need(rejected and all(x["bill"]["nine_stage_expression"] >= 1 << 192 + or x["bill"]["local_expression"] >= 1 << 104 for x in rejected), "guard negative controls") + names.append("all rejected nominees violate an exact integer cap") + bad_group = copy.deepcopy(certificate["group"]) + bad_group[1]["word"] = [] + try: + check_group(bad_group) + except ValueError: + names.append("corrupt shortest-word certificate") + else: + raise ValueError("group mutation accepted") + return {"rejected": names, "neutral_pair_extra_ADDs": 2} + + +def run(output, skip_native=False): + manifest = check_pins() + certificate = load(HERE / "CERTIFICATE.json") + need(certificate["format"] == "r439-helper-triples/1" and type(certificate["seed"]) is int + and certificate["seed"] == 12, "certificate format and seed") + need(certificate["stopping_rule"] == "one sorted pass through every strict-gain representative; no restart", "stopping rule") + output.mkdir(parents=True, exist_ok=False) + print("rebuild entire bounded search", flush=True) + generated = output / "regenerated" + subprocess.run([sys.executable, "-I", "-B", str(HERE / "search.py"), "--output", str(generated)], check=True) + same(load(generated / "CERTIFICATE.json"), certificate, "full certificate regeneration") + candidate = load(HERE / "candidate.json.gz") + same(load(generated / "candidate.json.gz"), candidate, "full canonical word regeneration") + original = load(ROOT / C["WORD"]) + parent = load(PRE / "vendor/pr915/candidate.json.gz") + previous = load(PRE / "candidate.json.gz") + print("independent GL(3,2), set-valued census and literal guards", flush=True) + search, h = independent_search(original, parent, previous, candidate, certificate) + words = {"baseline": original, "parent": parent, "previous": previous, "candidate": candidate} + reference = V["boundary_columns"](original) + for word in words.values(): + V["outside_d"](original, word) + for reverse in (False, True): + need(V["boundary_columns"](word, reverse) == reference, "661 arbitrary-input D columns") + print("all-column restoration, controls and unchanged owning E8 checks", flush=True) + negative = controls(original, candidate, certificate, reference, h) + source = V["source_checks"](ROOT, words) + result = {"status": "PASS_R439_HELPER_TRIPLES_FINITE", "base_commit": manifest["base_commit"], + "search": search, "bill": certificate["result"], "saved_ADDs": certificate["saved_ADDs"], + "D_boundary_columns": 661, "D_words_times_directions": 8, + "controls": negative, "source_checks": source, + "candidate_sha256": C["digest"](candidate)} + if not skip_native: + print("unchanged native legality and 5/9/11-stage checks", flush=True) + native = runpy.run_path(str(HERE / "native.py"))["run"]( + ROOT, ROOT / C["WORD"], PRE / "vendor/pr915/candidate.json.gz", + HERE / "candidate.json.gz", output / "native") + result["native"] = native + result["source_bound_precision"] = V["nine_stage_bound"](ROOT, native) + else: + result["status"] = "PASS_R439_HELPER_TRIPLES_PYTHON_ONLY" + return result + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, help="new directory retaining all evidence") + parser.add_argument("--python-only", action="store_true", help="explicitly skip C++ checks; partial evidence") + parser.add_argument("--record", action="store_true", help="write a new EXPECTED.json; never overwrite") + args = parser.parse_args() + with tempfile.TemporaryDirectory(prefix="r439-triples-") as temporary: + output = args.output or Path(temporary) / "run" + report = run(output, args.python_only) + if args.record: + need(not args.python_only, "cannot record incomplete evidence") + C["write"](HERE / "EXPECTED.json", report) + elif not args.python_only: + same(report, load(HERE / "EXPECTED.json"), "entire expected receipt") + C["write"](output / "REPORT.json", report) + print(report["status"] + ": 11,980 -> 11,840 ADDs; 40 helper triples; no new kappa") + + +if __name__ == "__main__": + main()