From 82f2b20fff8ecc869dd0994721b77652c6c5063a Mon Sep 17 00:00:00 2001 From: Ross Richardson Date: Wed, 14 Oct 2026 02:02:38 +1100 Subject: [PATCH 1/2] Finite bit construction: couple R439 helper triples for 140 fewer ADDs --- research/r439-helper-triples/CERTIFICATE.json | 8530 +++++++++++++++++ research/r439-helper-triples/CLAIM.json | 37 + research/r439-helper-triples/EXPECTED.json | 1897 ++++ research/r439-helper-triples/NOTICE.md | 45 + research/r439-helper-triples/PROOF.md | 116 + research/r439-helper-triples/README.md | 143 + research/r439-helper-triples/SOURCES.json | 26 + research/r439-helper-triples/VALIDATION.md | 59 + .../r439-helper-triples/candidate.json.gz | Bin 0 -> 39161 bytes research/r439-helper-triples/native.py | 112 + research/r439-helper-triples/search.py | 202 + research/r439-helper-triples/verify.py | 312 + 12 files changed, 11479 insertions(+) create mode 100644 research/r439-helper-triples/CERTIFICATE.json create mode 100644 research/r439-helper-triples/CLAIM.json create mode 100644 research/r439-helper-triples/EXPECTED.json create mode 100644 research/r439-helper-triples/NOTICE.md create mode 100644 research/r439-helper-triples/PROOF.md create mode 100644 research/r439-helper-triples/README.md create mode 100644 research/r439-helper-triples/SOURCES.json create mode 100644 research/r439-helper-triples/VALIDATION.md create mode 100644 research/r439-helper-triples/candidate.json.gz create mode 100644 research/r439-helper-triples/native.py create mode 100644 research/r439-helper-triples/search.py create mode 100644 research/r439-helper-triples/verify.py 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..7142a10ca8 --- /dev/null +++ b/research/r439-helper-triples/CLAIM.json @@ -0,0 +1,37 @@ +{ + "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": "pending", + "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 0000000000000000000000000000000000000000..e74d3a8edecac5ca9262b774a965702c19207bea GIT binary patch literal 39161 zcmXt81z6Kx)K-xON2q|5fI~V)iNpk@O9m1$QUn17M7ky=4MRr9=q~9-nh~OOkC2Yh z1IFOP|Mz`+_B_AmckjD%&VBED&pE$stl=cL{=M#8N3^Il@=Jw@K1=w3{PufP#_J?e z!CUxyvbQABop)&|Fe``Ii2-9Z0XCt^O%n=?R*|dl5y!LHvYx|7Fd!3^( zSggce!wueOhPc%ac?&~$m_O{WA@LQu-?A~5VCScofqB0^LFA{IfeBjA=D*Y8*P39W zVRZNV3v{?3vjfrFn|sse3uMlBd}u42o0&H#k2N|b4m2M(6u?F+nrcZzZzg`67%sfv z{VhRj1e<%fareT?0zAY1n{gv0bhKLGG3oJ8*XGSV$;~zC=1O*R{bOx-8Q5B~$2_{2Z>=X`nGdfIQ{1qS)&*zhLK4V?|C z7tloPN#G-LgJt;-(g@gN_;9mid2D;jozj0Hnbf&uNc;Y_?=BZ#f+28LjIfBa4(-PP&nU718lnU-grG1aRGa| z-e|*D8M%7*5uMMG*v&xt3tqVQ%>bqIofCk}KMj4jOlm~7(EMXJ6E{6e@Q?R`pV+AX zyAj_=SA9eFEd9j_`}w`1LdYWS36!)A_50JI4{drN+Id6q zyhins<|^-%#6Y>R1>2=YxP78&XIH?!gcudotg<%=Y?OfQ$55Bxl0(>IuG%<*n}KSf zD@|z zjS@!l_i8xv1^JVmziZ6fP0s(gxo>?38_xAA#dM-$H%#oLPTd}A&f966p0!q-=QNkn z1yE;i?^B6r)Y3vJlhGgUYlNh6GWf912EO>{b)cUozi}Ktum_%h0_>)>C{%%=!{zvx zc?HBc9G>Y&?Cn*K)Jbh)nLxvVgSH(ted3`X23-$CxhLpQ!YH#ouY*9S)XT2lyKHx( zY%KQTcsT#gZ352gr7Hzfsk||aCbxGQ9OY^Dd?oETW2VV;p0Pce9eUZy9>QMB^guH< zuC#7JBkNI%sWh8R%4*aNAaPP z8+URLP`s2bdfC`=xYeS|g29SK&&&5J6r11v)Mm2%?f0%zWh+R5lgyX*vsej|w(`4X z0=e}O@A&2q);%M<+Hlj7Qk$O16U~xu#XwEp-jQ#86L zg;aVaCOl#BxkU@$^MM1j{+NQf_Jc0d93PW_45atep)F-fY=>OG`54ap6!^-AnohKh zbo8a$$8s5{rMCdolMKMPz465&?6N)2*c$JD)ef9O?bMvG0m3+!BYaYs-M zhPd;7+iLP+miy+t5y3sqH!id$_XX$g=CMY2_KwQ*v~2^*qV}3Es(BYj1)iRq0 z?wjf3yIJgLEID)JfFdij5$MuX+=uO!?>=az6G$uAV@{Y;%3iQ+<9hc#$|^Z*@K)ae*A^aRMNl3}j#0;^91%@^Uu*jD$aqerWQvblG{`YDz`L#?4@<1)9!dxoHWZn6sYt?>}LHJ|B1P%(@bgk2s zW~@yKTQFejOeIe!i&z4GGkGfvcc5c6IorkG>d++29cXmt-+8lucNUxR5HOhx6S`Q+HF9m6XB`b{IqJxr)drhfCVuqt!YvppbZ&M8_bdLk zI4j35!T#YSsXNyqC7`%)sw6v5r2VxTcbA z7H63lU~LM+wzu+s&jVS;`3)r zpO(|@8%+{;Wa~4`Y6vva%_pB z#>CHSSMQvS_&8tOK0#&WJ)@|$pU%CxWVLJIDC zM_(_Fd~$BSnknDp#(SSHj`%p9g&v6O$f=Vy>yoj$iofKQP*JL5`M7yX?oFB5&L|M= z<8F>TsycE>OCO*r7oY65B>rJfBLs!YOm;NbrsVkQQg!1+J%S6{zm-P<1Vfg6>03r4 zAKXq*U7iQaw-nC0-0a5}apPMP0~h|%^#Ue|ajQeo^O{YpF03XOu^QkH=w3>OD?=am z7Agt6&C02ypa~CB3rFQ?m)E~{n$2w@cz@ef>7#|}XPuv1P|rDMTuh_M0$b%Vd4kVh z`)T^T!A(q~yLo`^0!~zHh@{>*Aer;av1<)@yQ8#s{9{yIVXJkU^Ul3{VRbInL*UJ+Y6naZqu2IIeM*bE zzzolT+pK3(y^F)lp^#}6;6CNPV1PsPUUQ2UYLA>X?r=6yg+5#);~yNAkH|`NPvCO7o7gblasM;M9p_SY7`IpL(Cq zjV|sjbPf+jFC4?)ZA>qOOYjYh_Rd;0BRrORjBRi$%%e%J`kFrO#Zc*azM=`xe4iDd znOOXJ%H~0`*ckQ)!2UAI^-e)8ahR4wyssnR*a{%k?NWWSO{VM4K2tmP8$JSaR0lp= zvZ&jh7EO=2=IY7Mi+|Y^&F+a{mna#~ZC^3c!IJL%jqWQ1)Ar@_R*!4n87%b>S1_}V z65?7<+hy2H+#RAB7IEGJ3$&ajz2%!y1iPVWy_~iU-3vA0VG@4LrD$*z z3}KSJ5Kh_VptGMNyj;-@Fna0I;Qo?kzf?g`U&wZcT*6th6|;14e?mXVYw2gjmS@Zl z+Dy}Cx`-*0g&{7H9ZUUY7k!rUNmeTms9kQ!T>Mhf|^&SAzGImM|>S`4XeK; zY*JB!@i+eQD6vP$s|>dA7JX5Ea(;fQg~N~fw!zvQ#@vd&Z#&aqSa;af&Cp8^W+mr& z7Ql%!1Ug>tS_Z=ky{{1%q*Dkq@N;5QD)kwSn?T+=;SHeY<@Fe=&`I!m=HdKRW@?X@ z?-m$(E%q|B7(mb@{`iN(Uqcr9=dSjErL-AFr8PV^Kze6UIU*&PJc$k~X6sRWV*xgI zb#8NgSqlcQq#+M93mq`qCvQgIS=g3Ojp^#P!un~;O=bfK6?gp#TjHJ)(GGPl|18$` z_7%cjk6v9?gTcGQT3!X4?w9$sy|{TNVUe_A4uYmizy3+B^ZNSO=ORKi*uxVYmfcL| z)vM3?Lryy1EF~Rn+I+X($qf3>--%m2Z~l4QY|^TFvlhoqE#ID47+3!Jr^8X!NsPUv z53lRc{kY+`0@~=E&ko&V3j@~t!>9Ad^i^g&!OJCx;kQw0n>&Q%xU0I$(vx$1hHKJ; zFJ4t#r~cPGFxWycZe^Xps>fA_c1h<)_=z7-h%a@H1#4pKfL*Lx{uqrLciuc+c3EGE z*SY>yb$u}Eds)p2-tE=$g1Q#ASlBvX+y>GfFV@!mEK|)tG#o&31p||2I;)j-=f@=M zJZgJedbvsc^otXbnDbp&{OQlJ1%vF}eAyN>PUOm{S3>Qa-&8Tvz}Lih$Ev7nh1m3> z!U$E^x+KfP(zg0%VbIbLJ!G|>FTIVOVXaooWx|=4CtfJ|@DS%=#RQ5H9P&re=-D5$ zO0;OaaDTS!2LfHR2(Ymm8#YA|#_grE1Cv*XJft0Ht9b923%sa(~ui&Go zUGoO4{fuX0&vd0}Uz%iJe1rAFwwo5@gsU}lS>3P9%3!|zTKq^by=U|~@#xVW68jRj zZrvQ7)+w@g<@EzCDA>xg5MF+GZ=&kW?2Qzsk_u$JZx`U*?eGT^PKogzm)iZtKxX=W z#iwjQS7xV0ZQ-Y?eeG7?!yL+LL>!YxJAJg8W zeAzk)*`WKJ;FL=8BxKeINaOuaGj0tsF{%AdO!c3Q;wR^*qNMc;Luc)5(t_qLY& z7&^v+?ahz>;$>zF2-e+^~DF^m&m`Jj#382v^<&Hd6sW2T0W!poiXgbV1VS(-&`9iGh+ zeDRt!)$6vGuTMk{pCUg1I(cg(Qg?@hQg;0s@FgpZc?X%At*f2fd1dQu?pGEGba&8r z3;LRvf2aKD`9=3Ma%l&!mcF@`5uV1El$h=?_!iA&QEX8ZeNZ6F6>W%4zmC^h*?wNb zvwz0j=K8Y$^YH0=zn@0Dvy4q5vjM1+@ItWJ7GR8$1yi~@de&RDIBqK`1K3H{Wlh{7 zIKsVavGg%3au`0swbosMTB}5OX-yM4!yRBztwQb zdF(R$w0Dw>bxI?H&U7>x66xsMaJ6}Jl%CCc;XeQliK2dMcWz8 zM}gMAq^q^&GAFEqyI6Gnah)10!#0AC*u>4}mB$$7^s>sV2n|C6KB_!|VIgRA?||tM z*ifIvX(zS*r=}XYx6Lipz1W;3&R?ekT*@`6GXdjjCw_&pLgNxM&}I9Jb{!#^=%pR> z)+lcAD()s_%FqYs-t!)a8+@i&&qifWXi7HGod7**6f7D=&?4Xd+8xpY53CQnA6YjW z_7ccN2=#&Yp2fOfE$VFRTyI3rFs@+>@r;cdC1SCMX>?dXd$*UEWv! zC#~~BnC}*H-9dd+WxG$)xt^UyaL&Zqxu^q7bACvo&vYs-i_+3pU5$; zU%fcWy?QLzBqOz7a#A=qGm6s`z$%j_pu7%N<%mvkBi#v?Iqt|2-(=Z*{nXt^<fU2oo#n7P!!Ip+3@i2SJ&T*#HCCMszC@l3g$i#AuDocgk)G{5 zfN!O6SWMI%mH^rWc!Eu-69O>HIm17v+s20veHRWd^)xZ$vR$RH!D#HoZK$`$Z*AYn zrWG}?t_0DgZ0M5Ji`}M8UOUNgV#<_??$`!g%8JWm@HlNd1&m7wqK&SSjT&&3L@ZdZmR0-c)-y=K_%7kab6d3MCjbsy zL)^wbtCeTjR<2WvHr)S?Jk%48v|bfunR{M!lT(KKtH9yah#R4|#?>LQbr(gmUv;kQ zGiwD-GYsjPUaFY6J$(J~3XLbWzRApOgWZ8QoyY~u_Pk)Fb1A5QX>d`S0c{xp76dwA>yLAxfL*pxs+bkrqwH++F|sY=jZ!8At8Y^P5p;jDgh5_xZYPk zSztTI=XW+8{$a^gKo!hA;j^SrBml2ozH)%u^pV=H=p(R83mfKf zuY22y!3qyjrfu`CUHsIArM+c6XfKd;oCxk@eCKUy%p;E1T;5^5DblbxmS?k_TJimq zI_E{Zl;}g77?ufMLI)3?(|sSm^?S{(pB(;-rH2*D2-WDH2MaaN6v)omPt3yvOq!ON zSQC5D4+qNL+#KOTnd9r5f;_&S>(p82ZDhCiRbG zz@><68xm!dFMHh`9TaT1&F_vr+O_~B7tya{tH^E$gCb7FvV(sOkc9fl zYX0TA$6`r+0Ta$zmUXKfeX1)^8vjmOFu|%lIDS5#23fb9zr1@GY0;&UdsD1f&I%J} z!4B>FQpQ$bwU6FCU6ScbOv6Hv*yh}uGLJO(ygJgkz8nLCPd=lYS1o>|#~*OefJ>L_ z;vHPtY?gntcOU+|N7*tyDZ?-qn&|%r50H@^EK3J$j2k zM{;33-YvYeW+BYYi?_ACP;h~N-@XRlWc#mqN!_LX?I(Py*0Iqx90nWs;$6Ld@e_={ zp2%PCK63P0M6R!5`G+O=;-`}xx|`x1650s7etznH*y&C;_^;k%z0$^8CmeplrgeoJ z&A}XNiSrI>6=X{A2RJ|2Z&>>JvJG3G>-K}DW+wMbL^)rbd!HZmT;L4juhVaZvU^Vh zd$k$}p(zhAZ-ivpmP}@k&h}v$Hw{nQm553C%92mEw_!-#s^2&P#`pmDu$j)hFTCl7 zi7)sTJA9R$&ngz;Q$JhY)GCm7>cH>TYM7M_eYVX(MDZ>>eu4Mb)obK{-;oa`=DF;6-FnlR!Hf19WEk>otFbSo zG;sgY1`L}SMxGw!<9%&?UI`65z4~Duan%dB;vZg@^C|;ej)J2Bu+oDg@3ymA7@yfn za_RDs&efhjR#h6dHH^Ht=`ph?bnqNCtus=Evi{a3e|T=5(Zv&Ojblw@>tA*|B9B6EOIZ%)2!%VX*9T)uT3*Bjad3t=+=&|IJ*F>^fg~O|O z*8YJbnVOsS$Kk|h-&Y&<)?nr&A`G3sxO-am)7O{#8~FA(OtBPjsRJu7xt9HhB>r_l zGSW+b(LT=WYbSZ)@C>I!B5Dsf|GLGo(7|u|(A3@I$x3)#N!WZkt^0fYdf^$~=K87{ zX6JQR*pdSG=dyiR=fG&dM!HjyMZV|rO|@j*`8>wrePM`<-dgd=o?CJ7xO_4c7kH+` z0#p1n9m2YDAWhWKtJbCV+Q>b>Vr+|??D`89%|dd!tplw4g(nGCu+1x0|M;xF6>KNe zKGA`G)!?@VSRMx3OCQW$efF&`7aT$o`WB;!#V$?NWRosr8Qc1I4IfGQJTZOg6A)Rx zxPFlO5Iu+=J(;GC?pt9lz%+KlKI4B%vk3OKt#2M=NH6%Wy_0Viz+&}gYtHSOWG&~V zP0FrEKGcig&qZtF&zl-rwU4}iwyxnq*N}HiC$MgRQ=i+gnx;$ior@*6pg>0Fc#SVk z^ytwojO)2*`k{KN;PPQz&+ku`4rqH;R~X0YUMI_zcgv4?772TwI>825rV|@=+xiSG zRk>|Wt51{cEdE`b+C6;Pk&D=R?55QGf-|&j?dl1^f$ZBYJJD8!r})4ghYDQaBz8_0 zd*u;z@B@S2s0Vk)U5_IlVLvBaBi9auFIzLHbG!} zM{;bkljFpX=|=i-dtY`g-CA>;$}`Z;*RLWK-e0(wMmsbu+3e!u9PF_iUM%}a^jurq zwN&3i?xoSnQ}=VwHMST7k!AA*)J--^Y$vq=&P*)@by{f@WG7p`669*_8!as6^XL!A zkIfv}mI!tQIJE{})ZQDdGXg!YK|-9JRy_rm-`SWHip6TlnwKXpv6gv-cE2=CcP;n$ z>ew{=!IyhrWesohon>F)ql{e?ceq|Fvle#v2VV6^osH$&_N3_On5f4>uT+nNqb#<| zM+)C5>KX-P+rRJxe+7r{B5CDZkFHARq`It~@Lzibmdxg9*L^OEHB(s`$e=#Nlj>I$ zSMed%e=jmZ|32aP#dy*Z1PeJbau!VI)be~Te~{`ed+q6)DDx-XbQmyov~#JAhIU;$ zdihypcle<2yrRr;L0q*M<8>NuLM$<)jPoySo!4e3!yYSD91Uf9x@=u2h!(;poPg)A zXI7~-l;6vB+~_BT=$LSMilD0L3hLAH_}W8SGV-Y4WqiN=lG$*~0Sa6BXDu?{ddYw@0LK`N(am=~FQ#!A^Mku-teJ+zd?sVtp_~clv`ww@ zU-bQ8m{Zds6GD8`(HAk;gW%5-6nY^_>sYxVb200~7}4+t#1a#)^d6ew;sI5`&snvr z3_q<%c~%a*Kafis&R{5A>%*0;RVU|Q{*>q~(l*H$9ldQ|SiB-jo({`q)9MnO%0&LI zdVl)2>BCN$eZ&10??>pdRl7LjXLo<}v;S^u1effsh5$A%*-vB?q#xBK6bXv;9=tL2 z-4B&s2B;2O^Z879zMPvkMX6^-gMU-!jzgmSq{8qT}hzI`Xq34 zB&rlE7hp3I?KuJ<|8Zq)=>JyAjOhE%A)l=H)jorQy;X@_M&Dm6pJenyRS1_+Jjo1xPV-#qvpRU$ zo*dRAMmq#>Pa5s%ZVSd^u|V*ELT4#T4rDKZx&qIo+6VYjtXl1!9m#-_0xcdgk7?RHj{1Y z=fMJ@wM@M=5zFt^7_WH((?z4;jODJyU60W;_cBJ>kyNjY{@cC76bKvt>Cm6?joR!j z#l$RQ0q@HwE{o*vRoZ!)jfdWUrFGZ8Th0vxuVZmiE}JQ5pRao1`B=~8Lc9bV5lh?} zK!9R%xR4$~eE9Xd9vCdYXnE^_i`A_jjeeL^4pRN;Zct9_z{3-~kEqfeCiC4z-KTt= zkIYxDh=#svdI|}-y!u>XGRz^+_mtTe@exoWAvjD~m{4Yu!yH;;cmAaZc_z~}qUX72 z+4A>xv1l}t-u3xW`8Ce;`o!T0!~J@Lxm2d)a}g(JZ@X6&H48hG+tF)zgC&_T(cr&B zuOzQYO8g`|LO6XQEZNb+<%TRWmTgvuKh=>EorC&Q9Nf!T0vpvH7+9h%!pf|^y z3_acV34hx;I{Cr(N&CdX98~ho1B15daZ$Skjat|0b>+Mgqgu}HBVB^zLY3G>k7Z5` zfov6weOZzggleZfrbz3{jK`YnPymPH5X?dKnPC#!9!|WQ$;iRvmWIl@&7I@PxD(4p z4Q6cQ-}J^uu9lm)Ko-BgDf?f1C@8w|r=?P*tIwO;;I)&F1^%;xtqsk0I~v`^b=t?b z^GFkzlm3e03tnjbao~I*=Q*>+AmU;o1IznGQ>GhpsP^T%2a%AmHoUyf8cD+h+2w4z z4?XSG$mK>D>P*%Il{F{z{0+U_+d}Xw@8ak9!Y|%=jwooDKUw31=~!(R9ZOWy6aqRYxm_Z)Ep)NYtk>r8VY5erJjRjjy>K za}1k8-9!qTf|mO{baf54MYGvfoffqkn$#LJw)CE^P}h?)d7}7d|Eph7d-zW6+p&L) z!dMh@!wt1{t7nbnrb%6{onTsH$$Iv!m#VDt zKGi8ESpS`@FVs*2HEmt#+-2?uy?{PF_BqwFH#x2S0}npw@iJY0F^I91LpRZyiaz3y zD$dFis?<2o(wRwfiLoav7uw23?1o!0n8%wuo^w`|WO+UI>Jf=K;yq8erJ(1IrQqxG zmIzDXe%EJ2RmQx#kLtWG1pCjuCF))}hP4kTy$`FT)8PPpKio5{z2X@#z2N7FI2&X|6cyT^x!mybWY-n*T>Y=Ib_ml#$@U(SUUFxsTyZVyH|%9%tQ8uIhd zWHTL-BqYgvL-XK7A6Qg z(N^}C$H2<1dy40`!kk{IJsk?^fs3Cj+-j(A&Wkv#UTx|5t4(DiX zRn=c!bv8-e!eb@z6`U&y{$}^dvo)b9`Q&^}aM@nT=i52mU@tg@{L}JwISPDPTDbMT z&5Ot}&gLg%##&A=yK~XUPOz!ksAiv=pFoA1c7s$;eyR8N;8XVj+UECt3BAvt&b~x^ zS^;0b*X$FIKn)K{_WAe6J|Ei9xs`<2+F#UA)P#MZdcwtpLA`K)&XYm7KS3z8&8rqv z`t$AzFJoCP$?;f+Aw0!c5MgZY#T!+oD|LAP?}e)pNX?M^72vnW*{=XMmMstZmR0UI z5}e1r4t}vpiY$wKUh+Vgd32FOanO^JFzxI4)A;^f{u;N^=7EU!WkXwb?&NB^2I`km%@`14R z{EhQ6DZe3Qw)bO&^Sc1IL&TCUN0PBWdWL?LB2})O1YUmkK~c58b&zP>*ZddB{U(i` zr=~(u;$-rEx&{ON;p3G@`sT8Hht1Y+?i$<^-L{Jc$woZ;#eBtMwWj%AzJ=j~TW@of94xnW#Ao~dzE+(} z)B4+?D?nNB%C+h>Pm0Hybb{fNhlbb|btu#zH6+_g{Ns^SNRY#tiVh2PM@56n74A<& zH+MpJ;LG-^OK#p+{|hcTa#^!Ik)xrYT+y8b8qPJ)6}11MIHPq=>o78%lr(PN_Mi_r za9ydhIzr$0>7D(m{=>nj4H`4@6J?@|zb#2W_Q0=*YQr}R&t&Y69Tt3lYfqP>uv2diUKR-{B$NN3O)igOH7X~uQFsb3ol0grh{O3z+DHQv} zsT)!mrYAy2wtb2SMOcu-{9Bp{AC;dEV?~~wko;IQ4TsEu-lcxG6xt!_cz#KpN|bYX z%Dm};XeTfVh^0sH&$3Uaeh-)PbKJu>UGGo;3v@^0Vs_$~DnYNyzw1&=3k%;>3Wjp6kOwF&2%ZFf+`Gl_V&#=$1N2_lB zS51?-PmvL)nI9$RUiUEf$5D#(<+;jVBuuGCZa1*RHHD3dY1UlIzB;;Vn{X}_$t@Yc zkQiDJS8(t7FhfG!6gLIIhb!t_vXWJ1xmkoWiOO_ZM_e`DD#|oh?knlv;xjv&t`HxF z{oh>fM0W4JJLHBvptIei`9Yg?2}=(+`3jdba&|u71vr6@uxjtQQc3j@`+s%UI0S5Q zd)u6;J1nnOo_2iY))0@K;>9Si=X`@a<|pt+mJMt$+unV1_ydWa{lGF4OXFJp*ehZ; zv$Lg$_Vc-6-EI8RlJ_z~@`RV@!K(&C)wd_Jf3VCUxfR_%Tu7hW&P|lpwzuau^?@5d zzv3$iiQRsv{4|7}LVUx~XyUb8`*+y(k2PJX$oyOEC@RM)pQy3jml1yXvSR%`RWR1< zc&>LEg*jz_-)Z;!&~1^YxU_FZ`~u^z&XqhbC1tdH`ny}7*Ysa~j!$n~3-I!%geo2K zQp*xnfM1j&%gP|h#AT@fgQ`}Oak*PL_hrOP_fL1w1AW|{x;&wibQL{XRHOP#ju&$u za>jzq3zbjKoGp-w38FLuf%y@FUX)IEKm#(GKBRVzd=+nxsq_L`OkD7gIJyJb(eI`nPY&4wVmo)9t4$c}pBG4t_(IC{N791hi`? z$z0;;+UR@z=i+mjNwL}GMq%DZRa0u7b$0WZL+yBbwo``(DqXdoR`1}-v!7CTtTHx@ z1l^9T;8A>azkc>SujG}0BOqTv40}Eids{XtSz47gWX9GjMLYCGi0`=8udC80S?`Fq z^e|wrb1WqCo_nUiy+VgJ18RZeeSa9D@A;f^U9HCIRbFIYAJ5iQTQ{jj<4CoV z5!It`l0nWPj?xDAo#IIV5yjJroEXsjl}zO3UDv(y74}%7id!ox;18>r$=43Ew-pdve{@6FOpi7gB*YO8%UUSj+B>L+Nf^-i|_q zh49dxldDLSA;MmJHab^*FB1H2(E8`LtUGpVv`^~XWI+_2wl1|;64r`>Xh(Pr0@LCqx*zU1W)3%qv?%5{`ZJSeBbmT zNsy%i8#hF`_5MSd+`iln`C_;~D&OjubYJ3a-9Irk z5PO^>My1E4{70Omm_2a(eg_YQ`N_A6t(OM;>?I&-y?m15w}InA5NFX2GA8rYsETDJ z1MVj!LNt1uq`b+2aj!ebc+6MhDlF6tHh~HpoFxLZdby;<(>WW9fe)NJ`lZaf)9;s> zYLk)`lLx&Cg&aq8s489E zE6JzPK^jLLR$eLrt$}H#BbS0*eE%$jJy42Lp$hs zcL~p$kuYtzZ#FJxmf-Z4WG%zO0d@MJ2fo zw!d>VVcQeVkDm4&B;dO*X9WP2!x@6*p|9BDv#4O&A=6x49``L?k{vt=qDRQjsj^Mv zQnBiU6moYh-OqC)(*XzBWOg95*~AN}hIK>yc)BzmSd@|-7zQPl$uk+Sxt35l=!IzW zcGWzvSRy<45|r2^pK8KZTTTTq2w~&vVt#1xfczjbD6vnT={?(NB~`g$$N^th(8D|x za-D*p&2jlbJ2uT)DkGziUVin1hZZpMgN`8j6?v!=TYLl6H8e3t`558b#h^B&@;UJN0_iL4X1;{VQ~059Ih1uuZw}R zeuoEthhx6O^<&{}vGAt|cr*fzMZitt;JtBh!FYH=Jp4KyZk+%hPJl}!!jXw^;v~33 z5_~cV4o-&WC&K|LaJLjVIt8wj3NKHE)1|>-Y4G(lxK=v6E*;K_ga;#YwvlkHjEbfV z_|r^ybY{*`CR{%Y-j{8kvIB% z!TKW&`hDB_eXIt3ItG2g1|tmyBbx?&jD~$$h8-}&j$*^US;IcS+rF1?``q4+6u#}7 zeLF&F)CV>i`E1meZPYhu!JaZ{F9*;-i*l6%_&XXQ^g>J-j-Zl<+@Vk*1wR2ki$VNWfZSmmuTX;cv#XFM zJppEXM>wiM{DoCW$DaVh`KJ6S5E z37o*hWW;N`LvXiM?6pRO1h?PP-?qrdPp`vCoDacWKVq+6-j_Z{c5a}qg=vtNm^&9L zp#)q&)eHo^KZKoP;w%7?MXMTW%mu8>MAQdEve;EalemCcSqS%VNS5$~K_rA-QZ@95 z3rLoOppSvDE31YIasw}N5K{;UyZ%IdJS59RH8hkPXpx6-PljZDQVs3q214=?&(a}T z-V^j05cWXTP*xsbV*z3+8^Ru|8fwG?EGk4K=0n)CCfo}lS%s>hH9SC?V#KpjNLIaS z=m8J#P6^_y0+Q7`F;xj+A65-j;|1E5A`)vM>b5Dvt~%vv1;fN zFR-H=an=UOB2Wuu<^xt%AnH3ISu~T0-4OOiYN2j?z(yZjvolE6U$xLoL10HK;tU7L zI+~oqL)dX@p*TSx?^i_XZ3u`=871);$moZF5<)->W75Qs%E!v6n8&~Xf5asjq*72B zHS`$xB>>TU4^k;RmP!QyDJr9G{vbLVh=AUQfZiyh-mw7(f)Gsf5Rm2AB?F|=P8rq0 z1{4WKG&4ggJ(W@CY(S0>gf|~>U=oLb=9Ez|4xm&NVonkQ+Ezw2 zaR7Ov5vei|(1kJz%K>DBBcO5+5UC1E6%+>$IDkMf=|VudDkxJRuqh5Prw;+WQ$eKwfyMEN zR3iw;Nd+|t1g0b)pr#Ozp9+eW6BwR|V0s4u!BtRNoItN6#GDlbgj7L=a{}#>5vjHi zP?-vLoC~5s7}A? zU>xcr7Hc|mq+fMwg2_)Tz-&m+pb9WC7YG5-siN$-fZLgf)DQ@WQx%oZ1)R-7KqDX^ zF;&zG7jPgO!32kZUa6v3xq(eNh`Cq@NJkZA#0@OYMWiM`Ko+W~1a4qT9s-&I0ex0Q zjdBCS^ASu)2l|ewws;Fxopi~KB?gs=kpo)^>1@e|6QfnZf8C8@UFOabe0d0VQHdRqoyg>4D z1XBwHbf${J@B(q=h`FB-5V0DHmk+pIfk^FwfF7!$toeYmKM>G92neW#%H{(OR3exL zAs|sT6q*m%RE3xuhJaqGp&0pr#np(^Q3wd4hSKK;rqm#ylMs-(8Y-3_7+#BDnuUNI z)lkFyK(9K)+yVpyQ$vvp0PX4#sml;hlp0D&0BF>JfUZG6X=_*<5Occ_P?H)8CjjJaMx-7cbc2|*xZ3j%rq0Zpr+zF@e#3}KN}_FVKb+S{;9 zdO(4MXLdp1udz0+i4!vz^Gkm9l2}oi-%3O?^_%%+YV{OtFX`l$u3}n#KIOT0~~o z;=b5+m02Lj^YMnX?`s%+&7m)bo!PLKAk6heWR1=AJzuFM*1LGK4>Mo0C0ys}vXk*rmC?l?rrYc=&{FwgMyKL6JdtE0;(x_J7HKAtdYiZuUa$ zWGR*Lf%pkjgsJ)Aub!z)zh%2X`_kS|SvndowTX)55w{ft_opaYxPOmJ3raO`WR1259x=jw>Zs9VBpq0Jv(YIyx8sV<6_mgA9lL2jSaNtTLD+%WCzR`pKlhZU z1Y&nHuq+?b$a_Z#x7`u9gXU)H(=rh@jOXbNO~!(Xf9$K#vYi)g6KF2{G~lEmBJ?-C zf`$QcR-VdOr1n@K!o-$H%_fOo@>l8+o$Bo66UORHE|K|D^ZV-r(j0nnn;ln<46nJv zWyQky#_xtDyNcgaH23S2d{|pG-pBd=w1+Fe)P1U0sPUt`;Wrcizofos+rUa=hG9>` z$ll@tX%~g|Q6n>lz`)}W(bilGw>Q)L+sW^1eLFG^e0@kq&G@)h~kkY>M(*MwS;1qD40E1x0eKKsnE=7$l5L{IckHc~^o) z@vry-{4MTg(6=uLrjM4)MN~4=bAcN8s_&7UQ^mjc?r!ILjW~6zQBb@~oDm0&3buPR z>BnGiScP&xQg?Rt449Fp4fL447rwK=*88%nkwo;?v2>vAkb5@a#K+1HEEXcS6&MUY zq8AFc?h&0>^u=PKGtz9jm_p1In zlP`TIsjFjS9oR$uS_o0fcdAwKKXiQsOkGj4Zd=@oTan^Uk%J#xio08JcPn1Jc#(s< zI~*u(#ogiHoKoCf5AyhP-%Z}j%}sVDYwu*std%u0*)!iaqruT|8oo9m(#XFT~PVp?gnan+&dL&6Z`!1L|?00=i9-NR^4e|4tu~x$Ib8YILyi8WVrO}gY5mUCyqE51VX<1PlcsQSq7>cm6k z99Eu$kTu6{f5gJIL1u=>emAY;_r-rOqdhC<4FVU&>3zM0^8Apt0YGIj4))k!Gh)=- zPobw72(jnLws-@m41ADqy2UF0TOq+o_9)??0_D1sdb$=bRonpWV#}@>2I?5jUIuES zsCp?D$-HYgxFfzU4R}#SYV)b|LatJAynD^~YRG0%kmxqHf@=f+5!t5N@?neKuK zt1%M`$>7a&55n**N2Kj}x8zFcbxP|U+Xw0J0G%vFFhxL6K}o8jsV?FaMOkV+GPl)~ zuBufI(+#IQd(ukmBW4{hk95z)aoti0)=)wH=kX7SR7Na|$M-M2XCx*so??q7$jMuu z8SK4NzIDM_Baw`N1In`Vt&tp^UYf*(-vD&7PFP9$ zgoWo_)&s8}-`v%PfUuESj*A#^JSGDlG2JR2kJB1sP=M{A(^!|dD1UGrFPh3@Lh#-U zX8vC}WwUV#ab3jj)O*(-y|qZk%D6RYsM7h2xO?$N%N3MXoI!@P6RcTpMVrWwTh)+!S( zby&y!wZuo`0TU6^Q~SMJ#Z#7B^~*0z^0`DEs$vh)=RVQcbiQFEb1$rbLNZ5mrw$2v z;~1Na{PWW+yox!MdH6da+uKyTH#hRac|}HTFqxB&TnmraMjuT($sqIR_%>DbUVU}k zZ6cwwV>>8snQFGQS0ytaR8*`u@bN~^6`qttT5T@`*v-{fIh%)`3F@fpo1TGGb_$_GOZgxjoEak ztCB@PQ0d57VPW!q=pi-dSCXwj1%TqRFUB*R3NaMqGVzn(ef;@PgZH@`=kZ*47JRR2 zSB)>Wgr)uzc*ovyj7e8sy2HOiY)MeretvIBg9w zn3;*1qEr)Ec5&!c&&LS6xQ!7NV)+^gTXdAh-Kjhg=l!H`ve@*pylaVgBIR<79Y{+z zxP{b5Jn30&$YKt>AdYfgMF0^{^6jnK(#2-b>$8(R)mCI}kXF+>Vx+}-`uhZn&X{CG zdAU)etTveLIV19J*Ru*cb zp-)THE1Jz!sM)H?WJ>iW`_42Vd!%Il6wmhGtHtYVC*u{(#M!|G%F&GrBWD7u@88DR zAdkzl_!bx(3Sut=RdCug8K4NqiEJ^k$LinpDQuhdWMlT!KTzi9z5p)4K~#>O=Y4E1 z6^6X}Z>~%YF>Jpp#;(H_uj^oO-!6Wwto%uA%X&I0QAuKzlCOVR*u$wx@TS#Ou0LqV z=wQVgsm7cq*Ow;uOyd8?)f5_H1aS7RM0papgZy6`-l8g4WXFw~!MnVlV8moVkL1@( zFB>npcJ-AW(_~0x58woif!f@h?*T14RaNqQKTBsoMW-|GAZ}Q8sw5-aQ!KjhNHPFJ zCZqt*abhxWrz>`W z>8b8VWYMm=f?;bllXmG&l73l$hz6Ix=X@L*6ARBDAt6^(fTn#!*;OOXRyWO+y~e4A zj6KStW)@{4gMRmg<)4dPWl&R9cV*El3F{hC%&z~11^dH`dBp@f)kx2GzQ&9E9`o0`qgF({k zu4UzutNJSUH=&4Br>!bAOS|vShq?GKc0zZU-;1d^M~&?<)wyuF6gS@zNMv_4_p6ViosF-RZ>S6rKx4))djUs9@ZV3+8d8pgLScx2wY6zMgujXeh8zR2gPXZ69*(PFimA8-rdt&4P z?B8S`qo{5MD-JEPaK##jKu#Q=izBWk^$kAkCPni8wUgb0jnj}5WPFkO!cZLci8h!A zj_`mo8Xav}EFidCP$mn`GeTZXfI^O})!LZ6p z6DD4Uznj`We@?b!Afai#I_(Hl$X?UZY3yqvyB!gjR>5^j z0Ys`a;~Z3zkDsrw@`@LNZGWm_SS@A#?PC(P4e}?_B*?qZ#>3Q6ze!t0T+wSg3ODaC zPBBjvdVa#yvYAG)ScV1Zr}WGj@hp9IpP<8HxD@v0R2{6h&&=%gFZze9?`1zi@EDi9 zF((uc@0;Y;o@Doa!mB@^-xc+QqzNP?rmaSMujU!2X?oCV)Gev_DZ7I~ToEm3+eH1S z51gA=*~qAhVxZ)UcoFK7ArZNaK*n!l6y+z@Y_%4QC50xNx$;*M_e)x6baL2bo;7Fx z6MVy|3Ou>#uqtZ2#o%m&f-rXehb{%;a!`^ZrMZKd#C6}s!^kGWoeG1sn82~9YF3aTdpIT%T!9{L8Rd#fD26mPj9bg~XVF8$hSsXoPbRvaEW3{&dj+6wbd48wqQ7^ib) z{6;OiK)ql^#zyv-Nw35^Cis5atpJbKCQ?uAVM#H_i{t zM==UIi9z7Vhat`ho|;VMnTXF|T$>2kw^i}OV;6)hd#*yAx;k$3`m7Q|+>I!6U93#L zsagrZ!;Rk#eGlzHQKSy&#uqdG>qL^DNfOdj$3TIbQl=?Eo&y`68 zfiCHIK+jmlaUU=tt6NyOA7N!?GJtF@`Y(=9}jvdrXB{pIR zA)dYnO`;X02jbWF(C{To#LcaXz24S$D+i0oEArOEC(01Sb*3t=vvV2YswnYp17$@? z{*2gsPe`HepeW+{I2y`A%gR~Y)o&rxGqUcr=N=A;0*yG zAz`k#W5cW;`;}_MLrNLnG^M|9OTg7k9`_DzeXHo}~ z<-ZfDr-{EZ&5R#K8BT>bAUsF^0+zX9W>21K_X-c7FvttW7@^RFO-(*TCt$LCSNzz^ zQ+$te`}rf!SE+Ff;4~K7-vtkX8@;%ANFioo7DErkOwT<-)Tn(rJKXT_~?%Bzj^!q`i4-%!8SYqFQG} zzg4u^)X8DMZ#ilQjL$4{1v}V?IfmKRTs0b2;LEIP1=loYcI;dj4Nug8+AW#2ceL0R zs&&rvW<2V!X#Ix_+i`+0^i>^r+o9Jm>7|YJ!!^fm@PQ&|$U;uUjBS}G9?vgK z0SfDlFdErbe&DJ1>0-kCuiX)1D2y}#zs7sz2TWejd$&uFQ9m<1a>#UBtWN*)VUy{Y z9j&zmvrweg@Jsct0euwD*{I^i^sjr6^xXr-)3{*uJZLM=-HjkS-*%SNjD2d(T`Y^F zRn=Ei@|76G`ZK|`9HyH-6}x%nt6a4XzVj4_wt zwVtf#oSgHjmcm*!{0}=%!{cT;Qs#`gA1j9JX7EyFt!fQW==%}p({VSQO|9NPy!5ii zf***9^kt7{<@6GFWzAsEYRYXQyn-Ej>(udTtV)r8(|@XI5rGLJCnq4=!| z_1^<4`6Tk>Wmf1*0q~FP}6FdoNiJ=|ox>0#Yce2GERr4)2CQ2823&bqd zik%2ute33(_Wr06*?AMn*@izRarKwU3*Q+hMN7eTLY?MJ%DV9v{p{Mt+92oFyppL3 zb9rFK)tA$@+w<2uUh#J?$wHjpzA=l@WVYw_ccE#Q2(s7d-U$Y`26ThPIX$G@(9ZW` zTqk{qK$!nIzT+7Vth}@tGcLWWi;b#K?y_~rvaZixw_fiAO&B)Ok%#q z^fPthLv~3b1{C-?dpctpE^qOC2?DtA^ima%4#dUp3Y>HUAUc z$m*vCOIVH8Xk`Uw5F=>?@XO-a&|bS;ndeXW6MQuPw=JFq6UFQ3@}8Zd*E))+%dIZb zvv&LxOc59g;JWhUU(`p0d;J?d;*Lx$OBPk(~u-7NEXwbz}YId}i~xEoHlgc1Hhw zXZ0z97yi!xELU0s-+JFDxxg|*q{^E~NkV6L3Z|paAqS7iEjNF+M>BjvI-zO%J_oFW zA#MMJ=^aV#^j+Ko@eOrdX+^y$a>Skjw0CiJJWsn;5h}tocdIVgZ~F~+12~uLYKm+d zd>3m(u{g}6Ff#~e8jNe^Ev8(Hp>gc=8@HRS1pBt9FjSmdz_EG6FZIqn+azI7U~ArP`4@@T>*2hcGBOO(QaVf&BHK7 zADS4V*L~45dK`W2N}sEsTn3?czc9JCbP1-2yUvBM???LaN-B>R!42#r>t3--sXX!T zs%`w99cCJqk_Ots<5+HU_MFpC7PA8*zE94K`tWmyTq+smIx)l2r!$(JxU{AO?_)v; zcyEs;&M2p8awRG$hx+)*e5lqG&T`gPcW+t`k0)oXwm=9d|N3>G&Qr~B`b#uF+I=V- zQ>TgFcnFPEzh=D();zzAOr7EnO*q&Lvl8ANhm36+QU}-!^ME~-b#s3O-{u>(G+)G9 zF?G%3cSGfUvnOVSEozK~TmO~2@CaX=CQa$riRVnJX$t|AmWX<~Ch7|%6~`Ti8SYDp zYjPqi$_;X3VaFC7s*@c0)xCny_SV#7>Caek^?^z$k>ZJcuz^vZ(b~v$Zf(N{zy| znsIFCiKN>lFPXBX-M@S%f#OEPBHv@lhpf)3;0Pt()gD*Y&1WWCi(2Lr$TvI^!{d?9 zgzt9HP45Es2SwG6cda-WO)lebl!2oeNX87K=g*y$YqIyulb*Y&S^;38i*vzGr&oB( zmP(1nmySW~YypKMM{`~Ss*~r2D*RAoc8i_$tr6)59t@9^r=vEbow$$2NYgBP#>cu& zy1IGryPe>*pUza*T1xcN-qG+|JW6?`HIP9k_oynq(b|GUq|Uy-{BWo?q{iQ40wBgv zce2f_z_w^eqaCy)d5)2WdHA!cWz!}f>#cFSSIy;wafED~i__Xu^|zC*og5PXI9I(i zmX7fs23$C1Z()SP(lBy>?dY{op^{^U5Nc^W;4|M=Kj{a-B-hL1hQ7CJN)3 z#)1a37V@Z^0nHf=ko5lF_MF7N;p=17uxt{8e+W zQdR?GV{0#7dDgs~t^Fw=gyY+}Hs=o#oRj9XTYbN&0z?KF@YIRJBvcD7BctV3M|;J9jc5;qSplz;**C(Bv`gV3qLNGGk*`5az!l_j{*?(s) zfM$ED783rrUG`6B!q=9hzk(DC??=-mCNioV!|;MtIGTPKnu1a$_J!{9m%$Y|!MwSO z9$7`%$IOa!oo;48*f)U36?2d6qZXCc)MBkb`lFLFEcba=yc^~}hq={0>pHIx27O%h z1RWJ=FaZ#lq!eVWwCYFNm*JNxsEYa1>O%@7TOO8-||yVgmBY zdW;q2bkM+*4G7r9NmorKzcJaWmqZim36*(cIhlN0CSm-^O z+kEFf<`%YBVn7RHWJ4c%0~)Vje_q`8szYu~-1cB|yj9gX2(I}!%E`snSIvGNM3tO- z&b>4d&*dJ_%#?}Gx22fHovv9RrToFsrQAB)Px^pWYj*x-GP>inVv6tfOQRWI`j>?* zLXmEk)f!?la!e=Vy>%*VH+BQ=pLknDS0}G}J8ZgxP7O0pPh3#_I^UL`5uSf+%u=hn zUHQAp;m>UNH!|jI2a9t?sUfA%cIpw4aUZzn8PAH{(*6%7AE1m{m++BV-SSzO(ADJh z?)LOGW0N^Xj+51aTIYRjYi~6_vn89EzqomWOaRr*qCbpa(aIk7Aa&ElBvY@Cl=Ha| zEf^YHK+Z?3@zAszr-5DDW^>J#iKFHk!OR-y($v|wVlH^7%PT8?9df`KT#J)=+FUJZ zvw9SNcJ~kZxPGU6`aBoI@Sv#7$5;M-s>|%EPJ=5u!`_sg0_#8$#1;hA);_)4+0Q!s zv_INl_(Hioh&fW9X@=TmoFqp#&f8Rqo~Y0UuDAEfl3wSMEeaX6wsQ{oQ*N#*Gz8+V z>+Yt^@1ImU`XSbVuY{C_hh;;cRv&YB;JDn8~S%7 zE&!eWhP)!(;kn~;kZYcTc7Y>Cm?14g@qH!l4;+_F2#svya+$9EG_1-2ZcF)v7Z43@t`bH?!T#sp`^)&R*Z*jg3&MED6BzV2@h1|`<1Gr zf#-SLnyvj_kwERAnP5&pdmE2)w7*|$Oft?{$3SPn%psJf9ld*}>pC0DSUX?~D1LM_ zaNsce@Dj0l>iJL%BQqcDoTV9Eq#bdjZ`-iY$no9}4KrwXPWJa_=MNZsNCgbgj-E8P z#hs%s>7Qau(fazi_!Pn(>yj)VZK&1EF3%SGw6R_`Hee5xHc27T2eovmk=6RQ;(hOV2WAJ(UlO zKrq_sqF*s(cKSey$}l(UV#S7?Zc`+n&9KQ^Hgons!P^yMaQ*f|_q(BIiQvh3bBqV4 ze>OTSTr+%u*X#kwRk`#EJ`rJA%YMj(5#y4jbAiNL|BvDEHVR`G+7KzwJ%Wq|%K$ht zDY&%dRdWwKb6S25-?+Sc)97j^pUkem#-aOQ0m)GJ@2NrU$^7ec+|45s#Xs0-jK1GK z-MQr*uRuUkRfh)@CcD<6{UUvKO@9qVg8}8rTvoW+^f`Tde7w4g}ZWR?>cbQEVyWMbI|s-rU%O*xS2||L*n8lK<-qa zMsq%w(dqov9VV9{rguMW`Hl~>Y&L$Em5BT)a96I^$L+g}T+hE|-nOYF*3AtI78aCk z$zwILWLfJyN@}(_`6%r7fNw>Jne#fyf>i^^CFKIi)GoX;$bf0VeOYX;_{nkHHRsGg zTdk=0%XLTB@@X7S;h?lTDh7aC6`^qr0*9#GWh6&oi~1w$b$0Ra|cSYVq7j za}=hP%c>$xV}3)@yntU=E5V-oY~o`x)1_N#N4L}!)FjiuJ?5u1a|QKi#(I?)K=( zO)=>0R>S&J=4k*Ow7o_i$a2wt2YlAve~5L;KU=XBE>6$3b8B@}u+npqIqRhGnv<>A zE`U1DY=+dlt!n_g@k zYB0_AR?JZb8u>i25;{&c^iR3v2Ssenwk8On7!rXqSLn#ZryEz#m8`}U(3>r0|NW}K zfNLFAWvQ=yNsy?c-|lqzb3RWje7D7>oeFx?@qy*az*i2zvF=H&N&n*hAtnB&ntb|0 z;oFZp=br-T|F72mUYZv=k zdLz+5_GTrEFG%WeAn?Z_3Uqw?I; zclhB<_N<~_X^jfcDK2! zq1J{t1g>`7b-p6o;3E|crupx$8|XJ~pVIWBXgn-#ugQ98&S7S(G0{Zwnl5cur&cvG z*?=1dm4*Bwdbq-@&MY{yq;D$}^$;Onev#So%5gjaY1@m?VMc=aP6al8lS75nVG9GNfztzezer$h%3n!t5ze}m37h|Yd!6&} zEYbh^eZA#Yw|jm;tsxRnUyGQOZauvKwAsO|Zm>f=59jLoy4rmD`~Y^lvi<(=j#5{) zo5b=+xh&n3&Uw+E5pbMX9T$p<>Sk zdr`48K{s^kwgYsjymYLbqiX^?Z^o!TcAw~x{-f|lD9^SLZ}Tw@DsajV$|2rb5%fcf zb+Rp$-rK;bBk^5$H*R;;k`hF&mvx_$Vdth3?FQgo1@PXl#Ml0@!1+1KyBLgH=~4t( z3l!{FUZ~#7oCutz+u8=!Tv@aE3I+U2Bp~*pfdqb94E$XI!1P45i63KqrNy{7ay>tH zYTV(^_d35Tx9T^hKl^&btMr$G`~xJy?PDI`vn@%?w@P78zcR%eU&#}W9_FCAM#+gK<|xR&X&+m^zJ}-l|oxuYY*hBqy(Gm7VEt-=Q6V(6U#e78q zCtnsDog*gwC4D}z@++ie@&a`DIOsXjU67(P4{Nj#oA1i)v+lm6GB{)T9vBc`FX%3{ zCR?NiDn>Y>^f@6_28ekLftZJQa`|)1(}?Ar0*@ozBSPs8KNjNBqd=Q(qzO_IQ?=IU z&?2uWqx=tx7a()HPhUZcXTIerv@D-f_blr(MmQT*3S2xVJFqJz-|tzEHMlDaip=Tb zJ?{ESdzyZ#e!4kd_xQ(;DZ(Y=O7?2{0(?F1^HP`2r4ydE>$U?<~kJIlNYUsYj#CtP60=B z;B>s2gq8(#Z8N5BA7>hBa&HFpdY;|do?lP=*C%QCC_f24; z-&VdI4$4z36?PCiBG@UWT2a3Qum9!-2;eY#%m8@D>1P#I6>UJefip&Psamvb&EichW4T`-e9|{;`pt3S8 zGUZ5zbhjG#2E11#!vQOco1P!)8yDMy6bMo;2TCO2TQPEZ1x}9(A~QxMnOt; z7ZjCHT^$hhz?}q&re_(pI;_q41nA?yjIZsnO1XJNCDxq84%{h$9LwS?`Sl|?W?56< zw3u4*_VKr}de2^I)Wk?dW>kLED2T0qtqe6udZBEzSUX1;VMsRw`A;xxV^B9uFgmLl zEL~DRz$h6aTc*pS`y_$rG|{b7aL!6sKgO=9+vtNv9XNja!4{eUoJ{c8NFVOZN}W#k;=itBGeNaOYqC8HG=2cT*TM!T8h zrEs;mR0E>RM7L=>F;08MrV53TUC~~q%`U}#`*5wU4bqZKyqQAnOvMFPnX>4e2W~b$ z(SF-Uq$J?`W_762k{T=GJv(su8oHTr)6r@jB+y~6EqH%c8~R$mYp=o&v#h7M^%>-4 zcO-ar!2Xojqhia_`Pow*bTcY}q3(^0#fl?Ac=UUdnYeR{hHmk4+t7_q(7fjfC!QQH z{*p*gMW0s5c`8a{sl5wY=5*7n_O+ zcjb1#=f*si_-_rbGjAhxcI(6E+ozU{gA!N8f|!V6p+z!z5-S-B!4VA5ThhqRc3)>? z__s*RX)DXEV13W#zVHVjIe2#8b?upN;S2Qm7>70|m6f_A9kq#l*PjeaY$4%Ntyi{k z+-3Q>1^nJoJsULz)iNPcy0j$bAJ14K3AP%cf}`c$rw}$!hE=J%Iqq3{-;(&qHa9MQ z1wGrc048~o9oK5w#`3gxwfkg`_2JC7A3XVYj-CsUw=`W&VyuI0XUzbm)_g;aU}YLh zD}x|2pTVh?GW<~xD?z?z+Wp>4gIZ?Tm$7&HhKOmBAbtTtUx@a{vyOj{vNf8apvWN0 z8A@&}DFAY2;QFQ9L&xv3S;~3V@J#%M1SZ;MzTHm%QceJAWZ|4lKokgw-tKnsJgA|F@vA^msa13t$KzIbiFg^yoYEzbxFIgZn?k*x{`9LwJR z!ysr;r(=y95Hq;NBz#JNw4WzjDid^J2QWrG&+~cjN?T}h5{@IoJ2_xix|Qo8UZ7jS z4aPB2+e?@7++7PQV5-EfX|ud+Tw%2IO2?m6^Nus=avToug`0DRgkIV6sEo-kWlgzO zenPr-HyGqpD@<#ba49=6aq-FACoL#X2mm7{VVKt|kSMW#E0L`pm_DESXEt5tfGZ#KKuixdAqbj;jG8lhn@6UGA=6U)f)j@w%rr zSOIi~%}uLSul>OTtf#8j95HSN=)qd7dLue!c-7{moIJx2yPi3z8O|X|)SssiQ$adk zk3ZhXw3$kl^^J(fuHwo5V>klij0xNBzgm2vC(5uWGd{uoo_`|1FKqoYTHUVVdDIH2 zdLK;-N^vya9*`6kv@EoJtJ&_CB6T#Hw69RV-cRqLI_aUb;x4u1u=0}m0LcoAc`;2X z<(XUYrql0=xxuvxk-hxhvLMOFOPHxELj#xF9F-^w#DQG;3qraEQmfCtFZc<@+DKlg zR|WryH1&ed|DIBTRJ>BJ6`^M*W1HD&4!qW15KfxnZ0j6;kuxVw%%5W8#UayQ8s7h- zS6=>ZnJdOM8V3GkX7II9LeMkh_>cLafvcrmWy5E%aX#;>aJ_DDwYCW-lN~_eAGk3s zN*CxGaO8oKVJz^qt65t2gB}J3Y28l>fona6zsl%{2Wmie4DT+41nl=*?>rmVwYF5J z5KT(oxSMKMXX=*~o7}2dMoV)ShSWrkGBGqgz~Sw|g%L)!U8Ns5Fvy)@~sblr;2YJsIe`PpXc|$c}T;4PZyl z2mp&EMJ6hW-NA--tYA5BNj|`>LE#alhMy}s+D1>lm}vYD+e@{*X(l34B|wy~N%P|j z!NOD{>9)p~6nVUPOAdnQ(?J@T&5;Xs4W=$*cAHTv+J_eSq*!~0&b7|gnQw!7)u}!; z*X!oCUBCHEzxWiy(#pMrU*c!CbcFO%Pu1kA9Ubu~|;Evv4lC;Z~e1q+h^a zLdzd^A2D+@`dO{Vay;Nhz~)O8td+dacc`Zha(`b{!|Xy1=|h0)bHT0YpMO$s+GRT# z{#XKNtlJ=f{Oc7k)agSz^fftQuR;rd!;S$tssQ00!*$Zc^XzVo6M3iUm672$vvnyX z5Zyi!dzD-ayXMx6P@TX}hdr%&E;=%pcH?5t{MwnAM-UT5!78ta#`8KQ^7-k$N1uij z->VG&nj8wqqnpROd}&GuR{u({j@L&!oHm~@GuFP}!ev3<73}Cu4W+7D`O1fuOjUG- zu92pSVvM|@0~63f%KJ%Dbf7qP#%*nBO_n9KvV4#g`+d@~8U9LWWFruK zN)Lg@@Ya*ZJBl&IP^(goYLw5fDX;WCJj@rb)+j4Hw5?J)tQB|AY7opTInraZ>uD1J zt4Kf=Qo~jnYS>ukt2}P(^C8uhA!q_)MZ#PjUk4H zn_F$<91x~KfkB-uq9Y132lJ}T7yt;o!3i-P6qwNITVC)AUzt)NTv><-_nEDMaL?y^ z0xI$Y8Y>-QJ!BV8-gJy+>~M z*UaCqDm&ie2D~c_*^1D6u8Hfeyl^^tHFJ8m$otL*b^H;-z3R(2x-ZeUK)7T7AO6^N zR>4Q5?>Y(cutJVz-aV5VI3XRw-T^f6bR?z_6>>&o$I@W{V}3kqVK=?*z-cQ zt)UB0x6T;t*0o2NeF+W`*7xmBf#3&e#Il`Vx>v-{Rt9x^_YM}VHz4iX}23V~7wL3meCdO>X%VEzQ z2DR+_aN)q-x*no!ek0?JQUu!QWsBp`@QeQ zX^9jQHfW;EzvzVNGh>n~u-J$BxN34HcpSawvnwV7JZ_Bezps2J{v$q_EGj9 z5yaWWj=6pUk-;LLZ`u00!k4Z-!albdMJ~x;`?8q6O6^bl^d|+EQs4Ua8~s|M$MOBz z_L8{di}R?~mIIoen!RZY6;4~Cp1YX}-N;z-!u54E?N&P8iS!pX#8NrNLhY0Q*D~CG z8VD$=(Pq5m2qQ0Ddd2fCG=*v$mq$HofeD#!Z3f6|YPy-P0|vV4mbeIDBc`>wixC9A z^QNzQ`wr3mPGEYr+pz(owk4~@o4*4u9nX^WBa5w+0u$TW# zzE#^%DP|`Gj3sz$J@j(2v`Pl+GE@G3Oc>v}4W1IZ%^P~TuJHn1HxA|8!NUuPFe0>O zB)!=K0iiozL5ll+J79q>=3#nYY16ELYwYo^6K$-$CPpgG`VRx1Y& zMy<|wieDCICkIV+PrMO}*LcMNm_SQf>Ju)jb|B6j!pRrgJ?`g~wZ}}{W=F+%n$8;4 z;Qe$Gnb|ujP+9_OEW|434mL9>k`w)wXq7PC`j8T(Xi7I|x_`EXYj{VYi=YZP9M-IY z1$>Jv&{(mhG1kuLG6ZaaI-gELElzDX6K~e5J!VS)hq>0Z+^j*~jDJfZUK!RUuT2dB zB{*TCSoBuqB@*P2Y8wf#z~Xtnh9_5kSvp8w;P@$2J5ZUF4MuQc%GU{SeQIq-3ZUF7*;4of6_ z^>r%H#}{N^5{Pk5S|r&Qj-XOz&-x>%@oRX>QL?*u7@SyQR||Ns#0*IIbwBwf zFxA5ZnppKEver}3Tw-AvbacBPek^G>Au_2GF6x;N#m z@^ny}8wiY#cztqee!Vh&F?rT-db-}}xPb;fTpEvwguY%MLA$0;rbM0}ue^Uf-J5x2 ztwUBl1*Jw=*DtHr;`Aw@D<{dArOtd7eT*bZBhIMd>TFr2CbaB(vGV8}476ci0(iwq zutkrgovFo7*7-!9q={rc=&mEnDJ?ycZURtjy|!>(ct1?zo*qjFr~M8il{LYE@JdUq ze|?waCn&YZ2vQ1i8%-evsqydmj^?YQXRGbEWOLr(wU+h+5l$JMlwEw~R@Iks>TmHH zON)RACyZ9g9KLeP>ccslw|L;vP$0rFqp|XZkKCeqOHTa_UUjKC5aEbX8>?VYHcq`N z{C_*Cb8%z7KvHy?wc`aSUOVx?}KsZgBu<_q#2eH{3 zOaCnbxjVsgq=Nq?682*yooIZhXGkMAzADiF-@&zX2`^`7!a=NplerJ|9BI0&{C^F? zHW;p@^LbG_Rrh1Xo$!1L&uynk!#4Q#V?+Lj`2PL~^%94zBOHzWUvFj0IVW3392)y} zFLUd;8ru^a`|C*0lW_^^YbpS@^|E`wXNOg-R>6|3qW6e0SN>VSw^RdP&0za?{f)Tb zUYRx>wF61l>>*j+S`ps1< z;K+Y=d)sH8nVs9=rO@ces#Upwev!F$$$JN%UkWQwxb~@a*gw2uk(o<=?GS|PyfZr9 zw8)GCXua&M?bz|Q8;PaijbnI~;O_?;rEl$z8si^XwQ(-8-i*pwcG5kJ+fVRY+>GWb zUkom)?_L^-)Q*Enr-6q`T?;_pmm-7OVn_1_gTp=bmkZFPK0)gxB#{~AQL(1Ck=F#G zcxLYtF+d)#wEXL4lr*}g_wuHnd3Nmq-PIA}k_Di9-!&nK&Pmdz*)*v6?wqEm<_s<1VssCKrOCNZx&djQL zBHeaNp1S$*_f^oUasDV@n_&KJa6P6(%&dFmwH#>7B6C{YDxl^H8>bAdB~$pBuiq%)yjJ?-+^Nv218bwk)Y4@2`O5Jf?fZc1G|wMe9P#FW3* z&uAs>#k`k-(LgEbB;&XCrk5mOf*xZ{n^JLbVruGFa+D{jR`x;`55p3cqy$hh?JrPG zW%7*|z6G+Of=OGOnl7DWye4E;v#d&+kZCL{6tHSKD+gBW*~|IGabk%zKTt6>pY2&^ zz+_2SCoGElZ*rWa8Ye;dCOaw176JUM?hx)s`^hz@h6NHO#6Y$EG08NQtFf-Sv0=Yp z>v+&KXRr!RTGtP!&OF|NAR#DB7GU_VI`?N)8~@Q;51-f`2NEvopn1(ww0VJ_v|3*7GT` zG`77mA%VW@z3p*{-pux+8RMM42?@Lvq*u~PDrO)aCX;5Y=}2g8evh!I zrM+uD+NFb$0;IVOZeGjYQO=_Kb0;Wsv*(~KkAVJO72N!S9eg)x zMFyR)I5ruwcz zqBk7N&EI5TO&_hr>Y+&`+NwK<5pA)dE2^x~(X$;KWnW%1w;dfDHkK8`#K~f}XtW~s zYOQOv^IvGlW!z=9BOa)+?@G(s0X_WFV{3}eWT&$xei->z zK{DT%C3AGttP9xRjoV!O)NFeHYucWD+RfhQct;LmBu7W4K;-qwiON1#&k-wTNd7?Y$D*Wi1(n`&;p?p9mdA~RDs?a5|Ycx+vZ zJsnC&j#A?~XASo0Tka5$H&3#o0*~;Wm<8xL&39dv#PO-g){6vw^!J#na*wnI`_5;)qJ&m^j| zHk)N_#=F3mG;}$QzG^T3Ds;1X6t~x@l4)w@JkvuJS+GjrcN?=LyOZBcT5k(SKbXiR z6YoflpwnY<(@G%3-n9>#v#Cui=G5o!&y@CHRZJws-e`9CX4Ku?vc}nPV|F>0#KSZRr9$5lvKNQ>HLdLO9~+9MSx*;>a;_ zsIgqCcJcxv_$Hr!$ADPEpdC*OijOstCjwTv$a%`xVi-uN5S7(O6gC-ty z<;kvQ|GwrDTg5BJ^^=svl0--<2}Ehjy7~)`I=Il>L9wd4tf=+6m}5PQ>x_0*zHsC| zj*F>fQpDFL?#sG~v$!9tU#&<4c|+?&G@9z!T)J};7Jjg&#OOTmSXd=mV7-X)o7euE ztFG0&i}g371T3;PvfR5ajEZi%Fk)b<4_VkqtoCSDyYbMfet=yVsIRtRqrTuvU+~65 zvek9DWvd(4s6<2Bax=eMf2mAV)Q!~KTDy7!s`KN@_|!e>)>=m0j2rL30Ug6!iG1Ad zy4Wo4_rA#+cT1RIHO6AOkq!s^QByx4lg?RIa=MjYj^mFbHLjlQM(Vv8Xl zp`S(K9gI`d(DeStaEAz#P~iI>s%b zbYEs2yV|BT5*j5sB{Z$3#-nK3CIPj|0yOTX2G^?6u9|?0;j6-d;bMvfc=7^_Z>R#UAOEmK`jc~DIAN~D+)ifKv{p+vcXjU55f!z zf2n)_(7nHa{@;IhWd!8{tN*t>z`WorfL)m&>SonAqVR!PEE&3;@kMy7F@aJ4nZIb< z!>Iq32@HP;6GX!YvGW0Q8R-926mGgBn*JYv2gt`|*g!PjRXHI|b^po(n=bv-U+DI= zVTRITMdBBclfaESGSu`iuyO*KVmJ^Mjcr=Fuqz=PO1E*xVPynb0F5mUkqxqT*({&6 z02VwO`W_CW5zts8!uimRfW{gIhtUO)avk#p=>K(_Y(`RA+0b;XRZWW~EO&cOINjgv zWiQ^%Ik6vuOaNvO&0pi*60~j>Tkbp{yP+O8kJSDHkB7j6HVv>vM(Uuk;ZPnc{D)Ea z7oDcYyacRJ(MM6hFEYXWJO-W>U6h2Qsv9(|I>}W{$yE{J&$Ruly5AujTJ<4O2NJVq z6gUf<0{IPvp94;!2OfRBWzwpz8!SOr_=_yL!zuXno+|u@th%5l`&p3mcUz@D>ymGM z$(zP67OpHj>ikisSX2{e?waIRNY=e+{&kVE(c6sbe`w4uo1=xf$+D6d6N+1*A@{~j zp!Vz0FU+oLe~T(gm>kz#RN=bx**U^k^{;Wys2fbggta{Y#nS1E-7{*i1>5AYe z?Avz7B_BLJyLulsqxTyWhOl~Y(jC?Q*ta7{cZ;G+J&r0G`qB2{GAjLbrS10K)cY9+ z7RpAPEB_qDtNm7-vt(;KT+G{yntu~<$-8sB>TkEC5yTVKUr{u&xrfE35gWQH^qiZ< zH?Xgbn)f_TSb8Q{_5Q~fo)_p&5!}#G1_{|PK0##w)0VZelzX5#*^B%C8 zcHkLK&kt-6RWR@jR|sRnX<{VH6h4g-#^~IjPjTH4R zU?p{6=54>eboHrwPus8GH3+z)SZ&&RQNJt>yEiCtlL>9iO*tW41p!hw1tmMpazQfI z^*YS8M}lay#ZkY1262Bo~6{m_C{W)8(YvE!e4~eQ90q5 zYJZkEC(>fh4u|pIG$vbx9h#NZgDjg4-=xFtC@=sc!wt^zQr8`5zCrZpc%d5{Ar%-HI2>U47-zrqs5#7tIjpaPYR5!{qx@Ik5%A?-sB<2mzzC7Fy^^lVlMd391)IqAPOf&3jtH-ddU zF054d<8C&|=C-<)y-CgO&{r;Ao3C|ZjmzfL2xFMqd#bih0I3im%+Ni;tN4^U1rBgk ziI2t-Az7%`B(z|mt8VyYTvpkvTri6lFg%&(5%DnaTIyN7HUA!Fyba(-#6cbCv}!D2 zz_vZq?k0W6iPFbaZ&l-k?b>H$x4C7Ct+PWi)`I%1+|Z53c-ohqt5J41-mq~YONZvK zF@7uY*CZXkiHmj47!Boq3}ZLA*>0RnZdb<b(*#o)Z^4L{PGET}>qZmD?)KrG#aR>x8JDRyQQh^uGl%Nf;JG`7pYvwdHoB`b4wG zUd}NVt1p{O(&iCZZNz$UXShvCwnt(^axOUEpgSPV=DT9OyT@hjc05t7+Z3#}d8%#A z6g_Sh4I=_^Q}!q-#dnpqOHZB6IT>v*8eom_ z9rr9ARW=%d9i9gQ-C!3hI@dxmJ7!Oyn=P5ort#U_9xXR$ROPA&C9g|m^?6v2%!S?O z{gGqv;b=8n0>%wX3p(0h_V$&@FY`Reah{+a>H}?!8=1Z z2U*TvW1}?O-Nb!9wXml1eoE;J@SgXge`NOGru50f?17gHyu3&Bysvu;%2jh)-VYV;OHVw43_P6sG46~Jex0;aM$inZ< z`2`B+fx=gF9{AyM!e7M|S9I=sE>6$@mM`X%p3Zv8$nWjB=Q5(DqF(UvoXS_6F=geq zCEJLeaxgs$-e`GEW58uY464m{vU+ntzl?>oy#@gER330-4s4Pp4m$}sv;r;7ePkz_ z0VCIe&s(qO^AbGmYQonzNIzlcuPcMs>x#zC`A8?0F+-@e;6|v2dV^NVy4hKPum5GwrYi@b6n!QLAZX5rW0kVE`I!q*%l@8J_Oc$sD8|25@$^58K^zB7JZ6S zC-ZdHR~c!yhiCl) zt*>TnN(lMtMAi@du_<4$#ubsR=VCm0G9-@pS2)J1oOt_E|kc&47R<;U|Hb>7T)TP0j zG6X2E^7vq?shb^F(|m=r11zhtZTHTm!Q6kHx(oI^ZCCVl8_)swrkwFQaUaMwKj#sjr~ zPmsb&pcCBIbEMhDY=y)xw>_96%`Rs9wBy1hZLe@~`OVp0k@o>K?rPEox0NvAXkZ6F z<>KqfJ_pD-n{)*9y}%UDW^9NIERo(p@=Yh|j2^^vzA-Ope24Joxz@H(Oz{2bQMubs#gWF#H@d=^WnE zDNp3_4C>j)Y^Qw%^|WMe(@xKu#Q31X2=a8N-G@M_i%N=oF;iQ;?E|1xXDB_J?^6c0 z^PMt8e1Wo8+-oQMA}c)Q;41<<)bEGc_kzGrCBzl$UJ*E(wC@*M;LN%A0fDa|%Kdz{ z7RUui83Lpa0gV8b4>@ z=lkuOPT3Z=_Vj&8K6nyq9zzqu&dVARF*c1bIy9s$YHey}1NzE(TrIc|09fHc-i19j zb_84H0gdoD?_xUNgs7{-RQ+h-BnTlbuO^B(e``c^n1$qB5%^&rA(*fsFwFS{0)L;x z7T4Fx6ZnPs{v8>(Pqqw{eT5aCPW9XIE=+ZKdzW3!^!qTaV}jN;?TyqXKVi&81!dhD z^)KY8_UzzjWNy$ITWdKX_QxWYq@OkzddE1%~)`9NcGX_ZwD$oCx9P)cwBf zJD;{~l`s=-&*(hVjR5DRGw`3)lK|xFW=doo}b@Hjwi+-Q@H`KCy|tcDAq3*`*?s0ZBUM_PUa^BaxkMF`Ml7WR1Nwf8Q@=y$&F@ z7pD9j5~pFNR}5haA@}*d$P?dwOJJW5b6uwby44#?iGPA z`Z~l{W_v~4tJ%KA5mWj;=tA+76}|=k`lv#AZ=SETYx;VYolNr0)qkl|$XD~~tHgY; zsa`5j|1H?`4VpffZm)s-kGD_%{ON~s`}F5u{_^v0pMLo9$Mv?@KXP*TJ8)0#n0xI` zyJzmmJ-Ea7+@15DXy@U!@Za;l!=1amb$9pf#>2>^^zU%Pu44+?_k#x{puYhsW;YVE4&r_sMW~KOV5FyK|r3y7znc z@lCU<{k{9-IUFw-0b%*s-MWuY-G|5S<6!s6X!pr*cRwDSA;X5FZ_RP`N-PS$_p^d9v?m;hLRxBk0-ua#PrmhXK${f_<_|GmG5&q;Mr=~kUv zmEZpV`tK|GcWmVm8@OxVnaq54^BwywyNagT8ohU$NNuj0xxck>Rv0I?IqotqeP=ae z(f1|zEk(e(`kU*!I+p!ytNU&G4*q_97iqSe-{RLH105UQS>^*gV%B|=|KH?UD7(wg zJ6d#pz@A`*vR0 z&`xP>f0v(McJs4*px=|tZ?@0dwc3sR(RJ8)Zn@E>Ki}6i(Gm9Bm!Ce9)O=JV{69uL z=> 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() From 6292e3774abd82f2d5202190b498f35cc1628c39 Mon Sep 17 00:00:00 2001 From: Ross Richardson Date: Wed, 14 Oct 2026 02:05:08 +1100 Subject: [PATCH 2/2] Record helper-triple sprint result and PR handoff --- research/r439-helper-triples/CLAIM.json | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/research/r439-helper-triples/CLAIM.json b/research/r439-helper-triples/CLAIM.json index 7142a10ca8..c5eef03d6e 100644 --- a/research/r439-helper-triples/CLAIM.json +++ b/research/r439-helper-triples/CLAIM.json @@ -28,7 +28,20 @@ "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": "pending", + "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",