From 84c19218bca3b2c963e98a545481f32d78e77b17 Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 11:47:49 +0700 Subject: [PATCH] =?UTF-8?q?Independently=20replay=20#4534's=20noncommuting?= =?UTF-8?q?=20p16=20identity=20in=20the=20free=20algebra:=20all=201,024=20?= =?UTF-8?q?entries,=20chronology-sensitive=20(no=20new=20=CE=BA)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 5.5 --- .../free-controller-replay/.gitattributes | 1 + .../FREE-CERTIFICATE-4534.json | 2664 +++++++++++++++++ research/free-controller-replay/README.md | 62 + research/free-controller-replay/SOURCES.json | 24 + research/free-controller-replay/TASK.json | 100 + research/free-controller-replay/VERIFY.json | 20 + research/free-controller-replay/verify.py | 141 + 7 files changed, 3012 insertions(+) create mode 100644 research/free-controller-replay/.gitattributes create mode 100644 research/free-controller-replay/FREE-CERTIFICATE-4534.json create mode 100644 research/free-controller-replay/README.md create mode 100644 research/free-controller-replay/SOURCES.json create mode 100644 research/free-controller-replay/TASK.json create mode 100644 research/free-controller-replay/VERIFY.json create mode 100644 research/free-controller-replay/verify.py diff --git a/research/free-controller-replay/.gitattributes b/research/free-controller-replay/.gitattributes new file mode 100644 index 0000000000..d7808a79e3 --- /dev/null +++ b/research/free-controller-replay/.gitattributes @@ -0,0 +1 @@ +FREE-CERTIFICATE-4534.json -text diff --git a/research/free-controller-replay/FREE-CERTIFICATE-4534.json b/research/free-controller-replay/FREE-CERTIFICATE-4534.json new file mode 100644 index 0000000000..9ecbdcb8bd --- /dev/null +++ b/research/free-controller-replay/FREE-CERTIFICATE-4534.json @@ -0,0 +1,2664 @@ +{ + "diagonal": [ + [ + -1, + [ + 1, + 0 + ] + ], + [ + -1, + [ + 3, + 1, + 0 + ] + ], + [ + -1, + [ + 5, + 3, + 1, + 0 + ] + ], + [ + -1, + [ + 7, + 5, + 3, + 1, + 0 + ] + ], + [ + -1, + [ + 9, + 7, + 5, + 3, + 1, + 0 + ] + ], + [ + -1, + [ + 11, + 9, + 7, + 5, + 3, + 1, + 0 + ] + ], + [ + -1, + [ + 13, + 11, + 9, + 7, + 5, + 3, + 1, + 0 + ] + ], + [ + -1, + [ + 32, + 31 + ] + ], + [ + -1, + [ + 32, + 31, + 29 + ] + ], + [ + -1, + [ + 32, + 31, + 29, + 27 + ] + ], + [ + -1, + [ + 32, + 31, + 29, + 27, + 25 + ] + ], + [ + -1, + [ + 32, + 31, + 29, + 27, + 25, + 23 + ] + ], + [ + -1, + [ + 32, + 31, + 29, + 27, + 25, + 23, + 21 + ] + ], + [ + -1, + [ + 32, + 31, + 29, + 27, + 25, + 23, + 21, + 19 + ] + ], + [ + -1, + [ + 32, + 31, + 29, + 27, + 25, + 23, + 21, + 19, + 17 + ] + ], + [ + -1, + [ + 32, + 31, + 29, + 27, + 25, + 23, + 21, + 19, + 17, + 15, + 13, + 11, + 9, + 7, + 5, + 3, + 1, + 0 + ] + ], + [ + 1, + [ + 1, + 0 + ] + ], + [ + 1, + [ + 3, + 1, + 0 + ] + ], + [ + 1, + [ + 5, + 3, + 1, + 0 + ] + ], + [ + 1, + [ + 7, + 5, + 3, + 1, + 0 + ] + ], + [ + 1, + [ + 9, + 7, + 5, + 3, + 1, + 0 + ] + ], + [ + 1, + [ + 11, + 9, + 7, + 5, + 3, + 1, + 0 + ] + ], + [ + 1, + [ + 13, + 11, + 9, + 7, + 5, + 3, + 1, + 0 + ] + ], + [ + 1, + [ + 32, + 31 + ] + ], + [ + 1, + [ + 32, + 31, + 29 + ] + ], + [ + 1, + [ + 32, + 31, + 29, + 27 + ] + ], + [ + 1, + [ + 32, + 31, + 29, + 27, + 25 + ] + ], + [ + 1, + [ + 32, + 31, + 29, + 27, + 25, + 23 + ] + ], + [ + 1, + [ + 32, + 31, + 29, + 27, + 25, + 23, + 21 + ] + ], + [ + 1, + [ + 32, + 31, + 29, + 27, + 25, + 23, + 21, + 19 + ] + ], + [ + 1, + [ + 32, + 31, + 29, + 27, + 25, + 23, + 21, + 19, + 17 + ] + ], + [ + 1, + [ + 32, + 31, + 29, + 27, + 25, + 23, + 21, + 19, + 17, + 15, + 13, + 11, + 9, + 7, + 5, + 3, + 1, + 0 + ] + ] + ], + "paid_idle": [ + [ + 1, + 0 + ], + [], + [ + 3, + 1, + 0 + ], + [], + [ + 5, + 3, + 1, + 0 + ], + [], + [ + 7, + 5, + 3, + 1, + 0 + ], + [], + [ + 9, + 7, + 5, + 3, + 1, + 0 + ], + [], + [ + 11, + 9, + 7, + 5, + 3, + 1, + 0 + ], + [], + [ + 13, + 11, + 9, + 7, + 5, + 3, + 1, + 0 + ], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [ + 32, + 31, + 29, + 27, + 25, + 23, + 21, + 19, + 17 + ], + [ + 32, + 31, + 29, + 27, + 25, + 23, + 21, + 19 + ], + [ + 32, + 31, + 29, + 27, + 25, + 23, + 21 + ], + [ + 32, + 31, + 29, + 27, + 25, + 23 + ], + [ + 32, + 31, + 29, + 27, + 25 + ], + [ + 32, + 31, + 29, + 27 + ], + [ + 32, + 31, + 29 + ], + [ + 32, + 31 + ] + ], + "left": [ + [ + "1", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "1", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "1", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ] + ], + "right": [ + [ + "1", + "-1", + "1", + "-1", + "1", + "-1", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1", + "-1", + "1", + "-1", + "1", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "1", + "-1", + "1", + "-1", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "1", + "-1", + "1", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "1", + "-1", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "1", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ] + ] +} \ No newline at end of file diff --git a/research/free-controller-replay/README.md b/research/free-controller-replay/README.md new file mode 100644 index 0000000000..986725486f --- /dev/null +++ b/research/free-controller-replay/README.md @@ -0,0 +1,62 @@ +# Independent free-algebra replay of #4534's noncommuting p16 identity + +**Claim type:** an independent exact replay by separately written code. **No new κ.** It covers the +noncommuting-stage theorem in Dugongue's [#4534](https://github.com/CrocSwap/integer-mult-bounds/pull/4534) +(head `90505ab1`, `research/frame-aware-native/noncommuting-controller`). That theorem says #4470's p16 +controller stays exactly diagonalizable when the stage operators `D_s` need not commute with each other, as +long as each commutes with the central query `Q`. This extends my commutative Laurent replay in #4516 to +ordered words. + +## What is checked + +The inputs are #4470's `CONTROLLER.json` on main and #4534's `FREE-CERTIFICATE.json`, vendored with its +SHA256 pinned. Each of the 32 lines is replayed with coefficients in the free algebra `ℚ⟨d_s⟩[q, q^{−1}]`, +with `q` central. A monomial is a pair: a `q` exponent and an **ordered** tuple of stage letters, and a +later operator is prepended on the left. + +| Event | Effect | +| --- | --- | +| `LOCAL` | the shear (`y += q^{−1}x`, or `y −= q·x` backward), then left-multiplication of both lines by `d_stage` | +| `QUERY_SHEAR` | the shear alone | +| `IDLE` on ascending stages `s_1 < … < s_k` | left-multiplication by `d_{s_k}⋯d_{s_1}` | +| `ADD`, `SIGNED_SWAP` | literal | + +Results: + +1. **The identity.** `L·W·R = diag(q^{ε_i} d_{w_i})` holds in **all 1,024 matrix entries**, coefficient by + coefficient over ordered words, with the certificate's rational `L`, `R` and diagonal. +2. **Chronology matters.** Reversing every idle word breaks 212 entries. A commutative replay could not + detect this. +3. **Structure.** There are 16 central exponents `+1` and 16 `−1`. The longest word is + `G = (32, 31, 29, …, 3, 1, 0)`, and the other 15 nonempty words are each a contiguous prefix or suffix + of `G`. +4. **The boundaries.** `L` and `R` are invertible, and they and their inverses have only dyadic entries, + consistent with #4534's dyadic scalar programs. + +## Not covered + +- #4534's monomial adapters, owned-response retiming and lazy-response tools. +- The physical realization of any noncommuting `D_s`. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/free-controller-replay --check-only +python3.12 -B scripts/research_package.py --package research/free-controller-replay +``` + +The verifier prints `PASS_FREE_CONTROLLER_REPLAY` in about a second, using only the standard library. + +## Open next questions + +1. **#4534's open question 2: an all-`p` free-algebra identity.** + - *First step:* replay the same constructor at `p = 4, 8, 12` in the free algebra, and look for the + inductive pattern of `L` and `R`. + +## Credit + +- The theorem and the certificate are Dugongue's (#4534). +- The p16 word is Cinna Davis's (1337isnot1337, #4470). + +Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. +Apache-2.0. diff --git a/research/free-controller-replay/SOURCES.json b/research/free-controller-replay/SOURCES.json new file mode 100644 index 0000000000..3df53e9984 --- /dev/null +++ b/research/free-controller-replay/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40", + "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/joint-helper-lattice/CONTROLLER.json", + "usage": "input", + "git_blob": "49a2f0675819f9deeea27ed77be2c2b6ff2e87e5", + "sha256": "1f5d6aa267e4e66048818714b5d3b5eae17a58abe91d15deeaa34574f7391a5f" + } + ] +} diff --git a/research/free-controller-replay/TASK.json b/research/free-controller-replay/TASK.json new file mode 100644 index 0000000000..69b7fa5375 --- /dev/null +++ b/research/free-controller-replay/TASK.json @@ -0,0 +1,100 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 7, + "base_commit": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc", + "original_card": { + "id": "independent-moment", + "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/staged544-mixed-fourth-entry/README.md", + "research/staged-fourth-mixture-ceiling/README.md", + "research/r437-two-window-carrier/README.md" + ], + "methods": [ + "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.", + "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Calling an aggregate histogram or source archive an independently accepted physical supplier." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering", + "4088", + "4091", + "4067", + "staged544-mixed-fourth-entry", + "staged-fourth-mixture-ceiling", + "r437-two-window-carrier" + ], + "existing_checks": [ + { + "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.", + "evidence": "research/staged-fourth-mixture-ceiling/README.md", + "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.", + "status": "author-checked", + "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.", + "evidence": "research/r437-two-window-carrier/README.md", + "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.", + "status": "author-checked", + "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Independent free-algebra replay of #4534's noncommuting p16 identity.", + "scope_change_reason": "Extends my commutative replay (#4516) to the new noncommuting claim.", + "bottleneck_link": "Independent coverage of a native-construction interface for the kappa ~0.00302 line.", + "budget_minutes": 30, + "stop_rule": "Stop at the p16 identity.", + "outcome": "completed", + "evidence": "0/1024 mismatches; reversed idles 212 mismatches; G and 15 prefix/suffix words; L,R invertible and dyadic.", + "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance", + "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance; no independent human review.", + "open_questions": [ + { + "question": "All-p free-algebra identity (#4534 open question 2).", + "why_it_matters": "Removes the fixed-p16 restriction.", + "first_step": "Replay the constructor at p=4,8,12 and find the inductive pattern of L and R.", + "blocked_by": "None." + } + ] +} diff --git a/research/free-controller-replay/VERIFY.json b/research/free-controller-replay/VERIFY.json new file mode 100644 index 0000000000..49fc7d6ea5 --- /dev/null +++ b/research/free-controller-replay/VERIFY.json @@ -0,0 +1,20 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/joint-helper-lattice/CONTROLLER.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Free-algebra replay of #4470's p16 controller against #4534's certificate: L W R = diag(q^e d_w) in all 1,024 entries over ordered words, reversed idles rejected (212 mismatches), 16/16 exponents, prefix/suffix words of G, L and R invertible and dyadic with dyadic inverses." + } + ] +} diff --git a/research/free-controller-replay/verify.py b/research/free-controller-replay/verify.py new file mode 100644 index 0000000000..29d3b8a42a --- /dev/null +++ b/research/free-controller-replay/verify.py @@ -0,0 +1,141 @@ +#!/usr/bin/env python3 +"""Independent free-algebra replay of #4534's noncommuting-stage identity for #4470's p16 controller. + +Reads #4470's CONTROLLER.json (on main) and #4534's FREE-CERTIFICATE.json (vendored, sha256 pinned to head 90505ab1). +Each of the 32 lines is a combination of the initial lines with coefficients in the free algebra Q[q, q^-1] +(q central): a monomial is (q exponent, ordered tuple of stage letters, leftmost first), and an operator applied +later is prepended. Events: LOCAL/QUERY_SHEAR as in my #4516 (shear y += Q^-1 x forward, y -= Q x backward; LOCAL +then left-multiplies both lines by d_stage); IDLE on ascending stages s_1..s_k left-multiplies by d_(s_k)...d_(s_1); +ADD and SIGNED_SWAP literally. Checks: L W R = diag(q^e d_w) in every one of the 1,024 entries, coefficient by +coefficient over ordered words; reversing every idle word breaks it; the 16/16 central exponents; every non-maximal +stage word is a contiguous prefix or suffix of G = (32, 31, 29, ..., 1, 0); L and R are invertible and they and +their inverses have dyadic entries. +Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. +""" +from collections import Counter +from fractions import Fraction as F +import hashlib +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +CERT_SHA = "12c732f840c2e9f375a73b941089bde5319b420688401276b7ac270cdd278350" + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +def main(): + for row_ in json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8"))["files"]: + need(hashlib.sha256((ROOT / row_["path"]).read_bytes()).hexdigest() == row_["sha256"], row_["path"]) + raw = (HERE / "FREE-CERTIFICATE-4534.json").read_bytes() + need(hashlib.sha256(raw).hexdigest() == CERT_SHA, "#4534 FREE-CERTIFICATE bytes") + global row, cert, p, n, thick + row = json.loads((ROOT / "research/joint-helper-lattice/CONTROLLER.json").read_bytes()) + cert = json.loads(raw) + p = row["pairs"] + n = 2 * p + thick = {0, 2 * p, *range(1, 2 * p, 2)} + need(check(replay(row["physical_events"])) == 0, "L W R = diag(q^e d_w) in all 1,024 entries") + broken = check(replay(row["physical_events"], reverse_idle=True)) + need(broken > 0, "reversed idle words are rejected") + diag = [(d[0], tuple(d[1])) for d in cert["diagonal"]] + need(Counter(e for e, w in diag) == Counter({1: 16, -1: 16}), "central exponents") + G = max((w for e, w in diag), key=len) + need(G == (32, 31, 29, 27, 25, 23, 21, 19, 17, 15, 13, 11, 9, 7, 5, 3, 1, 0), "longest word G") + words = {w for e, w in diag if w and w != G} + need(len(words) == 15 and all(G[:len(w)] == w or G[-len(w):] == w for w in words), "contiguous prefix/suffix words") + for name in ("left", "right"): + M = [[F(x) for x in r] for r in cert[name]] + need(det_nonzero(M), name + " invertible") + Mi = inverse(M) + need(all((x.denominator & (x.denominator - 1)) == 0 for r in M + Mi for x in r), name + " and inverse dyadic") + print(json.dumps({"status": "PASS_FREE_CONTROLLER_REPLAY", "entries_checked": n * n, "reversed_idle_mismatches": broken, + "words": len(words) + 1, "new_kappa_claimed": False}, indent=1)) + + +def replay(events, reverse_idle=False): + one=(0,()) + lines=[{i:{one:F(1)}} for i in range(n)] + def lmul(i,e,w): # left-multiply line i by q^e d_w (w tuple, leftmost first) + lines[i]={j:{(k[0]+e, tuple(w)+k[1]):v for k,v in poly.items()} for j,poly in lines[i].items()} + def add(dst,src,e,c): + for j,poly in lines[src].items(): + tgt=lines[dst].setdefault(j,{}) + for k,v in poly.items(): + kk=(k[0]+e,k[1]); x=tgt.get(kk,0)+c*v + if x: tgt[kk]=x + else: tgt.pop(kk,None) + if not tgt: lines[dst].pop(j) + for ev in events: + op=ev[0] + if op in ('LOCAL','QUERY_SHEAR'): + _,stage,pair,back=ev; x,y=2*pair,2*pair+1 + if back: x,y=y,x + add(y,x,1 if back else -1,-1 if back else 1) + if op=='LOCAL': lmul(x,0,(stage,)); lmul(y,0,(stage,)) + elif op=='IDLE': + _,pair,sel=ev + w=tuple(sorted(sel,reverse=True)) # D_{s_k} ... D_{s_1} for ascending list + if reverse_idle: w=tuple(reversed(w)) + lmul(2*pair,0,w); lmul(2*pair+1,0,w) + elif op=='ADD': + _,dst,src,*c=ev; add(dst,src,0,c[0] if c else 1) + elif op in ('SWAP','SIGNED_SWAP'): + _,x,y=ev; sg=-1 if op=='SIGNED_SWAP' else 1 + old=lines[x]; lines[x]=lines[y]; lines[y]={j:{k:sg*v for k,v in poly.items()} for j,poly in old.items()} + return lines +def check(lines): + L=[[F(x) for x in r] for r in cert['left']]; R=[[F(x) for x in r] for r in cert['right']] + diag=[(d[0],tuple(d[1])) for d in cert['diagonal']] + # (L W R)_{ik} = sum_j sum_l L_ij W_jl R_lk, per monomial + LW=[{} for _ in range(n)] # LW[i][l] = poly + for i in range(n): + acc={} + for j in range(n): + if L[i][j]: + for l,poly in lines[j].items(): + t=acc.setdefault(l,{}) + for k,v in poly.items(): t[k]=t.get(k,0)+L[i][j]*v + LW[i]=acc + bad=0 + for i in range(n): + out={} + for l,poly in LW[i].items(): + for kk in range(n): + if R[l][kk]: + t=out.setdefault(kk,{}) + for k,v in poly.items(): t[k]=t.get(k,0)+v*R[l][kk] + for kk in range(n): + poly={k:v for k,v in out.get(kk,{}).items() if v} + exp={diag[i]:F(1)} if i==kk else {} + if poly!=exp: bad+=1 + return bad +def det_nonzero(M): + M=[r[:] for r in M]; m=len(M) + for c in range(m): + piv=next((r for r in range(c,m) if M[r][c]),None) + if piv is None: return False + M[c],M[piv]=M[piv],M[c] + for r in range(c+1,m): + if M[r][c]: + f=M[r][c]/M[c][c]; M[r]=[a-f*b for a,b in zip(M[r],M[c])] + return True +def inverse(M): + m=len(M); A=[r[:]+[F(int(i==j)) for j in range(m)] for i,r in enumerate(M)] + for c in range(m): + piv=next(r for r in range(c,m) if A[r][c]); A[c],A[piv]=A[piv],A[c] + pv=A[c][c]; A[c]=[x/pv for x in A[c]] + for r in range(m): + if r!=c and A[r][c]: + f=A[r][c]; A[r]=[a-f*b for a,b in zip(A[r],A[c])] + return [r[m:] for r in A] +dy=lambda M: all((x.denominator & (x.denominator-1))==0 for r in M for x in r) + + +if __name__ == "__main__": + sys.exit(main())