diff --git a/research/hadamard-readout-census/CERTIFICATE.json b/research/hadamard-readout-census/CERTIFICATE.json new file mode 100644 index 0000000000..505e839d10 --- /dev/null +++ b/research/hadamard-readout-census/CERTIFICATE.json @@ -0,0 +1,4162 @@ +{ + "A_leaf_prices": [ + 4, + 10, + 16, + 28 + ], + "A_lengths": [ + 2, + 3, + 4, + 5 + ], + "B_leaf_prices": [ + 1, + 4, + 10, + 16 + ], + "B_lengths": [ + 1, + 2, + 3, + 4 + ], + "assignment_seed": 55, + "base_commit": "ce7ad1b6ab09452c3478723a2e96ed5ff212dc08", + "chosen_profile": [ + 8, + 4, + 2, + 2 + ], + "first_signs": [ + -1, + 1, + -1, + -1 + ], + "format": "hadamard-readout-census/1", + "frontier_words": [ + { + "profile": [ + 2, + 2, + 4, + 8 + ], + "word": [ + [ + "A", + 2, + 1 + ], + [ + "A", + 3, + 1 + ], + [ + "A", + 3, + 1 + ], + [ + "B", + 0, + -1 + ], + [ + "A", + 1, + -1 + ], + [ + "A", + 3, + -1 + ], + [ + "A", + 3, + -1 + ], + [ + "A", + 3, + -1 + ], + [ + "B", + 1, + -1 + ], + [ + "A", + 2, + -1 + ], + [ + "A", + 3, + 1 + ], + [ + "A", + 3, + 1 + ], + [ + "B", + 3, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "B", + 0, + 1 + ], + [ + "A", + 2, + 1 + ], + [ + "B", + 2, + 1 + ], + [ + "A", + 1, + 1 + ], + [ + "A", + 3, + -1 + ], + [ + "B", + 3, + 1 + ], + [ + "A", + 2, + -1 + ], + [ + "B", + 1, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "B", + 2, + -1 + ] + ] + }, + { + "profile": [ + 2, + 2, + 6, + 6 + ], + "word": [ + [ + "A", + 2, + 1 + ], + [ + "A", + 3, + 1 + ], + [ + "A", + 3, + 1 + ], + [ + "B", + 0, + -1 + ], + [ + "A", + 1, + -1 + ], + [ + "A", + 3, + -1 + ], + [ + "A", + 3, + -1 + ], + [ + "B", + 1, + -1 + ], + [ + "A", + 2, + -1 + ], + [ + "A", + 2, + -1 + ], + [ + "A", + 3, + 1 + ], + [ + "B", + 3, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 2, + 1 + ], + [ + "B", + 0, + 1 + ], + [ + "A", + 2, + 1 + ], + [ + "B", + 2, + 1 + ], + [ + "A", + 1, + 1 + ], + [ + "A", + 2, + -1 + ], + [ + "B", + 1, + 1 + ], + [ + "A", + 3, + -1 + ], + [ + "B", + 3, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "B", + 2, + -1 + ] + ] + }, + { + "profile": [ + 2, + 2, + 8, + 4 + ], + "word": [ + [ + "A", + 2, + 1 + ], + [ + "A", + 2, + 1 + ], + [ + "A", + 3, + 1 + ], + [ + "B", + 0, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 2, + -1 + ], + [ + "A", + 2, + -1 + ], + [ + "A", + 2, + -1 + ], + [ + "B", + 1, + 1 + ], + [ + "A", + 2, + 1 + ], + [ + "A", + 2, + 1 + ], + [ + "A", + 3, + -1 + ], + [ + "B", + 3, + 1 + ], + [ + "A", + 1, + -1 + ], + [ + "B", + 0, + 1 + ], + [ + "A", + 3, + 1 + ], + [ + "B", + 2, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "A", + 2, + -1 + ], + [ + "B", + 3, + -1 + ], + [ + "A", + 3, + -1 + ], + [ + "B", + 1, + -1 + ], + [ + "A", + 1, + 1 + ], + [ + "B", + 2, + -1 + ] + ] + }, + { + "profile": [ + 2, + 4, + 2, + 8 + ], + "word": [ + [ + "A", + 2, + 1 + ], + [ + "A", + 3, + 1 + ], + [ + "B", + 0, + -1 + ], + [ + "A", + 1, + -1 + ], + [ + "A", + 3, + -1 + ], + [ + "A", + 3, + -1 + ], + [ + "B", + 1, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 3, + 1 + ], + [ + "A", + 3, + 1 + ], + [ + "B", + 2, + 1 + ], + [ + "A", + 1, + 1 + ], + [ + "A", + 3, + -1 + ], + [ + "A", + 3, + -1 + ], + [ + "B", + 3, + 1 + ], + [ + "A", + 2, + -1 + ], + [ + "A", + 3, + 1 + ], + [ + "B", + 1, + 1 + ], + [ + "A", + 1, + -1 + ], + [ + "B", + 0, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "B", + 3, + -1 + ], + [ + "A", + 1, + 1 + ], + [ + "B", + 2, + -1 + ] + ] + }, + { + "profile": [ + 2, + 4, + 4, + 4 + ], + "word": [ + [ + "A", + 2, + 1 + ], + [ + "A", + 2, + 1 + ], + [ + "B", + 0, + -1 + ], + [ + "A", + 1, + -1 + ], + [ + "A", + 3, + -1 + ], + [ + "B", + 1, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 2, + -1 + ], + [ + "B", + 0, + 1 + ], + [ + "A", + 1, + 1 + ], + [ + "A", + 3, + 1 + ], + [ + "B", + 1, + 1 + ], + [ + "B", + 2, + 1 + ], + [ + "A", + 1, + 1 + ], + [ + "A", + 3, + -1 + ], + [ + "B", + 3, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "A", + 2, + -1 + ], + [ + "B", + 2, + -1 + ], + [ + "A", + 1, + -1 + ], + [ + "A", + 3, + 1 + ], + [ + "B", + 3, + -1 + ] + ] + }, + { + "profile": [ + 2, + 4, + 8, + 2 + ], + "word": [ + [ + "A", + 1, + 1 + ], + [ + "A", + 2, + 1 + ], + [ + "A", + 2, + 1 + ], + [ + "B", + 0, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 2, + -1 + ], + [ + "A", + 2, + -1 + ], + [ + "A", + 2, + -1 + ], + [ + "B", + 1, + 1 + ], + [ + "A", + 1, + -1 + ], + [ + "A", + 2, + 1 + ], + [ + "A", + 2, + 1 + ], + [ + "B", + 2, + 1 + ], + [ + "A", + 3, + -1 + ], + [ + "B", + 0, + 1 + ], + [ + "A", + 1, + 1 + ], + [ + "B", + 3, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "A", + 2, + -1 + ], + [ + "B", + 2, + -1 + ], + [ + "A", + 1, + -1 + ], + [ + "B", + 1, + -1 + ], + [ + "A", + 3, + 1 + ], + [ + "B", + 3, + -1 + ] + ] + }, + { + "profile": [ + 2, + 6, + 2, + 6 + ], + "word": [ + [ + "A", + 0, + 1 + ], + [ + "A", + 3, + 1 + ], + [ + "B", + 0, + -1 + ], + [ + "A", + 1, + -1 + ], + [ + "A", + 1, + -1 + ], + [ + "A", + 3, + -1 + ], + [ + "A", + 3, + -1 + ], + [ + "B", + 1, + -1 + ], + [ + "A", + 1, + 1 + ], + [ + "A", + 1, + 1 + ], + [ + "A", + 2, + -1 + ], + [ + "B", + 2, + -1 + ], + [ + "A", + 1, + -1 + ], + [ + "A", + 3, + 1 + ], + [ + "A", + 3, + 1 + ], + [ + "B", + 3, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 3, + -1 + ], + [ + "B", + 0, + 1 + ], + [ + "B", + 1, + 1 + ], + [ + "A", + 2, + 1 + ], + [ + "B", + 2, + 1 + ], + [ + "A", + 1, + 1 + ], + [ + "B", + 3, + 1 + ] + ] + }, + { + "profile": [ + 2, + 6, + 6, + 2 + ], + "word": [ + [ + "A", + 1, + 1 + ], + [ + "A", + 1, + 1 + ], + [ + "A", + 2, + 1 + ], + [ + "B", + 0, + -1 + ], + [ + "A", + 1, + -1 + ], + [ + "A", + 1, + -1 + ], + [ + "A", + 3, + -1 + ], + [ + "B", + 1, + -1 + ], + [ + "A", + 1, + 1 + ], + [ + "A", + 2, + -1 + ], + [ + "A", + 2, + -1 + ], + [ + "B", + 2, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 2, + 1 + ], + [ + "B", + 0, + 1 + ], + [ + "A", + 2, + 1 + ], + [ + "B", + 3, + 1 + ], + [ + "A", + 2, + -1 + ], + [ + "A", + 3, + 1 + ], + [ + "B", + 1, + 1 + ], + [ + "A", + 1, + -1 + ], + [ + "B", + 2, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "B", + 3, + -1 + ] + ] + }, + { + "profile": [ + 2, + 8, + 2, + 4 + ], + "word": [ + [ + "A", + 0, + 1 + ], + [ + "A", + 1, + 1 + ], + [ + "B", + 0, + -1 + ], + [ + "A", + 1, + -1 + ], + [ + "A", + 1, + -1 + ], + [ + "A", + 3, + -1 + ], + [ + "B", + 1, + -1 + ], + [ + "A", + 1, + 1 + ], + [ + "A", + 1, + 1 + ], + [ + "A", + 2, + -1 + ], + [ + "B", + 2, + -1 + ], + [ + "A", + 1, + -1 + ], + [ + "A", + 1, + -1 + ], + [ + "A", + 3, + 1 + ], + [ + "B", + 3, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 1, + 1 + ], + [ + "B", + 1, + 1 + ], + [ + "A", + 3, + -1 + ], + [ + "B", + 0, + 1 + ], + [ + "A", + 2, + 1 + ], + [ + "B", + 3, + 1 + ], + [ + "A", + 3, + 1 + ], + [ + "B", + 2, + 1 + ] + ] + }, + { + "profile": [ + 2, + 8, + 4, + 2 + ], + "word": [ + [ + "A", + 1, + 1 + ], + [ + "A", + 1, + 1 + ], + [ + "A", + 2, + 1 + ], + [ + "B", + 0, + -1 + ], + [ + "A", + 1, + -1 + ], + [ + "A", + 1, + -1 + ], + [ + "A", + 1, + -1 + ], + [ + "A", + 3, + -1 + ], + [ + "B", + 1, + -1 + ], + [ + "A", + 1, + 1 + ], + [ + "A", + 1, + 1 + ], + [ + "A", + 2, + -1 + ], + [ + "B", + 2, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "B", + 0, + 1 + ], + [ + "A", + 2, + 1 + ], + [ + "B", + 3, + 1 + ], + [ + "A", + 1, + -1 + ], + [ + "A", + 3, + 1 + ], + [ + "B", + 2, + 1 + ], + [ + "A", + 2, + -1 + ], + [ + "B", + 1, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "B", + 3, + -1 + ] + ] + }, + { + "profile": [ + 4, + 2, + 2, + 8 + ], + "word": [ + [ + "A", + 0, + 1 + ], + [ + "A", + 3, + 1 + ], + [ + "A", + 3, + 1 + ], + [ + "B", + 0, + -1 + ], + [ + "A", + 1, + -1 + ], + [ + "A", + 3, + -1 + ], + [ + "A", + 3, + -1 + ], + [ + "A", + 3, + -1 + ], + [ + "B", + 1, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 3, + 1 + ], + [ + "A", + 3, + 1 + ], + [ + "B", + 2, + 1 + ], + [ + "A", + 2, + -1 + ], + [ + "B", + 0, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "B", + 3, + -1 + ], + [ + "A", + 1, + 1 + ], + [ + "A", + 3, + -1 + ], + [ + "B", + 2, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "B", + 1, + 1 + ], + [ + "A", + 2, + 1 + ], + [ + "B", + 3, + 1 + ] + ] + }, + { + "profile": [ + 4, + 2, + 4, + 4 + ], + "word": [ + [ + "A", + 3, + 1 + ], + [ + "A", + 3, + 1 + ], + [ + "B", + 0, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 2, + -1 + ], + [ + "B", + 1, + 1 + ], + [ + "A", + 1, + -1 + ], + [ + "A", + 3, + -1 + ], + [ + "B", + 0, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "A", + 2, + 1 + ], + [ + "B", + 1, + -1 + ], + [ + "B", + 2, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "A", + 2, + -1 + ], + [ + "B", + 3, + -1 + ], + [ + "A", + 1, + 1 + ], + [ + "A", + 3, + -1 + ], + [ + "B", + 2, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 2, + 1 + ], + [ + "B", + 3, + 1 + ] + ] + }, + { + "profile": [ + 4, + 2, + 8, + 2 + ], + "word": [ + [ + "A", + 2, + 1 + ], + [ + "A", + 3, + 1 + ], + [ + "B", + 0, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 2, + -1 + ], + [ + "A", + 2, + -1 + ], + [ + "B", + 1, + 1 + ], + [ + "A", + 1, + -1 + ], + [ + "A", + 2, + 1 + ], + [ + "A", + 2, + 1 + ], + [ + "B", + 2, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "A", + 2, + -1 + ], + [ + "A", + 2, + -1 + ], + [ + "B", + 3, + -1 + ], + [ + "A", + 2, + 1 + ], + [ + "A", + 3, + -1 + ], + [ + "B", + 1, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "B", + 0, + 1 + ], + [ + "A", + 1, + 1 + ], + [ + "B", + 3, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "B", + 2, + -1 + ] + ] + }, + { + "profile": [ + 4, + 4, + 2, + 4 + ], + "word": [ + [ + "A", + 0, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "B", + 0, + -1 + ], + [ + "A", + 1, + -1 + ], + [ + "A", + 3, + -1 + ], + [ + "B", + 1, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 2, + -1 + ], + [ + "B", + 0, + 1 + ], + [ + "A", + 1, + 1 + ], + [ + "A", + 3, + 1 + ], + [ + "B", + 1, + 1 + ], + [ + "B", + 2, + -1 + ], + [ + "A", + 1, + -1 + ], + [ + "A", + 3, + 1 + ], + [ + "B", + 3, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 2, + 1 + ], + [ + "B", + 2, + 1 + ], + [ + "A", + 1, + 1 + ], + [ + "A", + 3, + -1 + ], + [ + "B", + 3, + 1 + ] + ] + }, + { + "profile": [ + 4, + 4, + 4, + 2 + ], + "word": [ + [ + "A", + 1, + 1 + ], + [ + "A", + 1, + 1 + ], + [ + "B", + 0, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 2, + -1 + ], + [ + "B", + 1, + 1 + ], + [ + "A", + 1, + -1 + ], + [ + "A", + 3, + -1 + ], + [ + "B", + 0, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "A", + 2, + 1 + ], + [ + "B", + 1, + -1 + ], + [ + "B", + 2, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 2, + 1 + ], + [ + "B", + 3, + 1 + ], + [ + "A", + 1, + -1 + ], + [ + "A", + 3, + 1 + ], + [ + "B", + 2, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "A", + 2, + -1 + ], + [ + "B", + 3, + -1 + ] + ] + }, + { + "profile": [ + 4, + 8, + 2, + 2 + ], + "word": [ + [ + "A", + 0, + 1 + ], + [ + "A", + 1, + 1 + ], + [ + "A", + 1, + 1 + ], + [ + "B", + 0, + -1 + ], + [ + "A", + 1, + -1 + ], + [ + "A", + 1, + -1 + ], + [ + "A", + 1, + -1 + ], + [ + "A", + 3, + -1 + ], + [ + "B", + 1, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 1, + 1 + ], + [ + "A", + 1, + 1 + ], + [ + "B", + 3, + 1 + ], + [ + "A", + 2, + -1 + ], + [ + "B", + 0, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "B", + 2, + -1 + ], + [ + "A", + 1, + -1 + ], + [ + "A", + 3, + 1 + ], + [ + "B", + 3, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "B", + 1, + 1 + ], + [ + "A", + 2, + 1 + ], + [ + "B", + 2, + 1 + ] + ] + }, + { + "profile": [ + 6, + 2, + 2, + 6 + ], + "word": [ + [ + "A", + 0, + 1 + ], + [ + "A", + 3, + 1 + ], + [ + "A", + 3, + 1 + ], + [ + "B", + 0, + -1 + ], + [ + "A", + 1, + -1 + ], + [ + "A", + 3, + -1 + ], + [ + "A", + 3, + -1 + ], + [ + "B", + 1, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 3, + 1 + ], + [ + "B", + 2, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "A", + 2, + -1 + ], + [ + "B", + 0, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "B", + 3, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 1, + 1 + ], + [ + "B", + 1, + 1 + ], + [ + "A", + 3, + -1 + ], + [ + "B", + 2, + -1 + ], + [ + "A", + 2, + 1 + ], + [ + "B", + 3, + 1 + ] + ] + }, + { + "profile": [ + 6, + 2, + 6, + 2 + ], + "word": [ + [ + "A", + 1, + 1 + ], + [ + "A", + 2, + 1 + ], + [ + "B", + 0, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 2, + -1 + ], + [ + "A", + 2, + -1 + ], + [ + "B", + 1, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "A", + 3, + -1 + ], + [ + "B", + 2, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 2, + 1 + ], + [ + "A", + 2, + 1 + ], + [ + "B", + 3, + 1 + ], + [ + "A", + 1, + -1 + ], + [ + "A", + 2, + -1 + ], + [ + "B", + 0, + 1 + ], + [ + "B", + 1, + -1 + ], + [ + "A", + 3, + 1 + ], + [ + "B", + 2, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "B", + 3, + -1 + ] + ] + }, + { + "profile": [ + 6, + 6, + 2, + 2 + ], + "word": [ + [ + "A", + 0, + 1 + ], + [ + "A", + 1, + 1 + ], + [ + "A", + 1, + 1 + ], + [ + "B", + 0, + -1 + ], + [ + "A", + 1, + -1 + ], + [ + "A", + 1, + -1 + ], + [ + "A", + 3, + -1 + ], + [ + "B", + 1, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 1, + 1 + ], + [ + "B", + 3, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "A", + 2, + -1 + ], + [ + "B", + 0, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "B", + 2, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 3, + 1 + ], + [ + "B", + 1, + 1 + ], + [ + "A", + 1, + -1 + ], + [ + "B", + 3, + -1 + ], + [ + "A", + 2, + 1 + ], + [ + "B", + 2, + 1 + ] + ] + }, + { + "profile": [ + 8, + 2, + 2, + 4 + ], + "word": [ + [ + "A", + 0, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "A", + 3, + 1 + ], + [ + "B", + 0, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 2, + -1 + ], + [ + "B", + 1, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "A", + 3, + -1 + ], + [ + "B", + 2, + -1 + ], + [ + "A", + 1, + -1 + ], + [ + "B", + 0, + 1 + ], + [ + "A", + 3, + 1 + ], + [ + "B", + 3, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 2, + 1 + ], + [ + "B", + 2, + 1 + ], + [ + "A", + 3, + -1 + ], + [ + "B", + 1, + -1 + ], + [ + "A", + 1, + 1 + ], + [ + "B", + 3, + 1 + ] + ] + }, + { + "profile": [ + 8, + 2, + 4, + 2 + ], + "word": [ + [ + "A", + 0, + 1 + ], + [ + "A", + 1, + 1 + ], + [ + "B", + 0, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 2, + -1 + ], + [ + "B", + 1, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "A", + 3, + -1 + ], + [ + "B", + 2, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 2, + 1 + ], + [ + "B", + 3, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "A", + 1, + -1 + ], + [ + "B", + 1, + -1 + ], + [ + "A", + 2, + -1 + ], + [ + "B", + 0, + 1 + ], + [ + "A", + 3, + 1 + ], + [ + "B", + 3, + -1 + ], + [ + "A", + 2, + 1 + ], + [ + "B", + 2, + 1 + ] + ] + }, + { + "profile": [ + 8, + 4, + 2, + 2 + ], + "word": [ + [ + "A", + 0, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "A", + 1, + 1 + ], + [ + "B", + 0, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 2, + -1 + ], + [ + "B", + 1, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "A", + 1, + -1 + ], + [ + "B", + 3, + -1 + ], + [ + "A", + 3, + -1 + ], + [ + "B", + 0, + 1 + ], + [ + "A", + 1, + 1 + ], + [ + "B", + 2, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 2, + 1 + ], + [ + "B", + 3, + 1 + ], + [ + "A", + 1, + -1 + ], + [ + "B", + 1, + -1 + ], + [ + "A", + 3, + 1 + ], + [ + "B", + 2, + 1 + ] + ] + } + ], + "minimum_leaf_calls": 222, + "minimum_queries": 22, + "pareto_profiles": [ + [ + 2, + 2, + 4, + 8 + ], + [ + 2, + 2, + 6, + 6 + ], + [ + 2, + 2, + 8, + 4 + ], + [ + 2, + 4, + 2, + 8 + ], + [ + 2, + 4, + 4, + 4 + ], + [ + 2, + 4, + 8, + 2 + ], + [ + 2, + 6, + 2, + 6 + ], + [ + 2, + 6, + 6, + 2 + ], + [ + 2, + 8, + 2, + 4 + ], + [ + 2, + 8, + 4, + 2 + ], + [ + 4, + 2, + 2, + 8 + ], + [ + 4, + 2, + 4, + 4 + ], + [ + 4, + 2, + 8, + 2 + ], + [ + 4, + 4, + 2, + 4 + ], + [ + 4, + 4, + 4, + 2 + ], + [ + 4, + 8, + 2, + 2 + ], + [ + 6, + 2, + 2, + 6 + ], + [ + 6, + 2, + 6, + 2 + ], + [ + 6, + 6, + 2, + 2 + ], + [ + 8, + 2, + 2, + 4 + ], + [ + 8, + 2, + 4, + 2 + ], + [ + 8, + 4, + 2, + 2 + ] + ], + "profile_histogram": [ + { + "paths": 32, + "profile": [ + 2, + 2, + 4, + 8 + ] + }, + { + "paths": 192, + "profile": [ + 2, + 2, + 6, + 6 + ] + }, + { + "paths": 32, + "profile": [ + 2, + 2, + 8, + 4 + ] + }, + { + "paths": 32, + "profile": [ + 2, + 4, + 2, + 8 + ] + }, + { + "paths": 576, + "profile": [ + 2, + 4, + 4, + 4 + ] + }, + { + "paths": 768, + "profile": [ + 2, + 4, + 4, + 6 + ] + }, + { + "paths": 128, + "profile": [ + 2, + 4, + 4, + 8 + ] + }, + { + "paths": 768, + "profile": [ + 2, + 4, + 6, + 4 + ] + }, + { + "paths": 128, + "profile": [ + 2, + 4, + 6, + 6 + ] + }, + { + "paths": 32, + "profile": [ + 2, + 4, + 6, + 8 + ] + }, + { + "paths": 32, + "profile": [ + 2, + 4, + 8, + 2 + ] + }, + { + "paths": 128, + "profile": [ + 2, + 4, + 8, + 4 + ] + }, + { + "paths": 32, + "profile": [ + 2, + 4, + 8, + 6 + ] + }, + { + "paths": 192, + "profile": [ + 2, + 6, + 2, + 6 + ] + }, + { + "paths": 768, + "profile": [ + 2, + 6, + 4, + 4 + ] + }, + { + "paths": 128, + "profile": [ + 2, + 6, + 4, + 6 + ] + }, + { + "paths": 32, + "profile": [ + 2, + 6, + 4, + 8 + ] + }, + { + "paths": 192, + "profile": [ + 2, + 6, + 6, + 2 + ] + }, + { + "paths": 128, + "profile": [ + 2, + 6, + 6, + 4 + ] + }, + { + "paths": 32, + "profile": [ + 2, + 6, + 8, + 4 + ] + }, + { + "paths": 32, + "profile": [ + 2, + 8, + 2, + 4 + ] + }, + { + "paths": 32, + "profile": [ + 2, + 8, + 4, + 2 + ] + }, + { + "paths": 128, + "profile": [ + 2, + 8, + 4, + 4 + ] + }, + { + "paths": 32, + "profile": [ + 2, + 8, + 4, + 6 + ] + }, + { + "paths": 32, + "profile": [ + 2, + 8, + 6, + 4 + ] + }, + { + "paths": 32, + "profile": [ + 4, + 2, + 2, + 8 + ] + }, + { + "paths": 576, + "profile": [ + 4, + 2, + 4, + 4 + ] + }, + { + "paths": 768, + "profile": [ + 4, + 2, + 4, + 6 + ] + }, + { + "paths": 128, + "profile": [ + 4, + 2, + 4, + 8 + ] + }, + { + "paths": 768, + "profile": [ + 4, + 2, + 6, + 4 + ] + }, + { + "paths": 128, + "profile": [ + 4, + 2, + 6, + 6 + ] + }, + { + "paths": 32, + "profile": [ + 4, + 2, + 6, + 8 + ] + }, + { + "paths": 32, + "profile": [ + 4, + 2, + 8, + 2 + ] + }, + { + "paths": 128, + "profile": [ + 4, + 2, + 8, + 4 + ] + }, + { + "paths": 32, + "profile": [ + 4, + 2, + 8, + 6 + ] + }, + { + "paths": 576, + "profile": [ + 4, + 4, + 2, + 4 + ] + }, + { + "paths": 768, + "profile": [ + 4, + 4, + 2, + 6 + ] + }, + { + "paths": 128, + "profile": [ + 4, + 4, + 2, + 8 + ] + }, + { + "paths": 576, + "profile": [ + 4, + 4, + 4, + 2 + ] + }, + { + "paths": 2688, + "profile": [ + 4, + 4, + 4, + 4 + ] + }, + { + "paths": 2688, + "profile": [ + 4, + 4, + 4, + 6 + ] + }, + { + "paths": 96, + "profile": [ + 4, + 4, + 4, + 8 + ] + }, + { + "paths": 768, + "profile": [ + 4, + 4, + 6, + 2 + ] + }, + { + "paths": 2688, + "profile": [ + 4, + 4, + 6, + 4 + ] + }, + { + "paths": 1024, + "profile": [ + 4, + 4, + 6, + 6 + ] + }, + { + "paths": 128, + "profile": [ + 4, + 4, + 6, + 8 + ] + }, + { + "paths": 128, + "profile": [ + 4, + 4, + 8, + 2 + ] + }, + { + "paths": 96, + "profile": [ + 4, + 4, + 8, + 4 + ] + }, + { + "paths": 128, + "profile": [ + 4, + 4, + 8, + 6 + ] + }, + { + "paths": 768, + "profile": [ + 4, + 6, + 2, + 4 + ] + }, + { + "paths": 128, + "profile": [ + 4, + 6, + 2, + 6 + ] + }, + { + "paths": 32, + "profile": [ + 4, + 6, + 2, + 8 + ] + }, + { + "paths": 768, + "profile": [ + 4, + 6, + 4, + 2 + ] + }, + { + "paths": 2688, + "profile": [ + 4, + 6, + 4, + 4 + ] + }, + { + "paths": 1024, + "profile": [ + 4, + 6, + 4, + 6 + ] + }, + { + "paths": 128, + "profile": [ + 4, + 6, + 4, + 8 + ] + }, + { + "paths": 128, + "profile": [ + 4, + 6, + 6, + 2 + ] + }, + { + "paths": 1024, + "profile": [ + 4, + 6, + 6, + 4 + ] + }, + { + "paths": 384, + "profile": [ + 4, + 6, + 6, + 6 + ] + }, + { + "paths": 32, + "profile": [ + 4, + 6, + 8, + 2 + ] + }, + { + "paths": 128, + "profile": [ + 4, + 6, + 8, + 4 + ] + }, + { + "paths": 32, + "profile": [ + 4, + 8, + 2, + 2 + ] + }, + { + "paths": 128, + "profile": [ + 4, + 8, + 2, + 4 + ] + }, + { + "paths": 32, + "profile": [ + 4, + 8, + 2, + 6 + ] + }, + { + "paths": 128, + "profile": [ + 4, + 8, + 4, + 2 + ] + }, + { + "paths": 96, + "profile": [ + 4, + 8, + 4, + 4 + ] + }, + { + "paths": 128, + "profile": [ + 4, + 8, + 4, + 6 + ] + }, + { + "paths": 32, + "profile": [ + 4, + 8, + 6, + 2 + ] + }, + { + "paths": 128, + "profile": [ + 4, + 8, + 6, + 4 + ] + }, + { + "paths": 192, + "profile": [ + 6, + 2, + 2, + 6 + ] + }, + { + "paths": 768, + "profile": [ + 6, + 2, + 4, + 4 + ] + }, + { + "paths": 128, + "profile": [ + 6, + 2, + 4, + 6 + ] + }, + { + "paths": 32, + "profile": [ + 6, + 2, + 4, + 8 + ] + }, + { + "paths": 192, + "profile": [ + 6, + 2, + 6, + 2 + ] + }, + { + "paths": 128, + "profile": [ + 6, + 2, + 6, + 4 + ] + }, + { + "paths": 32, + "profile": [ + 6, + 2, + 8, + 4 + ] + }, + { + "paths": 768, + "profile": [ + 6, + 4, + 2, + 4 + ] + }, + { + "paths": 128, + "profile": [ + 6, + 4, + 2, + 6 + ] + }, + { + "paths": 32, + "profile": [ + 6, + 4, + 2, + 8 + ] + }, + { + "paths": 768, + "profile": [ + 6, + 4, + 4, + 2 + ] + }, + { + "paths": 2688, + "profile": [ + 6, + 4, + 4, + 4 + ] + }, + { + "paths": 1024, + "profile": [ + 6, + 4, + 4, + 6 + ] + }, + { + "paths": 128, + "profile": [ + 6, + 4, + 4, + 8 + ] + }, + { + "paths": 128, + "profile": [ + 6, + 4, + 6, + 2 + ] + }, + { + "paths": 1024, + "profile": [ + 6, + 4, + 6, + 4 + ] + }, + { + "paths": 384, + "profile": [ + 6, + 4, + 6, + 6 + ] + }, + { + "paths": 32, + "profile": [ + 6, + 4, + 8, + 2 + ] + }, + { + "paths": 128, + "profile": [ + 6, + 4, + 8, + 4 + ] + }, + { + "paths": 192, + "profile": [ + 6, + 6, + 2, + 2 + ] + }, + { + "paths": 128, + "profile": [ + 6, + 6, + 2, + 4 + ] + }, + { + "paths": 128, + "profile": [ + 6, + 6, + 4, + 2 + ] + }, + { + "paths": 1024, + "profile": [ + 6, + 6, + 4, + 4 + ] + }, + { + "paths": 384, + "profile": [ + 6, + 6, + 4, + 6 + ] + }, + { + "paths": 384, + "profile": [ + 6, + 6, + 6, + 4 + ] + }, + { + "paths": 384, + "profile": [ + 6, + 6, + 6, + 6 + ] + }, + { + "paths": 32, + "profile": [ + 6, + 8, + 2, + 4 + ] + }, + { + "paths": 32, + "profile": [ + 6, + 8, + 4, + 2 + ] + }, + { + "paths": 128, + "profile": [ + 6, + 8, + 4, + 4 + ] + }, + { + "paths": 32, + "profile": [ + 8, + 2, + 2, + 4 + ] + }, + { + "paths": 32, + "profile": [ + 8, + 2, + 4, + 2 + ] + }, + { + "paths": 128, + "profile": [ + 8, + 2, + 4, + 4 + ] + }, + { + "paths": 32, + "profile": [ + 8, + 2, + 4, + 6 + ] + }, + { + "paths": 32, + "profile": [ + 8, + 2, + 6, + 4 + ] + }, + { + "paths": 32, + "profile": [ + 8, + 4, + 2, + 2 + ] + }, + { + "paths": 128, + "profile": [ + 8, + 4, + 2, + 4 + ] + }, + { + "paths": 32, + "profile": [ + 8, + 4, + 2, + 6 + ] + }, + { + "paths": 128, + "profile": [ + 8, + 4, + 4, + 2 + ] + }, + { + "paths": 96, + "profile": [ + 8, + 4, + 4, + 4 + ] + }, + { + "paths": 128, + "profile": [ + 8, + 4, + 4, + 6 + ] + }, + { + "paths": 32, + "profile": [ + 8, + 4, + 6, + 2 + ] + }, + { + "paths": 128, + "profile": [ + 8, + 4, + 6, + 4 + ] + }, + { + "paths": 32, + "profile": [ + 8, + 6, + 2, + 4 + ] + }, + { + "paths": 32, + "profile": [ + 8, + 6, + 4, + 2 + ] + }, + { + "paths": 128, + "profile": [ + 8, + 6, + 4, + 4 + ] + } + ], + "scope": "Exactly eight source calls, one positive and one negative per source; arbitrary repeated signed readouts at visited states; exact additive children, one dirty connector, no new kappa", + "signed_paths": 40320, + "source_path": [ + 0, + 1, + 3, + 0, + 2, + 3, + 1, + 2 + ], + "unsigned_paths": 2520, + "word": [ + [ + "A", + 0, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "A", + 1, + 1 + ], + [ + "B", + 0, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 2, + -1 + ], + [ + "B", + 1, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "A", + 1, + -1 + ], + [ + "B", + 3, + -1 + ], + [ + "A", + 3, + -1 + ], + [ + "B", + 0, + 1 + ], + [ + "A", + 1, + 1 + ], + [ + "B", + 2, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 2, + 1 + ], + [ + "B", + 3, + 1 + ], + [ + "A", + 1, + -1 + ], + [ + "B", + 1, + -1 + ], + [ + "A", + 3, + 1 + ], + [ + "B", + 2, + 1 + ] + ] +} diff --git a/research/hadamard-readout-census/CLAIM.json b/research/hadamard-readout-census/CLAIM.json new file mode 100644 index 0000000000..de1d80c9f3 --- /dev/null +++ b/research/hadamard-readout-census/CLAIM.json @@ -0,0 +1,50 @@ +{ + "track": "recursive interfaces", + "assignment_seed": 55, + "randomness": "Operating-system CSPRNG via secrets.randbelow(60); recorded draw", + "base_commit": "ce7ad1b6ab09452c3478723a2e96ed5ff212dc08", + "contributor": "Cinna Davis (@1337isnot1337), with substantial OpenAI Codex assistance", + "coordination": "No pinned GitHub issue at claim time; local claim", + "claimed_at_utc": "2026-10-13T18:59:00Z", + "expected_finish_utc": "2026-10-13T19:25:00Z", + "verification_start_utc": "2026-10-13T19:17:30Z", + "object": "PR997 signed 4x4 Hadamard connector: exactly one positive and one negative source call per source, arbitrary repeated signed readouts at visited states", + "method": "Exhaust all 2520 unsigned on/off paths and 16 first-sign choices; exact minimum readout multiplicities by bounded integer multiset sums, complete Pareto cost profiles, independent literal replay", + "deliverable": "Exact finite census, weighted price envelope, attaining word, complete child recurrence and negative controls; no supplier adoption or new kappa", + "predecessor": { + "pr": 997, + "head": "b3fda8d59436103b195069a6328cbf5d74f73bc0" + }, + "three_candidates": [ + { + "task": "Hosted restoration deferral", + "decision": "Already covered by PR1012; do not repeat" + }, + { + "task": "Rounded borrowed child contracts", + "decision": "Already covered by PR1135; do not repeat" + }, + { + "task": "Signed Hadamard weighted readout census", + "decision": "Chosen: PR997 only samples 4000 paths and bounds readouts to two differences; PR1088 addresses a different 3x3 object" + } + ], + "stopping_rule": "Complete the stated finite domain once, then verify and package one contribution", + "result": { + "status": "Completed research construction and exact finite census; no new kappa", + "pr_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1158", + "completed_at_utc": "2026-10-13T19:21:00Z", + "construction_commit": "dd4261c4208df476fb9a2aca80d95859014f6766", + "coverage": { + "signed_paths": 40320, + "profiles": 114, + "pareto_profiles": 22 + }, + "query_optimum": 22, + "matched_primitive_calls": { + "new": 222, + "pr997": 238 + }, + "validation": "Package and Git-index replay PASS; selected-record check and all 25 related tests PASS; no full cold supplier replay or remote CI claimed" + } +} diff --git a/research/hadamard-readout-census/HANDOFF-OVERLAP.json b/research/hadamard-readout-census/HANDOFF-OVERLAP.json new file mode 100644 index 0000000000..954c8a9854 --- /dev/null +++ b/research/hadamard-readout-census/HANDOFF-OVERLAP.json @@ -0,0 +1,493 @@ +{ + "checked_at_utc": "2026-10-13T19:12:05Z", + "open_count": 767, + "upstream_main": "ce7ad1b6ab09452c3478723a2e96ed5ff212dc08", + "predecessor_head_unchanged": true, + "relevant": [ + { + "author": { + "id": "U_kgDODYXfmQ", + "is_bot": false, + "login": "aliromman", + "name": "Ali Romman" + }, + "headRefOid": "4c35687d7c0da8e6cf33f17e418ecf31c95ff3ad", + "number": 1135, + "title": "Research: exact restoration contracts and resource bounds for rounded borrowing", + "updatedAt": "2026-10-13T18:53:46Z" + }, + { + "author": { + "id": "U_kgDOCt6exg", + "is_bot": false, + "login": "bbMisk", + "name": "" + }, + "headRefOid": "ae95248b3301e3fafe05c1c00020f69edcdceb98", + "number": 1083, + "title": "Scoped formalization: Lean certificate for 945 five-source connector pairings", + "updatedAt": "2026-10-13T17:49:10Z" + }, + { + "author": { + "id": "MDQ6VXNlcjE4NjIyMjg4", + "is_bot": false, + "login": "thakrarsagar", + "name": "" + }, + "headRefOid": "4ceaf380ed41b28dadcc41d2f974f025ac4d8c03", + "number": 1012, + "title": "Research note: restoration deferral is mass-neutral in the hosted T37 recurrence (no new kappa)", + "updatedAt": "2026-10-13T16:38:45Z" + }, + { + "author": { + "id": "U_kgDOCcbgOg", + "is_bot": false, + "login": "1337isnot1337", + "name": "Cinna Davis" + }, + "headRefOid": "b3fda8d59436103b195069a6328cbf5d74f73bc0", + "number": 997, + "title": "Recursive-interface construction: signed Hadamard batch saves 126 leaf calls (no new kappa)", + "updatedAt": "2026-10-13T16:10:07Z" + }, + { + "author": { + "id": "U_kgDOBhaNkw", + "is_bot": false, + "login": "shhxera", + "name": "" + }, + "headRefOid": "8c5e1b557f59bca29139c4c2dcc65edfb808372b", + "number": 822, + "title": "Research: reuse dirty echo connectors (no new kappa)", + "updatedAt": "2026-10-13T06:27:42Z" + } + ], + "new_arrivals": [ + { + "author": { + "id": "MDQ6VXNlcjQ0MDA1Mjc=", + "is_bot": false, + "login": "chafreaky", + "name": "chafreaky" + }, + "headRefOid": "d376209304f05551f975b0ddf6eaa84edc4ae31a", + "number": 1152, + "title": "Conditional \u03ba = 0.001674340686401949: rank-seven helper ends with T37 owner packing", + "updatedAt": "2026-10-13T19:10:53Z" + }, + { + "author": { + "id": "MDQ6VXNlcjE4NjIyMjg4", + "is_bot": false, + "login": "thakrarsagar", + "name": "" + }, + "headRefOid": "fdc24966a64d3494d8560ecbd69e73a329875950", + "number": 1151, + "title": "Tooling: opt-in parallel layer-end controls for the frontier1042 leaver chain, byte-identical receipts, 2.0-2.7x (extends #1059, no new kappa)", + "updatedAt": "2026-10-13T19:10:51Z" + }, + { + "author": { + "id": "MDQ6VXNlcjExNjU5ODM5", + "is_bot": false, + "login": "rohanarun", + "name": "" + }, + "headRefOid": "e72e8e96f3cd2666d08f39ca14a36bd950884f13", + "number": 1150, + "title": "Draft conditional kappa 0.001672705246144198: rank-seven T16 owner exchanges", + "updatedAt": "2026-10-13T19:10:25Z" + }, + { + "author": { + "id": "U_kgDOFDLgvw", + "is_bot": false, + "login": "woklerx", + "name": "" + }, + "headRefOid": "f66dd4019d67a9660921bc204532306b47f4196e", + "number": 1149, + "title": "Independent verification: complex canonical-frame rank identity on every frozen PR1042 edge", + "updatedAt": "2026-10-13T19:09:48Z" + }, + { + "author": { + "id": "MDQ6VXNlcjcwODMwNDM=", + "is_bot": false, + "login": "tomdif", + "name": "Thomas DiFiore" + }, + "headRefOid": "98235a9cf4ce355ec5cf3fac2eca7b3b98a20838", + "number": 1148, + "title": "Conditional \u03ba = 0.001675121647789207: changed k8 entrances, rank-seven ends, and T16 hosting", + "updatedAt": "2026-10-13T19:08:12Z" + }, + { + "author": { + "id": "U_kgDOCSGJmg", + "is_bot": false, + "login": "RaphaelFakhri", + "name": "Raphael Fakhri" + }, + "headRefOid": "0ffb3c804c44150153edd4a377d57685448d944d", + "number": 1147, + "title": "Research: a fifth joint exchange on X4 does not improve \u03ba (complete census)", + "updatedAt": "2026-10-13T19:07:52Z" + }, + { + "author": { + "id": "U_kgDOFGQjRQ", + "is_bot": false, + "login": "pir0u", + "name": "" + }, + "headRefOid": "96f5925144357c8f3dc309b0e664082bc7b22536", + "number": 1146, + "title": "Research/t24 global coupling pir0u", + "updatedAt": "2026-10-13T19:06:14Z" + }, + { + "author": { + "id": "MDQ6VXNlcjU2NTI3MTY=", + "is_bot": false, + "login": "RossRichardson", + "name": "Ross Richardson" + }, + "headRefOid": "fd4d5ffc448361297e717aa30eafed578caf8e61", + "number": 1145, + "title": "Scoped negative result: scratch-free CK/JP8 boundaries need extra primitives", + "updatedAt": "2026-10-13T19:05:27Z" + }, + { + "author": { + "id": "U_kgDOFDLgvw", + "is_bot": false, + "login": "woklerx", + "name": "" + }, + "headRefOid": "3a4da02f15d702f1900d15d55a675afc8d033e9b", + "number": 1144, + "title": "Verification engineering: preserve exact signed P112 audit with bounded modular recovery", + "updatedAt": "2026-10-13T19:04:42Z" + }, + { + "author": { + "id": "U_kgDOFDLgvw", + "is_bot": false, + "login": "woklerx", + "name": "" + }, + "headRefOid": "fee8dc25e104b2c45ddba1ded4dca846794ba32f", + "number": 1143, + "title": "Research: commuting ADD moves cannot escape the selected R480 frame runs", + "updatedAt": "2026-10-13T19:04:29Z" + }, + { + "author": { + "id": "U_kgDOFF-BGQ", + "is_bot": false, + "login": "martinxxx9", + "name": "" + }, + "headRefOid": "0c2873e6ac844b369a5962f06ef0a74ac86cf4a4", + "number": 1142, + "title": "Independent verification: selected PR1042 replay-capsule closure (no new \u03ba)", + "updatedAt": "2026-10-13T18:59:53Z" + } + ], + "finding": "No duplicate 4x4 exhaustive arbitrary-readout census found; PR997 is the direct predecessor and PR1088 has a distinct 3x3 object. PR1103 concerns rectangular output borrowing.", + "immediate_prepublication_refresh": { + "checked_at_utc": "2026-10-13T19:17:16Z", + "all_state_hadamard_query": [ + { + "headRefOid": "b3fda8d59436103b195069a6328cbf5d74f73bc0", + "number": 997, + "state": "OPEN", + "title": "Recursive-interface construction: signed Hadamard batch saves 126 leaf calls (no new kappa)" + }, + { + "headRefOid": "12c4789c61ac843dcd00e2c71e5388d362298b1a", + "number": 897, + "state": "OPEN", + "title": "No new \u03ba: covers of E7 by hyperplane flats are exactly the D4-frame triples; near-covers are the A3s (checked)" + }, + { + "headRefOid": "fa693bff1fc171a3be18fdaddaf1e196ecef9463", + "number": 335, + "state": "OPEN", + "title": "\u03ba = 7.77607473791708458474546e-4: refreshed donors and 54 final retimings" + }, + { + "headRefOid": "c0fa7e1be9e5f9f2316bb1f88e4c77298014492e", + "number": 331, + "state": "OPEN", + "title": "\u03ba = 7.76523967665819025774905e-4: nested donor entrances on the p10b word" + }, + { + "headRefOid": "367f55f22e5f5e3aff47e6437bf0dfbf743bacec", + "number": 334, + "state": "OPEN", + "title": "\u03ba = 7.77596191161693861459874e-4: all-rank donor flow and 52 final retimings" + }, + { + "headRefOid": "6d1faafc1ac58adb885349b2b08813467a938563", + "number": 330, + "state": "OPEN", + "title": "\u03ba = 7.7652200910342944936985e-4: cross-entrance retiming and operational PR327 supplier" + }, + { + "headRefOid": "44a703782a69a897350572b5b078d5292fdbf92d", + "number": 498, + "state": "OPEN", + "title": "Conditional kappa = 0.001301970637653655: geometric intersections and rational paired whole-owner hosting" + }, + { + "headRefOid": "f9136e76568100034aa37337251f93d684496c13", + "number": 332, + "state": "OPEN", + "title": "\u03ba = 7.77268259042371640048112e-4: oriented p10b source and 42 constructed-frame retimings" + }, + { + "headRefOid": "db3f75cdc5f03f3131d48fb220f6bf1958404ff3", + "number": 256, + "state": "OPEN", + "title": "The source-assisted complex word of #233 as one explicit numbered program (gcert/1): reference-checked, 7.547361\u00b710\u207b\u2074 in the Lean-checked five-stage layout (no new \u03ba)" + }, + { + "headRefOid": "a7aeea067ec1e2b7e91b0ecec660512b7cafca26", + "number": 209, + "state": "CLOSED", + "title": "Parallel-effort entry: Lean proof of #130's frame lemma and check of #193's complex word, Fourier side (no \u03ba claim)" + }, + { + "headRefOid": "40ed0456ab1990beb3440e61bb883ccf95fdcea4", + "number": 327, + "state": "OPEN", + "title": "A p = 10 complex supplier: five-stage complex saving 7795/10\u2077 (centre-sharing) and 7737/10\u2077 (#304 recipe), both kernel-checked in Lean (no new \u03ba; raises the complex cap above 7727)" + }, + { + "headRefOid": "b0396aad724fec58630fbd4d13a809c562f18d9e", + "number": 1088, + "state": "MERGED", + "title": "Research: exact weighted optimum for signed 3x3 connector repairs (no new kappa)" + }, + { + "headRefOid": "fa6f102e58feeb50ebc10eac3d0bd41081885e33", + "number": 326, + "state": "CLOSED", + "title": "\u03ba = 7.69571027349774217804511e-4: cross-group exchanges with growing-prime refinement" + }, + { + "headRefOid": "64bccfb67494f7c4549bfb2f186b400a3cfefb42", + "number": 315, + "state": "OPEN", + "title": "Conditional \u03ba = 7.64230861320245e-4: the paired-cube bit word at cube size p = 10 (h = 20, m = 100), with a new centre-sharing complex supplier (+1.21% over #314)" + }, + { + "headRefOid": "39112c2577452fa278489fb9fd77a9aecb2cdc24", + "number": 595, + "state": "MERGED", + "title": "Format limits (no \u03ba claim): certified ceiling \u03ba \u2264 5.1595e-3, spec census, structural lemmas, helper bounds and open problems" + }, + { + "headRefOid": "0eca9340a3df6141b8e71a41638c3937b3522888", + "number": 325, + "state": "OPEN", + "title": "Conditional \u03ba = 7.696840393833340e-4: a stronger p = 10 bit word \u2014 re-annealed pair module, p = 10 local design, balanced cube orientation, tiered reuse matching (+0.71% over #315's word)" + }, + { + "headRefOid": "c8b22bc5c10dba497ac25804e27d9647d818e2ff", + "number": 144, + "state": "MERGED", + "title": "Paired cubes and shared completed cores for conditional kappa = 4.609169e-4" + } + ], + "recent_open_prs": [ + { + "headRefOid": "9821c6e9388f3fc097e94b72be9fa7b41a849527", + "number": 1155, + "title": "Research note: restoration coalescing across a recursion batch (read-free + composable-family boundary; no new kappa)", + "updatedAt": "2026-10-13T19:16:57Z" + }, + { + "headRefOid": "390de2866a03758e7f4ddbb2846e5b2ee4e72154", + "number": 1154, + "title": "Conditional kappa = 0.001673260706543984: adaptive joint kernel demotion on PR1117", + "updatedAt": "2026-10-13T19:14:51Z" + }, + { + "headRefOid": "c744b52d839c52312bc70f90c0530543a5fb205f", + "number": 1153, + "title": "Finite construction: PR1042 R480 sign normalization saves 408 primitives per orientation (no new kappa)", + "updatedAt": "2026-10-13T19:15:14Z" + }, + { + "headRefOid": "d376209304f05551f975b0ddf6eaa84edc4ae31a", + "number": 1152, + "title": "Conditional \u03ba = 0.001674340686401949: rank-seven helper ends with T37 owner packing", + "updatedAt": "2026-10-13T19:10:53Z" + }, + { + "headRefOid": "fdc24966a64d3494d8560ecbd69e73a329875950", + "number": 1151, + "title": "Tooling: opt-in parallel layer-end controls for the frontier1042 leaver chain, byte-identical receipts, 2.0-2.7x (extends #1059, no new kappa)", + "updatedAt": "2026-10-13T19:10:51Z" + }, + { + "headRefOid": "bebf64ffda3fd5128342d19ee6d419b1150b49f7", + "number": 1150, + "title": "Conditional kappa 0.001672716806120974: rank-seven T16 owner exchanges", + "updatedAt": "2026-10-13T19:16:49Z" + }, + { + "headRefOid": "f66dd4019d67a9660921bc204532306b47f4196e", + "number": 1149, + "title": "Independent verification: complex canonical-frame rank identity on every frozen PR1042 edge", + "updatedAt": "2026-10-13T19:09:48Z" + }, + { + "headRefOid": "98235a9cf4ce355ec5cf3fac2eca7b3b98a20838", + "number": 1148, + "title": "Conditional \u03ba = 0.001675121647789207: changed k8 entrances, rank-seven ends, and T16 hosting", + "updatedAt": "2026-10-13T19:08:12Z" + }, + { + "headRefOid": "0ffb3c804c44150153edd4a377d57685448d944d", + "number": 1147, + "title": "Research: a fifth joint exchange on X4 does not improve \u03ba (complete census)", + "updatedAt": "2026-10-13T19:07:52Z" + }, + { + "headRefOid": "96f5925144357c8f3dc309b0e664082bc7b22536", + "number": 1146, + "title": "Research/t24 global coupling pir0u", + "updatedAt": "2026-10-13T19:06:14Z" + }, + { + "headRefOid": "fd4d5ffc448361297e717aa30eafed578caf8e61", + "number": 1145, + "title": "Scoped negative result: scratch-free CK/JP8 boundaries need extra primitives", + "updatedAt": "2026-10-13T19:05:27Z" + }, + { + "headRefOid": "3a4da02f15d702f1900d15d55a675afc8d033e9b", + "number": 1144, + "title": "Verification engineering: preserve exact signed P112 audit with bounded modular recovery", + "updatedAt": "2026-10-13T19:04:42Z" + }, + { + "headRefOid": "fee8dc25e104b2c45ddba1ded4dca846794ba32f", + "number": 1143, + "title": "Research: commuting ADD moves cannot escape the selected R480 frame runs", + "updatedAt": "2026-10-13T19:04:29Z" + }, + { + "headRefOid": "0c2873e6ac844b369a5962f06ef0a74ac86cf4a4", + "number": 1142, + "title": "Independent verification: selected PR1042 replay-capsule closure (no new \u03ba)", + "updatedAt": "2026-10-13T18:59:53Z" + }, + { + "headRefOid": "1627bf208f80e490522343590dd52f38b329e238", + "number": 1141, + "title": "Add a reversible quadratic phase stream with linear scalar work", + "updatedAt": "2026-10-13T18:56:42Z" + }, + { + "headRefOid": "8e2e18b93d8c6b302e540ad5edc767cb98cf1514", + "number": 1140, + "title": "Research: sharp k8 factory register bound and target frame barriers (no new kappa)", + "updatedAt": "2026-10-13T18:56:39Z" + }, + { + "headRefOid": "82da1e827c51d94691134c6aec346357d89622bc", + "number": 1139, + "title": "Research: sharp ten-coordinate threshold for doubly degenerate triple shared nodes", + "updatedAt": "2026-10-13T18:55:51Z" + }, + { + "headRefOid": "fd9661b67b5236a60114a1be296a4e4b7b853359", + "number": 1138, + "title": "Independent verification: exact dirt and label-span atlas for all leaver cell relabelings", + "updatedAt": "2026-10-13T18:55:40Z" + }, + { + "headRefOid": "e3b8fa39ef7378b7e3f8bbcfa6708be21feb18d8", + "number": 1137, + "title": "Tooling: fast exact HPE transport audit for the layer-end controls, 2.53x, 480/480 trials cross-checked (seed 93, no new kappa)", + "updatedAt": "2026-10-13T18:54:54Z" + }, + { + "headRefOid": "e6a8003673d55929be6925b22f9ee645d03c33c3", + "number": 1136, + "title": "Research: two-block native-query encoding theorem and paid boundary obstructions", + "updatedAt": "2026-10-13T18:54:44Z" + }, + { + "headRefOid": "4c35687d7c0da8e6cf33f17e418ecf31c95ff3ad", + "number": 1135, + "title": "Research: exact restoration contracts and resource bounds for rounded borrowing", + "updatedAt": "2026-10-13T18:53:46Z" + }, + { + "headRefOid": "ed5424aa3b6ca32fd5bb2c33a8e6afcd87170160", + "number": 1134, + "title": "Scoped obstruction: P111 query transport exceeds the frozen U8 host budget", + "updatedAt": "2026-10-13T18:52:56Z" + }, + { + "headRefOid": "8301a4698152cf63d3b4992145ecc8621942a6cd", + "number": 1133, + "title": "Research consolidation: rational support descent for fixed-reader single lifts (no new kappa)", + "updatedAt": "2026-10-13T18:53:11Z" + }, + { + "headRefOid": "36a82dd551cd18b8b32c2013ba928f59ad52678c", + "number": 1132, + "title": "Research consolidation: distinguish selected R480 replay from retained R492 evidence", + "updatedAt": "2026-10-13T18:50:31Z" + }, + { + "headRefOid": "fcdc42737b703323d8ed550a528141a482e68e96", + "number": 1131, + "title": "Conditional \u03ba = 0.001674097969905390: seven-slot k8 with T37 whole-owner packing", + "updatedAt": "2026-10-13T19:10:08Z" + }, + { + "headRefOid": "1558508e5cbff0b7c534d1c4cc7a0fb1b7145c1c", + "number": 1130, + "title": "Conditional \u03ba = 0.001673006105142741: eighth triangle slot X54, rank-seven helper ends and T16 owner packing on the eight-slot k8 word", + "updatedAt": "2026-10-13T18:47:31Z" + }, + { + "headRefOid": "a007dc2e1cc7ae7e8f7ec1343e8883fe43259f21", + "number": 1129, + "title": "Conditional \u03ba = 0.001674097969905390: an attaining T37 construction and fixed R480 owner optimum", + "updatedAt": "2026-10-13T19:13:17Z" + }, + { + "headRefOid": "df29b159239b79d7e451d6ddda826a73e0e50a67", + "number": 1128, + "title": "Research: two-sided boundary obstruction for R439 width-seven helpers", + "updatedAt": "2026-10-13T18:45:23Z" + }, + { + "headRefOid": "2e9dc9d3356a6b7258ed869ddcee46352907f746", + "number": 1127, + "title": "Research: exact 3->2 z-program rewrites of the PR589 word, 24,305 -> 23,495 ADDs (no new kappa)", + "updatedAt": "2026-10-13T18:46:01Z" + }, + { + "headRefOid": "da3b7475ba9b7747d10b147cffab2794521581a2", + "number": 1126, + "title": "Research: sharp 21-ADD positive-lift minimum for all eight k8 leaver cells", + "updatedAt": "2026-10-13T18:44:49Z" + } + ], + "finding": "PR997 remains the only Hadamard-specific title; latest other restoration coalescing submission PR1155 has a different mechanism. No competing exhaustive 4x4 readout census found." + } +} diff --git a/research/hadamard-readout-census/LICENSE b/research/hadamard-readout-census/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/hadamard-readout-census/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/research/hadamard-readout-census/NOTICE.md b/research/hadamard-readout-census/NOTICE.md new file mode 100644 index 0000000000..0cf7b95517 --- /dev/null +++ b/research/hadamard-readout-census/NOTICE.md @@ -0,0 +1,26 @@ +# Attribution and assistance + +New work by Cinna Davis (@1337isnot1337), prepared with substantial OpenAI +Codex assistance in reasoning, implementation, verification and writing. +Apache-2.0 applies. No independent human review, delegated worker or formal +verification of the multiplication theorem is claimed. + +Direct predecessor: Cinna Davis's PR997 signed Hadamard batch, commit +b3fda8d59436103b195069a6328cbf5d74f73bc0. Its exact construction, written proof, +README and notice are retained under sources/. This is a new independent +enumerator and interpreter extending the same contributor's earlier work. + +Martin (@martinxxx9), PR1088 at b0396aad724fec58630fbd4d13a809c562f18d9e, +provides the parallel weighted 3x3 repair precedent. Its README and notice +are retained byte for byte from the base repository. The four-by-four +Hadamard object and exhaustive readout price envelope here are distinct. + +The retained lineage includes @CubeJerry's PR889 common-factor fanout, +Ross Richardson's PR934/943/944 connector walk and signed-obstruction work, +and Chafik Boukhalfa (@chafreaky)'s PR628 balanced dirty-product commutator. +Their credit is preserved in the retained notices. The commutator and +Hadamard matrix are classical; no literature-priority claim is made. + +No predecessor executable code is imported. Selected frontier contributors +retain their attribution in the frozen base selected record; this package +neither changes that frontier nor incorporates their supplier implementation. diff --git a/research/hadamard-readout-census/OVERLAP.json b/research/hadamard-readout-census/OVERLAP.json new file mode 100644 index 0000000000..bd72b67558 --- /dev/null +++ b/research/hadamard-readout-census/OVERLAP.json @@ -0,0 +1,90 @@ +{ + "scope": "titles of full live open inventory plus targeted all-state connector/Hadamard queries", + "open_count": 756, + "relevant": [ + { + "author": { + "id": "U_kgDODYXfmQ", + "is_bot": false, + "login": "aliromman", + "name": "Ali Romman" + }, + "headRefOid": "4c35687d7c0da8e6cf33f17e418ecf31c95ff3ad", + "number": 1135, + "title": "Research: exact restoration contracts and resource bounds for rounded borrowing", + "updatedAt": "2026-10-13T18:53:46Z" + }, + { + "author": { + "id": "U_kgDOCt6exg", + "is_bot": false, + "login": "bbMisk", + "name": "" + }, + "headRefOid": "ae95248b3301e3fafe05c1c00020f69edcdceb98", + "number": 1083, + "title": "Scoped formalization: Lean certificate for 945 five-source connector pairings", + "updatedAt": "2026-10-13T17:49:10Z" + }, + { + "author": { + "id": "MDQ6VXNlcjE4NjIyMjg4", + "is_bot": false, + "login": "thakrarsagar", + "name": "" + }, + "headRefOid": "4ceaf380ed41b28dadcc41d2f974f025ac4d8c03", + "number": 1012, + "title": "Research note: restoration deferral is mass-neutral in the hosted T37 recurrence (no new kappa)", + "updatedAt": "2026-10-13T16:38:45Z" + }, + { + "author": { + "id": "U_kgDOCcbgOg", + "is_bot": false, + "login": "1337isnot1337", + "name": "Cinna Davis" + }, + "headRefOid": "b3fda8d59436103b195069a6328cbf5d74f73bc0", + "number": 997, + "title": "Recursive-interface construction: signed Hadamard batch saves 126 leaf calls (no new kappa)", + "updatedAt": "2026-10-13T16:10:07Z" + }, + { + "author": { + "id": "U_kgDOBhaNkw", + "is_bot": false, + "login": "shhxera", + "name": "" + }, + "headRefOid": "8c5e1b557f59bca29139c4c2dcc65edfb808372b", + "number": 822, + "title": "Research: reuse dirty echo connectors (no new kappa)", + "updatedAt": "2026-10-13T06:27:42Z" + }, + { + "author": { + "id": "U_kgDODYXfmQ", + "is_bot": false, + "login": "aliromman", + "name": "Ali Romman" + }, + "headRefOid": "302383e0c1ec71c50860362d3f394f85664c2445", + "number": 744, + "title": "Independent verification: fixed-space ternary echo minima and rounded leaves", + "updatedAt": "2026-10-13T05:10:23Z" + }, + { + "author": { + "id": "MDQ6VXNlcjQ0MDA1Mjc=", + "is_bot": false, + "login": "chafreaky", + "name": "chafreaky" + }, + "headRefOid": "0768f97d06c623b8211e651543c66135796b62bf", + "number": 628, + "title": "Uniform rounded prime-power cyclic inversion (no \u03ba claim)", + "updatedAt": "2026-10-13T00:00:33Z" + } + ] +} diff --git a/research/hadamard-readout-census/PROOF.md b/research/hadamard-readout-census/PROOF.md new file mode 100644 index 0000000000..b8e7db27bf --- /dev/null +++ b/research/hadamard-readout-census/PROOF.md @@ -0,0 +1,227 @@ +# Exact readout census for the eight-source-call Hadamard interface + +## Object and hypotheses + +This extends Cinna Davis's PR997 at +`b3fda8d59436103b195069a6328cbf5d74f73bc0`. PR997 samples 4,000 source +paths and allows at most two signed differences per output. Here every +eight-source-call path is covered, with arbitrary repeated signed readouts. +The finite optimum below concerns this explicit class, not arbitrary circuits. + +There are distinct read-only sources `x_j`, distinct accumulating outputs +`y_i`, and one arbitrary dirty connector `z`. A source query is +`z += s B_j x_j`; a readout is `y_i += s A_i z`, where `s` is +1 or -1. +Each `A_i` and `B_j` is an exact linear map. All private child workspace and +sources restore on return. Maps need not commute. Both signs have the same +complete query price, independent of state, placement and other queries. +No output is borrowed as scratch, no initialization of `z` is assumed, +and no further scalar operations on these rows are admitted in this class. +Correctness for the optimum means the coefficient identity for independent +formal A/B operators and independent initial-data symbols. Special maps with +additional relations (for example, a zero A map) can admit cheaper words and +are outside this lower bound. The emitted construction remains correct for +arbitrary exact linear maps, including singular ones. + +The desired coefficient matrix, in fixed output/source order, is + +``` +H = [ + + + + ] + [ + - + - ] + [ + + - - ] + [ + - - + ]. +``` + +The restriction is **exactly one positive and one negative B query per +source**. Thus there are eight source calls and `8! = 40,320` source orders. +Readouts may be repeated arbitrarily at any visited connector state. + +## Why finite enumeration covers arbitrary readout multiplicities + +At a visit with source coefficient vector `q`, the connector is +`z_initial + sum_j q_j B_j x_j`. A signed readout contributes its sign to +the coefficient of `A_i z_initial` and contributes that sign times `q` +to row i of the desired product coefficients. Since the connector dirt is +arbitrary, positive and negative readout counts must be equal, say k each. +Consequently a correct readout is precisely + +``` +sum_{r=1}^k q_positive[r] - sum_{r=1}^k q_negative[r] = H[i]. +``` + +The multisets can repeat states. Any integer coefficient representation +with zero coefficient sum has this form. Redundant cancellations cannot +improve a minimum with strictly positive readout prices. Each unit coordinate +difference is an edge of every admitted path; hence four differences always +realize every sign row of H. At most eight readout calls per output suffice. +Checking k=1,2,3,4 therefore finds a global minimum for that output on that +path, even though the original interface allows arbitrarily many readouts. + +Each coordinate's first sign is independently + or -. Remove those signs: +each coordinate follows 0 -> 1 -> 0, so the unsigned event orders are exactly +the `8!/(2!^4) = 2,520` multiset permutations of `00112233`. The 16 first-sign +choices restore all 40,320 signed paths. `census.py` enumerates those paths, +builds all equal-cardinality sums of visited vertices, and tests the equation +above with integer tuples. It does not restrict readouts to two differences. + +`verify.py` uses a different enumerator: all permutations of the eight +distinct signed events. Its readout calculation forms the difference set D +of visited states. A sign row needs two calls if it lies in D, four if in +D+D, six if it lies in D+D+D, and otherwise eight, by the unit-edge bound. +Both algorithms produce the exact same 114-profile frequency table. +The verifier caches 1,022 normalized vertex sets; it still counts every +distinct signed path, including different paths with the same visited set. + +Output minima are jointly attainable: readouts at a visit do not alter the +connector or sources and commute across distinct outputs. They can all be +inserted at their respective visits. There is no competition for a tap. + +This is an exact finite certificate with a written completeness argument. +It is not a proof-assistant verification or a proof of the multiplication +theorem. The finite histogram and all attaining words are in CERTIFICATE.json. + +## Result: query optimum and weighted envelope + +The 114 profiles have 22 undominated profiles. They are exactly all distinct +permutations of the following three patterns: + +``` +(2,4,4,4) 4 permutations +(2,2,6,6) 6 permutations +(2,2,4,8) 12 permutations. +``` + +The smallest total readout count is 14, so the minimum total query count +within this class is **22**. This independently closes PR997's unclaimed +finite optimum for the stated eight-source-call class. It excludes paths +with ten or more source calls, other query alphabets, output borrowing, +source-dependent prices, and non-linear or rounded children. + +Let a <= b <= c <= d be the four positive, complete A-query prices in sorted +order. Sorting prices only selects an attaining profile in fixed row order; +it does not reorder the demanded matrix or the factors of any child. Since +all listed profile permutations are attained, exchange of unequal weights +gives the minimum in each family by assigning more calls to cheaper rows: + +``` +family (2,4,4,4): 4a + 4b + 4c + 2d +family (2,2,6,6): 6a + 6b + 2c + 2d +family (2,2,4,8): 8a + 4b + 2c + 2d. +``` + +The third family is no dearer than the second because `2a-2b <= 0`. +Thus the exact readout-price envelope is + +``` +R(a,b,c,d) = 4a + 4b + 2c + 2d + min(2c,4a). +``` + +Add `2 sum_j price(B_j)` for the complete query price. If c < 2a, a +22-query word attains the optimum. If c > 2a, a 24-query word attains it. +At c=2a both families tie. Query count alone does not choose the cheaper +word under unequal child prices. All 22 frontier words are independently +replayed, rather than inferring unattested profile permutations. + +## Matched recursive lowering: 222 versus 238 leaves + +Use PR997's factor lengths, A=[2,3,4,5] and B=[1,2,3,4]. Every factor has a +single exact additive shear. For a product of n ordered factors, split into +b=floor(n/2) first factors and a=ceil(n/2) last factors. A fresh dirty row u +implements the positive product through the literal word + +``` +u += B source; target += A u; u -= B source; target -= A u. +``` + +Each negative call is the complete reversed word with signs negated. +Linearity cancels u's arbitrary initial value and restores every scratch +row. Source and target rows are distinct from the pool; all ancestors' +active rows stay outside it. The factors retain their original order. +All children and inverses are included in + +``` +C(1)=1, C(n)=2 C(b)+2 C(a) +I(1)=0, I(n)=1+2 I(b)+2 I(a) +S(1)=0, S(n)=1+max(S(b),S(a)). +``` + +C is executed primitive calls, I is executed internal echo nodes, and S is +simultaneously active child scratch. Lengths 1..5 give C=[1,4,10,16,28] and +I=[0,1,3,5,9]. The connector and three dirty child rows give four dirty rows +in both implementations. No clean data array is needed. + +The minimum-price profile for this fixture is `(8,4,2,2)`. The complete bill +is `2(1+4+10+16) + 8*4+4*10+2*16+2*28 = 222` primitives. +PR997's pinned `(4,4,4,2)` word has 238. The new word has 24 queries and 66 +internal echo nodes; the old word has 22 queries and 72 nodes. This is a +**16-call reduction (8/119, about 6.72%)**, with six fewer echo nodes and two +more top-level queries. No measured multiplication-runtime claim follows. + +## Complete cost recurrence and physical obligations + +Let E(L,w) price one exact primitive factor shear at row length L and a +common sufficient integer width w. It includes coefficient/phase/source +access, local arithmetic, validation, source restoration and scalar cleanup. +Let D(L,w) price one internal echo node's extra control, and let Q(L,w) +price outer-query dispatch/return and any constant, common port adapter. +Then the exact balanced child recurrence is + +``` +T_1=E, T_n=2 T_b+2 T_a+D. +T_batch = P + sum_j 2 T_Bj + sum_i profile[i] T_Ai + + (#queries) Q + R(word). +``` + +P includes preparing and restoring program/coefficient/control storage, +port admission, precision setup and final cleanup. There are 24 distinct +factor matrices in either fixture, so matrix input storage is `24 L^2 w` +bits, plus rows and metadata. R(word) explicitly charges placement-dependent +frame changes, coefficient routing, address dispatch and complete head +travel including final return. Every emitted child and inverse is counted. +There is no uncharged call outside this recurrence. + +For a literal dense scalar backend, each primitive uses L^2 multiplications, +L^2 additions/subtractions (including the target update), L^2 coefficient +reads, L^2 source reads, L target reads and L target writes. Two scalar +work registers can be initialized once and cleared after every primitive; +the 4 dirty scratch rows and 8 data rows require `12 L w` bits. Arbitrary +initial dirt is represented independently in the free-operator interpreter. +Finite integers are exact; a physical bounded-word backend must choose w +from a proven prefix bound, or charge exact multiprecision arithmetic. +Rounded children are outside the restoration hypothesis. + +For the matched finite dense fixtures, initial entries have magnitude at most +7 and each factor has infinity operator norm at most 6. The separate prefix +bound includes partial dot products, target addition before cancellation and +the appended literal inverses. Its exact common bound and sufficient signed +width are emitted in the verifier receipt for both words in this domain. This is +not an all-length precision theorem or a physical word/tape admission. + +With common E,D,Q and the same P, the two displayed words cost + +``` +new: P + 222 E + 66 D + 24 Q + R(new) +old: P + 238 E + 72 D + 22 Q + R(old). +``` + +Their comparison requires `2Q + R(new)-R(old) < 16E+6D`. +If R is constant, the exact envelope switches at `Q=8E+3D`, consistent +with c=2a after including each query's dispatch in its price. If Q=100, +E=1,D=0,R=0, the new word is more expensive; the verifier retains this +negative control. No arbitrary-price dominance of the displayed word is +asserted. Applying the envelope with placement-dependent R requires a +different optimization; the census does not prove its optimum. + +No selected supplier hosting, frame realization, tape compiler, rounded +restoration or improved moment has been supplied. The selected κ therefore +remains unchanged, conditional on its inherited interfaces. + +## Attribution + +PR997 is the direct four-by-four predecessor and supplies the comparison +fixture and interface. Martin's PR1088 (`b0396aad724fec58630fbd4d13a809c562f18d9e`) +establishes a different weighted three-by-three repair; it motivated checking +prices rather than query totals. CubeJerry's PR889, Ross Richardson's +PR934/943/944 and Chafik Boukhalfa's PR628 retain their respective fanout, +connector and balanced-echo credit. No predecessor executable code is +imported. Source notices and exact bytes are retained under sources/. +New work by Cinna Davis, with substantial OpenAI Codex assistance; Apache-2.0. diff --git a/research/hadamard-readout-census/README.md b/research/hadamard-readout-census/README.md new file mode 100644 index 0000000000..8bb0721e43 --- /dev/null +++ b/research/hadamard-readout-census/README.md @@ -0,0 +1,82 @@ +# Signed Hadamard readout census and weighted recursive price + +**Research construction / finite scoped optimum. No new κ.** + +This extends PR997's signed four-source/four-output batch by exhausting its +eight-source-call class and permitting arbitrary repeated readouts. The +complete census covers **40,320** source orders, yields **114** minimum +profiles and **22** Pareto profiles, and certifies a minimum of **22 queries** +in that class. Two independent integer algorithms agree on every frequency. + +For positive complete A-query prices sorted as a<=b<=c<=d, the exact readout +price is `4a+4b+2c+2d+min(2c,4a)`. Add twice the sum of B-query prices. +The optimum uses a 24-query profile when `c>2a`, illustrating why fewer +queries need not mean less recursive work. + +Using PR997's exact A=[2,3,4,5], B=[1,2,3,4] balanced children, an emitted +24-query word uses **222 primitive calls versus 238**, **66 echo nodes +versus 72**, and the same **four dirty scratch rows**. All 22 frontier words, +the comparison word, noncommuting factor order, arbitrary dirty inputs and +literal inverses are checked. The complete recurrence prices source and +coefficient operations, every child and inverse, helper rows, control, +adapters, storage, frame changes and head return. Two extra query dispatches +remain a real expense; the benefit requires the inequality in PROOF.md. + +## Reproduce + +Python 3.10+; standard library only, from the repository root (absolute +script paths also work from other directories): + +```sh +python3 -I -O -B research/hadamard-readout-census/test_package.py +``` + +Expected final markers: + +``` +PASS_HADAMARD_READOUT_CENSUS signed_paths=40320 profiles=114 pareto=22 queries=22 leaf_calls=222_vs_238 controls=10 no_new_kappa +PASS_HADAMARD_READOUT_PACKAGE regeneration=PASS relocation=PASS controls=4 +``` + +The package test reproduces the certificate, runs a relocated read-only +optimized-Python check, and tests deliberate corruption of a source pin, +coverage table and restoring word, plus occupied-output preservation. +The verifier includes 624 dense basis/dirty replays and exact free-operator +checks for each attaining profile. To regenerate separately, use a **new** +output path; existing output files are refused: + +```sh +python3 -I -B research/hadamard-readout-census/census.py --output /tmp/hadamard-census-new.json +``` + +## Pins, scope and handoff + +Exact base: `ce7ad1b6ab09452c3478723a2e96ed5ff212dc08`; OS-random assignment +seed **55**, recursive interfaces. Source and context pins are in SOURCES.json. +PR997 is pinned at `b3fda8d59436103b195069a6328cbf5d74f73bc0` and its word +is replayed through the same new backend as the candidate. + +The domain fixes exactly one + and one - B call per source, an arbitrary +dirty connector and exact linear additive children. +Correctness for the optimum is the independent formal-operator coefficient +identity; special maps with additional algebraic relations are excluded. +Enumeration stops after +all 40,320 source paths; readout cardinality is completely covered by the +proved eight-call upper bound. Signed prices must agree and be independent +of placement/state. The envelope excludes varying frame/travel charges, +additional source calls, output borrowing and other query alphabets. + +The base selected κ is `836330098538459/500000000000000000`, from PR1094. +This package does not alter the selection or supply a new hosted supplier, +recursive moment, physical tape implementation, measured speedup or full +multiplication theorem. All-size/compiler, realization, hosting, precision, +exact recovery and analytic obligations remain as documented upstream. + +PR1088 concerns a different 3x3 weighted repair; PR1012 concerns hosted +restoration deferral; PR1135 concerns rounded borrowed child contracts. This +adds complete 4x4 coverage and an arbitrary-positive-price envelope to PR997's +sampled construction. Local sprint claim and overlap checks are included. + +Prepared by **Cinna Davis (@1337isnot1337)** with substantial **OpenAI Codex +assistance** in reasoning, implementation, verification and writing. +Apache-2.0. See NOTICE.md and retained predecessor notices for credit. diff --git a/research/hadamard-readout-census/SOURCES.json b/research/hadamard-readout-census/SOURCES.json new file mode 100644 index 0000000000..8dcbdbdf6a --- /dev/null +++ b/research/hadamard-readout-census/SOURCES.json @@ -0,0 +1,63 @@ +{ + "base_commit": "ce7ad1b6ab09452c3478723a2e96ed5ff212dc08", + "context_pins": { + "certificates/selected-result.json": { + "commit": "ce7ad1b6ab09452c3478723a2e96ed5ff212dc08", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + "docs/research/community-batch1099-review.md": { + "commit": "ce7ad1b6ab09452c3478723a2e96ed5ff212dc08", + "sha256": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb" + }, + "docs/research/current-status.md": { + "commit": "ce7ad1b6ab09452c3478723a2e96ed5ff212dc08", + "sha256": "1f59d648763c77d574d18dc59ea8bf62d2ee74aaed3c202c9c8cfa4f901badbd" + }, + "research/weighted-signed-connector-seed58/NOTICE.md": { + "commit": "ce7ad1b6ab09452c3478723a2e96ed5ff212dc08", + "sha256": "fb7c34c6745dcb79bcf63dab3370ed24b2ec6f776d1bd3e1cae3905c0f4e3dd9" + }, + "research/weighted-signed-connector-seed58/README.md": { + "commit": "ce7ad1b6ab09452c3478723a2e96ed5ff212dc08", + "sha256": "53cfd7805b48ddf8143e1120de74845d287e4806be9669e61989c0ad45b985ec" + } + }, + "files": { + "sources/BASE-selected-result.json": { + "commit": "ce7ad1b6ab09452c3478723a2e96ed5ff212dc08", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "source_path": "certificates/selected-result.json" + }, + "sources/PR1088-NOTICE.md": { + "commit": "ce7ad1b6ab09452c3478723a2e96ed5ff212dc08", + "sha256": "fb7c34c6745dcb79bcf63dab3370ed24b2ec6f776d1bd3e1cae3905c0f4e3dd9", + "source_path": "research/weighted-signed-connector-seed58/NOTICE.md" + }, + "sources/PR1088-README.md": { + "commit": "ce7ad1b6ab09452c3478723a2e96ed5ff212dc08", + "sha256": "53cfd7805b48ddf8143e1120de74845d287e4806be9669e61989c0ad45b985ec", + "source_path": "research/weighted-signed-connector-seed58/README.md" + }, + "sources/PR997-CONSTRUCTION.json": { + "commit": "b3fda8d59436103b195069a6328cbf5d74f73bc0", + "sha256": "abbf5d5aaec4fdc0355da2fefc66069e41152423964a27132625825577df5c75", + "source_path": "research/signed-hadamard-batch-seed55/CONSTRUCTION.json" + }, + "sources/PR997-NOTICE.md": { + "commit": "b3fda8d59436103b195069a6328cbf5d74f73bc0", + "sha256": "50c0de78f6374ef3ff4c6c9cac669b9cd5af896c3f9ae901330e67dc58c7e7ec", + "source_path": "research/signed-hadamard-batch-seed55/NOTICE.md" + }, + "sources/PR997-PROOF.md": { + "commit": "b3fda8d59436103b195069a6328cbf5d74f73bc0", + "sha256": "7150f641a1a805560d89268b78ac7fdf226ce0092c484b394744694a4e9e24c2", + "source_path": "research/signed-hadamard-batch-seed55/PROOF.md" + }, + "sources/PR997-README.md": { + "commit": "b3fda8d59436103b195069a6328cbf5d74f73bc0", + "sha256": "408401c5e83c78a61621c08250f24578f289306d6e7d62b9132039cc9a152ecc", + "source_path": "research/signed-hadamard-batch-seed55/README.md" + } + }, + "pr997_head": "b3fda8d59436103b195069a6328cbf5d74f73bc0" +} diff --git a/research/hadamard-readout-census/VALIDATION.json b/research/hadamard-readout-census/VALIDATION.json new file mode 100644 index 0000000000..432ae2c4fb --- /dev/null +++ b/research/hadamard-readout-census/VALIDATION.json @@ -0,0 +1,70 @@ +{ + "base_commit": "ce7ad1b6ab09452c3478723a2e96ed5ff212dc08", + "certificate_sha256": "7eee383c225d0fe65fdf1e868b209a45dd569ea749bb0640ea901133c4aa6ea5", + "environment": { + "machine": "x86_64", + "python": "3.14.7", + "system": "Linux" + }, + "format": "hadamard-readout-validation/1", + "pass_markers": [ + "PASS_HADAMARD_READOUT_CENSUS signed_paths=40320 profiles=114 pareto=22 queries=22 leaf_calls=222_vs_238 controls=10 no_new_kappa", + "PASS_HADAMARD_READOUT_PACKAGE regeneration=PASS relocation=PASS controls=4" + ], + "publication": { + "construction_commit": "dd4261c4208df476fb9a2aca80d95859014f6766", + "handoff_changes": "Publication metadata and formal-operator scope clarification; verified code, certificate and source inputs unchanged", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1158" + }, + "receipt": { + "chosen_primitive_calls": 222, + "chosen_primitive_sha256": "25e6b30e240955184e24787e04d5a4ba55908b495d53a914e3f1ddbc882e1dbd", + "common_prefix_absolute_bound": 169230901, + "common_signed_width_bits": 29, + "dense_basis_and_dirty_replays": 624, + "frontier_free_operator_replays": 22, + "independent_vertex_sets": 1022, + "local_child_contracts": 16, + "new_invoice": { + "child_call_entries": 288, + "coefficient_matrices": 24, + "dirty_arrays": 4, + "echo_nodes": 66, + "output_rows": 4, + "primitive_leaves": 222, + "queries": 24, + "source_rows": 4 + }, + "predecessor_invoice": { + "child_call_entries": 310, + "coefficient_matrices": 24, + "dirty_arrays": 4, + "echo_nodes": 72, + "output_rows": 4, + "primitive_leaves": 238, + "queries": 22, + "source_rows": 4 + }, + "predecessor_primitive_calls": 238, + "predecessor_primitive_sha256": "1075133b12720c7f26feeeb5812460e708919f431e440a2198c37d4a484d3c2c", + "rational_price_cases": 1296 + }, + "scope": "Finite exact additive interface; no new kappa, full make verify, selected cold replay, hosting/tape compiler, remote CI or human review", + "selected_record_check": { + "exit_code": 0, + "output": "PASS selected record, exact kappa, original source inventory and proof supplement: 836330098538459/500000000000000000\n" + }, + "selected_tests": { + "count": 25, + "exit_code": 0, + "output": ".........................\n----------------------------------------------------------------------\nRan 25 tests in 0.559s\n\nOK\n" + }, + "source_provenance": "Seven retained source files and all context hashes matched exact Git bytes at their pinned commits", + "status": "PASS", + "submitted_index_replay": { + "elapsed_seconds": 10.051804718999847, + "export_root": "/tmp/hadamard-submitted-c63e0xwz", + "exported_files": 20, + "returncode": 0 + } +} diff --git a/research/hadamard-readout-census/VALIDATION.md b/research/hadamard-readout-census/VALIDATION.md new file mode 100644 index 0000000000..20839af4a8 --- /dev/null +++ b/research/hadamard-readout-census/VALIDATION.md @@ -0,0 +1,62 @@ +# Validation and handoff scope + +Base commit: `ce7ad1b6ab09452c3478723a2e96ed5ff212dc08`. +Local environment: Linux, CPython 3.14.7. New material is confined to +`research/hadamard-readout-census/`. No generator, selected frontier, +existing research package or `upstream/` source is edited. + +Relevant commands: + +```sh +python3 -I -O -B research/hadamard-readout-census/test_package.py +python3 -B scripts/verify_selected_result.py +python3 -B -m unittest discover -s tests -p 'test_selected*.py' +git diff --cached --check +``` + +The package command passes with byte-exact deterministic regeneration, +read-only relocated replay under optimized Python, and four real subprocess +controls. The independent verifier passes on all 40,320 signed source orders, +114 profile frequencies, 22 Pareto profiles and all their attaining words. +It checks 16 individual signed child contracts, 624 dense basis/dirty cases, +literal inverses, 1,296 exact rational price fixtures, the three profile +families, full restoration/control invoices and ten mathematical controls. +No mathematical condition depends on Python assertions. + +The selected-record source inventory, exact κ and proof binding pass. +All 25 selected-result/inventory/proof tests pass. All seven retained source +files match their exact Git bytes at the recorded predecessor/base commits; +all additional context hashes match the recorded base Git bytes. The final +submitted package is additionally replayed from files exported from the Git +index, with exact command output stored in VALIDATION.json. + +The full source-order census completes its stated domain. Arbitrary repeated +readouts are covered by the written four-difference/eight-readout upper bound. +No failure to find a candidate is presented as an impossibility theorem. +The independent calculation enumerates signed-event permutations and shortest +sums of state differences; it imports neither census.py nor predecessor code. + +The two recursive implementations are compared on exactly PR997's same factor +lengths and dirty interface through the same new primitive backend. The +emitted primitive-word digests and a common exact integer prefix bound, with +sufficient signed width for the stated finite norm domain, are in the command +receipt. The bound includes scalar intermediates and the appended inverses. + +Full repository `make verify`, selected supplier cold replay, hosting/tape +execution, remote CI and human peer review are not claimed. This standalone +research package does not modify a selected construction or regenerate +unrelated artifacts. Relevant package checks and selected-record checks are +the completed validation scope; the result is an exact interface operation +count and scoped finite optimum, not a measured multiplication speedup or +formal proof of the complete theorem. + +The handoff metadata refresh at 19:12 UTC on October 13 found 767 open PRs +through #1152; main and the PR997 source pin were unchanged. PR1088's weighted +3x3 repair, PR1103's rectangular output borrowing and PR997's sampled 4x4 +construction have different scopes. This package extends PR997 with complete +coverage and a new price envelope. No pinned coordination issue existed; +CLAIM.json contains the local claim. Handoff and later publication details +are recorded there once after publication. + +Contributor, predecessor and substantial AI-assistance credit are retained +in NOTICE.md and the frozen source notices. New material is Apache-2.0. diff --git a/research/hadamard-readout-census/census.py b/research/hadamard-readout-census/census.py new file mode 100644 index 0000000000..5161c2b403 --- /dev/null +++ b/research/hadamard-readout-census/census.py @@ -0,0 +1,162 @@ +"""Exact finite census; no floating point and no predecessor executable code.""" + +import argparse +from collections import Counter +from itertools import combinations_with_replacement, product +import json +from pathlib import Path + +H = ((1, 1, 1, 1), (1, -1, 1, -1), + (1, 1, -1, -1), (1, -1, -1, 1)) +TARGETS = tuple((1,) + t for t in product((-1, 1), repeat=3)) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def paths(prefix=(), counts=(0, 0, 0, 0)): + """Every permutation of the multiset 00112233 exactly once.""" + if len(prefix) == 8: + yield prefix + else: + for j in range(4): + if counts[j] < 2: + c = list(counts) + c[j] += 1 + yield from paths(prefix + (j,), tuple(c)) + + +def states(path): + q = [0] * 4 + out = [tuple(q)] + for j in path: + q[j] = 1 - q[j] + out.append(tuple(q)) + return tuple(out) + + +def readouts(qs): + """Solve min ||a||_1 subject to sum a=0, sum a*q=target. + + At most four positive and four negative taps suffice, since each of the + four unit coordinate differences occurs on the path. Exhaust all smaller + equal-cardinality multisets. Repetition includes every integer coefficient. + """ + vertices = tuple(dict.fromkeys(qs)) + unresolved = set(TARGETS) + answer = {} + for k in range(1, 5): + sums = {} + for ids in combinations_with_replacement(range(len(vertices)), k): + total = tuple(sum(vertices[i][j] for i in ids) for j in range(4)) + sums.setdefault(total, ids) + for target in sorted(unresolved): + for total, pos in sums.items(): + neg = sums.get(tuple(total[j] - target[j] for j in range(4))) + if neg is not None: + answer[target] = (2 * k, tuple(vertices[i] for i in pos), + tuple(vertices[i] for i in neg)) + break + unresolved -= answer.keys() + if not unresolved: + break + require(not unresolved, 'unit-edge upper bound failed') + return answer + + +def profile_for(minima, signs): + profile, reps = [], [] + for row in H: + target = tuple(row[j] * signs[j] for j in range(4)) + orient = target[0] + canonical = tuple(orient * x for x in target) + n, positive, negative = minima[canonical] + if orient < 0: + positive, negative = negative, positive + profile.append(n) + reps.append((positive, negative)) + return tuple(profile), tuple(reps) + + +def emit(path, signs, reps): + qs = states(path) + taps = [[] for _ in qs] + for i, (positive, negative) in enumerate(reps): + for sign, vertices in ((1, positive), (-1, negative)): + for v in vertices: + taps[qs.index(v)].append(['A', i, sign]) + word = [] + for t, v in enumerate(qs): + word.extend(taps[t]) + if t < 8: + j = path[t] + word.append(['B', j, signs[j] * (1 if v[j] == 0 else -1)]) + return word + + +def dominates(a, b): + return a != b and all(x <= y for x, y in zip(a, b)) + + +def balanced_calls(n): + require(isinstance(n, int) and n >= 1, 'positive factor length required') + if n == 1: + return 1 + return 2 * balanced_calls(n // 2) + 2 * balanced_calls(n - n // 2) + + +def run(): + histogram = Counter() + examples = {} + count = 0 + for path in paths(): + count += 1 + minima = readouts(states(path)) + for signs in product((-1, 1), repeat=4): + profile, reps = profile_for(minima, signs) + histogram[profile] += 1 + examples.setdefault(profile, (path, signs, reps)) + frontier = sorted(p for p in histogram + if not any(dominates(q, p) for q in histogram)) + prices = tuple(balanced_calls(n) for n in (2, 3, 4, 5)) + bprices = tuple(balanced_calls(n) for n in (1, 2, 3, 4)) + chosen = min(frontier, key=lambda p: (sum(x * y for x, y in zip(p, prices)), p)) + path, signs, reps = examples[chosen] + return { + 'format': 'hadamard-readout-census/1', + 'base_commit': 'ce7ad1b6ab09452c3478723a2e96ed5ff212dc08', + 'assignment_seed': 55, + 'unsigned_paths': count, + 'signed_paths': sum(histogram.values()), + 'profile_histogram': [{'profile': list(p), 'paths': histogram[p]} + for p in sorted(histogram)], + 'pareto_profiles': [list(p) for p in frontier], + 'minimum_queries': 8 + min(map(sum, histogram)), + 'A_lengths': [2, 3, 4, 5], 'B_lengths': [1, 2, 3, 4], + 'A_leaf_prices': list(prices), 'B_leaf_prices': list(bprices), + 'chosen_profile': list(chosen), + 'minimum_leaf_calls': 2 * sum(bprices) + sum(x * y for x, y in zip(chosen, prices)), + 'source_path': list(path), 'first_signs': list(signs), + 'word': emit(path, signs, reps), + 'frontier_words': [{'profile': list(p), 'word': emit(*examples[p])} for p in frontier], + 'scope': 'Exactly eight source calls, one positive and one negative per source; arbitrary repeated signed readouts at visited states; exact additive children, one dirty connector, no new kappa', + } + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--output', type=Path) + args = parser.parse_args() + result = run() + payload = json.dumps(result, indent=2, sort_keys=True) + '\n' + if args.output: + with args.output.open('x', encoding='utf-8', newline='\n') as f: + f.write(payload) + print(json.dumps({k: result[k] for k in ('unsigned_paths', 'signed_paths', + 'pareto_profiles', 'minimum_queries', 'minimum_leaf_calls')})) + + +if __name__ == '__main__': + main() diff --git a/research/hadamard-readout-census/sources/BASE-selected-result.json b/research/hadamard-readout-census/sources/BASE-selected-result.json new file mode 100644 index 0000000000..ae6a99f28a --- /dev/null +++ b/research/hadamard-readout-census/sources/BASE-selected-result.json @@ -0,0 +1,222 @@ +{ + "status": "Maintainer-reviewed conditional finite construction; see the integration receipt for publication and PR resolution status", + "kappa": "836330098538459/500000000000000000", + "decimal": "0.001672660197076918", + "source_prs": [ + 1094, + 1087, + 1082, + 1074, + 1068, + 1065, + 1063, + 1061, + 1056, + 1055, + 1053, + 1050, + 1042, + 1031, + 1028, + 1022, + 1018, + 1005, + 1004, + 987, + 942, + 890, + 870, + 869, + 858, + 799, + 741, + 699, + 685, + 676, + 664, + 660, + 659, + 656, + 655, + 653, + 658, + 649, + 645, + 635, + 589, + 555, + 545, + 626, + 623, + 622, + 620, + 617, + 615, + 604, + 601, + 596, + 592, + 591, + 593, + 599, + 588, + 543, + 584, + 586, + 583, + 582, + 579, + 576, + 575, + 574, + 571, + 569, + 568, + 567, + 564, + 562, + 561, + 559, + 558, + 552, + 550, + 548, + 541, + 535, + 510, + 503, + 531, + 523, + 493, + 514, + 507, + 484, + 496, + 505, + 522, + 520, + 472, + 458, + 445, + 442, + 425, + 433, + 370, + 361, + 315 + ], + "source_manifest": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "certificate": "research/community-frontier1094-audit/ASSEMBLY.json", + "certificate_sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045", + "proof": "docs/research/community-batch1099-review.md", + "proof_supplements": { + "research/e8-bit-r420/README.md": "9807be57c6adf26b30e4f54e2f8160075bbc05091f1a6d157e43d2a4620c1c9f", + "research/complex-571-free4fc8/NOTICE.md": "a4c084abdc1c7a9ac683eeb11124335d51cff8a6deba6ee92ba5a12bceaa2c97", + "research/complex-multicold/proof/CONSTRUCTION.md": "27ece5e1c11b90d97a808b56eff897b998c10e61016db95867f84e6e6aef132f", + "research/complex-multicold/vendor/pr559/PROOF.md": "d5d498edc56fdef8c5798af7f5ec66948bd2f66c553b9efe366cdaab01bd3453", + "research/structural-gain/frontier-composition/README.md": "70f0f791cbe3b2603f85d85bb9055aa0ee1df6dc06ba82fc1921356948312887", + "research/complex-joint-prefix/proof/CONSTRUCTION.md": "a92e610e7a598d99c612d1b63d1a03a49c0cd1e15ddd29fa55c465ddd8c18105", + "research/kernel-frame-coalescing/PROOF.md": "fa8b2f36b9590ee80ff45d3f7724f8c7de8ad29a29f366d5133010c77e41fe1b", + "research/complex-571-hpeq5/README.md": "4000b37f6c07c09d971dc4010ceb137c13340f3a8809d3272046ccaf746c3e2b", + "research/hyperplane-end-lean/PROOF.md": "1cbce5cf0ff0152f71e8ae7bef25841d1ce13010af248ff7209182d2328c21c9", + "docs/research/community-hyperplane599-review.md": "3298cd0d451541508af232cac72efbd7c10580e6c6ad493a855ab0faa01ade8c", + "research/complex-571-cold14-b3/README.md": "1945785785c153c7d0e8d4c071adabe626c1091b71721ff85d2d67191b376b96", + "research/complex-571-cold14-b3/PROOF-NOTE.md": "1cf592cbc8ab8e21d2dd8c1e945a5c64c6d5cde1216fb06e05a36c1c6ec6613d", + "scripts/verify_cold617_interface.py": "95d7a9094c05ad975fb72f5ab7605593003245a503c8456764987e512028fa6a", + "docs/research/community-cold617-review.md": "b3f2bcbae1249f1f651032022ce1e6e2bfb3f563ce580bf53671f50a074d7046", + "research/complex-k492-owner-repair/README.md": "ee5a1ace4828f7a073be97e95c2d931988774dd3a29a877e65abdf429aeec902", + "research/complex-k492-owner-repair/PROOF-NOTE.md": "337d70fe7abd9afca1d90954c23bde87f4dc27888cc1a6b4bb80506fd6fbf8c5", + "research/complex-k492-owner-repair/PROOF-NOTE-R.md": "22312bb347bdf159e6a01a45c47675e6170d33b258e2fd9ed52aee88fb92c0ed", + "docs/research/community-k492-review.md": "3b731d30e80010b15408a289b0b32192700885474c8b36d48ee3320a7a8c5c47", + "scripts/verify_frontier626.py": "2207bd0ef04a19ef276869085afdedad80a0938fa75db5e1aa7ab73fd3429444", + "scripts/verify_frontier626_bindings.py": "cda63ff41c6d6e2e352c7bf75b84e690c0ce57e4ec6c0355573bb5d9b1f98280", + "scripts/verify_frontier588_bindings.py": "6d1932eea7b1936598118ea8e607b09c29b6e31b749ec41bbe0744ea4f0b606d", + "scripts/verify_hpe_lean_binding.py": "52aa1d23641e4c716b43c98f6b883ad042087dd03a9d01369e8e6a735b07aa03", + "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean": "eebf3a3982af7ab9be45777b272a6aaa523206fa7667ceb6df63ad6589fd8183", + "docs/research/community-frontier741-review.md": "4634694fa75ea9e749ecf19d3db3e4d82effe3b61a2efdf08ac5a97275fb676a", + "research/complex-sw4-frame8/PROVENANCE.md": "c7648719b01dd93af2c3a2c6e951a54711d13892dc4bd4339d16edb4c37c9bf0", + "research/e8-bit-p111-tuned/tune/README.md": "46c7917fb252949f38b7bcd88cf568efc282e3ea065b61d11e457e41673d0b2d", + "scripts/verify_frontier741.py": "215ee6a12de8dc2392e6811a1b8f2140035f6b2d2a0d2100ff4bd2fdcb8bb39b", + "scripts/verify_frontier741_bindings.py": "eff455167e2fd0bc9a67d35241d0e69d8edc58f3a23e776dcfe8f500ca8e8d67", + "docs/research/community-frontier799-review.md": "bd91c10c67f2a873fd456b95cbb43f715a43dac0e0a66938737d591c6b754052", + "scripts/verify_frontier799.py": "19fe1b32079095160dc00fe2f7df75e0fcbc82cff37f7159b755c8a63bd5ce99", + "scripts/verify_frontier799_bindings.py": "43897b3c99212d6134870898a1840f32898aa1b3679b299e654901568ad7e19b", + "research/gauge44-frames-x/PROOF-NOTE-FRAMES-X4.md": "39c50420ebb6e8813706a49b2cf759f277c4afac9f6780fc0a7ac6a5fb86e036", + "docs/research/community-frontier890-review.md": "cd03b7c2c6c09db2cfa89ae40133ae44e1deb6e32ec5ddd23aacecc9c50f2fea", + "scripts/verify_frontier890.py": "88ea38dbef62dd7c0dd46e212618520cc89213edddb2032800e5509993958175", + "scripts/verify_replay_coverage.py": "babe5941d7e6dac4248613ef01f950ee7bb6199e7355021aea4cf854fd1b91c5", + "scripts/verify_frontier741_bridge_coverage.py": "9a14f26762b6126eb54ed43db90371773374fe98733ada80ee871a74afa3b836", + "certificates/replay-coverage/pr741-sw4-v1.json": "7acd5033bc78e3f473718269edaa267c2785d84fbe95ccf6815a33dcf58c2756", + "research/complex-t21-owners/PROOF.md": "78721b32fceb34b21b8e77c95381c38c60276e72e6d9c2e9c6262cb347457def", + "research/complex-t21-owner-bound/PROOF.md": "2aa0aa6ec1d87402138564c38749b5ca0f058c16817efdf58a2685d2d90cb417", + "research/gauge44-barch/PROOF-NOTE-BARCH.md": "c24f211b09358b25d6cf47dd18e4bbd8bcf4ecf279e6f1c6c90613cfa230818d", + "research/complex-double-replica-owners/PROOF.md": "db99599e3966bec253c577c23915e2a2899c4c4e8568044efc11c7918b137bbc", + "docs/research/community-batch952-review.md": "04db59dfc2c31453229b6061bbf59547e71ce3abdc0ce0f6779144bb0dde127b", + "scripts/verify_frontier942.py": "27c6713532d9f53f55dfff4884d55a2d9ae74b68156e37a44596c0418fbed5b7", + "research/complex-t37-owners/PROOF.md": "09b39ad0d5f1f59f54dcff15c16640f7a7acf27e6597660acaf957b95c7e8510", + "research/complex-t37-owners/ALL-T-PROOF.md": "4c0c71ccd0afb850538af1b467e5208b7eb3edd0260fded84e02a8c01dfc868b", + ".github/workflows/t37-owners.yml": "c13acc2902c007237103072b7ec10caf5ca21c1b319d27934f194af2f7d87026", + "docs/research/community-batch1047-review.md": "a6271faf5db0afe3ff7d24a34a3be7a959cdc33ee37784572fba014ee5358787", + "scripts/verify_frontier1042.py": "700fdcaeb6e8f57f6e63c71c2dd1652fc5b183e8d706cd092779bdc0d271e854", + "docs/research/community-batch1099-review.md": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb", + "scripts/verify_frontier1094.py": "c7e20f59968ed5736fb859735de4de207de3418083e37012310ebcded946b949", + "research/community-batch1099-audit/check_frontier1094.py": "2608ef213260a43d09a40b3429742f7a5f280861b54acae66400a7c29a123f51" + }, + "review": "docs/research/community-batch1099-review.md", + "validation": "docs/research/community-batch1099-integration.json", + "reproduce": "make frontier1094-verify", + "scope": "Finite composition under inherited all-size/compiler, common-label/mutable-source, whole-call hosting, precision/tape, analytic and bit H1-H5 assumptions. Not a full Lean multiplication theorem.", + "previous_kappa": "1672188119205421/1000000000000000000", + "previous_record": "certificates/checkpoints/frontier1042.json", + "audited_source_head": "0fc329d0bec93ca7cd288eaea1295172e8789810", + "reviewed_dependency_heads": { + "588": "6d0e53b66c29abd17981881a09eaff41ac862d85", + "543": "2065fe4f72a914d907f1046603f5a36f17018535", + "568": "71c99ac935a33bb7b59a1b4a7af8725a939b0b90", + "569": "1424da81263a5305b35e4cf74ef686c275f03f3f", + "571": "b7bdc5a8de18fcf418cfb9c7d83a2b1097a5e4a3", + "575": "eac6f7e378ab622dac50a2fd4b7ef6eab014de44", + "583": "89be768f0157f5a3d8e4db69cf1748768605eac9", + "586": "4846fee5b06af770e9b3a10c36200f673d656725", + "591": "f622547244bf6d895a571a7b035142ba66279806", + "592": "1f471c445c06a45a32e2c47e8d74c8264b68356b", + "593": "fdb6dcc6d7bc29764c5b6b4d32b7fa050acf74a4", + "596": "7732dd5e46863ff294b5e443661cb9d99abf4e01", + "599": "bc13c8a3e000442606bd2dbe8583a17649ba6c32", + "601": "529ab7dcb59d5ea7a5798e9e06cf5b3aee8a1550", + "604": "1b795c5d7dea746ba310572585c0ef067574b4a6", + "615": "bf8a49a34350599763cced8592db81dc62c2c1c0", + "617": "904d62855723c00f8acef9a287a10768598fdeb2", + "622": "f69477f4f6d3c7eb1f740b166881bffed4ffa9f6", + "623": "e39a615ca601ce5d62abeb24f3fcdb8644ca1005", + "626": "660de893d27bb7abd1d5b01b1640207528a5c851", + "589": "a5afc8c6169ea61ba7c51dfd3cade02cc7b13b46", + "741": "e516b1463606840a15f80aac1995d64ce0092e89", + "799": "80e6463157cfc80b85af09e7e2f14748fe2dac60", + "858": "ae2e25fee91540c83ceee5a60e3b07422ce21c7d", + "869": "73e86f69bf9a391e3c334999f7bbe3825dc42759", + "870": "b734850dc348800942f0ffd1f0723fdec7539b2b", + "890": "4b3bd8cbe8e3e81c44161017c9b72c905a8040a8", + "942": "1960cfa919a0945d0ca4cb14ea96237000037903", + "1004": "1974578f82a30158dd5fcdcdf226b83df8e7196f", + "1005": "779e80aef469bc3a28b19f1adde199871a9a22e3", + "1018": "eac7547cb191f875d5f5ea5f9bbb1d2b8c51c4ef", + "1022": "58618bcbfe88a252467755fc283c04c3db5ca4fd", + "1028": "be4bd89cb4483dcee43257200cd27601f938f13d", + "1031": "e900534f0beda892c726723524203b97471fb9a3", + "1042": "7e8ef087c02a77038a28a337a7ee3a77039cac0d", + "1094": "0fc329d0bec93ca7cd288eaea1295172e8789810", + "1087": "589d1cedf5ef5f231182f4ec86408616311a8af0", + "1082": "0c2e294ec204e83846d27344f829d15ed9ee7cc6", + "1074": "052afc128954f7b6a2b3c409eb4d72248e4020f2", + "1068": "cc71375eae4e8754da0f5d940cb519d66625fb2e", + "1065": "387d935e354a931d636e2c5e6ee63a6910f78a1b", + "1063": "d9377d32e0c97e41338e704c3960fd6f2fa73806", + "1061": "223f581afb1d63d5f8476a69040617e11bcd50e4", + "1056": "d0201efbd68c4acc9832b84bcc986c8781b83c4f", + "1055": "a8ea308976f1709eef0a328463f010cf51469277", + "1053": "6f92ce8884929c9fd4730c86a28e2e3735de02af", + "1050": "c87242f846cfab8c0b97fd889b5fecb0eacef939", + "987": "5142511af0437572aca71b35d1987cd2b47bb5e3" + } +} diff --git a/research/hadamard-readout-census/sources/PR1088-NOTICE.md b/research/hadamard-readout-census/sources/PR1088-NOTICE.md new file mode 100644 index 0000000000..f4e763bba6 --- /dev/null +++ b/research/hadamard-readout-census/sources/PR1088-NOTICE.md @@ -0,0 +1,34 @@ +# Attribution and license + +Prepared for GitHub contributor **@martinxxx9**, with substantial **OpenAI +Codex assistance** in reasoning, code, experiments, verification and prose. +Apache-2.0 under the repository root LICENSE. No independent human, +delegated-agent or proof-assistant review is claimed. + +**Ross Richardson (@RossRichardson), PR944**, reviewed submission head +`5dbcfbc63f646de5a1354f6b9760ec03837233f0`, supplies the signed three-by-three +classification, canonical 14-query obstruction repair, support lower bound, +balanced child lowering and accounting framework. Its README and notice are +retained from the exact experimental repository base, with SHA256 pins. +This contribution generalizes its particular cheapest-B0 weighted example to +every positive sign-symmetric price vector and every cheapest-operator choice. +No predecessor executable implementation is imported. + +The retained PR944 notice credits **@CubeJerry's PR889** common-factor signed +fanout contract; **Ross Richardson's PR934** binary walks and **PR943** universal +binary boundary; and **Chafik Boukhalfa (@chafreaky), PR628**, for the dirty +commutator and literal inverse convention. Those attributions remain intact. + +Concurrent **@1337isnot1337's PR997** at +`b3fda8d59436103b195069a6328cbf5d74f73bc0` concerns a different four-by-four +Hadamard batch, with no weighted optimum claim. **Gareth Davidson's PR1057** at +`78a062df1dcab2bffea5ff4d8243f3da6e465414` uses exact-additive ancestor-port +borrowing, a different workspace contract. Their work informed overlap selection; +their code/results are not mathematical dependencies of this package. + +Jeremy Kothe, Jonathan Capalbo, Hao Yan, Chafik Boukhalfa, DreamingOfClouds, +eumemic, icekylinx, Rohan Arun, and the retained community keep credit for the +selected supplier lineage. The OpenAI #109 upstream framework and all inherited +full-theorem obligations remain separate. Signed linear algebra, reversible +commutators and finite path enumeration are standard methods; no literature +priority is claimed for them. diff --git a/research/hadamard-readout-census/sources/PR1088-README.md b/research/hadamard-readout-census/sources/PR1088-README.md new file mode 100644 index 0000000000..cb3a42764f --- /dev/null +++ b/research/hadamard-readout-census/sources/PR1088-README.md @@ -0,0 +1,236 @@ +# Exact weighted repair for the signed three-by-three connector obstruction + +**Recursive-interface research construction and scoped optimum; no new kappa.** +For the 288 signed/permuted obstructed patterns in Ross Richardson's +[PR944](https://github.com/CrocSwap/integer-mult-bounds/pull/944), every one of +the six operators can carry the necessary extra restoration pair. Thus, for +arbitrary positive complete-query prices equal between signs, the exact cost is + +``` +2 (c_B0 + c_B1 + c_B2 + c_A0 + c_A1 + c_A2) + 2 min_F c_F. +``` + +PR944 proves this formula for its particular example with B0 cheapest. This +contribution supplies all six repairs and proves it for every price ordering +in the same query alphabet. Seed 58 selects a different child-length ordering: +the cheapest child is A1. Its full balanced lowering uses **308 primitive +calls**, versus **332** when retaining the B0-repeat choice. All four borrowed +dirty rows restore. These are operation counts, not measured runtime savings. + +From the repository root, Python 3.10+ and the standard library suffice: + +```sh +python3 -I -O -B research/weighted-signed-connector-seed58/verify.py +python3 -I -O -B research/weighted-signed-connector-seed58/test_package.py +``` + +The first prints +`PASS_WEIGHTED_SIGNED_CONNECTOR witnesses=6 orbit=288 paths=61200 leaves=308_vs_332 dense=378 no_new_kappa`. +The second prints JSON with `status: PASS_WEIGHTED_SIGNED_PACKAGE`, `count: 47`, +and passing isolated optimized replay and deterministic regeneration. To select +an exact priced word, append `--prices 16 28 40 52 4 10` to the first command. +Its additional JSON has `repeated: A1`, `minimum: 308` and the literal query word. +Rational prices such as `1/7` are accepted; zero/negative prices are rejected. + +## Fixed interface and statement + +There are distinct length-L arrays x0,x1,x2,y0,y1,y2,z over characteristic zero. +Every initial value, including z and each y, is arbitrary. Fixed additive linear +maps A_i,B_j need not commute or be invertible. Sources and coefficients are +immutable. The required map is + +``` +x_j unchanged; z unchanged; y_i += sum_j M_ij A_i B_j x_j, +M = [[1,1,1], [1,1,-1], [1,-1,0]]. +``` + +The only queries are `B_j^s: z += s B_j x_j` and `A_i^s: y_i += s A_i z`, +where s is +1 or -1. A negative query subtracts the same increment; it does not +invert A_i or B_j. Each complete query restores its private work and tape heads, +preserves its source and other data, and is independent of old target contents. +All seven data rows stay reserved during children. Outputs are observed only +after completion. There are no other data operations, extra root connectors, +combined queries, direct products, free copies, frame changes or overwrites. + +The optimum concerns uniform correctness for arbitrary admissible operators +and inputs. Particular zero maps or algebraic relations can reduce the cost. +The complete price c_F is a fixed positive charge common to both signs and +all admissible incoming states, at fixed ports. It includes child execution, +source/coefficient access, restoration, routing, frame adapters, head return, +and per-query dispatch. State-, sign- or word-dependent costs require their own +optimization; the displayed minimum is not asserted in those models. + +## Proof of the weighted optimum + +In any correct word, restoring z forces the signed sum of each B_j's occurrences +to be zero. Canceling each A_i z_initial forces the signed sum of each A_i's +occurrences to be zero. Every row and column of M is active, so each of the six +operators appears at least twice, and each occurrence count is even. + +At twelve queries each B_j occurs exactly once with each sign. Let q_t be the +three signed source coefficients in z after its first t B queries. Each A_i +has one negative and one positive readout, so row i must be a difference of +two visited q vertices. There are exactly `6! = 720` source words with one +positive and one negative occurrence of each labeled B. None supports all +three rows of M. The independent DFS in verify.py exhausts precisely this +finite reduction; it is not a heuristic search failure. Thirteen queries are +excluded by evenness. Consequently some operator has at least four occurrences, +and every valid word costs at least `2 sum_F c_F + 2 min_F c_F`. + +Here are six attaining words. Each has four occurrences of its named operator, +two of every other operator, and balanced signs: + +``` +B0: B0- A1- B0+ B0+ A2+ B1+ A0+ B0- A2- B2- A1+ B1- A0- B2+ +B1: A0+ A2+ B0- B1+ A2- B1- B1- A1- B2- A0- B0+ B1+ A1+ B2+ +B2: B0- A2- B1- A0- A1- B0+ A2+ B1+ B2- A1+ B2+ B2+ A0+ B2- +A0: A2+ B0- A1- B1+ A2- B2- A0- B0+ A1+ B2+ A0+ A0+ B1- A0- +A1: A2+ B1+ A1+ A0+ B0- A2- B1- A1- A1- B2- A1+ A0- B2+ B0+ +A2: A2- B0+ A2+ A2+ B1+ A2- A1+ B2+ A0+ B1- B0- A1- B2- A0- +``` + +For a word with balanced operator signs its product coefficient M_ij is the +sum of `s_A s_B` over B_j calls preceding A_i calls. Reversing chronology and +exchanging A/B therefore transposes that coefficient matrix. Since this M is +symmetric, it turns each B-repeat witness into an A-repeat witness. No factor +commutation is used: the new word is checked in its new source/output roles. + +For clarity, the A1 word has source-prefix vertices +`(0,0,0),(0,1,0),(-1,1,0),(-1,0,0),(-1,0,-1),(-1,0,0),(0,0,0)`. +Its A0 and A2 readouts have differences `(1,1,1)` and `(1,-1,0)`. +Its four A1 readouts sum to `(1,1,-1)` and cancel the initial connector dirt. +All six words can also be checked directly by this coefficient sum. + +Permute rows/columns and multiply them by signs to obtain any member of the +288-matrix orbit. Relabel the corresponding queries and multiply their signs. +This preserves the six occurrence profiles, merely permuting their operator +names. Choosing the cheapest named operator attains the lower bound for every +positive price vector throughout the orbit. The verifier checks all 288 maps +and all six transformed words (1,728 query replays). + +This is a written algebraic reduction plus exact finite certificates, not +proof-assistant verification of the statement or the multiplication theorem. + +## Complete recursive price and the seed fixture + +For ordered factors F=(f1,...,fn) in application order, split into the first +floor(n/2) factors R and the remainder S. With one fresh dirty child connector w: + +``` +R(x,w); S(w,y); inverse(R)(x,w); inverse(S)(w,y). +``` + +An inverse reverses the entire literal primitive word and negates every sign. +Induction gives y += SR x, with x and w unchanged, for exact additive children +over arbitrary noncommuting factors. Descendant private scratch is disjoint +from all current ports and restores on return. The complete recurrence is + +``` +C([f]) = c_f + d_leaf, +C(F) = 2 C(R) + 2 C(S) + d_node, +h([f]) = 0; h(F) = 1 + max(h(R),h(S)). +``` + +Each c_f includes coefficient/source operations, full-row work, source +restoration, fixed-port/frame admission and head return. The d terms pay +control, selection and literal inverse dispatch. If costs differ by sign, +price the four actual child invocations separately and do not use the +sign-symmetric optimum. Shared initial admission I and factor preparation +P_F are paid once; no output count divides a full-row cost. The full batch bill +is `I + sum_F P_F + E + 2 sum_F C(F) + 2 min_F C(F)`, where E pays selector, +instruction emission/storage and any batch metadata not already in C. +A distinct E for different words is outside the fixed-price optimum. + +For uniform unit primitive prices, the balanced leaf recurrence is +`ell(1)=1; ell(n)=2 ell(floor(n/2))+2 ell(ceil(n/2))`. +Seed `58 mod 6 = 4` places the length-two child at index four in B0,B1,B2,A0,A1,A2 +order. The resulting lengths and complete primitive counts are: + +| Operator | B0 | B1 | B2 | A0 | A1 | A2 | +|---|---:|---:|---:|---:|---:|---:| +| Factor length | 4 | 5 | 6 | 7 | 2 | 3 | +| Primitive calls | 16 | 28 | 40 | 52 | 4 | 10 | +| Batch repeating this operator | 332 | 356 | 380 | 404 | 308 | 320 | + +These six literal primitive words are stored in CERTIFICATE.json and rebuilt +by an independent iterative expander. The free noncommutative interpreter +retains all ten independent dirty input symbols, checks the entire map and +its literal inverse, and forbids any primitive write to the three sources. +One batch connector plus maximum child depth `ceil(log2 7)=3` uses four +borrowed length-L dirty rows. Seven data rows plus three private child rows +make ten mutable rows total. Preparation, controller and scalar work are separate. + +## Paid dense realization and limits + +EXPECTED.json gives a literal dense integer realization for L=1,2,3 for every +repair word, with no zero-entry skipping. The data tape has ten mutable rows, +then 27 read-only L by L coefficient matrices. For every dot-product term, +the head visits its coefficient and source cell, then its target cell after +the dot product. Each primitive starts and ends at data cell zero. A separately +derived travel formula matches all 18 traces. + +For N primitives it pays `N L^2` coefficient reads and source reads, +`N L` target read/write pairs, `N L^2` multiplies, and `N(L^2+L)` add/subtracts. +Four clean scalar work registers hold source, coefficient, product and +accumulator. Each term clears its three operand/product registers; each output +clears the reused target register and accumulator and begins with a zero +accumulator: `N(3L^2+3L)` scalar zero assignments plus four startup assignments. +There are O(log L + log N) additional loop/address/control bits. These scalar +operations and address arithmetic must be charged in the chosen backend. + +A separate sequential read-only instruction tape stores 14 bits per primitive: +five factor bits, two four-bit ports and one sign bit. Reading it once and +returning its head costs 14N bit reads and 28N bit-cell movements. Emission and +the six-price selector are separately paid; this is no free precomputed advice. +The fixture's 27 supplied coefficient matrices cost 27L^2 read-only words; +constructing them from another representation is additional preparation. +Initial shape/port/word admission reads the `10L+27L^2` supplied data and +coefficient words; a separate supplied program is also scanned and priced. +No frame conversion is used by the dense fixture. Other realizations pay theirs. + +With coefficient bound H and initial magnitude D>=1, N primitives have +intermediate infinity norm at most `D(1+LH)^N`. A sufficient common signed +word width for all six schedules is +`w=2+ceil(log2(max(1,D,H)))+404 ceil(log2(1+LH))`, also covering dot-product +intermediates. Loads/stores/zero assignments and word-cell motion pay w bits; +integer multiplication/addition use the backend's w-bit costs. The data-head +trace is not the program-head trace or a free random-access model. + +The Python backend checks algebra and this specified accounting. It does not +implement a full physical tape compiler or benchmark runtime. Port-specific +head travel can differ between schedules; 308 versus 332 alone does not prove +a total runtime advantage for every backend. No precision or rounded-linearity +claim is made. The nonlinear control restores z but has a dirt-dependent output. + +## Completed coverage, provenance and handoff + +The search domain is exactly six repeated-operator source-path classes, with +counts (4,2,2) and balanced signs, plus the (2,2,2) lower-bound class. Stopping +rule: exhaust these domains, no stochastic pruning or further search. Independent +coverage is 720 support paths and six times 10,080 repeated paths, with feasible +counts 544,544,512 for each orientation. These censuses support the explicit +words; the global positive-price lower bound follows from the reduction above. + +The checker additionally covers 378 dense basis/dirty cases, seven rational +price order/tie fixtures, literal recursive expansion, all data restoration, +and exact expected invoices. test_package.py has 47 controls, including every +root query's deletion and sign flip, noncommuting factor order, lost input +dirt, missing/aliased/unpaid work, a valid nonoptimal word, invalid prices, +nonlinear readouts, and optimized-process source/certificate/receipt corruptions. +It relocates the package and requires byte-identical deterministic regeneration. + +Exact experimental base: `abdc6a7002abdbcd9e21bfc5e1a795784deacfdf`. +SOURCES.json pins the retained PR944 texts from that base and the read-only +orientation context. Mutable selected-pointer context is recorded, not consumed +by the standalone mathematical checker. The selected PR942/T37 construction +and conditional kappa `1661960547713947/10^18` remain unchanged. + +The pattern has not been located or hosted in a selected supplier. Common-label +and mutable-source realization, compatible frames, owner/whole-call admission, +all-size compilation, precision/tape and outer analytic transfer remain open +or inherited. No binding supplier improvement, new moment/kappa, architecture-wide +optimum or full theorem is claimed. The exact query-alphabet optimum is broader +than a finite price search but narrower than an arbitrary-circuit optimum. + +See CLAIM.md for task selection/overlap, VALIDATION.md for execution, and +NOTICE.md for contributor attribution and substantial AI assistance. diff --git a/research/hadamard-readout-census/sources/PR997-CONSTRUCTION.json b/research/hadamard-readout-census/sources/PR997-CONSTRUCTION.json new file mode 100644 index 0000000000..832996b307 --- /dev/null +++ b/research/hadamard-readout-census/sources/PR997-CONSTRUCTION.json @@ -0,0 +1,242 @@ +{ + "A_lengths": [ + 2, + 3, + 4, + 5 + ], + "B_lengths": [ + 1, + 2, + 3, + 4 + ], + "assignment_seed": 55, + "base_commit": "bbc600db2fc15007b7c914f4f2b2ed55fa909c87", + "format": "signed-hadamard-batch-seed55/1", + "leaf_calls": 238, + "matrix": [ + [ + 1, + 1, + 1, + 1 + ], + [ + 1, + -1, + 1, + -1 + ], + [ + 1, + 1, + -1, + -1 + ], + [ + 1, + -1, + -1, + 1 + ] + ], + "query_calls": 22, + "readout_pairs": [ + [ + [ + 0, + 6 + ], + [ + 3, + 7 + ] + ], + [ + [ + 2, + 0 + ], + [ + 2, + 4 + ] + ], + [ + [ + 1, + 3 + ], + [ + 5, + 7 + ] + ], + [ + [ + 4, + 0 + ] + ] + ], + "search": { + "admitted_trials": 491, + "distinct_source_paths": 3814, + "domain": "one positive and one negative query for each of four sources; each output gets one or two signed differences of visited connector states", + "optimality_claim": false, + "query_histogram": { + "22": 237, + "24": 254 + }, + "stopping_rule": "Complete exactly 4000 seed-55 shuffled source paths; select minimum charged leaf cost, then query count and lexicographic word.", + "trials": 4000 + }, + "source_path": [ + [ + 0, + -1 + ], + [ + 1, + 1 + ], + [ + 3, + -1 + ], + [ + 2, + 1 + ], + [ + 3, + 1 + ], + [ + 0, + 1 + ], + [ + 2, + -1 + ], + [ + 1, + -1 + ] + ], + "winning_trial": 2969, + "word": [ + [ + "A", + 0, + -1 + ], + [ + "A", + 1, + 1 + ], + [ + "A", + 3, + 1 + ], + [ + "B", + 0, + -1 + ], + [ + "A", + 2, + -1 + ], + [ + "B", + 1, + 1 + ], + [ + "A", + 1, + -1 + ], + [ + "A", + 1, + -1 + ], + [ + "B", + 3, + -1 + ], + [ + "A", + 0, + -1 + ], + [ + "A", + 2, + 1 + ], + [ + "B", + 2, + 1 + ], + [ + "A", + 1, + 1 + ], + [ + "A", + 3, + -1 + ], + [ + "B", + 3, + 1 + ], + [ + "A", + 2, + -1 + ], + [ + "B", + 0, + 1 + ], + [ + "A", + 0, + 1 + ], + [ + "B", + 2, + -1 + ], + [ + "A", + 0, + 1 + ], + [ + "A", + 2, + 1 + ], + [ + "B", + 1, + -1 + ] + ] +} diff --git a/research/hadamard-readout-census/sources/PR997-NOTICE.md b/research/hadamard-readout-census/sources/PR997-NOTICE.md new file mode 100644 index 0000000000..17949c72a5 --- /dev/null +++ b/research/hadamard-readout-census/sources/PR997-NOTICE.md @@ -0,0 +1,24 @@ +# Attribution and license + +Submitted through @1337isnot1337, prepared with substantial OpenAI Codex +assistance in research, implementation, exact verification and writing. +Apache-2.0 applies; LICENSE is copied from the repository root. No independent +human review or delegated worker is claimed. + +@CubeJerry's PR889 supplies the signed common-factor fanout contract, star +comparators and full child/storage/tape accounting. Ross Richardson's PR934 +and PR944 supply binary connector walks and the signed three-by-three +extension, including the free-operator and dirty-readout conventions. +Their PR889/944 READMEs and notices are retained byte for byte under vendor/, +with frozen heads and hashes in SOURCES.json. No executable predecessor code +is imported. PR943's binary four/five-source boundary is related and credited. + +Chafik Boukhalfa / chafreaky's PR628 supplies the balanced dirty-product +commutator and literal-inverse convention used by those predecessors. +The commutator and Hadamard matrix are classical; no literature-priority +claim is made. This contribution supplies the new signed four-by-four batch, +completed bounded nomination, literal lowering, invoices and exact evidence. + +Concurrent PR982 introduces output borrowing for a common-factor fanout. +Its changed scratch contract is separate and is not silently used here. +Existing source-local credit, assistance notices and licenses remain intact. diff --git a/research/hadamard-readout-census/sources/PR997-PROOF.md b/research/hadamard-readout-census/sources/PR997-PROOF.md new file mode 100644 index 0000000000..7c17a2a399 --- /dev/null +++ b/research/hadamard-readout-census/sources/PR997-PROOF.md @@ -0,0 +1,56 @@ +# Exact signed batch and restored recursive children + +At any point let +`z=z_initial+sum_j q_j B_j x_j`. A B_j query updates only q_j. An A_i query +of sign s adds `s A_i z_initial+sum_j s q_j A_i B_j x_j` to y_i. Therefore +the literal word is correct for free noncommuting linear maps precisely when +the final q is zero, each output's signed readout count is zero, and its +signed sum of q vectors is row i of H. `verify.py` checks these integer +conditions directly from the word, separately from the path constructor. +They also prove restoration on arbitrary dirty inputs at every L. + +The constructor finds two-difference representations for outputs 0,1,2 and +a one-difference representation for output 3. Both sides of every difference +are actual connector states along the same eight-step path. Inserting the +negative and positive readouts at those respective visits gives the desired +row, irrespective of which visit comes first. Readouts do not modify z or a +source; distinct output ports and restored child scratch permit them at the +same visit. All fourteen output calls are counted, including repeated taps. + +For an ordered product F with first half B applied before second half A, +borrow an arbitrary distinct dirty row u. The positive product shear is + +```text +u += B source; target += A u; u -= B source; target -= A u. +``` + +Linearity cancels the initial u contribution, leaves target increased by +A B source and restores u. Sources and all other arrays are unchanged. +This uses no inverse of A or B. Every negative product call is the literal +reverse of its positive primitive program, with each additive sign inverted. +Induction proves exact restoration and the recurrence +`C(F)=2C(B)+2C(A)+d_node`, with one fresh dirty row per active recursion level. +Pool rows never overlap the eight data rows or the batch connector. + +`verify.py` lowers every query into literal single-factor additive shears. +Its separate formal replay gives each of the twelve initial dirty rows an +independent symbol and treats every matrix factor as a free noncommuting +letter. The full polynomial endpoint must have only the sixteen demanded +Hadamard product terms and the initial output symbols; all eight non-output +rows restore. Appending the literal inverse must restore all twelve rows. +This is an exact algebraic certificate for the finite emitted factor lists; +the induction above explains the general product-child interface. + +The comparison words implement the identical H endpoint. Source stars hold +each B_j once while updating all outputs; output stars form each requested +signed source sum separately. All of their connector restores, output dirt +subtractions, product children and inverses are emitted and counted. The +unit-leaf lengths give complete totals 238, 364 and 526, with the same four +borrowed dirty arrays. Nonuniform child-price formulas and every further +adapter/dispatch/tape obligation are retained explicitly in README.md. + +No query minimum is asserted. The support lower bound of sixteen queries +does not by itself characterize signed four-by-four matrices, and the failed +ten/twelve-source-step screenings do not prove that eighteen or twenty +queries are impossible. The new evidence is the literal 22-query construction +and its complete 238-call realization in the priced exact interface. diff --git a/research/hadamard-readout-census/sources/PR997-README.md b/research/hadamard-readout-census/sources/PR997-README.md new file mode 100644 index 0000000000..fb146527f0 --- /dev/null +++ b/research/hadamard-readout-census/sources/PR997-README.md @@ -0,0 +1,183 @@ +# Signed Hadamard batching with one dirty connector + +**Recursive-interface research construction; no new kappa.** This supplies a +literal 22-query word for four sources and four outputs with Sylvester Hadamard +coefficients, replacing 40 queries for either separate-star orientation. It +retains a shared dirty connector between readouts and restores all sources, +the connector and every recursive child's scratch exactly. + +For factor lengths `|B|=[1,2,3,4]`, `|A|=[2,3,4,5]`, complete balanced child +lowering uses **238 primitive calls**, versus **364** for output stars and +**526** for source stars. All three use **four borrowed dirty arrays** in +addition to the eight source/output arrays. Every child and inverse operates +on the full length-L row and is counted. No clean row is assumed. + +| Exact quantity | Candidate | Output stars | Source stars | +|---|---:|---:|---:| +| Complete queries | 22 | 40 | 40 | +| B query counts | 2,2,2,2 | 8,8,8,8 | 2,2,2,2 | +| A query counts | 4,4,4,2 | 2,2,2,2 | 8,8,8,8 | +| Complete primitive calls | 238 | 364 | 526 | +| Borrowed dirty rows | 4 | 4 | 4 | +| L=2 literal tape travel, word slots | 130,596 | 152,288 | 329,732 | +| L=2 observed signed word bits | 47 | 47 | 47 | + +The tape counts are for the fully specified dense integer reference trace, +including returning home after every leaf; they are not timing measurements +or an implementation of the paper's native supplier. Work with nonuniform +operator prices is given explicitly below, without inferring a generic bit +complexity gain from the unit-price fixture. + +## Reproduce + +From the repository root, standard-library Python 3.11+ suffices: + +```sh +python3 -I -B research/signed-hadamard-batch-seed55/verify.py --replay-search +python3 -I -B research/signed-hadamard-batch-seed55/test_package.py +``` + +Expected final markers: + +```text +PASS_SIGNED_HADAMARD_BATCH queries=22_vs_40 leaf_calls=238_vs_364_vs_526 dirty_arrays=4 controls=8 no_new_kappa +PASS_SIGNED_HADAMARD_PACKAGE standalone_optimized_replay=PASS controls=8 +``` + +The first command regenerates the completed search and compares every +construction field, checks the signed query identity, emits balanced recursive +products, replays all twelve arbitrary dirty input columns as free +noncommutative polynomials, checks literal inverses, and executes dense integer +fixtures of dimensions two and three. The receipt includes all leaf +multiplicities, primitive-word digests, coefficient/source access, arithmetic, +storage, preflight checks, instruction bits and exact head travel. + +Use `--output /absolute/new/directory` to retain all three literal primitive +programs. Existing destinations are refused. The standalone test uses an +optimized Python process and a path with spaces, and rejects eight source, +construction, invoice, receipt and output-preservation faults. The verifier +has eight further obligation-specific controls. It imports neither the +constructor nor a predecessor implementation. + +## Contract and literal construction + +There are distinct arbitrary dirty rows `x_0,...,x_3`, `y_0,...,y_3` and `z`. +A_i and B_j are exact additive linear maps and need not commute or be +invertible. A complete restored query is either + +```text +B_j^s: z += s B_j x_j +A_i^s: y_i += s A_i z, s = -1 or +1. +``` + +It preserves its source, other data, private scratch and prescribed head +positions. The sources and operator coefficients are fixed, and intermediate +outputs are exclusively owned. The demanded endpoint is + +```text +y_i += sum_j H_ij A_i B_j x_j, +H = [[1,1,1,1],[1,-1,1,-1],[1,1,-1,-1],[1,-1,-1,1]]. +``` + +`CONSTRUCTION.json` contains the literal word and every readout pair. Its B +path is + +```text +B0- B1+ B3- B2+ B3+ B0+ B2- B1-. +``` + +Each B_j is applied and unapplied once. Outputs 0,1,2 each take four signed +readouts, and output 3 takes two. For each output the readout signs sum to +zero, cancelling its contribution from arbitrary initial z, while their +signed connector coefficients equal the corresponding Hadamard row. This +proves the full identity at every row length with noncommuting operators; +the program also restores z. [PROOF.md](PROOF.md) details the identity and +child lowering. No optimum is claimed. + +## Complete cost and storage recurrence + +Let C(F;L,w) price a restored additive child for the ordered factor list F, +using the maximum price of its two signs. Leaf prices include coefficients, +source access, target update, routing, head returns and arithmetic. The +inherited binary dirty commutator gives + +```text +C([f]) = c_f + d_leaf, +C(F) = 2 C(F_first) + 2 C(F_second) + d_node(F). +``` + +Both halves execute on full length-L rows. The node borrows a distinct dirty +row; its four complete child calls restore that row. Negative children are +literal inverses, with the same call multiplicities. In the unit-price fixture, +L(1)=1 and L(n)=2L(floor(n/2))+2L(ceil(n/2)). + +Write B=sum_j C(B_j), and let R price the additional batch coefficient/sign +preparation, dispatch, program storage, source/port bindings, any required +frame adapters, parking and tape returns not already in child prices. Then + +```text +C_candidate = 2 B + 4(C(A0)+C(A1)+C(A2)) + 2 C(A3) + R_candidate, +C_source_stars = 2 B + 8 sum_i C(A_i) + R_source_stars, +C_output_stars = 8 B + 2 sum_i C(A_i) + R_output_stars. +``` + +Against source stars the child saving is +`4(C(A0)+C(A1)+C(A2))+6C(A3)`; against output stars it is +`6B-2(C(A0)+C(A1)+C(A2))`. R differences must still be paid. Thus the +candidate need not beat output stars under every positive price assignment. +At the stated unit-leaf lengths the child saving against the better star +comparator is exactly **126**, with the full counts 238/364/526. +The receipt also checks a positive-price counterexample: +`C(B_j)=1`, `C(A_0)=C(A_1)=C(A_2)=1000`, `C(A_3)=1` gives candidate +cost 12,010 and output-star cost 6,034, before additional R. This prevents +interpreting the fixture's benefit as universal domination of both comparators. + +Child scratch is reused only after return, and the eight data rows and z are +excluded from it. The peak is +`1+max(max_i ceil(log2 |A_i|), max_j ceil(log2 |B_j|))` borrowed dirty rows, here four. +Read-only coefficient storage, the emitted program, descriptors and loop state +are additional. The dense reference uses 12L dirty data words and 24L² +coefficient words, one scalar dot-product accumulator, and paid index/control +state. Every matrix row, coefficient/data alias and pair of data roles is +checked before the trace. The certificate prices each leaf instruction with +both role IDs, factor ID and sign. At word size w the literal travel costs +travel*w bit movement, plus listed loads/stores, multiplications, additions, +negations and pointer/control work. This is a reference invoice, not an +all-size precision or fixed-tape implementation theorem. + +## Search, provenance and limits + +OS seed **55**, exact base **`bbc600db2fc15007b7c914f4f2b2ed55fa909c87`**. +The selected certificate there is PR942's conditional +`1661960547713947/10^18`; it is unchanged. Three alternatives and the local +claim are in `CLAIM.json`. No pinned coordination issue existed. + +The final domain is exactly 4,000 shuffled eight-step signed source paths, +one positive and one negative query per B_j. Each output is expressed by +one or two signed differences of visited states. All trials complete: +3,814 distinct paths, 491 admitted trials, with 237 22-query and 254 24-query +nominees. Select minimum complete unit-leaf cost, then query count and +lexicographic word. No rescan or additional seeds are used. This is not an +exhaustion of the full query alphabet or an optimality theorem. + +The earlier 16,000 ten-source-step and 20,000 twelve-source-step screenings +found no path supplying all four rows with two readouts each. These are failed +bounded searches, not exclusions. The single mechanism revision allows more +output readouts while retaining the minimum source-call profile; the completed +construction is the positive result packaged here. + +The signed query contract and product lowering build on @CubeJerry's PR889 +and Ross Richardson's PR934/944. PR943 covers binary four-source batching; +this signed Hadamard object differs. Source heads and retained notices are +in `SOURCES.json` and `vendor/`. PR982's new output-borrowed fanout changes +the common-factor scratch contract; it is distinct from this multi-source +signed batch with a dedicated connector. Full open-PR scans and targeted +all-state searches were refreshed repeatedly through that arrival. + +This is a completed exact recursive-interface construction, not a selected +supplier. No physical owner/frame compiler, hosted invoice, assembly change, +new moment/kappa, measured speedup or multiplication theorem is supplied. +Finite dense traces do not discharge inherited tape, precision, rounding, +all-size compiler, mutable-source or analytic transfer assumptions. +Original sources, `upstream/` and the selected frontier remain untouched. +See `NOTICE.md` for attribution and substantial AI-assistance disclosure. diff --git a/research/hadamard-readout-census/test_package.py b/research/hadamard-readout-census/test_package.py new file mode 100644 index 0000000000..425bdeb794 --- /dev/null +++ b/research/hadamard-readout-census/test_package.py @@ -0,0 +1,72 @@ +"""Regeneration, read-only relocation, and real subprocess rejection controls.""" + +import hashlib +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +ROOT = Path(__file__).resolve().parent + + +def run(script, *args, cwd=None, good=True): + result = subprocess.run([sys.executable, '-I', '-O', '-B', str(script), *map(str, args)], + cwd=cwd, capture_output=True, text=True) + if good and result.returncode != 0: + raise RuntimeError(result.stdout + result.stderr) + if not good and result.returncode == 0: + raise RuntimeError('deliberate failure unexpectedly accepted') + return result + + +def main(): + verified = run(ROOT / 'verify.py') + print(verified.stdout, end='') + with tempfile.TemporaryDirectory(prefix='hadamard-census-') as temporary: + tmp = Path(temporary) + generated = tmp / 'regenerated.json' + run(ROOT / 'census.py', '--output', generated, cwd=tmp) + if generated.read_bytes() != (ROOT / 'CERTIFICATE.json').read_bytes(): + raise ValueError('byte-exact certificate regeneration mismatch') + relocated = tmp / 'relocated' + shutil.copytree(ROOT, relocated) + for path in relocated.rglob('*'): + if path.is_file(): + path.chmod(0o444) + result = run(relocated / 'verify.py', cwd=tmp) + if result.stdout != verified.stdout: + raise ValueError('read-only relocated receipt mismatch') + certificate = relocated / 'CERTIFICATE.json' + certificate.chmod(0o644) + original = certificate.read_bytes() + data = json.loads(original) + data['profile_histogram'][0]['paths'] += 1 + certificate.write_text(json.dumps(data) + '\n') + failure = run(relocated / 'verify.py', cwd=tmp, good=False) + if 'independent exhaustive histogram mismatch' not in failure.stderr: + raise ValueError('wrong coverage rejection') + certificate.write_bytes(original) + data = json.loads(original) + data['word'].pop() + certificate.write_text(json.dumps(data) + '\n') + failure = run(relocated / 'verify.py', cwd=tmp, good=False) + if 'dirty connector not restored' not in failure.stderr: + raise ValueError('wrong restoration rejection') + certificate.write_bytes(original) + source = relocated / 'sources/PR997-CONSTRUCTION.json' + source.chmod(0o644) + source.write_bytes(source.read_bytes() + b' ') + failure = run(relocated / 'verify.py', cwd=tmp, good=False) + if 'source pin mismatch' not in failure.stderr: + raise ValueError('wrong provenance rejection') + before = hashlib.sha256(generated.read_bytes()).hexdigest() + failure = run(ROOT / 'census.py', '--output', generated, cwd=tmp, good=False) + if 'FileExistsError' not in failure.stderr or hashlib.sha256(generated.read_bytes()).hexdigest() != before: + raise ValueError('occupied output was not preserved') + print('PASS_HADAMARD_READOUT_PACKAGE regeneration=PASS relocation=PASS controls=4') + + +if __name__ == '__main__': + main() diff --git a/research/hadamard-readout-census/verify.py b/research/hadamard-readout-census/verify.py new file mode 100644 index 0000000000..20f4f204a5 --- /dev/null +++ b/research/hadamard-readout-census/verify.py @@ -0,0 +1,369 @@ +"""Independent permutation census, free-operator replay, and package checks.""" + +from collections import Counter +from fractions import Fraction +import hashlib +from itertools import permutations, product +import json +from pathlib import Path +import random + +ROOT = Path(__file__).resolve().parent +H = ((1, 1, 1, 1), (1, -1, 1, -1), + (1, 1, -1, -1), (1, -1, -1, 1)) +TARGETS = tuple((1,) + t for t in product((-1, 1), repeat=3)) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def balanced_calls(n): + # Price literal emitted programs rather than importing the generator's + # analytical count recurrence. + return len(product_word(tuple(('price', 0, j) for j in range(n)), 0, 1, + tuple(range(2, 12)))) + + +def difference_minima(vertices): + """Independent shortest sum of state differences; no multiset enumerator.""" + d1 = {tuple(a[j] - b[j] for j in range(4)) for a in vertices for b in vertices} + d2 = {tuple(a[j] + b[j] for j in range(4)) for a in d1 for b in d1} + out = {} + for t in TARGETS: + if t in d1: + out[t] = 2 + elif t in d2: + out[t] = 4 + elif any(tuple(t[j] - d[j] for j in range(4)) in d2 for d in d1): + out[t] = 6 + else: + # Every coordinate unit difference occurs in this loop; four + # pairs give an explicit upper bound for every target sign row. + out[t] = 8 + return out + + +def independent_census(): + histogram = Counter() + cache = {} + events = tuple((j, s) for j in range(4) for s in (-1, 1)) + for word in permutations(events): + first = [0] * 4 + q = [0] * 4 + qs = [(0, 0, 0, 0)] + for j, s in word: + if first[j] == 0: + first[j] = s + q[j] += s + qs.append(tuple(q)) + require(q == [0] * 4, 'source loop failed') + vertices = tuple(sorted({tuple(v[j] * first[j] for j in range(4)) for v in qs})) + if vertices not in cache: + cache[vertices] = difference_minima(vertices) + minima = cache[vertices] + profile = [] + for row in H: + target = tuple(row[j] * first[j] for j in range(4)) + target = tuple(target[0] * x for x in target) + profile.append(minima[target]) + histogram[tuple(profile)] += 1 + return histogram, len(cache) + + +def query_replay(word, expected=H): + q = [0] * 4 + initial = [0] * 4 + endpoint = [[0] * 4 for _ in range(4)] + calls = {'A': [0] * 4, 'B': [0] * 4} + for kind, i, sign in word: + require(kind in calls and type(i) is int and 0 <= i < 4 and sign in (-1, 1), 'bad query') + calls[kind][i] += 1 + if kind == 'B': + q[i] += sign + else: + initial[i] += sign + for j in range(4): + endpoint[i][j] += sign * q[j] + require(q == [0] * 4, 'dirty connector not restored') + require(initial == [0] * 4, 'initial connector dirt leaks into outputs') + require(tuple(map(tuple, endpoint)) == tuple(map(tuple, expected)), 'wrong signed endpoint') + return calls + + +def inverse(word): + return [(d, s, a, -sign) for d, s, a, sign in reversed(word)] + + +def product_word(factors, source, target, pool): + if len(factors) == 1: + return [(target, source, factors[0], 1)] + require(pool, 'insufficient dirty child pool') + middle, deeper = pool[0], pool[1:] + split = len(factors) // 2 + b = product_word(factors[:split], source, middle, deeper) + a = product_word(factors[split:], middle, target, deeper) + return b + a + inverse(b) + inverse(a) + + +def lower(word, alengths, blengths): + out = [] + for kind, i, sign in word: + n = alengths[i] if kind == 'A' else blengths[i] + factors = tuple((kind, i, j) for j in range(n)) + source, target = (8, 4 + i) if kind == 'A' else (i, 8) + query = product_word(factors, source, target, (9, 10, 11)) + out.extend(query if sign > 0 else inverse(query)) + return out + + +def formal_replay(program, alengths, blengths, query=None): + initial = [{((), r): 1} for r in range(12)] + state = [dict(p) for p in initial] + maximum_terms = 1 + + def apply(program): + nonlocal maximum_terms + for dst, src, factor, sign in program: + require(dst != src, 'source/target alias') + require(dst >= 4, 'external source written at a prefix') + for (letters, row), coefficient in list(state[src].items()): + key = ((factor,) + letters, row) + state[dst][key] = state[dst].get(key, 0) + sign * coefficient + if not state[dst][key]: + del state[dst][key] + maximum_terms = max(maximum_terms, max(map(len, state))) + + apply(program) + expected = [dict(p) for p in initial] + if query is None: + for i, row in enumerate(H): + for j, sign in enumerate(row): + letters = tuple(('A', i, k) for k in reversed(range(alengths[i]))) + letters += tuple(('B', j, k) for k in reversed(range(blengths[j]))) + expected[4 + i][(letters, j)] = sign + else: + kind, i, sign = query + n = alengths[i] if kind == 'A' else blengths[i] + source, target = (8, 4 + i) if kind == 'A' else (i, 8) + letters = tuple((kind, i, k) for k in reversed(range(n))) + expected[target][(letters, source)] = sign + require(state == expected, 'free noncommuting dirty-state endpoint failed') + apply(inverse(program)) + require(state == initial, 'literal primitive inverse failed') + return maximum_terms + + +def prefix_bound(program, operator_bound=6, input_bound=7): + """Bound row and scalar intermediates, including independent initial dirt.""" + state = [{((), r): 1} for r in range(12)] + largest = input_bound + for dst, src, factor, sign in program: + target_bound = input_bound * sum(abs(c) * operator_bound ** len(key[0]) + for key, c in state[dst].items()) + increment_bound = input_bound * sum(abs(c) * operator_bound ** (len(key[0]) + 1) + for key, c in state[src].items()) + # Also cover partial dot products, coefficient products and target + # addition before symbolic cancellation can lower the row bound. + largest = max(largest, target_bound + increment_bound) + for (letters, row), coefficient in list(state[src].items()): + key = ((factor,) + letters, row) + state[dst][key] = state[dst].get(key, 0) + sign * coefficient + if state[dst][key] == 0: + del state[dst][key] + bound = input_bound * sum(abs(c) * operator_bound ** len(key[0]) + for key, c in state[dst].items()) + largest = max(largest, bound) + return largest + + +def dense_checks(program, alengths, blengths, dimension): + rng = random.Random(55 + dimension) + factors = {(kind, i, j): tuple(tuple(rng.randrange(-2, 3) for _ in range(dimension)) + for _ in range(dimension)) for kind, lengths in (('A', alengths), ('B', blengths)) + for i, length in enumerate(lengths) for j in range(length)} + + def mv(matrix, vector): + return [sum(a * b for a, b in zip(row, vector)) for row in matrix] + + def chain(kind, i, length, vector): + for j in range(length): + vector = mv(factors[kind, i, j], vector) + return vector + + def apply(state, instructions): + for dst, src, factor, sign in instructions: + increment = mv(factors[factor], state[src]) + state[dst] = [x + sign * y for x, y in zip(state[dst], increment)] + + cases = [] + for index in range(12 * dimension): + state = [[0] * dimension for _ in range(12)] + state[index // dimension][index % dimension] = 1 + cases.append(state) + cases.append([[rng.randrange(-7, 8) for _ in range(dimension)] for _ in range(12)]) + for initial in cases: + expected = [list(row) for row in initial] + for i, hrow in enumerate(H): + for j, sign in enumerate(hrow): + value = chain('B', j, blengths[j], list(initial[j])) + value = chain('A', i, alengths[i], value) + expected[4 + i] = [x + sign * y for x, y in zip(expected[4 + i], value)] + state = [list(row) for row in initial] + apply(state, program) + require(state == expected, 'independent dense endpoint failed') + apply(state, inverse(program)) + require(state == initial, 'independent dense inverse failed') + return len(cases) + + +def internal_nodes(n): + return 0 if n == 1 else 1 + 2 * internal_nodes(n // 2) + 2 * internal_nodes(n - n // 2) + + +def complete_invoice(word, alengths, blengths): + calls = query_replay(word) + leaves = sum(calls[kind][i] * balanced_calls(n) + for kind, lengths in (('A', alengths), ('B', blengths)) + for i, n in enumerate(lengths)) + nodes = sum(calls[kind][i] * internal_nodes(n) + for kind, lengths in (('A', alengths), ('B', blengths)) + for i, n in enumerate(lengths)) + return {'queries': len(word), 'primitive_leaves': leaves, 'echo_nodes': nodes, + 'child_call_entries': leaves + nodes, 'dirty_arrays': 4, + 'source_rows': 4, 'output_rows': 4, + 'coefficient_matrices': sum(alengths) + sum(blengths)} + + +def source_checks(): + pins = json.loads((ROOT / 'SOURCES.json').read_text()) + names = {'sources/PR997-' + n for n in ('CONSTRUCTION.json', 'PROOF.md', 'NOTICE.md', 'README.md')} + names |= {'sources/BASE-selected-result.json', 'sources/PR1088-README.md', 'sources/PR1088-NOTICE.md'} + require(set(pins['files']) == names, 'source inventory coverage gap') + for name, pin in pins['files'].items(): + path = ROOT / name + require(hashlib.sha256(path.read_bytes()).hexdigest() == pin['sha256'], 'source pin mismatch: ' + name) + + +def main(): + source_checks() + result = json.loads((ROOT / 'CERTIFICATE.json').read_text()) + predecessor = json.loads((ROOT / 'sources/PR997-CONSTRUCTION.json').read_text()) + require(result['format'] == 'hadamard-readout-census/1' and result['assignment_seed'] == 55, + 'experiment metadata mismatch') + require(result['base_commit'] == 'ce7ad1b6ab09452c3478723a2e96ed5ff212dc08', 'base mismatch') + require(result['A_lengths'] == predecessor['A_lengths'] and + result['B_lengths'] == predecessor['B_lengths'], 'comparison fixture changed') + histogram, cache_count = independent_census() + expected = Counter({tuple(p['profile']): p['paths'] for p in result['profile_histogram']}) + require(histogram == expected, 'independent exhaustive histogram mismatch') + require(sum(histogram.values()) == 40320, 'signed coverage gap') + require(result['unsigned_paths'] == 2520 and result['signed_paths'] == 40320, 'reported coverage mismatch') + require(len(histogram) == 114, 'profile coverage mismatch') + frontier = sorted(p for p in histogram if not any( + q != p and all(x <= y for x, y in zip(q, p)) for q in histogram)) + require(list(map(list, frontier)) == result['pareto_profiles'], 'Pareto mismatch') + families = {p for pattern in ((2, 4, 4, 4), (2, 2, 6, 6), (2, 2, 4, 8)) + for p in permutations(pattern)} + require(set(frontier) == families, 'written profile families differ') + require(8 + min(map(sum, histogram)) == result['minimum_queries'] == 22, 'query optimum mismatch') + ap = [balanced_calls(n) for n in result['A_lengths']] + bp = [balanced_calls(n) for n in result['B_lengths']] + require(ap == result['A_leaf_prices'] and bp == result['B_leaf_prices'], 'price receipt mismatch') + best = 2 * sum(bp) + min(sum(x * y for x, y in zip(p, ap)) for p in histogram) + require(best == result['minimum_leaf_calls'] == 222, 'weighted optimum mismatch') + price_cases = 0 + for prices in product((Fraction(1, 2), Fraction(1), Fraction(3, 2), + Fraction(2), Fraction(3), Fraction(4)), repeat=4): + a, b, c, d = sorted(prices) + envelope = 4*a + 4*b + 2*c + 2*d + min(2*c, 4*a) + actual = min(sum(x*y for x, y in zip(p, prices)) for p in histogram) + require(envelope == actual, 'rational price envelope mismatch') + price_cases += 1 + local_queries = 0 + for kind in ('A', 'B'): + for i in range(4): + for sign in (-1, 1): + query = (kind, i, sign) + formal_replay(lower([query], result['A_lengths'], result['B_lengths']), + result['A_lengths'], result['B_lengths'], query=query) + local_queries += 1 + dense = 0 + require([tuple(entry['profile']) for entry in result['frontier_words']] == frontier, + 'frontier witness coverage gap') + for entry in result['frontier_words']: + calls = query_replay(entry['word']) + require(calls['A'] == entry['profile'] and calls['B'] == [2] * 4, 'witness call profile mismatch') + program = lower(entry['word'], result['A_lengths'], result['B_lengths']) + formal_replay(program, result['A_lengths'], result['B_lengths']) + dense += dense_checks(program, result['A_lengths'], result['B_lengths'], 2) + calls = query_replay(result['word']) + require(calls['A'] == result['chosen_profile'], 'chosen word profile mismatch') + bevents = [(i, sign) for kind, i, sign in result['word'] if kind == 'B'] + first = [0] * 4 + for i, sign in bevents: + if first[i] == 0: + first[i] = sign + require([i for i, sign in bevents] == result['source_path'] and first == result['first_signs'], + 'source path receipt mismatch') + program = lower(result['word'], result['A_lengths'], result['B_lengths']) + require(len(program) == best, 'complete lowering count mismatch') + dense += dense_checks(program, result['A_lengths'], result['B_lengths'], 3) + query_replay(predecessor['word']) + old = lower(predecessor['word'], predecessor['A_lengths'], predecessor['B_lengths']) + formal_replay(old, predecessor['A_lengths'], predecessor['B_lengths']) + require(len(old) == predecessor['leaf_calls'] == 238, 'matched predecessor count mismatch') + dense += dense_checks(old, predecessor['A_lengths'], predecessor['B_lengths'], 3) + new_invoice = complete_invoice(result['word'], result['A_lengths'], result['B_lengths']) + old_invoice = complete_invoice(predecessor['word'], predecessor['A_lengths'], predecessor['B_lengths']) + require(new_invoice['echo_nodes'] == 66 and old_invoice['echo_nodes'] == 72, 'echo invoice mismatch') + require(new_invoice['child_call_entries'] == 288 and old_invoice['child_call_entries'] == 310, + 'child dispatch invoice mismatch') + bound = max(prefix_bound(program + inverse(program)), prefix_bound(old + inverse(old))) + common_signed_width = bound.bit_length() + 1 + controls = 0 + mutations = [] + for kind in ('A', 'B'): + for index in [k for k, event in enumerate(result['word']) if event[0] == kind][:2]: + removed = [list(e) for e in result['word']] + del removed[index] + mutations.append(removed) + flipped = [list(e) for e in result['word']] + flipped[index][2] *= -1 + mutations.append(flipped) + for word in mutations: + try: + query_replay(word) + except ValueError: + controls += 1 + else: + raise ValueError('mutation unexpectedly passed') + try: + formal_replay(program[:-1], result['A_lengths'], result['B_lengths']) + except ValueError: + controls += 1 + else: + raise ValueError('missing restoration leaf passed') + require(controls == 9, 'control count mismatch') + # Equal complete query prices prefer a 22-query profile, and sufficiently + # costly outer dispatch reverses this particular operation-count benefit. + require(8 + sum(result['chosen_profile']) == 24, 'weighted word query count mismatch') + require(best + 100 * 24 > 238 + 100 * 22, 'expensive dispatch control failed') + controls += 1 + print('PASS_HADAMARD_READOUT_CENSUS signed_paths=40320 profiles=114 pareto=22 ' + 'queries=22 leaf_calls=222_vs_238 controls=10 no_new_kappa') + print(json.dumps({'independent_vertex_sets': cache_count, + 'frontier_free_operator_replays': len(frontier), + 'dense_basis_and_dirty_replays': dense, + 'rational_price_cases': price_cases, 'local_child_contracts': local_queries, + 'common_prefix_absolute_bound': bound, 'common_signed_width_bits': common_signed_width, + 'chosen_primitive_sha256': hashlib.sha256(json.dumps(program, separators=(',', ':')).encode()).hexdigest(), + 'predecessor_primitive_sha256': hashlib.sha256(json.dumps(old, separators=(',', ':')).encode()).hexdigest(), + 'new_invoice': new_invoice, 'predecessor_invoice': old_invoice, + 'chosen_primitive_calls': len(program), + 'predecessor_primitive_calls': len(old)})) + + +if __name__ == '__main__': + main()