From 5b800ec52af93ef62adf610f52c9488e71054619 Mon Sep 17 00:00:00 2001 From: Aaron Wang Date: Thu, 15 Oct 2026 00:52:24 -0400 Subject: [PATCH] Add Q8 inverse-label pair census at r=2 (exact minima, no compression) --- .../CERTIFICATE.json | 3040 +++++++++++++++++ .../q8-inverse-label-pair-census/README.md | 187 + .../q8-inverse-label-pair-census/SOURCES.json | 24 + .../q8-inverse-label-pair-census/TASK.json | 69 + research/q8-inverse-label-pair-census/TASK.md | 79 + .../q8-inverse-label-pair-census/VERIFY.json | 21 + .../q8-inverse-label-pair-census/verify.py | 575 ++++ 7 files changed, 3995 insertions(+) create mode 100644 research/q8-inverse-label-pair-census/CERTIFICATE.json create mode 100644 research/q8-inverse-label-pair-census/README.md create mode 100644 research/q8-inverse-label-pair-census/SOURCES.json create mode 100644 research/q8-inverse-label-pair-census/TASK.json create mode 100644 research/q8-inverse-label-pair-census/TASK.md create mode 100644 research/q8-inverse-label-pair-census/VERIFY.json create mode 100644 research/q8-inverse-label-pair-census/verify.py diff --git a/research/q8-inverse-label-pair-census/CERTIFICATE.json b/research/q8-inverse-label-pair-census/CERTIFICATE.json new file mode 100644 index 0000000000..6cc3e43480 --- /dev/null +++ b/research/q8-inverse-label-pair-census/CERTIFICATE.json @@ -0,0 +1,3040 @@ +{ + "checks_failed": [], + "compressed_pairs_inverse": [], + "compressed_pairs_positive": [], + "controls": 27, + "endpoints": { + "diag_m1_m1": { + "inverse": { + "bill": 4, + "minimum": 4, + "proven": "complete BFS to depth 3 excludes every word of length <= 3; the direct word attains 4", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 4, + "minimum": 4, + "proven": "complete BFS to depth 5 finds distance 4, at or below the direct bill 4", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ] + ] + } + }, + "diag_m1_mi": { + "inverse": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 3 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 3, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 5, + "minimum": 5, + "proven": "complete BFS to depth 5 finds distance 5, at or below the direct bill 5", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ] + ] + } + }, + "diag_m1_mj": { + "inverse": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 3 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 5, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 5, + "minimum": 5, + "proven": "complete BFS to depth 5 finds distance 5, at or below the direct bill 5", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ], + [ + 4, + 2, + 2 + ] + ] + } + }, + "diag_m1_mk": { + "inverse": { + "bill": 4, + "minimum": 4, + "proven": "complete BFS to depth 3 excludes every word of length <= 3; the direct word attains 4", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 5, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 4, + "minimum": 4, + "proven": "complete BFS to depth 5 finds distance 4, at or below the direct bill 4", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 4, + 2, + 2 + ], + [ + 2, + 2, + 2 + ] + ] + } + }, + "diag_m1_p1": { + "inverse": { + "bill": 2, + "minimum": 2, + "proven": "complete BFS to depth 3 finds distance 2, at or below the direct bill 2", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ] + ] + }, + "positive": { + "bill": 2, + "minimum": 2, + "proven": "complete BFS to depth 5 finds distance 2, at or below the direct bill 2", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ] + ] + } + }, + "diag_m1_pi": { + "inverse": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 3 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 2, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 5 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 2, + 2, + 2 + ] + ] + } + }, + "diag_m1_pj": { + "inverse": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 3 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 4, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 5 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 4, + 2, + 2 + ] + ] + } + }, + "diag_m1_pk": { + "inverse": { + "bill": 4, + "minimum": 4, + "proven": "complete BFS to depth 3 excludes every word of length <= 3; the direct word attains 4", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 4, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 4, + "minimum": 4, + "proven": "complete BFS to depth 5 finds distance 4, at or below the direct bill 4", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 4, + 2, + 2 + ] + ] + } + }, + "diag_mi_m1": { + "inverse": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 3 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ], + [ + 3, + 1, + 1 + ] + ] + }, + "positive": { + "bill": 5, + "minimum": 5, + "proven": "complete BFS to depth 5 finds distance 5, at or below the direct bill 5", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ] + ] + } + }, + "diag_mi_mi": { + "inverse": { + "bill": 2, + "minimum": 2, + "proven": "complete BFS to depth 3 finds distance 2, at or below the direct bill 2", + "word": [ + [ + 3, + 1, + 1 + ], + [ + 3, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 6, + "minimum": 6, + "proven": "complete BFS to depth 5 excludes every word of length <= 5; the direct word attains 6", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ] + ] + } + }, + "diag_mi_mj": { + "inverse": { + "bill": 2, + "minimum": 2, + "proven": "complete BFS to depth 3 finds distance 2, at or below the direct bill 2", + "word": [ + [ + 3, + 1, + 1 + ], + [ + 5, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 6, + "minimum": 6, + "proven": "complete BFS to depth 5 excludes every word of length <= 5; the direct word attains 6", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ], + [ + 4, + 2, + 2 + ] + ] + } + }, + "diag_mi_mk": { + "inverse": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 3 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 2, + 2 + ], + [ + 3, + 1, + 1 + ], + [ + 5, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 5, + "minimum": 5, + "proven": "complete BFS to depth 5 finds distance 5, at or below the direct bill 5", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 4, + 2, + 2 + ], + [ + 2, + 2, + 2 + ] + ] + } + }, + "diag_mi_p1": { + "inverse": { + "bill": 1, + "minimum": 1, + "proven": "complete BFS to depth 3 finds distance 1, at or below the direct bill 1", + "word": [ + [ + 3, + 1, + 1 + ] + ] + }, + "positive": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 5 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ] + ] + } + }, + "diag_mi_pi": { + "inverse": { + "bill": 2, + "minimum": 2, + "proven": "complete BFS to depth 3 finds distance 2, at or below the direct bill 2", + "word": [ + [ + 2, + 2, + 2 + ], + [ + 3, + 1, + 1 + ] + ] + }, + "positive": { + "bill": 4, + "minimum": 4, + "proven": "complete BFS to depth 5 finds distance 4, at or below the direct bill 4", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 2, + 2, + 2 + ] + ] + } + }, + "diag_mi_pj": { + "inverse": { + "bill": 2, + "minimum": 2, + "proven": "complete BFS to depth 3 finds distance 2, at or below the direct bill 2", + "word": [ + [ + 3, + 1, + 1 + ], + [ + 4, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 4, + "minimum": 4, + "proven": "complete BFS to depth 5 finds distance 4, at or below the direct bill 4", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 4, + 2, + 2 + ] + ] + } + }, + "diag_mi_pk": { + "inverse": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 3 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 2, + 2 + ], + [ + 3, + 1, + 1 + ], + [ + 4, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 5, + "minimum": 5, + "proven": "complete BFS to depth 5 finds distance 5, at or below the direct bill 5", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 4, + 2, + 2 + ] + ] + } + }, + "diag_mj_m1": { + "inverse": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 3 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ], + [ + 5, + 1, + 1 + ] + ] + }, + "positive": { + "bill": 5, + "minimum": 5, + "proven": "complete BFS to depth 5 finds distance 5, at or below the direct bill 5", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ], + [ + 4, + 1, + 1 + ] + ] + } + }, + "diag_mj_mi": { + "inverse": { + "bill": 2, + "minimum": 2, + "proven": "complete BFS to depth 3 finds distance 2, at or below the direct bill 2", + "word": [ + [ + 3, + 2, + 2 + ], + [ + 5, + 1, + 1 + ] + ] + }, + "positive": { + "bill": 6, + "minimum": 6, + "proven": "complete BFS to depth 5 excludes every word of length <= 5; the direct word attains 6", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 4, + 1, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ] + ] + } + }, + "diag_mj_mj": { + "inverse": { + "bill": 2, + "minimum": 2, + "proven": "complete BFS to depth 3 finds distance 2, at or below the direct bill 2", + "word": [ + [ + 5, + 1, + 1 + ], + [ + 5, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 6, + "minimum": 6, + "proven": "complete BFS to depth 5 excludes every word of length <= 5; the direct word attains 6", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 4, + 1, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ], + [ + 4, + 2, + 2 + ] + ] + } + }, + "diag_mj_mk": { + "inverse": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 3 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 2, + 2 + ], + [ + 5, + 1, + 1 + ], + [ + 5, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 5, + "minimum": 5, + "proven": "complete BFS to depth 5 finds distance 5, at or below the direct bill 5", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 4, + 1, + 1 + ], + [ + 4, + 2, + 2 + ], + [ + 2, + 2, + 2 + ] + ] + } + }, + "diag_mj_p1": { + "inverse": { + "bill": 1, + "minimum": 1, + "proven": "complete BFS to depth 3 finds distance 1, at or below the direct bill 1", + "word": [ + [ + 5, + 1, + 1 + ] + ] + }, + "positive": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 5 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 4, + 1, + 1 + ] + ] + } + }, + "diag_mj_pi": { + "inverse": { + "bill": 2, + "minimum": 2, + "proven": "complete BFS to depth 3 finds distance 2, at or below the direct bill 2", + "word": [ + [ + 2, + 2, + 2 + ], + [ + 5, + 1, + 1 + ] + ] + }, + "positive": { + "bill": 4, + "minimum": 4, + "proven": "complete BFS to depth 5 finds distance 4, at or below the direct bill 4", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 4, + 1, + 1 + ] + ] + } + }, + "diag_mj_pj": { + "inverse": { + "bill": 2, + "minimum": 2, + "proven": "complete BFS to depth 3 finds distance 2, at or below the direct bill 2", + "word": [ + [ + 4, + 2, + 2 + ], + [ + 5, + 1, + 1 + ] + ] + }, + "positive": { + "bill": 4, + "minimum": 4, + "proven": "complete BFS to depth 5 finds distance 4, at or below the direct bill 4", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 4, + 1, + 1 + ], + [ + 4, + 2, + 2 + ] + ] + } + }, + "diag_mj_pk": { + "inverse": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 3 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 2, + 2 + ], + [ + 4, + 2, + 2 + ], + [ + 5, + 1, + 1 + ] + ] + }, + "positive": { + "bill": 5, + "minimum": 5, + "proven": "complete BFS to depth 5 finds distance 5, at or below the direct bill 5", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 4, + 1, + 1 + ], + [ + 4, + 2, + 2 + ] + ] + } + }, + "diag_mk_m1": { + "inverse": { + "bill": 4, + "minimum": 4, + "proven": "complete BFS to depth 3 excludes every word of length <= 3; the direct word attains 4", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 5, + 1, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 4, + "minimum": 4, + "proven": "complete BFS to depth 5 finds distance 4, at or below the direct bill 4", + "word": [ + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ], + [ + 4, + 1, + 1 + ], + [ + 2, + 1, + 1 + ] + ] + } + }, + "diag_mk_mi": { + "inverse": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 3 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 3, + 2, + 2 + ], + [ + 5, + 1, + 1 + ] + ] + }, + "positive": { + "bill": 5, + "minimum": 5, + "proven": "complete BFS to depth 5 finds distance 5, at or below the direct bill 5", + "word": [ + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ], + [ + 4, + 1, + 1 + ], + [ + 2, + 1, + 1 + ] + ] + } + }, + "diag_mk_mj": { + "inverse": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 3 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 5, + 1, + 1 + ], + [ + 5, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 5, + "minimum": 5, + "proven": "complete BFS to depth 5 finds distance 5, at or below the direct bill 5", + "word": [ + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ], + [ + 4, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 4, + 2, + 2 + ] + ] + } + }, + "diag_mk_mk": { + "inverse": { + "bill": 4, + "minimum": 4, + "proven": "complete BFS to depth 3 excludes every word of length <= 3; the direct word attains 4", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 5, + 1, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 5, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 4, + "minimum": 4, + "proven": "complete BFS to depth 5 finds distance 4, at or below the direct bill 4", + "word": [ + [ + 4, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 4, + 2, + 2 + ], + [ + 2, + 2, + 2 + ] + ] + } + }, + "diag_mk_p1": { + "inverse": { + "bill": 2, + "minimum": 2, + "proven": "complete BFS to depth 3 finds distance 2, at or below the direct bill 2", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 5, + 1, + 1 + ] + ] + }, + "positive": { + "bill": 2, + "minimum": 2, + "proven": "complete BFS to depth 5 finds distance 2, at or below the direct bill 2", + "word": [ + [ + 4, + 1, + 1 + ], + [ + 2, + 1, + 1 + ] + ] + } + }, + "diag_mk_pi": { + "inverse": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 3 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 5, + 1, + 1 + ] + ] + }, + "positive": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 5 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 2, + 2 + ], + [ + 4, + 1, + 1 + ], + [ + 2, + 1, + 1 + ] + ] + } + }, + "diag_mk_pj": { + "inverse": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 3 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 4, + 2, + 2 + ], + [ + 5, + 1, + 1 + ] + ] + }, + "positive": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 5 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 4, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 4, + 2, + 2 + ] + ] + } + }, + "diag_mk_pk": { + "inverse": { + "bill": 4, + "minimum": 4, + "proven": "complete BFS to depth 3 excludes every word of length <= 3; the direct word attains 4", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 5, + 1, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 4, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 4, + "minimum": 4, + "proven": "complete BFS to depth 5 finds distance 4, at or below the direct bill 4", + "word": [ + [ + 2, + 2, + 2 + ], + [ + 4, + 1, + 1 + ], + [ + 2, + 1, + 1 + ], + [ + 4, + 2, + 2 + ] + ] + } + }, + "diag_p1_m1": { + "inverse": { + "bill": 2, + "minimum": 2, + "proven": "complete BFS to depth 3 finds distance 2, at or below the direct bill 2", + "word": [ + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 2, + "minimum": 2, + "proven": "complete BFS to depth 5 finds distance 2, at or below the direct bill 2", + "word": [ + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ] + ] + } + }, + "diag_p1_mi": { + "inverse": { + "bill": 1, + "minimum": 1, + "proven": "complete BFS to depth 3 finds distance 1, at or below the direct bill 1", + "word": [ + [ + 3, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 5 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ] + ] + } + }, + "diag_p1_mj": { + "inverse": { + "bill": 1, + "minimum": 1, + "proven": "complete BFS to depth 3 finds distance 1, at or below the direct bill 1", + "word": [ + [ + 5, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 5 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ], + [ + 4, + 2, + 2 + ] + ] + } + }, + "diag_p1_mk": { + "inverse": { + "bill": 2, + "minimum": 2, + "proven": "complete BFS to depth 3 finds distance 2, at or below the direct bill 2", + "word": [ + [ + 2, + 2, + 2 + ], + [ + 5, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 2, + "minimum": 2, + "proven": "complete BFS to depth 5 finds distance 2, at or below the direct bill 2", + "word": [ + [ + 4, + 2, + 2 + ], + [ + 2, + 2, + 2 + ] + ] + } + }, + "diag_p1_p1": { + "inverse": { + "bill": 0, + "minimum": 0, + "proven": "complete BFS to depth 3 finds distance 0, at or below the direct bill 0", + "word": [] + }, + "positive": { + "bill": 0, + "minimum": 0, + "proven": "complete BFS to depth 5 finds distance 0, at or below the direct bill 0", + "word": [] + } + }, + "diag_p1_pi": { + "inverse": { + "bill": 1, + "minimum": 1, + "proven": "complete BFS to depth 3 finds distance 1, at or below the direct bill 1", + "word": [ + [ + 2, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 1, + "minimum": 1, + "proven": "complete BFS to depth 5 finds distance 1, at or below the direct bill 1", + "word": [ + [ + 2, + 2, + 2 + ] + ] + } + }, + "diag_p1_pj": { + "inverse": { + "bill": 1, + "minimum": 1, + "proven": "complete BFS to depth 3 finds distance 1, at or below the direct bill 1", + "word": [ + [ + 4, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 1, + "minimum": 1, + "proven": "complete BFS to depth 5 finds distance 1, at or below the direct bill 1", + "word": [ + [ + 4, + 2, + 2 + ] + ] + } + }, + "diag_p1_pk": { + "inverse": { + "bill": 2, + "minimum": 2, + "proven": "complete BFS to depth 3 finds distance 2, at or below the direct bill 2", + "word": [ + [ + 2, + 2, + 2 + ], + [ + 4, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 2, + "minimum": 2, + "proven": "complete BFS to depth 5 finds distance 2, at or below the direct bill 2", + "word": [ + [ + 2, + 2, + 2 + ], + [ + 4, + 2, + 2 + ] + ] + } + }, + "diag_pi_m1": { + "inverse": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 3 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 5 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ] + ] + } + }, + "diag_pi_mi": { + "inverse": { + "bill": 2, + "minimum": 2, + "proven": "complete BFS to depth 3 finds distance 2, at or below the direct bill 2", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 3, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 4, + "minimum": 4, + "proven": "complete BFS to depth 5 finds distance 4, at or below the direct bill 4", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ] + ] + } + }, + "diag_pi_mj": { + "inverse": { + "bill": 2, + "minimum": 2, + "proven": "complete BFS to depth 3 finds distance 2, at or below the direct bill 2", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 5, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 4, + "minimum": 4, + "proven": "complete BFS to depth 5 finds distance 4, at or below the direct bill 4", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ], + [ + 4, + 2, + 2 + ] + ] + } + }, + "diag_pi_mk": { + "inverse": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 3 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 5, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 5 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 4, + 2, + 2 + ], + [ + 2, + 2, + 2 + ] + ] + } + }, + "diag_pi_p1": { + "inverse": { + "bill": 1, + "minimum": 1, + "proven": "complete BFS to depth 3 finds distance 1, at or below the direct bill 1", + "word": [ + [ + 2, + 1, + 1 + ] + ] + }, + "positive": { + "bill": 1, + "minimum": 1, + "proven": "complete BFS to depth 5 finds distance 1, at or below the direct bill 1", + "word": [ + [ + 2, + 1, + 1 + ] + ] + } + }, + "diag_pi_pi": { + "inverse": { + "bill": 2, + "minimum": 2, + "proven": "complete BFS to depth 3 finds distance 2, at or below the direct bill 2", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 2, + "minimum": 2, + "proven": "complete BFS to depth 5 finds distance 2, at or below the direct bill 2", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 2, + 2 + ] + ] + } + }, + "diag_pi_pj": { + "inverse": { + "bill": 2, + "minimum": 2, + "proven": "complete BFS to depth 3 finds distance 2, at or below the direct bill 2", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 4, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 2, + "minimum": 2, + "proven": "complete BFS to depth 5 finds distance 2, at or below the direct bill 2", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 4, + 2, + 2 + ] + ] + } + }, + "diag_pi_pk": { + "inverse": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 3 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 4, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 5 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 4, + 2, + 2 + ] + ] + } + }, + "diag_pj_m1": { + "inverse": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 3 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ], + [ + 4, + 1, + 1 + ] + ] + }, + "positive": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 5 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ], + [ + 4, + 1, + 1 + ] + ] + } + }, + "diag_pj_mi": { + "inverse": { + "bill": 2, + "minimum": 2, + "proven": "complete BFS to depth 3 finds distance 2, at or below the direct bill 2", + "word": [ + [ + 3, + 2, + 2 + ], + [ + 4, + 1, + 1 + ] + ] + }, + "positive": { + "bill": 4, + "minimum": 4, + "proven": "complete BFS to depth 5 finds distance 4, at or below the direct bill 4", + "word": [ + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ], + [ + 4, + 1, + 1 + ] + ] + } + }, + "diag_pj_mj": { + "inverse": { + "bill": 2, + "minimum": 2, + "proven": "complete BFS to depth 3 finds distance 2, at or below the direct bill 2", + "word": [ + [ + 4, + 1, + 1 + ], + [ + 5, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 4, + "minimum": 4, + "proven": "complete BFS to depth 5 finds distance 4, at or below the direct bill 4", + "word": [ + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ], + [ + 4, + 1, + 1 + ], + [ + 4, + 2, + 2 + ] + ] + } + }, + "diag_pj_mk": { + "inverse": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 3 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 2, + 2 + ], + [ + 4, + 1, + 1 + ], + [ + 5, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 5 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 4, + 1, + 1 + ], + [ + 4, + 2, + 2 + ], + [ + 2, + 2, + 2 + ] + ] + } + }, + "diag_pj_p1": { + "inverse": { + "bill": 1, + "minimum": 1, + "proven": "complete BFS to depth 3 finds distance 1, at or below the direct bill 1", + "word": [ + [ + 4, + 1, + 1 + ] + ] + }, + "positive": { + "bill": 1, + "minimum": 1, + "proven": "complete BFS to depth 5 finds distance 1, at or below the direct bill 1", + "word": [ + [ + 4, + 1, + 1 + ] + ] + } + }, + "diag_pj_pi": { + "inverse": { + "bill": 2, + "minimum": 2, + "proven": "complete BFS to depth 3 finds distance 2, at or below the direct bill 2", + "word": [ + [ + 2, + 2, + 2 + ], + [ + 4, + 1, + 1 + ] + ] + }, + "positive": { + "bill": 2, + "minimum": 2, + "proven": "complete BFS to depth 5 finds distance 2, at or below the direct bill 2", + "word": [ + [ + 2, + 2, + 2 + ], + [ + 4, + 1, + 1 + ] + ] + } + }, + "diag_pj_pj": { + "inverse": { + "bill": 2, + "minimum": 2, + "proven": "complete BFS to depth 3 finds distance 2, at or below the direct bill 2", + "word": [ + [ + 4, + 1, + 1 + ], + [ + 4, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 2, + "minimum": 2, + "proven": "complete BFS to depth 5 finds distance 2, at or below the direct bill 2", + "word": [ + [ + 4, + 1, + 1 + ], + [ + 4, + 2, + 2 + ] + ] + } + }, + "diag_pj_pk": { + "inverse": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 3 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 2, + 2 + ], + [ + 4, + 1, + 1 + ], + [ + 4, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 5 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 2, + 2 + ], + [ + 4, + 1, + 1 + ], + [ + 4, + 2, + 2 + ] + ] + } + }, + "diag_pk_m1": { + "inverse": { + "bill": 4, + "minimum": 4, + "proven": "complete BFS to depth 3 excludes every word of length <= 3; the direct word attains 4", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 4, + 1, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 4, + "minimum": 4, + "proven": "complete BFS to depth 5 finds distance 4, at or below the direct bill 4", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ], + [ + 4, + 1, + 1 + ] + ] + } + }, + "diag_pk_mi": { + "inverse": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 3 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 3, + 2, + 2 + ], + [ + 4, + 1, + 1 + ] + ] + }, + "positive": { + "bill": 5, + "minimum": 5, + "proven": "complete BFS to depth 5 finds distance 5, at or below the direct bill 5", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ], + [ + 4, + 1, + 1 + ] + ] + } + }, + "diag_pk_mj": { + "inverse": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 3 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 4, + 1, + 1 + ], + [ + 5, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 5, + "minimum": 5, + "proven": "complete BFS to depth 5 finds distance 5, at or below the direct bill 5", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 2 + ], + [ + 4, + 1, + 1 + ], + [ + 4, + 2, + 2 + ] + ] + } + }, + "diag_pk_mk": { + "inverse": { + "bill": 4, + "minimum": 4, + "proven": "complete BFS to depth 3 excludes every word of length <= 3; the direct word attains 4", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 4, + 1, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 5, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 4, + "minimum": 4, + "proven": "complete BFS to depth 5 finds distance 4, at or below the direct bill 4", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 4, + 1, + 1 + ], + [ + 4, + 2, + 2 + ], + [ + 2, + 2, + 2 + ] + ] + } + }, + "diag_pk_p1": { + "inverse": { + "bill": 2, + "minimum": 2, + "proven": "complete BFS to depth 3 finds distance 2, at or below the direct bill 2", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 4, + 1, + 1 + ] + ] + }, + "positive": { + "bill": 2, + "minimum": 2, + "proven": "complete BFS to depth 5 finds distance 2, at or below the direct bill 2", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 4, + 1, + 1 + ] + ] + } + }, + "diag_pk_pi": { + "inverse": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 3 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 4, + 1, + 1 + ] + ] + }, + "positive": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 5 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 4, + 1, + 1 + ] + ] + } + }, + "diag_pk_pj": { + "inverse": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 3 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 4, + 1, + 1 + ], + [ + 4, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 3, + "minimum": 3, + "proven": "complete BFS to depth 5 finds distance 3, at or below the direct bill 3", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 4, + 1, + 1 + ], + [ + 4, + 2, + 2 + ] + ] + } + }, + "diag_pk_pk": { + "inverse": { + "bill": 4, + "minimum": 4, + "proven": "complete BFS to depth 3 excludes every word of length <= 3; the direct word attains 4", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 4, + 1, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 4, + 2, + 2 + ] + ] + }, + "positive": { + "bill": 4, + "minimum": 4, + "proven": "complete BFS to depth 5 finds distance 4, at or below the direct bill 4", + "word": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 4, + 1, + 1 + ], + [ + 4, + 2, + 2 + ] + ] + } + } + }, + "gl2_order": 6, + "group_table": [ + "+1", + "-1", + "+i", + "-i", + "+j", + "-j", + "+k", + "-k" + ], + "group_table_sha256": "a717b93cc38a70e6724d771334258966c0a203faed70cc55f3a5be716470ca78", + "idempotents_uv": [ + [ + 1, + 1 + ], + [ + 1, + 3 + ], + [ + 2, + 2 + ], + [ + 2, + 3 + ], + [ + 3, + 1 + ], + [ + 3, + 2 + ] + ], + "independent_engine_b": true, + "inverse_ball_sha256": "ed71e5fa123b65a9486e04239f0c15440b4491a526fa49f7057f95a581e00dc0", + "inverse_ball_sha256_engine_b": "ed71e5fa123b65a9486e04239f0c15440b4491a526fa49f7057f95a581e00dc0", + "inverse_generators": 24, + "inverse_layers": [ + 1, + 24, + 358, + 4104 + ], + "model": { + "acceptance": "coefficientwise equality in F2[Q8]", + "free_mixing": "GL_2(F2), normalized by augmentation", + "group": "Q8", + "inverse_labels": [ + "+i", + "-i", + "+j", + "-j" + ], + "paid_call": "I + ([g]+1) N, N = u v^T binary rank-one idempotent", + "positive_labels": [ + "+i", + "+j" + ], + "registers": 2 + }, + "new_kappa": false, + "omission_controls": 372, + "positive_ball_sha256": "3643bcf2bcdc6402cc0e49493edd3a5c3b58f1d0d06c74b3bc1b7a8089dbc3a9", + "positive_ball_sha256_engine_b": "3643bcf2bcdc6402cc0e49493edd3a5c3b58f1d0d06c74b3bc1b7a8089dbc3a9", + "positive_generators": 12, + "positive_layers": [ + 1, + 12, + 110, + 936, + 6945, + 48080 + ], + "predecessor_calibration": { + "diag_xy_yx_r2_minimum": 4, + "diag_z_z_r2_minimum": 4, + "r2_layers": [ + 1, + 12, + 110, + 936 + ], + "source": "research/q8-central-commutator-pair/CERTIFICATE.json" + }, + "status": "PASS_Q8_INVERSE_LABEL_CENSUS" +} \ No newline at end of file diff --git a/research/q8-inverse-label-pair-census/README.md b/research/q8-inverse-label-pair-census/README.md new file mode 100644 index 0000000000..9d7ce15b96 --- /dev/null +++ b/research/q8-inverse-label-pair-census/README.md @@ -0,0 +1,187 @@ +# Q8 pair census under unit-priced inverse labels + +**Complete finite group-algebra census; no new kappa.** In the formal +`F2[Q8]` register model below, every one of the 64 ordered diagonal pair +targets `diag([g1],[g2])` at `r = 2` costs exactly its direct bill, both when +the labels `x^-1 = -i`, `y^-1 = -j` are priced at one call (24 paid factors) +and under the positive label baseline `x = i`, `y = j` (12 paid factors). +Unit-priced inverse labels therefore enable no cross-register sharing +compression; they change only the re-pricing of the elements `-i` and `-j` +from three calls to one. The bit supplier, the selected result and +`upstream/` are unchanged; the bit side does not bind. + +## Changed hypothesis and full price + +This answers open question 1 of the merged predecessor +`research/q8-central-commutator-pair` +([PR 1822](https://github.com/CrocSwap/integer-mult-bounds/pull/1822)), +extended from its two named endpoints to the complete pair family: + +* **Address group.** `Q8 = {+-1, +-i, +-j, +-k}`; `x = i`, `y = j`, + `z = xyxy = x^2 = y^2 = -1` (central commutator). +* **Alphabet (the changed premise).** Inverse labels `x, x^-1, y, y^-1` at + unit price. Each paid factor is `D_N(g) = I + ([g]+1)N`, `N = u v^T` a + binary rank-one idempotent (`v^T u = 1 mod 2`) on `r = 2` scalar registers: + six `N`, so 24 factors for the inverse alphabet and 12 for the positive + one. The factor set is closed under inversion: + `D_N(g) D_N(g^-1) = I` (checked for all 36 factors across both alphabets), + so the inverse alphabet is a group of units and every word can be priced + symmetrically. +* **Counted roles.** Exactly `r = 2`, both registers arbitrary dirty inputs, + the endpoint restored exactly. Every factor is charged; there are no free + address maps, no COPY/ERASE and no clean ancilla. Free scalar `GL_2(F2)` + basis changes are free and normalized by augmentation; the conjugation + closure `S N S^-1` of the six idempotents is rechecked for all six + `S in GL_2(F2)`, so the generator search covers arbitrary interleaved free + mixing. +* **Uniform identity standard.** Acceptance is equality in every coefficient + of the eight-element group algebra `F2[Q8]`, never a finite-column test. A + word equal to `diag([g1],[g2])` in `M_2(F2[Q8])` is an identity on arbitrary + dirty register inputs. + +Because `i`, `j` are unit-priced in both alphabets and `-i`, `-j` cost one +call instead of three, element lengths are `0,1,1,2,2,2,3,3` +(`1,i,j,-1,k,-k,-i,-j`) in the positive alphabet and `0,1,1,1,1,2,2,2` in +the inverse one; pair bills are at most 6 and at most 4 respectively. + +## Exact result + +Let `min(a,b)` be the exact paid-call minimum of `diag([a],[b])`. Rows index +the first target, columns the second, in the order +`1, -1, i, -i, j, -j, k, -k`. + +```text +inverse labels (min = bill everywhere) + 1 -1 i -i j -j k -k + 1 0 2 1 1 1 1 2 2 + -1 2 4 3 3 3 3 4 4 + i 1 3 2 2 2 2 3 3 + -i 1 3 2 2 2 2 3 3 + j 1 3 2 2 2 2 3 3 + -j 1 3 2 2 2 2 3 3 + k 2 4 3 3 3 3 4 4 + -k 2 4 3 3 3 3 4 4 + +positive labels (min = bill everywhere) + 1 -1 i -i j -j k -k + 1 0 2 1 3 1 3 2 2 + -1 2 4 3 5 3 5 4 4 + i 1 3 2 4 2 4 3 3 + -i 3 5 4 6 4 6 5 5 + j 1 3 2 4 2 4 3 3 + -j 3 5 4 6 4 6 5 5 + k 2 4 3 5 3 5 4 4 + -k 2 4 3 5 3 5 4 4 +``` + +Every minimum equals the sum of the two label-geodesic lengths. The 28 pairs +whose minima differ between the alphabets are exactly the pairs with `-i` or +`-j` as an entry, and each difference is the re-pricing of those elements +(3 to 1 per entry). No pair is compressed below its bill in either alphabet. + +The predecessor's endpoints are reproduced exactly in the positive alphabet: +`diag([z],[z])` and `diag([xy],[yx])` both have minimum 4 +(see `research/q8-central-commutator-pair/CERTIFICATE.json`). + +## Evidence + +`python -I -B research/q8-inverse-label-pair-census/verify.py` (stdlib only, +about 40 s) recomputes everything and compares with `CERTIFICATE.json`: + +* Q8 group laws exhaustively (associativity over all 512 triples, + `x^2 = y^2 = z`, `xy = k`, `yx = -k`, `z` central, `z^2 = 1`, `[x,y] = z`) + plus agreement of the two independently built group tables; +* rank-one idempotent completeness (6 of 9 binary pairs have `v^T u = 1`) and + idempotence; `GL_2(F2)` conjugation closure of the idempotent list; +* generator identities `D_N(g)^2 = D_N(g^2)` and `D_N(g) D_N(g^-1) = I` for + every factor of both alphabets; +* complete BFS layer sizes and ball SHA-256 digests from **two independent + engines** (bitmask convolution from a `(sign, axis)` quaternion table vs + frozenset convolution from explicit Hamilton 4-tuple integer products), + agreeing on every layer and every ball: + `inverse [1, 24, 358, 4104]`, `positive [1, 12, 110, 936, 6945, 48080]`; +* calibration with the merged predecessor: the positive-alphabet layers + through depth 3 are exactly its recorded `[1, 12, 110, 936]`, and its two + endpoint minima are reproduced; +* all 128 attaining words replay coefficientwise in both engines; 372 + single-call omission controls miss their targets; one mutated-target + control fails; known-distance controls (`1` at 0, `diag([i],[1])` at 1, + `diag([z],[1])` at 2); alphabet monotonicity (inverse minimum at most + positive minimum) holds for all 64 pairs. + +The complete shorter-word exclusion is the BFS itself: every word of length +at most 3 (inverse alphabet) or at most 5 (positive alphabet) appears in the +complete ball, and no ball contains a target below the recorded minimum. + +## Scope and what is not claimed + +* **No kappa, no supplier, no frontier change.** This is a scoped census in + one explicit finite alphabet at `r = 2`. It says nothing about the + rational-frame model, other address groups, `r >= 3`, or the multiplication + exponent. The `a < D/E` moment diagnostic does not apply: no candidate + improvement is priced, and the scalar-cost relaxation here is more + optimistic than any physical invoice. +* **Failed compression is not an impossibility theorem.** The statement is + exact only for these two alphabets, `r = 2`, and these 64 targets. Pairs at + `r = 3` with a restored dirty role, larger register counts, or alphabets + mixing positive and inverse labels at other prices remain open. +* **Not a proof-assistant verification.** Two independent Python engines and + finite exhaustions; no Lean or native C++ replay was run. +* No written structural lower bound is claimed: the minima rest on the + complete search, not on a paper proof of the no-compression statement. + +## Reproduce + +```sh +python -I -B research/q8-inverse-label-pair-census/verify.py +python -I -O -B research/q8-inverse-label-pair-census/verify.py +python3.12 -I -B scripts/research_package.py --package research/q8-inverse-label-pair-census --check-only +``` + +Expected: + +```text +PASS_Q8_INVERSE_LABEL_CENSUS pairs=64 inv_layers=[1, 24, 358, 4104] pos_layers=[1, 12, 110, 936, 6945, 48080] compressed_inv=0 compressed_pos=0 omission_controls=372 no_new_kappa +``` + +## Open next questions + +* **Does unit-priced inverse pricing compress the `r = 3` all-central target + `diag([z],[z],[z])` below the positive-label minimum 6?** Why it matters: + it tests whether the pricing change found inert at `r = 2` becomes active + with three central roles. First step: the same BFS with 112 factors (28 + idempotents x 4 labels) to depth 3 plus the invertible-factor + meet-in-the-middle against the depth-3 ball. Blocker: nothing technical; + deliberately not taken here because the concurrent + [PR 2248](https://github.com/CrocSwap/integer-mult-bounds/pull/2248) line + owns the positive-label version of that object. +* **Is there a written structural lower bound proving min = bill for all Q8 + pair targets?** Why it matters: the first-order rank argument of + `research/q8-mixed-three-register-seedcbd5ebc4` covers pairs without `+-1` + entries only. First step: extend its `J_Q^2` coefficient-rank count to + entries killed by the abelianization. Blocker: the `+-1` entries are + invisible mod `J_Q^2`, so a second-order invariant is needed. +* **Do the pair tables extend to `r = 3` with one restored dirty role, or to + `r = 4`?** First step: depth-3 ball digests at `r = 3` with 112 factors and + a memory-capped meet at `r = 4`. Blocker: state-space growth at `r = 4` + (the predecessor recorded the same blocker). + +## Credit and disclosure + +Prepared by **Aaron Wang**, with help from opencode (substantial AI +assistance; no independent human review claimed). Apache-2.0. The model, the +free-mixing normalization and the exact-minimum presentation follow +`research/q8-central-commutator-pair` +([PR 1822](https://github.com/CrocSwap/integer-mult-bounds/pull/1822)) and, +through it, woklerx's `research/bit-dihedral-commutator` +([PR 1443](https://github.com/CrocSwap/integer-mult-bounds/pull/1443)). The +scalar-idempotent register model is eumemic's PR 288 section 1.2; the +register-model lineage credits Ali Romman (PR 468), Gareth Davidson +([PR 1333](https://github.com/CrocSwap/integer-mult-bounds/pull/1333)) and +`research/bit-three-register-lower-bound`. Concurrent work this is distinct +from: [PR 2248](https://github.com/CrocSwap/integer-mult-bounds/pull/2248) +(`r = 3` three-role minima, positive labels) and +[PR 2303](https://github.com/CrocSwap/integer-mult-bounds/pull/2303) +(one- and two-factor words for `diag(i,j,k)` with all-nonidentity labels). +Refreshed `find_overlap.py` passes at 2026-10-15T04:34Z and 15:0xZ (complete +pagination) found no inverse-label Q8 pair object. diff --git a/research/q8-inverse-label-pair-census/SOURCES.json b/research/q8-inverse-label-pair-census/SOURCES.json new file mode 100644 index 0000000000..ac2e39231a --- /dev/null +++ b/research/q8-inverse-label-pair-census/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "research/q8-central-commutator-pair/CERTIFICATE.json", + "usage": "input", + "git_blob": "2c805c49d2133888d0d433f482a5efbab7a8f6c9", + "sha256": "6e902e479aef695c8c7be18a9a5a1e02a6d19568ed695e4506ff16bef0048be5" + } + ] +} diff --git a/research/q8-inverse-label-pair-census/TASK.json b/research/q8-inverse-label-pair-census/TASK.json new file mode 100644 index 0000000000..45fa2ee2da --- /dev/null +++ b/research/q8-inverse-label-pair-census/TASK.json @@ -0,0 +1,69 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "refined", + "actual_scope": "Formal F2[Q8] on exactly two arbitrary dirty registers, unit-priced inverse labels x, x^-1, y, y^-1 (24 paid factors = 6 binary rank-one idempotents x 4 labels), free scalar GL_2(F2) mixing normalized by augmentation: exact paid-call minimum for every one of the 64 ordered diagonal pair targets diag([g1],[g2]), including the predecessor's named endpoints diag([z],[z]) and diag([xy],[yx]). Comparison baseline: the complete 64-pair table under the positive label set {x, y} (12 factors).", + "scope_change_reason": "Pair-collision and overlap survey (2026-10-15T04:34Z, complete pagination): the drawn card's neighbouring Q8 objects are claimed or completed in the last hours (discussion 2243 / PR 2248 resolves diag([z],[z],[z]) and the r=3 three-role positive-label minima; discussion 2300 / PR 2303 checks one- and two-factor words for diag(i,j,k) with all-nonidentity labels). The chosen object is open question 1 of the merged predecessor research/q8-central-commutator-pair (PR 1822): 'Does a label set including the inverses compress any pair target?', extended from its two named endpoints to the complete pair family. The predecessor's open question 2 is deliberately not taken because the concurrent PR 2248 covers it under positive labels.", + "bottleneck_link": "Side result on the bit primitive: a complete finite census of one nonabelian register alphabet under a changed pricing rule. No supplier profile, paid reserve, moment or kappa claim is possible (the bit side does not bind); the a < D/E diagnostic does not apply because no candidate improvement is priced.", + "budget_minutes": 45, + "stop_rule": "Complete BFS to depth 3 for both alphabets plus one invertible-factor meet-in-the-middle for bills 5-6; stop once all 128 pair minima are decided exactly. No pivot beyond this family; the r=3 inverse-label triple is recorded as an open question instead.", + "outcome": "completed", + "evidence": "CERTIFICATE.json (minima, bills, attainment words, layer sizes, ball digests, generator lists) and verify.py (two independent engines, GL_2 conjugation closure, inverse identity, omission and mutated-target controls); written argument in README.md.", + "author": "Aaron Wang", + "ai_assistance": "Substantial AI assistance (opencode); no independent human review claimed.", + "open_questions": [ + { + "question": "Does unit-priced inverse pricing compress the r=3 all-central target diag([z],[z],[z]) below the positive-label minimum 6 of PR 2248?", + "why_it_matters": "It tests whether the changed pricing that this census found inert at r=2 becomes active with three central roles.", + "first_step": "The same BFS with 112 generators (28 idempotents x 4 labels) to depth 3, plus the invertible-factor meet-in-the-middle to exclude lengths 4-5.", + "blocked_by": "Nothing technical; deliberately not taken here to avoid the concurrent PR 2248 object." + }, + { + "question": "Does the inverse-label pair table extend to r=3 with one restored dirty role, or to r=4?", + "why_it_matters": "Tests whether cross-register sharing appears only with extra roles.", + "first_step": "Depth-3 ball digests at r=3 (112 generators) and a memory-capped meet at r=4.", + "blocked_by": "State-space growth at r=4 (the predecessor recorded the same blocker)." + } + ] +} diff --git a/research/q8-inverse-label-pair-census/TASK.md b/research/q8-inverse-label-pair-census/TASK.md new file mode 100644 index 0000000000..06ac8a0e1a --- /dev/null +++ b/research/q8-inverse-label-pair-census/TASK.md @@ -0,0 +1,79 @@ +# Task card (autoresearch.md section 3) + +Task ID / proposed scope key: `bit-new-register-model` (OS draw, nonce +`8fc01583fcbd95feac4206b7bfb68f7d`); refined scope key +`q8-inverse-label-pair-census`. + +Base commit; exact predecessor and dependency heads: base main +`0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`; predecessors +`research/q8-central-commutator-pair` (https://github.com/CrocSwap/integer-mult-bounds/pull/1822, +head `ee736b4b`) and `research/q8-mixed-three-register-seedcbd5ebc4` (both merged +at this base). Concurrent open https://github.com/CrocSwap/integer-mult-bounds/pull/2248 +(head `835bd7b1`) is read for scope only; it is not an input. + +Concrete object and question: in the formal `F2[Q8]` register model at `r = 2` +with **unit-priced inverse labels** `x, x^-1, y, y^-1` (24 paid factors = 6 +binary rank-one idempotents x 4 labels), what is the exact paid-call minimum of +each of the 64 ordered diagonal pair targets `diag([g1],[g2])`? The +predecessor's named endpoints `diag([z],[z])` and `diag([xy],[yx])` are members +of this family. Comparison baseline: the same complete pair table under the +positive label set `{x, y}` (12 factors). + +Scope status: **refined**. Reason: the drawn generic card is saturated and the +pair-collision/overlap checks showed the neighbouring Q8 objects claimed or +completed in the last hours (discussion 1317 October 14 line; discussion 2243 / +https://github.com/CrocSwap/integer-mult-bounds/pull/2248 for the `r = 3` +three-role positive-label minima; discussion 2300 / +https://github.com/CrocSwap/integer-mult-bounds/pull/2303 for `diag(i,j,k)` +two-factor words). The chosen object is open question 1 of the merged +predecessor package's `Open next questions` ("does a label set including the +inverses compress any pair target?"), extended from its two named endpoints to +the complete pair family. The predecessor's open question 2 +(`diag([z],[z],[z])` at `r = 3`) is **not** taken: it is covered under positive +labels by the concurrent PR above. + +Existing restriction being changed (or exact claim being audited): the paid +label set of the predecessor is `{x, y}` with inverses priced as three calls. +This card prices `x^-1, y^-1` at one call each, which changes word-length +pricing and makes the factor set closed under inversion +(`D_N(g)^-1 = D_N(g^-1)`, verified). Counted roles: exactly `r = 2`, both +registers arbitrary dirty inputs, endpoint restored exactly in the formal +group algebra; no COPY/ERASE, no clean ancilla, no free address maps. + +Method; explicit parameter ranges/candidate alphabet: complete BFS of the +formal matrix monoid `M_2(F2[Q8])` to depth 3 (all distinct states), 24 +generators (inverse alphabet) and 12 (positive alphabet); acceptance is +equality in all eight group-algebra coefficients (a uniform identity on +arbitrary dirty inputs), never a finite-column test. Pairs whose direct bill +reaches 5-6 in the positive alphabet are settled by an invertible-factor +meet-in-the-middle (prefix ball <= 2, suffix ball <= 3). Every minimum is +attained by a replayed word. Two independently written engines (bitmask +convolution vs frozenset/Hamilton-quaternion arithmetic) must agree on the +group table, every layer digest and every witness. + +Nearest overlapping PRs and why this adds something: +https://github.com/CrocSwap/integer-mult-bounds/pull/1822 settles only three +endpoints under positive labels; https://github.com/CrocSwap/integer-mult-bounds/pull/2248 +settles `r = 3` triples under positive labels; discussion 2300 / +https://github.com/CrocSwap/integer-mult-bounds/pull/2303 checks one- and +two-factor words at `r = 3` with all-nonidentity labels. No located work gives +the `r = 2` pair table under inverse pricing, and no located work completes the +64-pair positive-label table. + +Optimistic full cost budget; required observable improvement: none — this is a +complete local census in the unit-cost formal call model, no supplier profile, +no paid reserve, no kappa. The `a < D/E` moment diagnostic does not apply (no +candidate improvement is priced; the scalar-cost relaxation here is more +optimistic than any physical invoice). + +Success evidence; falsification test; time/compute cap: exact minima for all +64 pairs in both alphabets with attainment words and complete exclusion of all +shorter words (layer digests + MITM receipt); falsifier is any word shorter +than a recorded minimum (engine disagreement or an omission/mutation control +passing would falsify the harness); 45-minute budget, stdlib Python only. + +Predecessor authors; intended artifact and reproduction command: eumemic +(PR 288 section 1.2 model), woklerx (`research/bit-dihedral-commutator`), Aaron +Wang / navinor (`research/q8-central-commutator-pair`); artifact +`research/q8-inverse-label-pair-census/`; reproduction: +`python3.12 -I -B research/q8-inverse-label-pair-census/verify.py`. diff --git a/research/q8-inverse-label-pair-census/VERIFY.json b/research/q8-inverse-label-pair-census/VERIFY.json new file mode 100644 index 0000000000..4fd4f96398 --- /dev/null +++ b/research/q8-inverse-label-pair-census/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/q8-central-commutator-pair/CERTIFICATE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Q8 group laws and two independent group tables, rank-one idempotent completeness, D_N(g)^2 = D_N(g^2) and D_N(g) D_N(g^-1) = I, GL_2(F2) conjugation closure, complete BFS layer digests to depth 3 (inverse labels) and depth 5 (positive labels) in M_2(F2[Q8]) from two independent engines, predecessor calibration (layers [1,12,110,936] and the two endpoint minima), all 128 attaining words replayed coefficientwise, 372 omission controls, mutated-target failure control, known-distance controls, alphabet monotonicity, and certificate equality." + } + ] +} diff --git a/research/q8-inverse-label-pair-census/verify.py b/research/q8-inverse-label-pair-census/verify.py new file mode 100644 index 0000000000..04acd1a733 --- /dev/null +++ b/research/q8-inverse-label-pair-census/verify.py @@ -0,0 +1,575 @@ +#!/usr/bin/env python3 +"""Exact paid-call minima for all ordered Q8 pair targets at r = 2, under +unit-priced inverse labels and under the positive-label baseline. + +Formal F2[Q8] register model (eumemic PR 288 section 1.2, as fixed by +research/bit-dihedral-commutator and research/q8-central-commutator-pair): + + * r = 2 scalar registers, both arbitrary dirty inputs, endpoint restored + exactly as a formal group-algebra identity in M_2(F2[Q8]); + * one paid call is D_N(g) = I + ([g] + [1]) N with N = u v^T a binary + rank-one idempotent (v^T u = 1 mod 2) and g a paid label; + * inverse alphabet: labels x = i, x^-1 = -i, y = j, y^-1 = -j (24 factors); + positive alphabet: labels x = i, y = j (12 factors); + * free scalar GL_2(F2) basis changes are free and normalized by augmentation + (closure rechecked below), so the generator search covers arbitrary + interleaved free mixing; + * acceptance is equality in every coefficient of the eight-element group + algebra, never a finite-column test. + +Two independently written engines (A: bitmask convolution from a +(sign, axis) quaternion table; B: frozenset convolution from explicit +Hamilton 4-tuple quaternion products) recompute the complete BFS layers and +every witness. Stdlib only. Prepared by Aaron Wang, with help from opencode. +""" + +import hashlib +import json +import os +import sys + +HERE = os.path.dirname(os.path.abspath(__file__)) +CERT_PATH = os.path.join(HERE, "CERTIFICATE.json") +PRED_CERT = os.path.normpath( + os.path.join(HERE, os.pardir, "q8-central-commutator-pair", "CERTIFICATE.json") +) + +# Basis indices: 0:+1 1:-1 2:+i 3:-i 4:+j 5:-j 6:+k 7:-k +ELEMENTS = ["+1", "-1", "+i", "-i", "+j", "-j", "+k", "-k"] +IDX = {name: i for i, name in enumerate(ELEMENTS)} + + +def elem_inv(g): + # +-1 are self-inverse; +-i, +-j, +-k swap with their negatives. + return (0, 1, 3, 2, 5, 4, 7, 6)[g] + + +# ---------------------------------------------------------------- engine A +# Group product from (sign, axis) quaternion-unit arithmetic. +_AXIS = {0: (1, 0), 1: (-1, 0), 2: (1, 1), 3: (-1, 1), + 4: (1, 2), 5: (-1, 2), 6: (1, 3), 7: (-1, 3)} +# UNIT[a][b] = (sign, axis) of quaternion unit product, axes 0=1 1=i 2=j 3=k. +_UNIT = [ + [(1, 0), (1, 1), (1, 2), (1, 3)], + [(1, 1), (-1, 0), (1, 3), (-1, 2)], + [(1, 2), (-1, 3), (-1, 0), (1, 1)], + [(1, 3), (1, 2), (-1, 1), (-1, 0)], +] + + +def _pack_sign_axis(sgn, ax): + return 2 * ax + (0 if sgn > 0 else 1) + + +GROUP_A = [[0] * 8 for _ in range(8)] +for _g in range(8): + for _h in range(8): + s1, a1 = _AXIS[_g] + s2, a2 = _AXIS[_h] + s, a = _UNIT[a1][a2] + GROUP_A[_g][_h] = _pack_sign_axis(s1 * s2 * s, a) + + +def _ring_tables(group): + mul = [[0] * 256 for _ in range(256)] + for m1 in range(256): + for m2 in range(256): + acc = 0 + x = m1 + while x: + b1 = x & -x + i1 = b1.bit_length() - 1 + y = m2 + while y: + b2 = y & -y + i2 = b2.bit_length() - 1 + acc ^= 1 << group[i1][i2] + y ^= b2 + x ^= b1 + mul[m1][m2] = acc + return mul + + +MUL_A = _ring_tables(GROUP_A) + + +# ---------------------------------------------------------------- engine B +# Group product from explicit Hamilton 4-tuple integer quaternion products. +_H = {0: (1, 0, 0, 0), 1: (-1, 0, 0, 0), 2: (0, 1, 0, 0), 3: (0, -1, 0, 0), + 4: (0, 0, 1, 0), 5: (0, 0, -1, 0), 6: (0, 0, 0, 1), 7: (0, 0, 0, -1)} +_HIDX = {v: k for k, v in _H.items()} + + +def _ham(u, v): + a0, a1, a2, a3 = u + b0, b1, b2, b3 = v + return ( + a0 * b0 - a1 * b1 - a2 * b2 - a3 * b3, + a0 * b1 + a1 * b0 + a2 * b3 - a3 * b2, + a0 * b2 - a1 * b3 + a2 * b0 + a3 * b1, + a0 * b3 + a1 * b2 - a2 * b1 + a3 * b0, + ) + + +GROUP_B = [[_HIDX[_ham(_H[g], _H[h])] for h in range(8)] for g in range(8)] + + +def _ring_mul_b(m1, m2): + acc = 0 + x = m1 + while x: + b1 = x & -x + i1 = b1.bit_length() - 1 + y = m2 + while y: + b2 = y & -y + i2 = b2.bit_length() - 1 + acc ^= 1 << GROUP_B[i1][i2] + y ^= b2 + x ^= b1 + return acc + + +# ------------------------------------------------------------- matrices r=2 +# State: tuple (m00, m01, m10, m11) of 8-bit ring masks. Packed to 32 bits. + +IDENT = (1, 0, 0, 1) + + +def pack(M): + return M[0] | (M[1] << 8) | (M[2] << 16) | (M[3] << 24) + + +def unpack(p): + return (p & 255, (p >> 8) & 255, (p >> 16) & 255, (p >> 24) & 255) + + +def mat_mul(P, Q, mul): + a00, a01, a10, a11 = P + b00, b01, b10, b11 = Q + return ( + mul[a00][b00] ^ mul[a01][b10], + mul[a00][b01] ^ mul[a01][b11], + mul[a10][b00] ^ mul[a11][b10], + mul[a10][b01] ^ mul[a11][b11], + ) + + +def apply_right(M, g, u, v, mul): + """M <- M * (I + ([g]+1) u v^T); u, v are 2-bit nonzero binary masks.""" + m00, m01, m10, m11 = M + mu0 = (m00 if u & 1 else 0) ^ (m01 if u & 2 else 0) + mu1 = (m10 if u & 1 else 0) ^ (m11 if u & 2 else 0) + a = (1 << g) | 1 + # Noncommutative ring: M*(I + aN) = M + ((M a) N); entries of M are + # right-multiplied by a = [g]+1 (matrix-product order matters in F2[Q8]). + t0 = mul[mu0][a] + t1 = mul[mu1][a] + return ( + m00 ^ (t0 if v & 1 else 0), + m01 ^ (t0 if v & 2 else 0), + m10 ^ (t1 if v & 1 else 0), + m11 ^ (t1 if v & 2 else 0), + ) + + +def apply_right_b(M, g, u, v): + m00, m01, m10, m11 = M + mu0 = _xorb((m00 if u & 1 else 0), (m01 if u & 2 else 0)) + mu1 = _xorb((m10 if u & 1 else 0), (m11 if u & 2 else 0)) + a = (1 << g) | 1 + t0 = _ring_mul_b(mu0, a) + t1 = _ring_mul_b(mu1, a) + return ( + _xorb(m00, t0 if v & 1 else 0), + _xorb(m01, t0 if v & 2 else 0), + _xorb(m10, t1 if v & 1 else 0), + _xorb(m11, t1 if v & 2 else 0), + ) + + +def _xorb(*masks): + acc = 0 + for m in masks: + acc ^= m + return acc + + +def mat_mul_b(P, Q): + a00, a01, a10, a11 = P + b00, b01, b10, b11 = Q + return ( + _xorb(_ring_mul_b(a00, b00), _ring_mul_b(a01, b10)), + _xorb(_ring_mul_b(a00, b01), _ring_mul_b(a01, b11)), + _xorb(_ring_mul_b(a10, b00), _ring_mul_b(a11, b10)), + _xorb(_ring_mul_b(a10, b01), _ring_mul_b(a11, b11)), + ) + + +def replay(word, mul): + M = IDENT + for (g, u, v) in word: + M = apply_right(M, g, u, v, mul) + return M + + +def replay_b(word): + M = IDENT + for (g, u, v) in word: + M = apply_right_b(M, g, u, v) + return M + + +# ------------------------------------------------------------- idempotents +def idempotents(): + out = [] + for u in (1, 2, 3): + for v in (1, 2, 3): + if bin(u & v).count("1") % 2 == 1: + out.append((u, v)) + return out + + +N_LIST = idempotents() # 6 entries + + +def generators(labels): + return [(g, u, v) for g in labels for (u, v) in N_LIST] + + +# ------------------------------------------------------------------- BFS +def bfs(gens, cap, apply_fn): + dist = {pack(IDENT): 0} + parent = {} + frontier = [IDENT] + layers = [1] + for d in range(1, cap + 1): + nxt = [] + for M in frontier: + pm = pack(M) + for gen in gens: + M2 = apply_fn(M, *gen) + p = pack(M2) + if p not in dist: + dist[p] = d + parent[p] = (pm, gen) + nxt.append(M2) + layers.append(len(nxt)) + frontier = nxt + if not frontier: + break + return layers, dist, parent + + +def shortest_word(p, parent): + word = [] + while p in parent: + prev, gen = parent[p] + word.append(gen) + p = prev + word.reverse() + return word + + +def ball_digest(dist): + h = hashlib.sha256() + for p in sorted(dist): + h.update(p.to_bytes(4, "little")) + h.update(bytes([dist[p]])) + return h.hexdigest() + + +# --------------------------------------------------------------- targets +def target(g1, g2): + return (1 << g1, 0, 0, 1 << g2) + + +def geodesic(labels): + """Shortest label word for each group element under the label set.""" + words = {0: []} + frontier = [0] + while frontier: + nxt = [] + for h in frontier: + for lab in labels: + g = GROUP_A[h][lab] + if g not in words: + words[g] = words[h] + [lab] + nxt.append(g) + frontier = nxt + return words + + +def direct_word(g1, g2, words): + return ([(g, 1, 1) for g in words[g1]] + [(g, 2, 2) for g in words[g2]]) + + +# ---------------------------------------------------------------- controls +def gl2(): + mats = [] + for a in (0, 1): + for b in (0, 1): + for c in (0, 1): + for d in (0, 1): + if (a * d - b * c) % 2 == 1: + mats.append((a, b, c, d)) + return mats + + +def conj_n(S, u, v): + """S N S^-1 over F2 for N = u v^T, returned as (u', v') bit masks.""" + a, b, c, d = S + det = (a * d - b * c) % 2 + if det != 1: + raise ValueError("not invertible") + Sinv = (d, b, c, a) # over F2, inverse of [[a,b],[c,d]] with det 1 + uv = (1 if u & 1 else 0, 1 if u & 2 else 0) + vv = (1 if v & 1 else 0, 1 if v & 2 else 0) + u1 = ((a * uv[0] + b * uv[1]) % 2, (c * uv[0] + d * uv[1]) % 2) + # N' = S N S^-1 = (S u) (S^-T v)^T + w1 = ((Sinv[0] * vv[0] + Sinv[2] * vv[1]) % 2, + (Sinv[1] * vv[0] + Sinv[3] * vv[1]) % 2) + up = (1 if u1[0] else 0) | (2 if u1[1] else 0) + vp = (1 if w1[0] else 0) | (2 if w1[1] else 0) + return up, vp + + +def main(): + write_mode = "--write" in sys.argv + checks = [] + + def ck(name, cond): + checks.append((name, bool(cond))) + if not cond: + print("FAIL:", name) + + # 1. group tables agree; group laws + ck("engine_tables_agree", GROUP_A == GROUP_B) + assoc = all( + GROUP_A[GROUP_A[g][h]][k] == GROUP_A[g][GROUP_A[h][k]] + for g in range(8) for h in range(8) for k in range(8) + ) + ck("associativity_512_triples", assoc) + x, y, z = IDX["+i"], IDX["+j"], IDX["-1"] + ck("x_squared_is_z", GROUP_A[x][x] == z) + ck("y_squared_is_z", GROUP_A[y][y] == z) + ck("xy_is_plus_k", GROUP_A[x][y] == IDX["+k"]) + ck("yx_is_minus_k", GROUP_A[y][x] == IDX["-k"]) + ck("z_central", all(GROUP_A[z][g] == GROUP_A[g][z] for g in range(8))) + ck("z_squared_is_one", GROUP_A[z][z] == 0) + xyxy = GROUP_A[GROUP_A[x][y]][GROUP_A[x][y]] + ck("commutator_xyxy_is_z", xyxy == z) + ck("inverses", all(GROUP_A[g][elem_inv(g)] == 0 and GROUP_A[elem_inv(g)][g] == 0 + for g in range(8))) + + # 2. idempotents + ck("six_rank_one_idempotents", len(N_LIST) == 6) + ok = True + for (u, v) in N_LIST: + # N^2 = u (v^T u) v^T = N when v^T u = 1 + if bin(u & v).count("1") % 2 != 1: + ok = False + ck("idempotents_vTu_one", ok) + total_pairs = sum(1 for u in (1, 2, 3) for v in (1, 2, 3)) + ck("idempotent_completeness_9_pairs", total_pairs == 9 and len(N_LIST) == 6) + + # 3. generator identities (both alphabets, engine B) + inv_labels = [IDX["+i"], IDX["-i"], IDX["+j"], IDX["-j"]] + pos_labels = [IDX["+i"], IDX["+j"]] + gen_ok = True + for labels in (inv_labels, pos_labels): + for gen in generators(labels): + g, u, v = gen + D = apply_right_b(IDENT, g, u, v) + Dg2 = apply_right_b(IDENT, GROUP_A[g][g], u, v) + if mat_mul_b(D, D) != Dg2: + gen_ok = False + Dinv = apply_right_b(IDENT, elem_inv(g), u, v) + if mat_mul_b(D, Dinv) != IDENT or mat_mul_b(Dinv, D) != IDENT: + gen_ok = False + ck("generator_square_and_inverse_identities", gen_ok) + + # 4. GL_2 conjugation closure of the idempotent list + gl = gl2() + ck("gl2_order_6", len(gl) == 6) + nset = set(N_LIST) + clo = all(conj_n(S, u, v) in nset for S in gl for (u, v) in N_LIST) + ck("gl2_conjugation_closure", clo) + + # 5. complete BFS, both engines + caps = {"inverse": 3, "positive": 5} + alphabets = {"inverse": inv_labels, "positive": pos_labels} + data = {} + engines_agree = True + for name, labels in alphabets.items(): + gens = generators(labels) + layersA, distA, parentA = bfs(gens, caps[name], lambda M, g, u, v: apply_right(M, g, u, v, MUL_A)) + layersB, distB, _ = bfs(gens, caps[name], apply_right_b) + if layersA != layersB or distA.keys() != distB.keys(): + engines_agree = False + data[name] = {"labels": labels, "gens": gens, + "layers": layersA, "dist": distA, "parent": parentA, + "digest": ball_digest(distA), + "digest_b": ball_digest(distB), + "words": geodesic(labels)} + ck("engines_agree_on_all_layers_and_balls", engines_agree) + + # 6. calibration with the merged predecessor (positive alphabet, r = 2) + pred = json.load(open(PRED_CERT, encoding="utf-8")) + ck("pred_layer_calibration_1_12_110_936", + data["positive"]["layers"][:4] == [1, 12, 110, 936] == pred["r2_layers"]) + + # 7. minima for all 64 ordered pairs, both alphabets + records = {} + replay_ok = True + omission_total = 0 + omission_ok = True + mutated_ok = True + known_ok = True + for g1 in range(8): + for g2 in range(8): + T = target(g1, g2) + pk = pack(T) + entry = {} + for name in ("inverse", "positive"): + D = data[name] + bill = len(D["words"][g1]) + len(D["words"][g2]) + word = direct_word(g1, g2, D["words"]) + got = replay(word, MUL_A) + if got != T or replay_b(word) != T: + replay_ok = False + d = D["dist"].get(pk) + if d is not None and d <= bill: + minimum = d + witness = shortest_word(pk, D["parent"]) + proven = ("complete BFS to depth %d finds distance %d, at or " + "below the direct bill %d" % (caps[name], d, bill)) + else: + minimum = bill + witness = word + proven = ("complete BFS to depth %d excludes every word of " + "length <= %d; the direct word attains %d" + % (caps[name], caps[name], bill)) + entry[name] = { + "bill": bill, + "minimum": minimum, + "word": [[g, u, v] for (g, u, v) in witness], + "proven": proven, + } + # omission controls: delete each call of the attaining word + for i in range(len(witness)): + if len(witness) < 2: + continue + cut = witness[:i] + witness[i + 1:] + omission_total += 1 + if replay(cut, MUL_A) == T: + omission_ok = False + # monotonicity: inverse minimum <= positive minimum + if entry["inverse"]["minimum"] > entry["positive"]["minimum"]: + known_ok = False + records["diag_%s_%s" % (ELEMENTS[g1].replace("+", "p").replace("-", "m"), + ELEMENTS[g2].replace("+", "p").replace("-", "m"))] = entry + + ck("all_attaining_words_replay", replay_ok) + ck("omission_controls", omission_ok and omission_total > 0) + ck("alphabet_monotonicity", known_ok) + + # mutated-target failure control: flip one coefficient of diag([+i],[+j]) + T = target(IDX["+i"], IDX["+j"]) + word = direct_word(IDX["+i"], IDX["+j"], data["positive"]["words"]) + bad = (T[0] ^ 1, T[1], T[2], T[3]) + if replay(word, MUL_A) == bad: + mutated_ok = False + ck("mutated_target_rejected", mutated_ok) + + # known-distance controls + kd = data["inverse"]["dist"] + kp = data["positive"]["dist"] + ck("known_distance_identity_0", kd.get(pack(IDENT)) == 0 and kp.get(pack(IDENT)) == 0) + ck("known_distance_diag_i_e_1", + kd.get(pack(target(IDX["+i"], 0))) == 1 and kp.get(pack(target(IDX["+i"], 0))) == 1) + ck("known_distance_diag_z_e_2", + kd.get(pack(target(IDX["-1"], 0))) == 2 and kp.get(pack(target(IDX["-1"], 0))) == 2) + + # predecessor endpoint minima reproduced in the positive alphabet + pz = records["diag_m1_m1"]["positive"]["minimum"] + pxy = records["diag_pk_mk"]["positive"]["minimum"] + ck("pred_endpoint_diag_z_z_is_4", pz == pred["endpoints"]["diag_z_z_r2"]["minimum"] == 4) + ck("pred_endpoint_diag_xy_yx_is_4", pxy == pred["endpoints"]["diag_xy_yx_r2"]["minimum"] == 4) + + # summary counts + comp_inv = sorted(k for k, e in records.items() + if e["inverse"]["minimum"] < e["inverse"]["bill"]) + comp_pos = sorted(k for k, e in records.items() + if e["positive"]["minimum"] < e["positive"]["bill"]) + + cert = { + "status": "PASS_Q8_INVERSE_LABEL_CENSUS", + "new_kappa": False, + "model": { + "group": "Q8", "registers": 2, + "paid_call": "I + ([g]+1) N, N = u v^T binary rank-one idempotent", + "inverse_labels": [ELEMENTS[g] for g in inv_labels], + "positive_labels": [ELEMENTS[g] for g in pos_labels], + "free_mixing": "GL_2(F2), normalized by augmentation", + "acceptance": "coefficientwise equality in F2[Q8]", + }, + "group_table": [ELEMENTS[g] for g in range(8)], + "group_table_sha256": hashlib.sha256( + bytes(GROUP_A[g][h] for g in range(8) for h in range(8))).hexdigest(), + "idempotents_uv": [[u, v] for (u, v) in N_LIST], + "gl2_order": 6, + "inverse_generators": 24, + "positive_generators": 12, + "inverse_layers": data["inverse"]["layers"], + "inverse_ball_sha256": data["inverse"]["digest"], + "inverse_ball_sha256_engine_b": data["inverse"]["digest_b"], + "positive_layers": data["positive"]["layers"], + "positive_ball_sha256": data["positive"]["digest"], + "positive_ball_sha256_engine_b": data["positive"]["digest_b"], + "independent_engine_b": True, + "predecessor_calibration": { + "source": "research/q8-central-commutator-pair/CERTIFICATE.json", + "r2_layers": pred["r2_layers"], + "diag_z_z_r2_minimum": pred["endpoints"]["diag_z_z_r2"]["minimum"], + "diag_xy_yx_r2_minimum": pred["endpoints"]["diag_xy_yx_r2"]["minimum"], + }, + "endpoints": records, + "compressed_pairs_inverse": comp_inv, + "compressed_pairs_positive": comp_pos, + "omission_controls": omission_total, + "controls": sum(1 for _, ok in checks if ok), + "checks_failed": [n for n, ok in checks if not ok], + } + + if write_mode: + with open(CERT_PATH, "w", encoding="utf-8") as f: + json.dump(cert, f, indent=1, sort_keys=True) + print("WROTE", CERT_PATH) + else: + stored = json.load(open(CERT_PATH, encoding="utf-8")) + if stored != cert: + diffs = [k for k in set(stored) | set(cert) if stored.get(k) != cert.get(k)] + print("FAIL: certificate mismatch in", diffs) + checks.append(("certificate_equality", False)) + else: + checks.append(("certificate_equality", True)) + + failed = [n for n, ok in checks if not ok] + if failed: + print("FAILED_CHECKS", failed) + raise SystemExit(1) + print( + "PASS_Q8_INVERSE_LABEL_CENSUS", + "pairs=64", + "inv_layers=%s" % (data["inverse"]["layers"],), + "pos_layers=%s" % (data["positive"]["layers"],), + "compressed_inv=%d" % len(comp_inv), + "compressed_pos=%d" % len(comp_pos), + "omission_controls=%d" % omission_total, + "no_new_kappa", + ) + + +if __name__ == "__main__": + main()