From 15e0987e5fa88d1c15699215ac0cd70b47a535a6 Mon Sep 17 00:00:00 2001 From: Hanson Sun <182361798+bbMisk@users.noreply.github.com> Date: Tue, 13 Oct 2026 22:55:54 -0400 Subject: [PATCH] Certify exact dirty shear costs for three helpers and four targets --- .../CERTIFICATE.json | 2674 +++++++++++++++++ .../bit-zero-frame-feedback-3x4/README.md | 190 ++ .../bit-zero-frame-feedback-3x4/SOURCES.json | 40 + .../bit-zero-frame-feedback-3x4/TASK.json | 146 + .../bit-zero-frame-feedback-3x4/VERIFY.json | 39 + .../independent.py | 184 ++ .../test_certificate.py | 90 + .../bit-zero-frame-feedback-3x4/verify.py | 279 ++ 8 files changed, 3642 insertions(+) create mode 100644 research/bit-zero-frame-feedback-3x4/CERTIFICATE.json create mode 100644 research/bit-zero-frame-feedback-3x4/README.md create mode 100644 research/bit-zero-frame-feedback-3x4/SOURCES.json create mode 100644 research/bit-zero-frame-feedback-3x4/TASK.json create mode 100644 research/bit-zero-frame-feedback-3x4/VERIFY.json create mode 100644 research/bit-zero-frame-feedback-3x4/independent.py create mode 100644 research/bit-zero-frame-feedback-3x4/test_certificate.py create mode 100644 research/bit-zero-frame-feedback-3x4/verify.py diff --git a/research/bit-zero-frame-feedback-3x4/CERTIFICATE.json b/research/bit-zero-frame-feedback-3x4/CERTIFICATE.json new file mode 100644 index 0000000000..fd52721370 --- /dev/null +++ b/research/bit-zero-frame-feedback-3x4/CERTIFICATE.json @@ -0,0 +1,2674 @@ +{ + "all_inputs_arbitrary": true, + "ancillas": 0, + "controls": { + "exact_coset_products": 672, + "gl3_matrices": 168, + "negative_controls": [ + "unrestored_helper", + "dirty_target_mixing", + "wrong_helper_input", + "feedback_in_restricted_alphabet", + "noninvertible_self_xor", + "boolean_gate_index", + "insufficient_radius" + ], + "positive_feedback_cost": 5, + "positive_star_cost": 3 + }, + "feedback_gains": 0, + "gate_cost": 1, + "helpers": 3, + "maps": 4096, + "minimum_histogram": [ + 1, + 12, + 66, + 220, + 495, + 810, + 1017, + 922, + 529, + 24 + ], + "orbits": [ + { + "k": 0, + "minimum": 0, + "orbit_size": 1, + "restricted_witness": [] + }, + { + "k": 1, + "minimum": 1, + "orbit_size": 12, + "restricted_witness": [ + [ + 3, + 0 + ] + ] + }, + { + "k": 3, + "minimum": 2, + "orbit_size": 12, + "restricted_witness": [ + [ + 3, + 0 + ], + [ + 3, + 1 + ] + ] + }, + { + "k": 7, + "minimum": 3, + "orbit_size": 4, + "restricted_witness": [ + [ + 3, + 0 + ], + [ + 3, + 1 + ], + [ + 3, + 2 + ] + ] + }, + { + "k": 9, + "minimum": 2, + "orbit_size": 18, + "restricted_witness": [ + [ + 3, + 0 + ], + [ + 4, + 0 + ] + ] + }, + { + "k": 10, + "minimum": 2, + "orbit_size": 36, + "restricted_witness": [ + [ + 3, + 1 + ], + [ + 4, + 0 + ] + ] + }, + { + "k": 11, + "minimum": 3, + "orbit_size": 72, + "restricted_witness": [ + [ + 3, + 0 + ], + [ + 3, + 1 + ], + [ + 4, + 0 + ] + ] + }, + { + "k": 14, + "minimum": 3, + "orbit_size": 36, + "restricted_witness": [ + [ + 3, + 1 + ], + [ + 3, + 2 + ], + [ + 4, + 0 + ] + ] + }, + { + "k": 15, + "minimum": 4, + "orbit_size": 36, + "restricted_witness": [ + [ + 3, + 0 + ], + [ + 3, + 1 + ], + [ + 3, + 2 + ], + [ + 4, + 0 + ] + ] + }, + { + "k": 27, + "minimum": 4, + "orbit_size": 18, + "restricted_witness": [ + [ + 0, + 1 + ], + [ + 3, + 0 + ], + [ + 4, + 0 + ], + [ + 0, + 1 + ] + ] + }, + { + "k": 29, + "minimum": 4, + "orbit_size": 36, + "restricted_witness": [ + [ + 3, + 0 + ], + [ + 3, + 2 + ], + [ + 4, + 0 + ], + [ + 4, + 1 + ] + ] + }, + { + "k": 31, + "minimum": 5, + "orbit_size": 36, + "restricted_witness": [ + [ + 3, + 1 + ], + [ + 3, + 2 + ], + [ + 4, + 0 + ], + [ + 4, + 1 + ], + [ + 3, + 0 + ] + ] + }, + { + "k": 63, + "minimum": 5, + "orbit_size": 6, + "restricted_witness": [ + [ + 3, + 4 + ], + [ + 4, + 0 + ], + [ + 4, + 1 + ], + [ + 4, + 2 + ], + [ + 3, + 4 + ] + ] + }, + { + "k": 73, + "minimum": 3, + "orbit_size": 12, + "restricted_witness": [ + [ + 3, + 0 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ] + ] + }, + { + "k": 74, + "minimum": 3, + "orbit_size": 72, + "restricted_witness": [ + [ + 3, + 1 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ] + ] + }, + { + "k": 75, + "minimum": 4, + "orbit_size": 72, + "restricted_witness": [ + [ + 3, + 0 + ], + [ + 3, + 1 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ] + ] + }, + { + "k": 78, + "minimum": 4, + "orbit_size": 36, + "restricted_witness": [ + [ + 3, + 1 + ], + [ + 3, + 2 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ] + ] + }, + { + "k": 79, + "minimum": 5, + "orbit_size": 36, + "restricted_witness": [ + [ + 3, + 1 + ], + [ + 3, + 2 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ], + [ + 3, + 0 + ] + ] + }, + { + "k": 83, + "minimum": 4, + "orbit_size": 72, + "restricted_witness": [ + [ + 3, + 0 + ], + [ + 3, + 1 + ], + [ + 4, + 1 + ], + [ + 5, + 0 + ] + ] + }, + { + "k": 84, + "minimum": 3, + "orbit_size": 24, + "restricted_witness": [ + [ + 3, + 2 + ], + [ + 4, + 1 + ], + [ + 5, + 0 + ] + ] + }, + { + "k": 85, + "minimum": 4, + "orbit_size": 144, + "restricted_witness": [ + [ + 3, + 0 + ], + [ + 3, + 2 + ], + [ + 4, + 1 + ], + [ + 5, + 0 + ] + ] + }, + { + "k": 87, + "minimum": 5, + "orbit_size": 72, + "restricted_witness": [ + [ + 3, + 1 + ], + [ + 3, + 2 + ], + [ + 4, + 1 + ], + [ + 5, + 0 + ], + [ + 3, + 0 + ] + ] + }, + { + "k": 91, + "minimum": 5, + "orbit_size": 72, + "restricted_witness": [ + [ + 3, + 1 + ], + [ + 4, + 0 + ], + [ + 4, + 1 + ], + [ + 5, + 0 + ], + [ + 3, + 0 + ] + ] + }, + { + "k": 93, + "minimum": 5, + "orbit_size": 72, + "restricted_witness": [ + [ + 3, + 2 + ], + [ + 4, + 0 + ], + [ + 4, + 1 + ], + [ + 5, + 0 + ], + [ + 3, + 0 + ] + ] + }, + { + "k": 94, + "minimum": 5, + "orbit_size": 144, + "restricted_witness": [ + [ + 3, + 2 + ], + [ + 4, + 0 + ], + [ + 4, + 1 + ], + [ + 5, + 0 + ], + [ + 3, + 1 + ] + ] + }, + { + "k": 95, + "minimum": 6, + "orbit_size": 144, + "restricted_witness": [ + [ + 3, + 2 + ], + [ + 4, + 0 + ], + [ + 4, + 1 + ], + [ + 5, + 0 + ], + [ + 3, + 1 + ], + [ + 3, + 0 + ] + ] + }, + { + "k": 118, + "minimum": 5, + "orbit_size": 36, + "restricted_witness": [ + [ + 3, + 2 + ], + [ + 4, + 1 + ], + [ + 4, + 2 + ], + [ + 5, + 0 + ], + [ + 3, + 1 + ] + ] + }, + { + "k": 119, + "minimum": 6, + "orbit_size": 72, + "restricted_witness": [ + [ + 3, + 2 + ], + [ + 4, + 1 + ], + [ + 4, + 2 + ], + [ + 5, + 0 + ], + [ + 3, + 1 + ], + [ + 3, + 0 + ] + ] + }, + { + "k": 127, + "minimum": 6, + "orbit_size": 36, + "restricted_witness": [ + [ + 3, + 4 + ], + [ + 4, + 1 + ], + [ + 4, + 2 + ], + [ + 5, + 0 + ], + [ + 4, + 0 + ], + [ + 3, + 4 + ] + ] + }, + { + "k": 219, + "minimum": 5, + "orbit_size": 12, + "restricted_witness": [ + [ + 0, + 1 + ], + [ + 3, + 0 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ], + [ + 0, + 1 + ] + ] + }, + { + "k": 221, + "minimum": 6, + "orbit_size": 72, + "restricted_witness": [ + [ + 0, + 1 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ], + [ + 0, + 1 + ], + [ + 3, + 2 + ], + [ + 3, + 0 + ] + ] + }, + { + "k": 223, + "minimum": 6, + "orbit_size": 36, + "restricted_witness": [ + [ + 0, + 1 + ], + [ + 3, + 2 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ], + [ + 3, + 0 + ], + [ + 0, + 1 + ] + ] + }, + { + "k": 238, + "minimum": 6, + "orbit_size": 24, + "restricted_witness": [ + [ + 4, + 0 + ], + [ + 4, + 2 + ], + [ + 5, + 0 + ], + [ + 5, + 1 + ], + [ + 3, + 2 + ], + [ + 3, + 1 + ] + ] + }, + { + "k": 239, + "minimum": 7, + "orbit_size": 72, + "restricted_witness": [ + [ + 4, + 0 + ], + [ + 4, + 2 + ], + [ + 5, + 0 + ], + [ + 5, + 1 + ], + [ + 3, + 2 + ], + [ + 3, + 1 + ], + [ + 3, + 0 + ] + ] + }, + { + "k": 255, + "minimum": 7, + "orbit_size": 36, + "restricted_witness": [ + [ + 0, + 1 + ], + [ + 4, + 0 + ], + [ + 4, + 2 + ], + [ + 5, + 0 + ], + [ + 3, + 2 + ], + [ + 3, + 0 + ], + [ + 0, + 1 + ] + ] + }, + { + "k": 511, + "minimum": 7, + "orbit_size": 4, + "restricted_witness": [ + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ], + [ + 3, + 0 + ], + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ] + }, + { + "k": 585, + "minimum": 4, + "orbit_size": 3, + "restricted_witness": [ + [ + 3, + 0 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ] + ] + }, + { + "k": 586, + "minimum": 4, + "orbit_size": 24, + "restricted_witness": [ + [ + 3, + 1 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ] + ] + }, + { + "k": 587, + "minimum": 5, + "orbit_size": 24, + "restricted_witness": [ + [ + 3, + 1 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ], + [ + 3, + 0 + ] + ] + }, + { + "k": 590, + "minimum": 5, + "orbit_size": 12, + "restricted_witness": [ + [ + 3, + 2 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ], + [ + 3, + 1 + ] + ] + }, + { + "k": 591, + "minimum": 6, + "orbit_size": 12, + "restricted_witness": [ + [ + 3, + 2 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ], + [ + 3, + 1 + ], + [ + 3, + 0 + ] + ] + }, + { + "k": 594, + "minimum": 4, + "orbit_size": 18, + "restricted_witness": [ + [ + 3, + 1 + ], + [ + 4, + 1 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ] + ] + }, + { + "k": 595, + "minimum": 5, + "orbit_size": 72, + "restricted_witness": [ + [ + 3, + 1 + ], + [ + 4, + 1 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ], + [ + 3, + 0 + ] + ] + }, + { + "k": 596, + "minimum": 4, + "orbit_size": 36, + "restricted_witness": [ + [ + 3, + 2 + ], + [ + 4, + 1 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ] + ] + }, + { + "k": 597, + "minimum": 5, + "orbit_size": 72, + "restricted_witness": [ + [ + 3, + 2 + ], + [ + 4, + 1 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ], + [ + 3, + 0 + ] + ] + }, + { + "k": 598, + "minimum": 5, + "orbit_size": 72, + "restricted_witness": [ + [ + 3, + 2 + ], + [ + 4, + 1 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ], + [ + 3, + 1 + ] + ] + }, + { + "k": 599, + "minimum": 6, + "orbit_size": 72, + "restricted_witness": [ + [ + 3, + 2 + ], + [ + 4, + 1 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ], + [ + 3, + 1 + ], + [ + 3, + 0 + ] + ] + }, + { + "k": 603, + "minimum": 6, + "orbit_size": 36, + "restricted_witness": [ + [ + 4, + 0 + ], + [ + 4, + 1 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ], + [ + 3, + 1 + ], + [ + 3, + 0 + ] + ] + }, + { + "k": 605, + "minimum": 6, + "orbit_size": 36, + "restricted_witness": [ + [ + 4, + 0 + ], + [ + 4, + 1 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ], + [ + 3, + 2 + ], + [ + 3, + 0 + ] + ] + }, + { + "k": 606, + "minimum": 6, + "orbit_size": 72, + "restricted_witness": [ + [ + 4, + 0 + ], + [ + 4, + 1 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ], + [ + 3, + 2 + ], + [ + 3, + 1 + ] + ] + }, + { + "k": 607, + "minimum": 7, + "orbit_size": 72, + "restricted_witness": [ + [ + 4, + 0 + ], + [ + 4, + 1 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ], + [ + 3, + 2 + ], + [ + 3, + 1 + ], + [ + 3, + 0 + ] + ] + }, + { + "k": 630, + "minimum": 6, + "orbit_size": 18, + "restricted_witness": [ + [ + 4, + 1 + ], + [ + 4, + 2 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ], + [ + 3, + 2 + ], + [ + 3, + 1 + ] + ] + }, + { + "k": 631, + "minimum": 7, + "orbit_size": 36, + "restricted_witness": [ + [ + 4, + 1 + ], + [ + 4, + 2 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ], + [ + 3, + 2 + ], + [ + 3, + 1 + ], + [ + 3, + 0 + ] + ] + }, + { + "k": 639, + "minimum": 7, + "orbit_size": 18, + "restricted_witness": [ + [ + 3, + 4 + ], + [ + 4, + 2 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ], + [ + 4, + 1 + ], + [ + 4, + 0 + ], + [ + 3, + 4 + ] + ] + }, + { + "k": 667, + "minimum": 6, + "orbit_size": 36, + "restricted_witness": [ + [ + 4, + 0 + ], + [ + 4, + 1 + ], + [ + 5, + 1 + ], + [ + 6, + 0 + ], + [ + 3, + 1 + ], + [ + 3, + 0 + ] + ] + }, + { + "k": 668, + "minimum": 5, + "orbit_size": 72, + "restricted_witness": [ + [ + 4, + 0 + ], + [ + 4, + 1 + ], + [ + 5, + 1 + ], + [ + 6, + 0 + ], + [ + 3, + 2 + ] + ] + }, + { + "k": 669, + "minimum": 6, + "orbit_size": 144, + "restricted_witness": [ + [ + 4, + 0 + ], + [ + 4, + 1 + ], + [ + 5, + 1 + ], + [ + 6, + 0 + ], + [ + 3, + 2 + ], + [ + 3, + 0 + ] + ] + }, + { + "k": 671, + "minimum": 7, + "orbit_size": 72, + "restricted_witness": [ + [ + 4, + 0 + ], + [ + 4, + 1 + ], + [ + 5, + 1 + ], + [ + 6, + 0 + ], + [ + 3, + 2 + ], + [ + 3, + 1 + ], + [ + 3, + 0 + ] + ] + }, + { + "k": 679, + "minimum": 6, + "orbit_size": 24, + "restricted_witness": [ + [ + 3, + 2 + ], + [ + 4, + 2 + ], + [ + 5, + 1 + ], + [ + 6, + 0 + ], + [ + 3, + 1 + ], + [ + 3, + 0 + ] + ] + }, + { + "k": 685, + "minimum": 6, + "orbit_size": 72, + "restricted_witness": [ + [ + 4, + 0 + ], + [ + 4, + 2 + ], + [ + 5, + 1 + ], + [ + 6, + 0 + ], + [ + 3, + 2 + ], + [ + 3, + 0 + ] + ] + }, + { + "k": 686, + "minimum": 6, + "orbit_size": 72, + "restricted_witness": [ + [ + 4, + 0 + ], + [ + 4, + 2 + ], + [ + 5, + 1 + ], + [ + 6, + 0 + ], + [ + 3, + 2 + ], + [ + 3, + 1 + ] + ] + }, + { + "k": 687, + "minimum": 7, + "orbit_size": 144, + "restricted_witness": [ + [ + 4, + 0 + ], + [ + 4, + 2 + ], + [ + 5, + 1 + ], + [ + 6, + 0 + ], + [ + 3, + 2 + ], + [ + 3, + 1 + ], + [ + 3, + 0 + ] + ] + }, + { + "k": 703, + "minimum": 7, + "orbit_size": 36, + "restricted_witness": [ + [ + 3, + 4 + ], + [ + 4, + 2 + ], + [ + 5, + 1 + ], + [ + 6, + 0 + ], + [ + 4, + 1 + ], + [ + 4, + 0 + ], + [ + 3, + 4 + ] + ] + }, + { + "k": 731, + "minimum": 6, + "orbit_size": 24, + "restricted_witness": [ + [ + 6, + 0 + ], + [ + 0, + 1 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ], + [ + 3, + 0 + ], + [ + 0, + 1 + ] + ] + }, + { + "k": 733, + "minimum": 7, + "orbit_size": 72, + "restricted_witness": [ + [ + 4, + 1 + ], + [ + 5, + 0 + ], + [ + 5, + 1 + ], + [ + 6, + 0 + ], + [ + 4, + 0 + ], + [ + 3, + 2 + ], + [ + 3, + 0 + ] + ] + }, + { + "k": 734, + "minimum": 7, + "orbit_size": 72, + "restricted_witness": [ + [ + 4, + 1 + ], + [ + 5, + 0 + ], + [ + 5, + 1 + ], + [ + 6, + 0 + ], + [ + 4, + 0 + ], + [ + 3, + 2 + ], + [ + 3, + 1 + ] + ] + }, + { + "k": 735, + "minimum": 7, + "orbit_size": 72, + "restricted_witness": [ + [ + 6, + 0 + ], + [ + 0, + 1 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ], + [ + 3, + 2 + ], + [ + 3, + 0 + ], + [ + 0, + 1 + ] + ] + }, + { + "k": 750, + "minimum": 7, + "orbit_size": 72, + "restricted_witness": [ + [ + 4, + 2 + ], + [ + 5, + 0 + ], + [ + 5, + 1 + ], + [ + 6, + 0 + ], + [ + 4, + 0 + ], + [ + 3, + 2 + ], + [ + 3, + 1 + ] + ] + }, + { + "k": 751, + "minimum": 8, + "orbit_size": 72, + "restricted_witness": [ + [ + 3, + 2 + ], + [ + 4, + 0 + ], + [ + 4, + 2 + ], + [ + 6, + 0 + ], + [ + 0, + 1 + ], + [ + 5, + 0 + ], + [ + 3, + 0 + ], + [ + 0, + 1 + ] + ] + }, + { + "k": 758, + "minimum": 7, + "orbit_size": 72, + "restricted_witness": [ + [ + 4, + 2 + ], + [ + 5, + 0 + ], + [ + 5, + 1 + ], + [ + 6, + 0 + ], + [ + 4, + 1 + ], + [ + 3, + 2 + ], + [ + 3, + 1 + ] + ] + }, + { + "k": 759, + "minimum": 8, + "orbit_size": 144, + "restricted_witness": [ + [ + 3, + 2 + ], + [ + 4, + 1 + ], + [ + 4, + 2 + ], + [ + 6, + 0 + ], + [ + 0, + 1 + ], + [ + 5, + 0 + ], + [ + 3, + 0 + ], + [ + 0, + 1 + ] + ] + }, + { + "k": 767, + "minimum": 8, + "orbit_size": 72, + "restricted_witness": [ + [ + 4, + 2 + ], + [ + 6, + 0 + ], + [ + 0, + 1 + ], + [ + 5, + 0 + ], + [ + 4, + 0 + ], + [ + 3, + 2 + ], + [ + 3, + 0 + ], + [ + 0, + 1 + ] + ] + }, + { + "k": 950, + "minimum": 6, + "orbit_size": 12, + "restricted_witness": [ + [ + 1, + 2 + ], + [ + 4, + 1 + ], + [ + 5, + 1 + ], + [ + 6, + 0 + ], + [ + 3, + 1 + ], + [ + 1, + 2 + ] + ] + }, + { + "k": 951, + "minimum": 7, + "orbit_size": 36, + "restricted_witness": [ + [ + 1, + 2 + ], + [ + 4, + 1 + ], + [ + 5, + 1 + ], + [ + 6, + 0 + ], + [ + 3, + 1 + ], + [ + 3, + 0 + ], + [ + 1, + 2 + ] + ] + }, + { + "k": 959, + "minimum": 8, + "orbit_size": 36, + "restricted_witness": [ + [ + 1, + 2 + ], + [ + 4, + 1 + ], + [ + 5, + 1 + ], + [ + 6, + 0 + ], + [ + 4, + 0 + ], + [ + 3, + 1 + ], + [ + 3, + 0 + ], + [ + 1, + 2 + ] + ] + }, + { + "k": 1023, + "minimum": 8, + "orbit_size": 12, + "restricted_witness": [ + [ + 6, + 0 + ], + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 5, + 0 + ], + [ + 4, + 0 + ], + [ + 3, + 0 + ], + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ] + }, + { + "k": 1755, + "minimum": 6, + "orbit_size": 3, + "restricted_witness": [ + [ + 0, + 1 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ], + [ + 3, + 0 + ], + [ + 0, + 1 + ] + ] + }, + { + "k": 1757, + "minimum": 7, + "orbit_size": 24, + "restricted_witness": [ + [ + 3, + 0 + ], + [ + 0, + 1 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ], + [ + 4, + 0 + ], + [ + 3, + 2 + ], + [ + 0, + 1 + ] + ] + }, + { + "k": 1759, + "minimum": 7, + "orbit_size": 12, + "restricted_witness": [ + [ + 0, + 1 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ], + [ + 3, + 2 + ], + [ + 3, + 0 + ], + [ + 0, + 1 + ] + ] + }, + { + "k": 1773, + "minimum": 8, + "orbit_size": 18, + "restricted_witness": [ + [ + 0, + 2 + ], + [ + 3, + 0 + ], + [ + 4, + 0 + ], + [ + 0, + 2 + ], + [ + 0, + 1 + ], + [ + 6, + 0 + ], + [ + 5, + 0 + ], + [ + 0, + 1 + ] + ] + }, + { + "k": 1774, + "minimum": 8, + "orbit_size": 36, + "restricted_witness": [ + [ + 3, + 1 + ], + [ + 3, + 2 + ], + [ + 4, + 0 + ], + [ + 4, + 2 + ], + [ + 0, + 1 + ], + [ + 6, + 0 + ], + [ + 5, + 0 + ], + [ + 0, + 1 + ] + ] + }, + { + "k": 1775, + "minimum": 8, + "orbit_size": 72, + "restricted_witness": [ + [ + 4, + 0 + ], + [ + 0, + 1 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ], + [ + 4, + 2 + ], + [ + 3, + 2 + ], + [ + 3, + 0 + ], + [ + 0, + 1 + ] + ] + }, + { + "k": 1791, + "minimum": 8, + "orbit_size": 18, + "restricted_witness": [ + [ + 0, + 1 + ], + [ + 4, + 2 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ], + [ + 4, + 0 + ], + [ + 3, + 2 + ], + [ + 3, + 0 + ], + [ + 0, + 1 + ] + ] + }, + { + "k": 1911, + "minimum": 9, + "orbit_size": 24, + "restricted_witness": [ + [ + 3, + 0 + ], + [ + 3, + 1 + ], + [ + 3, + 2 + ], + [ + 4, + 1 + ], + [ + 4, + 2 + ], + [ + 5, + 0 + ], + [ + 5, + 2 + ], + [ + 6, + 0 + ], + [ + 6, + 1 + ] + ] + }, + { + "k": 1919, + "minimum": 8, + "orbit_size": 36, + "restricted_witness": [ + [ + 0, + 2 + ], + [ + 5, + 0 + ], + [ + 0, + 1 + ], + [ + 4, + 0 + ], + [ + 3, + 0 + ], + [ + 0, + 2 + ], + [ + 6, + 0 + ], + [ + 0, + 1 + ] + ] + }, + { + "k": 2047, + "minimum": 8, + "orbit_size": 12, + "restricted_witness": [ + [ + 0, + 1 + ], + [ + 6, + 0 + ], + [ + 0, + 2 + ], + [ + 5, + 0 + ], + [ + 4, + 0 + ], + [ + 3, + 0 + ], + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ] + }, + { + "k": 4095, + "minimum": 8, + "orbit_size": 1, + "restricted_witness": [ + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ], + [ + 4, + 0 + ], + [ + 3, + 0 + ], + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ] + } + ], + "radius": 4, + "restricted": { + "cosets": 9954, + "outside_double_radius": [ + 1911, + 1918, + 1967, + 1981, + 2030, + 2037, + 2807, + 2814, + 2975, + 3003, + 3038, + 3059, + 3311, + 3325, + 3423, + 3451, + 3549, + 3563, + 3822, + 3829, + 3934, + 3955, + 3997, + 4011 + ], + "spheres": [ + 1, + 30, + 534, + 7113, + 75645 + ], + "unordered_distinct_pairs": 5285278 + }, + "schema_version": 1, + "targets": 4, + "unrestricted": { + "cosets": 99565, + "outside_double_radius": [ + 1911, + 1918, + 1967, + 1981, + 2030, + 2037, + 2807, + 2814, + 2975, + 3003, + 3038, + 3059, + 3311, + 3325, + 3423, + 3451, + 3549, + 3563, + 3822, + 3829, + 3934, + 3955, + 3997, + 4011 + ], + "spheres": [ + 1, + 42, + 1092, + 22141, + 375480 + ], + "unordered_distinct_pairs": 9768694 + } +} diff --git a/research/bit-zero-frame-feedback-3x4/README.md b/research/bit-zero-frame-feedback-3x4/README.md new file mode 100644 index 0000000000..3aa2cecc93 --- /dev/null +++ b/research/bit-zero-frame-feedback-3x4/README.md @@ -0,0 +1,190 @@ +# Target feedback saves no XORs for three-helper / four-target dirty shears + +**Finite exact result; no new supplier or kappa.** For all 4,096 binary +4-by-3 matrices K, allowing targets to feed helpers does not reduce the minimum +unit XOR cost of `(h,y) -> (h,y+Kh)`. There are three helpers and four targets; +every register starts with arbitrary independent data and there are no extra +registers. The maximum minimum is nine gates. + +This answers the next finite case requested by @commdata2338 in +[PR1306](https://github.com/CrocSwap/integer-mult-bounds/pull/1306) and +[Discussion1290](https://github.com/CrocSwap/integer-mult-bounds/discussions/1290). +That predecessor established the equality for up to three helpers and three +targets and supplied the common-zero-frame substitution lemma. Its pinned head +is `0d4c0069f1f4592833304a9ea6e61e676c566113`; its theorem and lemma are credited, +not claimed here. This package adds the seven-register census, a simultaneous +shear-coset calculation, and a separate truth-table verification. + +## Model and exact result + +Registers are `h0,h1,h2,y0,y1,y2,y3`, numbered 0 through 6. A gate `[d,s]` +means `register[d] ^= register[s]`, with distinct indices. Each gate costs one, +including preparation and restoration. The restricted alphabet has 30 gates: +it excludes only helper destinations with target sources. Helper mixing and +target mixing remain allowed. The unrestricted alphabet has all 42 gates. + +The complete required matrix is + +```text +T_K = [ I_3 0 ] + [ K I_4 ]. +``` + +The helpers and the initial target data must all be restored as shown. Testing +only zero workspace would be insufficient. The model has no allocation, +COPY/ERASE, frame changes, paid recursive calls, free basis changes or free +permutations. A length-L word costs L scalar ADDs and zero of these other events. +This is a local algebraic bill, not a hosted-supplier or precision certificate. + +Both alphabets have this exact distribution: + +| Minimum gates | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | +|---|---:|---:|---:|---:|---:|---:|---:|---:|---:|---:| +| Labeled K | 1 | 12 | 66 | 220 | 495 | 810 | 1,017 | 922 | 529 | 24 | + +The 24 nine-gate maps are precisely the permutations of these four rows: + +```text +[1,1,1], [0,1,1], [1,0,1], [1,1,0]. +``` + +No word of at most eight gates in either alphabet realizes one of them. The +nine direct helper-to-target XORs attain the bound. This includes unrestricted +words with temporary target feedback. The other 4,072 maps have explicit +restricted witnesses of length at most eight. [CERTIFICATE.json](CERTIFICATE.json) +stores 87 helper/target permutation representatives, their costs, orbit sizes +and restricted witnesses, as well as the complete search statistics. + +## Why the finite calculation certifies global minima + +Every XOR generator is its own inverse. Let B4 be the complete radius-four +ball in either alphabet, with breadth-first distances. Every word of length +at most eight splits into two words of length at most four. Its endpoint is +T_K exactly when there are A,B in B4 with `B = A T_K`; the corresponding word +runs B and then the reverse of A. Minimizing `distance(A)+distance(B)` over +these pairs therefore gives every minimum at most eight. An absent pair +proves a lower bound of nine. It becomes an exact minimum only when an explicit +nine-gate word is checked; the verifier refuses to fill a larger search gap. + +The primary checker finds all pairs simultaneously. Write an invertible matrix +M by its three helper columns X and four target columns Y. Right multiplication +by T_K leaves Y unchanged and replaces X by `X+YK`. Reduce each column of X +modulo the span of Y, using a deterministic echelon basis derived only from Y. +Keep the reduction coefficients Q, so `M T_Q` is the canonical representative. +The four columns of Y are independent, making Q unique. + +Two matrices have the same representative if and only if they differ by a +right shear. If their recorded coefficients are Q_A and Q_B, then +`A^-1 B = T_(Q_A+Q_B)`. Grouping B4 by these exact representatives and visiting +every distinct unordered pair thus loses no eligible pair. Pair reversal +preserves the shear because T_K is an involution; the identity is handled +separately. The primary computation prices all 4,096 labeled maps before +using any symmetry to shorten the certificate. + +The radius-four sphere sizes are: + +| Alphabet | 0 | 1 | 2 | 3 | 4 | +|---|---:|---:|---:|---:|---:| +| Restricted | 1 | 30 | 534 | 7,113 | 75,645 | +| Unrestricted | 1 | 42 | 1,092 | 22,141 | 375,480 | + +`independent.py` imports no primary or predecessor checker. It represents each +seven-register map by its literal outputs on all 128 bit inputs, builds the +unrestricted B4 by table composition, and directly tests `B=A T_K` for every +word shorter than each claimed minimum. It does not use the coset quotient. +For a claimed cost c <= 9, balanced splits require left distances only through +`floor((c-1)/2)` and right distances through four. Thus its shorter-word tests +are complete, including the eight-gate exclusion for the nine-gate class. + +Separate helper and target permutations conjugate each alphabet into itself +and preserve cost. They transport endpoints and witnesses rather than execute +free gates. The second checker verifies that the 87 orbits partition all 4,096 +matrices, and replays the transported restricted witnesses on all 128 inputs +for every labeled matrix. Restricted upper bounds and unrestricted lower bounds +agree. The shared mathematical principle is meet-in-the-middle; the code, +representation and pair enumeration differ. Both were written in one AI-assisted +session, not by independent human reviewers. + +## Reproduce and failure controls + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -I -B scripts/research_package.py --package research/bit-zero-frame-feedback-3x4 +``` + +This registered replay runs both checkers and the subprocess controls. The +checkers print `PASS_SHEAR_3X4_COSETS` and `PASS_SHEAR_3X4_TRUTH_TABLES`; the +runner ends with `PASS_REGISTERED_RESEARCH_PACKAGE` and `outcome=negative-result`. +To regenerate the certificate explicitly: + +```sh +python3.12 -I -B research/bit-zero-frame-feedback-3x4/verify.py --write +``` + +Controls check a restored helper star and a complete feedback word, and reject +missing restoration, residual target dirt, wrong helper columns, forbidden +feedback, self-XOR, Boolean indices and an insufficient radius. The primary +checker validates all 672 shear products on the full 168-element GL(3,2). +The truth-table checker also traverses all 20,160 elements of GL(4,2), compares +all 16 two-by-two shear distances and rejects each overstated minimum. + +The subprocess tests copy both checkers and the certificate to a fresh directory +and run under isolated, optimized Python. Both engines must reject four actual +certificate corruptions: a longer valid word falsely labeled optimal, a wrong +dirty-input column, a missing orbit and an understated sphere count. A further +test reproduces the predecessor's three-by-three distribution with the new +coset algorithm. No assertions are needed for the checkers' rejection paths. + +The complete registered replay passed under CPython 3.12.13, including all +three test groups. The repository's 20 research-workflow tests also passed +under Python 3.12 with no skips. Source-pin and package +metadata checks passed; these checks are distinct from mathematical acceptance. + +## Scope, sources and task selection + +The base is main `55a02580ce1b283026e9d3b3510b218f8c93a4de`. +[TASK.json](TASK.json) records the selector nonce, changed scope, overlap checks +and stop rule. The original card was `bit-helper-contract`. PR1194 and PR1311 +already address its H2/K question; this follows PR1306's adjacent D-local H1 +cost question. It is a prerequisite/negative result, not an interface adoption. +[Discussion1544](https://github.com/CrocSwap/integer-mult-bounds/discussions/1544) +records the claim and result. No predecessor implementation or candidate is +imported. Catalogue/selected-record provenance and contextual source identities +are in [SOURCES.json](SOURCES.json). + +The result is limited to these seven registers, F2, unit-cost single-source +XORs and the stated alphabets. It does not exclude feedback savings in larger +dimensions, with extra registers, weighted or multi-source gates, other fields, +or changed frame contracts. No R439 word, selected frontier or frozen input +is changed. Native replay, hosted emission, all-size/compiler and common-frame +realization, intermediate precision/tape bounds, outer analytic transfer and +proof-assistant formalization are not checked. No new multiplication exponent +follows, and the selected frontier's cold replay is not rerun for this package. + +## Open next questions + +Does feedback save gates with four helpers and four targets? A concrete strict +gain would make the D-local relaxation useful. First obtain a specific K and a +fully restored unrestricted witness beating a *certified* restricted lower +bound. Larger search balls and the absence of a candidate remain blockers; +this result alone does not justify an unbounded larger census. Any candidate +would still need actual frame, precision and hosting costs before supplier use. +The structured question is in [TASK.json](TASK.json). The three-by-four domain +itself needs no further search. + +## Credit + +Hanson Sun (@bbMisk), with substantial OpenAI Codex assistance in mathematics, +implementation, verification and writing. Apache-2.0. No subagents or independent +human review. Emulate processing was unavailable; the prose was checked against +the sources and executed results under the donor's stated fallback. + +Credit @commdata2338 / PR1306 for the prior census, model, substitution lemma, +meet-in-the-middle setup and explicit handoff; @woklerx / PR1194 and PR1105 for +the semantic-D and feedback-cleanup lineage; and Arham Tahir / PR1311 for the +independent semantic-D application. Retain Zhihao Chen / PR425, eumemic / PR555, +DreamingOfClouds / PR589, Gareth Davidson / PR926, @theon199 / PR967 and Sagar +Thakrar / PR1062, with Aaron Wang / PR1015 and Ross Richardson / PR923, as the +underlying bit-word/checker lineage. This result does not claim a new version +of their constructions or substitution arguments. diff --git a/research/bit-zero-frame-feedback-3x4/SOURCES.json b/research/bit-zero-frame-feedback-3x4/SOURCES.json new file mode 100644 index 0000000000..b35774bdb6 --- /dev/null +++ b/research/bit-zero-frame-feedback-3x4/SOURCES.json @@ -0,0 +1,40 @@ +{ + "schema_version": 1, + "base_commit": "55a02580ce1b283026e9d3b3510b218f8c93a4de", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + }, + { + "path": "research/e8-bit-p111-tuned/code/xcheck_p.py", + "usage": "provenance", + "git_blob": "184f5dcf94a486cc7db91ca4db5865916bf26009", + "sha256": "af3decc877e27c00001cf56f50c6c09566e8e101297ab34c7860aed96a06d80e" + }, + { + "path": "research/r439-bsection-stars-seed01/README.md", + "usage": "provenance", + "git_blob": "188175a52bb2a3ad65c701b3bd218ae3fc0bdfde", + "sha256": "3a32ecbf886d6605eb7441c63ca934c6aab0942d0e7e570c3dd0795d1cf00336" + } + ], + "contextual_predecessors": [ + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1306", + "head": "0d4c0069f1f4592833304a9ea6e61e676c566113", + "path": "research/bit-zero-frame-feedback/README.md", + "git_blob": "60ef66f366c107d606c0a00c5fefcaa03d83f84b", + "sha256": "c788006ee2723bdbf0835526e36e817df42567ffaa327bd8e5ff2f81889a623f", + "usage": "Attribution and mathematical context only; not imported, executed, or required for replay." + } + ] +} diff --git a/research/bit-zero-frame-feedback-3x4/TASK.json b/research/bit-zero-frame-feedback-3x4/TASK.json new file mode 100644 index 0000000000..c94984cc95 --- /dev/null +++ b/research/bit-zero-frame-feedback-3x4/TASK.json @@ -0,0 +1,146 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 2, + "base_commit": "55a02580ce1b283026e9d3b3510b218f8c93a4de", + "original_card": { + "id": "bit-helper-contract", + "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?", + "starting_points": [ + "research/r439-bsection-stars-seed01/README.md", + "research/r439-copy-path-sharing-barrier/README.md" + ], + "methods": [ + "Derive a replacement interface lemma and price its implementation.", + "Seek an exact dirty-input or chronological-cut counterexample to the proposed replacement." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient.", + "first_step": { + "command": [ + "python3", + "-B", + "research/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.", + "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.", + "allowed_variations": [ + "Choose one helper-star or quartet instance; narrow to one boundary implication." + ], + "scope_change_triggers": [ + "Changing only source count or scalar addition count without an interface argument." + ], + "overlap_terms": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D", + "helper-star" + ] + }, + "scope_status": "changed", + "actual_scope": "For every binary 4-by-3 K, compare the exact unit-XOR minimum for the complete dirty boundary (h,y)->(h,y+Kh), with and without helper<-target feedback; three helpers, four targets, no extra registers.", + "scope_change_reason": "PR1194 and PR1311 already address the original H2/K substitution question. Follow the explicit PR1306 next question on the adjacent D-local H1 feedback relaxation, increasing the finite domain to three helpers and four targets.", + "bottleneck_link": "A prerequisite/negative result: D-local target feedback cannot improve scalar cost in this complete seven-register domain. No paid recursive profile or supplier changes; scalar savings would still need full physical accounting.", + "budget_minutes": 60, + "stop_rule": "Stop after 30 minutes of computation, a radius gap without an attaining witness, or a verified finite outcome. Do not infer an impossibility outside the enumerated alphabet/domain.", + "outcome": "negative-result", + "evidence": "Complete radius-four coset pairing on all 4096 labeled K and a separate truth-table shorter-word exclusion agree: histogram [1,12,66,220,495,810,1017,922,529,24], maximum minimum 9, feedback gains 0. Restricted witnesses are replayed on all 128 dirty inputs for every K.", + "author": "Hanson Sun (@bbMisk)", + "ai_assistance": "Substantial OpenAI Codex assistance in mathematics, code, validation and writing. Both implementations were written in one session; no subagents or independent human review. Emulate processing was unavailable; prose checked against sources and executed evidence under the donor fallback.", + "open_questions": [ + { + "question": "Can four helpers and four targets admit a strict unit-XOR advantage from D-local target feedback?", + "why_it_matters": "A strict gain would make this relaxation locally useful, though physical admission remains separate.", + "first_step": "Find one explicit K and a fully restored unrestricted word beating a certified restricted lower bound; use the coset method only in a bounded exclusion.", + "blocked_by": "No shorter candidate is known here; larger balls grow quickly. This result does not justify unbounded enumeration, and any candidate still needs precision/frame/hosting accounting." + } + ], + "selection_nonce": "437983a3b9b6e2b08f4dd5a1f510e5e4", + "catalogue_scope_key": "bfb61f829a81535adeae", + "scope_key": "bit-helper-contract/dirty-shear/H3-T4/F2/unit-XOR/no-ancillas/all-K/coset-BFS4", + "optimistic_full_cost_budget": "Every ordered single-source XOR costs one, including preparation and restoration. No allocations, COPY/ERASE, frame changes, recursive calls or free basis changes. A positive result would require a strictly shorter unrestricted witness with an exact restricted lower bound.", + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1544", + "nearest_overlap": [ + { + "pr": 1306, + "head": "0d4c0069f1f4592833304a9ea6e61e676c566113", + "delta": "Direct predecessor; exact H,T<=3 no-gain census and explicit H3/T4 handoff. New domain and all-shear coset enumeration." + }, + { + "pr": 1194, + "head": "2e39c98238f543d988f9efc1b076590a4b780dca", + "delta": "Semantic-D substitution, credited context; no new claim to its lemma." + }, + { + "pr": 1311, + "head": "a2875c1834b9c9ef42a84eda4890d5462cc98fa5", + "delta": "Independent semantic-D application to an R439 word; this package changes no supplier word." + }, + { + "pr": 1420, + "head": "d19a944897714f2ecae72720b7dafc3e256f2f8d", + "delta": "Raw/projected cleanup loops; different endpoint question, no relaxation of chronological cleanup here." + } + ], + "overlap_initial": { + "searched_at": "2026-10-14T02:37:34.559692+00:00", + "open_prs": 732, + "discussion_records": 206, + "complete_pagination": true, + "warnings": [], + "limits": "Open PR bodies, discussion bodies/comments/replies, top-level package READMEs/TASKs and ledger; not arbitrary diffs or nested sources. No match does not prove novelty." + }, + "unchecked_obligations": [ + "larger dimensions or extra registers", + "weighted/multi-source XOR alphabets or other fields", + "native and hosted-supplier replay", + "all-size/compiler and common-frame realization", + "intermediate precision/tape and outer analytic transfer", + "proof-assistant formalization", + "selected-frontier cold replay" + ], + "overlap_final": { + "searched_at": "2026-10-14T02:53:23.536530+00:00", + "coverage": { + "open_prs": { + "fetched_at": "2026-10-14T02:52:53.949869+00:00", + "complete_pagination": true, + "records": 715 + }, + "discussions": { + "fetched_at": "2026-10-14T02:53:23.477359+00:00", + "complete_pagination": true, + "records": 216 + } + }, + "warnings": [], + "limits": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "scope_review": "Only PR1306 and its Discussion1290 handoff match the H3/T4 shear question; PR1347 and PR1323 use rectangular star-trim matrices on different objects. Our own Discussion1544 is excluded as novelty evidence." + }, + "submission_main": "c5108f0f68d482e5712a8e26a5978d47762dfc16", + "validation": { + "registered_replay": { + "command": "python3.12 -I -B scripts/research_package.py --package research/bit-zero-frame-feedback-3x4", + "exit_code": 0, + "python": "CPython 3.12.13", + "checks": [ + "exact coset recomputation", + "independent truth-table exclusions and all labeled witnesses", + "three subprocess/regression test groups; four corruption variants rejected by both engines; optimized relocation" + ] + }, + "repository_workflow_tests": { + "command": "python3.12 -B -m unittest discover -s tests -p 'test_research_*.py'", + "exit_code": 0, + "loaded_and_run": 20, + "skipped": 0 + }, + "initial_positive_controls": [ + "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "PASS_R439_BSECTION_STARS blocks=10 gates=388->254 ADDs=11783->11515->11500 guard_rejections=24->0 columns=661 controls=8 no_new_kappa" + ], + "metadata_and_source_pins": "passed; this is not mathematical acceptance" + } +} diff --git a/research/bit-zero-frame-feedback-3x4/VERIFY.json b/research/bit-zero-frame-feedback-3x4/VERIFY.json new file mode 100644 index 0000000000..7af608669e --- /dev/null +++ b/research/bit-zero-frame-feedback-3x4/VERIFY.json @@ -0,0 +1,39 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Recompute exact all-K minima in both alphabets using complete radius-four coset pairing, attaining words and meaningful controls." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Independent truth-table shorter-word exclusions and every labeled restricted witness on all 128 dirty inputs; full GL4 controls." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_certificate.py" + ], + "timeout_seconds": 180, + "checks": "Both engines reject four actual certificate corruptions; isolated optimized relocated replay; reproduce predecessor 3x3 costs with the new coset method." + } + ] +} diff --git a/research/bit-zero-frame-feedback-3x4/independent.py b/research/bit-zero-frame-feedback-3x4/independent.py new file mode 100644 index 0000000000..10b8f2a2fa --- /dev/null +++ b/research/bit-zero-frame-feedback-3x4/independent.py @@ -0,0 +1,184 @@ +#!/usr/bin/env python3 +"""Literal Boolean-map lower bounds and dirty-input witness verification. + +Hanson Sun (@bbMisk), with substantial OpenAI Codex assistance. Apache-2.0. +No primary/predecessor checker imports, matrix packing, or coset calculation. +Shared mathematics: invertible XORs, meet-in-the-middle and permutation symmetry. +This is independent code/representation, not independent human review. +""" +import argparse +from collections import Counter +from itertools import permutations +import json +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent + + +class Invalid(ValueError): + pass + + +def require(condition, reason): + if not condition: + raise Invalid(reason) + + +def xor_table(destination, source): + return bytes(x ^ (((x >> source) & 1) << destination) for x in range(256)) + + +def expected(k, helpers, targets): + values = [] + for x in range(1 << (helpers + targets)): + y = x + for r in range(targets): + row = (k >> (r * helpers)) & ((1 << helpers) - 1) + if (row & x).bit_count() % 2: + y ^= 1 << (helpers + r) + values.append(y) + return bytes(values) + + +def replay(word, helpers, targets, restricted=True): + n = helpers + targets + table = bytes(range(1 << n)) + require(type(word) is list, "word type") + for gate in word: + require(type(gate) is list and len(gate) == 2 + and all(type(x) is int and 0 <= x < n for x in gate), "gate type") + d, s = gate + require(d != s, "noninvertible gate") + require(not restricted or not (d < helpers <= s), "forbidden feedback") + table = table.translate(xor_table(d, s)) + return table + + +def truth_ball(n, radius): + gates = [xor_table(d, s) for d in range(n) for s in range(n) if d != s] + first = bytes(range(1 << n)) + distances, layers = {first: 0}, [[first]] + for depth in range(1, radius + 1): + following = [] + for table in layers[-1]: + for gate in gates: + reached = table.translate(gate) + if reached not in distances: + distances[reached] = depth + following.append(reached) + layers.append(following) + return distances, layers + + +def exclude_shorter(shear, claimed, distances, layers): + # Balance every word of length L < claimed into halves of length at most + # floor(L/2) and ceil(L/2); both are in B4 when claimed <=9. + require(0 <= claimed <= 9, "lower-bound radius insufficient") + for depth in range(min(4, (claimed - 1) // 2) + 1): + for left in layers[depth]: + # A o T: T(x) is the input to A. Do not compose in reverse order. + right = shear.translate(left + bytes(256 - len(left))) + other = distances.get(right) + require(other is None or depth + other >= claimed, + "shorter unrestricted word exists") + + +def transport(k, word, helpers, targets): + for hp in permutations(range(helpers)): + for tp in permutations(range(targets)): + mapping = hp + tuple(helpers + x for x in tp) + moved = 0 + for r in range(targets): + for c in range(helpers): + if k & (1 << (r * helpers + c)): + moved |= 1 << (tp[r] * helpers + hp[c]) + yield moved, [[mapping[d], mapping[s]] for d, s in word] + + +def verify(data): + for key, value in {"schema_version": 1, "helpers": 3, "targets": 4, + "maps": 4096, "gate_cost": 1, "ancillas": 0, + "radius": 4, "feedback_gains": 0}.items(): + require(type(data.get(key)) is int and data[key] == value, "header " + key) + require(data.get("all_inputs_arbitrary") is True, "arbitrary input contract") + distances, layers = truth_ball(7, 4) + require([len(layer) for layer in layers] == data["unrestricted"]["spheres"], + "unrestricted sphere counts differ") + covered, histogram = set(), Counter() + for item in data["orbits"]: + k, cost, word = item["k"], item["minimum"], item["restricted_witness"] + require(type(k) is int and 0 <= k < 4096, "representative range") + require(type(cost) is int and cost == len(word), "cost/witness length") + require(replay(word, 3, 4) == expected(k, 3, 4), "representative dirty endpoint") + exclude_shorter(expected(k, 3, 4), cost, distances, layers) + members = {} + for moved, witness in transport(k, word, 3, 4): + members.setdefault(moved, witness) + require(k == min(members), "noncanonical representative") + require(type(item["orbit_size"]) is int and len(members) == item["orbit_size"], + "orbit cardinality") + require(covered.isdisjoint(members), "overlapping orbits") + for moved, witness in members.items(): + require(replay(witness, 3, 4) == expected(moved, 3, 4), + "transported dirty endpoint") + covered.update(members) + histogram[cost] += len(members) + require(covered == set(range(4096)), "missing labeled shear") + require([histogram[i] for i in range(10)] == data["minimum_histogram"], "histogram") + return len(data["orbits"]) + + +def controls(): + failures = [] + + def reject(name, action): + try: + action() + except Invalid: + failures.append(name) + else: + raise Invalid("failure control accepted: " + name) + + distances, layers = truth_ball(4, 10) + require(len(distances) == 20160 and not layers[-1], "complete GL4 control") + for k in range(16): + shear = expected(k, 2, 2) + actual = distances[shear] + exclude_shorter(shear, actual, distances, layers) + reject("overstated_minimum_" + str(k), + lambda: exclude_shorter(shear, actual + 1, distances, layers)) + feedback = [[0, 1], [1, 0], [0, 1], [1, 0], [0, 1]] + require(replay(feedback, 1, 1, False) == expected(1, 1, 1), "feedback positive") + reject("feedback_alphabet", lambda: replay(feedback, 1, 1)) + star = [[0, 1], [2, 0], [0, 1]] + require(replay(star, 2, 1) == expected(3, 2, 1), "star positive") + require(replay(star[:-1], 2, 1) != expected(3, 2, 1), "missing restoration control") + dirty_fault = replay([[1, 0], [2, 1]], 1, 2) + require(dirty_fault[:2] == expected(3, 1, 2)[:2], "zero-target positive trap") + require(dirty_fault != expected(3, 1, 2), "dirty-target fault undetected") + reject("radius_guard", lambda: exclude_shorter(expected(1, 1, 1), 10, {}, [])) + return len(failures) + + +def load(path): + def unique(pairs): + data = {} + for key, value in pairs: + require(key not in data, "duplicate JSON key") + data[key] = value + return data + return json.loads(path.read_text(), object_pairs_hook=unique) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--certificate", type=Path, default=PACKAGE / "CERTIFICATE.json") + args = parser.parse_args() + orbits = verify(load(args.certificate)) + negatives = controls() + print("PASS_SHEAR_3X4_TRUTH_TABLES labeled_maps=4096 dirty_inputs_per_map=128 orbits=" + + str(orbits) + " full_GL4=20160 negative_controls=" + str(negatives)) + + +if __name__ == "__main__": + main() diff --git a/research/bit-zero-frame-feedback-3x4/test_certificate.py b/research/bit-zero-frame-feedback-3x4/test_certificate.py new file mode 100644 index 0000000000..2865682889 --- /dev/null +++ b/research/bit-zero-frame-feedback-3x4/test_certificate.py @@ -0,0 +1,90 @@ +#!/usr/bin/env python3 +"""Subprocess corruption and relocation controls for the research certificate. + +Hanson Sun (@bbMisk), with substantial OpenAI Codex assistance. Apache-2.0. +""" +import copy +import importlib.util +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +PACKAGE = Path(__file__).resolve().parent + + +class CertificateControls(unittest.TestCase): + def run_script(self, script, cwd, certificate=None): + command = [sys.executable, "-I", "-O", "-B", str(script)] + if certificate is not None: + command += ["--certificate", str(certificate)] + return subprocess.run(command, cwd=cwd, capture_output=True, text=True, + timeout=90, check=False) + + def test_relocated_optimized_positive_replay(self): + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + relocated = root / "package" + relocated.mkdir() + for name in ("verify.py", "independent.py", "CERTIFICATE.json"): + shutil.copyfile(PACKAGE / name, relocated / name) + for name in ("verify.py", "independent.py"): + with self.subTest(engine=name): + result = self.run_script(relocated / name, root) + self.assertEqual(result.returncode, 0, result.stdout + result.stderr) + self.assertIn("PASS_SHEAR_3X4", result.stdout) + + def test_corrupted_certificates_are_rejected(self): + original = json.loads((PACKAGE / "CERTIFICATE.json").read_text()) + variants = [] + # Same correct endpoint, but the asserted minimum is deliberately too + # large. Only a shorter-word check can rule out the new claimed cost. + inflated = copy.deepcopy(original) + one = next(row for row in inflated["orbits"] if row["minimum"] == 1) + one["restricted_witness"] = [[0, 1], [0, 1]] + one["restricted_witness"] + one["minimum"] += 2 + variants.append(("inflated_minimum_with_valid_word", inflated, + "shorter unrestricted word exists")) + dirty = copy.deepcopy(original) + one = next(row for row in dirty["orbits"] if row["minimum"] == 1) + one["restricted_witness"][0][1] = 1 + variants.append(("wrong_dirty_input_column", dirty, "representative dirty endpoint")) + omitted = copy.deepcopy(original) + omitted["orbits"].pop() + variants.append(("omitted_orbit", omitted, "missing labeled shear")) + spheres = copy.deepcopy(original) + spheres["unrestricted"]["spheres"][-1] -= 1 + variants.append(("incomplete_ball_receipt", spheres, "sphere counts differ")) + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + for label, data, diagnostic in variants: + path = root / (label + ".json") + path.write_text(json.dumps(data)) + for name in ("verify.py", "independent.py"): + with self.subTest(corruption=label, engine=name): + result = self.run_script(PACKAGE / name, root, path) + self.assertNotEqual(result.returncode, 0, result.stdout) + self.assertIn("certificate differs" if name == "verify.py" + else diagnostic, result.stderr) + + def test_predecessor_3x3_census(self): + # Recompute the smaller PR1306 theorem with the new coset method. + # Neither the predecessor implementation nor its certificate is loaded. + spec = importlib.util.spec_from_file_location("coset_checker", PACKAGE / "verify.py") + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + expected = [1, 9, 36, 84, 126, 132, 96, 28] + for feedback, spheres in ( + (False, [1, 21, 264, 2436, 17142]), + (True, [1, 30, 570, 8415, 101610])): + with self.subTest(feedback=feedback): + result = module.census(3, 3, feedback) + self.assertEqual(result["spheres"], spheres) + self.assertEqual([result["lengths"].count(i) for i in range(8)], expected) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/bit-zero-frame-feedback-3x4/verify.py b/research/bit-zero-frame-feedback-3x4/verify.py new file mode 100644 index 0000000000..25fbac67e5 --- /dev/null +++ b/research/bit-zero-frame-feedback-3x4/verify.py @@ -0,0 +1,279 @@ +#!/usr/bin/env python3 +"""Exact dirty-shear minima by complete radius-four shear-coset pairing. + +Hanson Sun (@bbMisk), with substantial OpenAI Codex assistance. Apache-2.0. +The meet-in-the-middle setup follows @commdata2338, PR1306. This implementation +adds simultaneous all-shear coset pairing; no predecessor code is imported. +""" +import argparse +from collections import Counter +from itertools import permutations +import json +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +H, T, RADIUS = 3, 4, 4 + + +class Reject(ValueError): + pass + + +def need(condition, message): + if not condition: + raise Reject(message) + + +def identity(n): + return sum(1 << (i * n + i) for i in range(n)) + + +def step(matrix, gate, n): + destination, source = gate + return matrix ^ (((matrix >> (source * n)) & ((1 << n) - 1)) + << (destination * n)) + + +def target(k, h, t): + n = h + t + return identity(n) ^ sum(((k >> (r * h)) & ((1 << h) - 1)) + << ((h + r) * n) for r in range(t)) + + +def ball(h, t, feedback, radius): + """All complete matrices at distances <= radius, retaining first parents.""" + n = h + t + gates = [(d, s) for d in range(n) for s in range(n) + if d != s and (feedback or not (d < h <= s))] + seen = {identity(n): (0, -1)} + layer, spheres = [identity(n)], [1] + for depth in range(1, radius + 1): + following = [] + for matrix in layer: + for index, gate in enumerate(gates): + reached = step(matrix, gate, n) + if reached not in seen: + seen[reached] = (depth, index) + following.append(reached) + spheres.append(len(following)) + layer = following + return seen, gates, spheres + + +def coset(matrix, h, t): + """Return (representative of M*S, Q), where M*T_Q = representative. + + S consists of all shears T_K. Reduce helper columns modulo the ordered + target-column span, retaining exact coefficients. Invertibility makes + the target columns independent. The key is packed by columns. + """ + n = h + t + columns = [sum(((matrix >> (r * n + c)) & 1) << r for r in range(n)) + for c in range(n)] + basis = {} + for j, column in enumerate(columns[h:]): + coefficient = 1 << j + while column: + pivot = (column & -column).bit_length() - 1 + if pivot not in basis: + basis[pivot] = column, coefficient + break + vector, combination = basis[pivot] + column ^= vector + coefficient ^= combination + else: + raise Reject("dependent target columns") + key, label = 0, 0 + for c in range(h): + column, coefficient = columns[c], 0 + for pivot in sorted(basis): + if column & (1 << pivot): + vector, combination = basis[pivot] + column ^= vector + coefficient ^= combination + key |= column << (n * c) + for r in range(t): + label |= ((coefficient >> r) & 1) << (r * h + c) + for c in range(h, n): + key |= columns[c] << (n * c) + return key, label + + +def word_for(matrix, seen, gates, n): + backwards = [] + while matrix != identity(n): + depth, index = seen[matrix] + gate = gates[index] + backwards.append(list(gate)) + matrix = step(matrix, gate, n) + need(seen[matrix][0] == depth - 1, "BFS parent depth") + return backwards[::-1] + + +def check_word(word, k, h, t, feedback=False): + n, matrix = h + t, identity(h + t) + need(type(word) is list, "word must be a list") + for gate in word: + need(type(gate) is list and len(gate) == 2 + and all(type(index) is int and 0 <= index < n for index in gate), + "typed gate indices") + d, s = gate + need(d != s, "self XOR is not reversible") + need(feedback or not (d < h <= s), "target feedback forbidden") + matrix = step(matrix, gate, n) + need(matrix == target(k, h, t), "complete dirty boundary mismatch") + return len(word) + + +def census(h, t, feedback, radius=RADIUS): + seen, gates, spheres = ball(h, t, feedback, radius) + groups = {} + for matrix, (depth, _) in seen.items(): + key, label = coset(matrix, h, t) + groups.setdefault(key, []).append((label, depth, matrix)) + best = [None] * (1 << (h * t)) + first = identity(h + t) + best[0] = (0, first, first) + pairs = 0 + for group in groups.values(): + for i, (ka, da, a) in enumerate(group): + for kb, db, b in group[i + 1:]: + pairs += 1 + k, cost = ka ^ kb, da + db + if best[k] is None or cost < best[k][0]: + best[k] = cost, a, b + lengths, words, outside = [], [], [] + for k, hit in enumerate(best): + if hit is None: + # Exclusion through 2*radius plus an explicit 2*radius+1 word + # closes the gap. A miss alone never establishes a minimum. + witness = [[h + r, c] for r in range(t) for c in range(h) + if k & (1 << (r * h + c))] + need(len(witness) == 2 * radius + 1, + "insufficient radius: direct witness does not close the gap") + length = len(witness) + outside.append(k) + else: + length, a, b = hit + witness = (word_for(b, seen, gates, h + t) + + word_for(a, seen, gates, h + t)[::-1]) + need(check_word(witness, k, h, t, feedback) == length, "witness length") + lengths.append(length) + words.append(witness) + return {"spheres": spheres, "cosets": len(groups), + "unordered_distinct_pairs": pairs, "outside_double_radius": outside, + "lengths": lengths, "words": words} + + +def orbit(k, h, t): + return {sum(((k >> (r * h + c)) & 1) << (rr * h + cc) + for rr, r in enumerate(rows) for cc, c in enumerate(columns)) + for rows in permutations(range(t)) for columns in permutations(range(h))} + + +def controls(): + rejected = [] + + def reject(name, action): + try: + action() + except Reject: + rejected.append(name) + else: + raise Reject("negative control accepted: " + name) + + star = [[0, 1], [2, 0], [0, 1]] + check_word(star, 3, 2, 1) + feedback = [[0, 1], [1, 0], [0, 1], [1, 0], [0, 1]] + check_word(feedback, 1, 1, 1, True) + reject("unrestored_helper", lambda: check_word(star[:-1], 3, 2, 1)) + reject("dirty_target_mixing", lambda: check_word([[1, 0], [2, 1]], 3, 1, 2)) + reject("wrong_helper_input", lambda: check_word([[2, 0]], 3, 2, 1)) + reject("feedback_in_restricted_alphabet", lambda: check_word(feedback, 1, 1, 1)) + reject("noninvertible_self_xor", lambda: check_word([[0, 0]], 0, 1, 1)) + reject("boolean_gate_index", lambda: check_word([[True, 0]], 1, 1, 1)) + reject("insufficient_radius", lambda: census(2, 2, True, 1)) + small, _, _ = ball(1, 2, True, 6) + need(len(small) == 168, "GL3 positive control incomplete") + fibers = Counter() + for matrix in small: + key, label = coset(matrix, 1, 2) + fibers[key] += 1 + for k in range(4): + product, right = 0, target(k, 1, 2) + for row in range(3): + value = 0 + for col in range(3): + if matrix & (1 << (row * 3 + col)): + value ^= (right >> (col * 3)) & 7 + product |= value << (row * 3) + need(coset(product, 1, 2) == (key, label ^ k), "coset product control") + need(len(fibers) == 42 and set(fibers.values()) == {4}, "complete coset fibers") + return {"positive_star_cost": 3, "positive_feedback_cost": 5, + "gl3_matrices": 168, "exact_coset_products": 672, + "negative_controls": rejected} + + +def build(): + restricted = census(H, T, False) + unrestricted = census(H, T, True) + need(restricted["lengths"] == unrestricted["lengths"], + "feedback saving found; do not issue a no-gain certificate") + missing = restricted["outside_double_radius"] + need(missing == unrestricted["outside_double_radius"], "different radius misses") + expected_missing = [k for k in range(1 << (H * T)) + if sorted((k >> (r * H)) & 7 for r in range(T)) == [3, 5, 6, 7]] + need(missing == expected_missing and len(missing) == 24, "nine-gate class") + remaining, representatives = set(range(1 << (H * T))), [] + while remaining: + k = min(remaining) + members = orbit(k, H, T) + need(members <= remaining, "orbit partition") + length = restricted["lengths"][k] + need(all(restricted["lengths"][other] == length for other in members), + "orbit costs differ") + representatives.append({"k": k, "orbit_size": len(members), "minimum": length, + "restricted_witness": restricted["words"][k]}) + remaining -= members + def stats(result): + return {key: value for key, value in result.items() if key not in ("lengths", "words")} + histogram = Counter(restricted["lengths"]) + return {"schema_version": 1, "helpers": H, "targets": T, + "maps": 1 << (H * T), "gate_cost": 1, "ancillas": 0, + "all_inputs_arbitrary": True, "radius": RADIUS, "feedback_gains": 0, + "minimum_histogram": [histogram[i] for i in range(10)], + "restricted": stats(restricted), "unrestricted": stats(unrestricted), + "orbits": representatives, "controls": controls()} + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":"), allow_nan=False) + + +def load(path): + def unique(pairs): + data = {} + for key, value in pairs: + need(key not in data, "duplicate JSON key") + data[key] = value + return data + return json.loads(path.read_text(), object_pairs_hook=unique) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", action="store_true") + parser.add_argument("--certificate", type=Path, default=PACKAGE / "CERTIFICATE.json") + args = parser.parse_args() + result = build() + if args.write: + args.certificate.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n") + else: + need(canonical(load(args.certificate)) == canonical(result), + "certificate differs from complete exact regeneration") + print("PASS_SHEAR_3X4_COSETS maps=4096 orbits=" + str(len(result["orbits"])) + + " max_minimum=9 feedback_gains=0 no_new_kappa") + + +if __name__ == "__main__": + main()