diff --git a/research/three-source-envelope-floor/CERTIFICATE.json b/research/three-source-envelope-floor/CERTIFICATE.json new file mode 100644 index 0000000000..5fc53da268 --- /dev/null +++ b/research/three-source-envelope-floor/CERTIFICATE.json @@ -0,0 +1,4500 @@ +{ + "schema_version": 1, + "claim": "minimum_peak_four_cost_2n_plus_2", + "cases": [ + { + "targets": 2, + "auxiliaries": 0, + "word": [ + [ + 0, + 1 + ], + [ + 3, + 0 + ], + [ + 4, + 0 + ], + [ + 0, + 1 + ], + [ + 3, + 2 + ], + [ + 4, + 2 + ] + ], + "cost": 6, + "forward_peak": 4, + "reverse_peak": 4 + }, + { + "targets": 2, + "auxiliaries": 1, + "word": [ + [ + 0, + 1 + ], + [ + 3, + 0 + ], + [ + 4, + 0 + ], + [ + 0, + 1 + ], + [ + 3, + 2 + ], + [ + 4, + 2 + ] + ], + "cost": 6, + "forward_peak": 4, + "reverse_peak": 4 + }, + { + "targets": 2, + "auxiliaries": 5, + "word": [ + [ + 0, + 1 + ], + [ + 3, + 0 + ], + [ + 4, + 0 + ], + [ + 0, + 1 + ], + [ + 3, + 2 + ], + [ + 4, + 2 + ] + ], + "cost": 6, + "forward_peak": 4, + "reverse_peak": 4 + }, + { + "targets": 3, + "auxiliaries": 0, + "word": [ + [ + 0, + 1 + ], + [ + 3, + 0 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ], + [ + 0, + 1 + ], + [ + 3, + 2 + ], + [ + 4, + 2 + ], + [ + 5, + 2 + ] + ], + "cost": 8, + "forward_peak": 4, + "reverse_peak": 4 + }, + { + "targets": 3, + "auxiliaries": 1, + "word": [ + [ + 0, + 1 + ], + [ + 3, + 0 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ], + [ + 0, + 1 + ], + [ + 3, + 2 + ], + [ + 4, + 2 + ], + [ + 5, + 2 + ] + ], + "cost": 8, + "forward_peak": 4, + "reverse_peak": 4 + }, + { + "targets": 3, + "auxiliaries": 5, + "word": [ + [ + 0, + 1 + ], + [ + 3, + 0 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ], + [ + 0, + 1 + ], + [ + 3, + 2 + ], + [ + 4, + 2 + ], + [ + 5, + 2 + ] + ], + "cost": 8, + "forward_peak": 4, + "reverse_peak": 4 + }, + { + "targets": 4, + "auxiliaries": 0, + "word": [ + [ + 0, + 1 + ], + [ + 3, + 0 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ], + [ + 0, + 1 + ], + [ + 3, + 2 + ], + [ + 4, + 2 + ], + [ + 5, + 2 + ], + [ + 6, + 2 + ] + ], + "cost": 10, + "forward_peak": 4, + "reverse_peak": 4 + }, + { + "targets": 4, + "auxiliaries": 1, + "word": [ + [ + 0, + 1 + ], + [ + 3, + 0 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ], + [ + 0, + 1 + ], + [ + 3, + 2 + ], + [ + 4, + 2 + ], + [ + 5, + 2 + ], + [ + 6, + 2 + ] + ], + "cost": 10, + "forward_peak": 4, + "reverse_peak": 4 + }, + { + "targets": 4, + "auxiliaries": 5, + "word": [ + [ + 0, + 1 + ], + [ + 3, + 0 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ], + [ + 0, + 1 + ], + [ + 3, + 2 + ], + [ + 4, + 2 + ], + [ + 5, + 2 + ], + [ + 6, + 2 + ] + ], + "cost": 10, + "forward_peak": 4, + "reverse_peak": 4 + }, + { + "targets": 8, + "auxiliaries": 0, + "word": [ + [ + 0, + 1 + ], + [ + 3, + 0 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ], + [ + 7, + 0 + ], + [ + 8, + 0 + ], + [ + 9, + 0 + ], + [ + 10, + 0 + ], + [ + 0, + 1 + ], + [ + 3, + 2 + ], + [ + 4, + 2 + ], + [ + 5, + 2 + ], + [ + 6, + 2 + ], + [ + 7, + 2 + ], + [ + 8, + 2 + ], + [ + 9, + 2 + ], + [ + 10, + 2 + ] + ], + "cost": 18, + "forward_peak": 4, + "reverse_peak": 4 + }, + { + "targets": 8, + "auxiliaries": 1, + "word": [ + [ + 0, + 1 + ], + [ + 3, + 0 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ], + [ + 7, + 0 + ], + [ + 8, + 0 + ], + [ + 9, + 0 + ], + [ + 10, + 0 + ], + [ + 0, + 1 + ], + [ + 3, + 2 + ], + [ + 4, + 2 + ], + [ + 5, + 2 + ], + [ + 6, + 2 + ], + [ + 7, + 2 + ], + [ + 8, + 2 + ], + [ + 9, + 2 + ], + [ + 10, + 2 + ] + ], + "cost": 18, + "forward_peak": 4, + "reverse_peak": 4 + }, + { + "targets": 8, + "auxiliaries": 5, + "word": [ + [ + 0, + 1 + ], + [ + 3, + 0 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ], + [ + 7, + 0 + ], + [ + 8, + 0 + ], + [ + 9, + 0 + ], + [ + 10, + 0 + ], + [ + 0, + 1 + ], + [ + 3, + 2 + ], + [ + 4, + 2 + ], + [ + 5, + 2 + ], + [ + 6, + 2 + ], + [ + 7, + 2 + ], + [ + 8, + 2 + ], + [ + 9, + 2 + ], + [ + 10, + 2 + ] + ], + "cost": 18, + "forward_peak": 4, + "reverse_peak": 4 + }, + { + "targets": 16, + "auxiliaries": 0, + "word": [ + [ + 0, + 1 + ], + [ + 3, + 0 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ], + [ + 7, + 0 + ], + [ + 8, + 0 + ], + [ + 9, + 0 + ], + [ + 10, + 0 + ], + [ + 11, + 0 + ], + [ + 12, + 0 + ], + [ + 13, + 0 + ], + [ + 14, + 0 + ], + [ + 15, + 0 + ], + [ + 16, + 0 + ], + [ + 17, + 0 + ], + [ + 18, + 0 + ], + [ + 0, + 1 + ], + [ + 3, + 2 + ], + [ + 4, + 2 + ], + [ + 5, + 2 + ], + [ + 6, + 2 + ], + [ + 7, + 2 + ], + [ + 8, + 2 + ], + [ + 9, + 2 + ], + [ + 10, + 2 + ], + [ + 11, + 2 + ], + [ + 12, + 2 + ], + [ + 13, + 2 + ], + [ + 14, + 2 + ], + [ + 15, + 2 + ], + [ + 16, + 2 + ], + [ + 17, + 2 + ], + [ + 18, + 2 + ] + ], + "cost": 34, + "forward_peak": 4, + "reverse_peak": 4 + }, + { + "targets": 16, + "auxiliaries": 1, + "word": [ + [ + 0, + 1 + ], + [ + 3, + 0 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ], + [ + 7, + 0 + ], + [ + 8, + 0 + ], + [ + 9, + 0 + ], + [ + 10, + 0 + ], + [ + 11, + 0 + ], + [ + 12, + 0 + ], + [ + 13, + 0 + ], + [ + 14, + 0 + ], + [ + 15, + 0 + ], + [ + 16, + 0 + ], + [ + 17, + 0 + ], + [ + 18, + 0 + ], + [ + 0, + 1 + ], + [ + 3, + 2 + ], + [ + 4, + 2 + ], + [ + 5, + 2 + ], + [ + 6, + 2 + ], + [ + 7, + 2 + ], + [ + 8, + 2 + ], + [ + 9, + 2 + ], + [ + 10, + 2 + ], + [ + 11, + 2 + ], + [ + 12, + 2 + ], + [ + 13, + 2 + ], + [ + 14, + 2 + ], + [ + 15, + 2 + ], + [ + 16, + 2 + ], + [ + 17, + 2 + ], + [ + 18, + 2 + ] + ], + "cost": 34, + "forward_peak": 4, + "reverse_peak": 4 + }, + { + "targets": 16, + "auxiliaries": 5, + "word": [ + [ + 0, + 1 + ], + [ + 3, + 0 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ], + [ + 7, + 0 + ], + [ + 8, + 0 + ], + [ + 9, + 0 + ], + [ + 10, + 0 + ], + [ + 11, + 0 + ], + [ + 12, + 0 + ], + [ + 13, + 0 + ], + [ + 14, + 0 + ], + [ + 15, + 0 + ], + [ + 16, + 0 + ], + [ + 17, + 0 + ], + [ + 18, + 0 + ], + [ + 0, + 1 + ], + [ + 3, + 2 + ], + [ + 4, + 2 + ], + [ + 5, + 2 + ], + [ + 6, + 2 + ], + [ + 7, + 2 + ], + [ + 8, + 2 + ], + [ + 9, + 2 + ], + [ + 10, + 2 + ], + [ + 11, + 2 + ], + [ + 12, + 2 + ], + [ + 13, + 2 + ], + [ + 14, + 2 + ], + [ + 15, + 2 + ], + [ + 16, + 2 + ], + [ + 17, + 2 + ], + [ + 18, + 2 + ] + ], + "cost": 34, + "forward_peak": 4, + "reverse_peak": 4 + }, + { + "targets": 32, + "auxiliaries": 0, + "word": [ + [ + 0, + 1 + ], + [ + 3, + 0 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ], + [ + 7, + 0 + ], + [ + 8, + 0 + ], + [ + 9, + 0 + ], + [ + 10, + 0 + ], + [ + 11, + 0 + ], + [ + 12, + 0 + ], + [ + 13, + 0 + ], + [ + 14, + 0 + ], + [ + 15, + 0 + ], + [ + 16, + 0 + ], + [ + 17, + 0 + ], + [ + 18, + 0 + ], + [ + 19, + 0 + ], + [ + 20, + 0 + ], + [ + 21, + 0 + ], + [ + 22, + 0 + ], + [ + 23, + 0 + ], + [ + 24, + 0 + ], + [ + 25, + 0 + ], + [ + 26, + 0 + ], + [ + 27, + 0 + ], + [ + 28, + 0 + ], + [ + 29, + 0 + ], + [ + 30, + 0 + ], + [ + 31, + 0 + ], + [ + 32, + 0 + ], + [ + 33, + 0 + ], + [ + 34, + 0 + ], + [ + 0, + 1 + ], + [ + 3, + 2 + ], + [ + 4, + 2 + ], + [ + 5, + 2 + ], + [ + 6, + 2 + ], + [ + 7, + 2 + ], + [ + 8, + 2 + ], + [ + 9, + 2 + ], + [ + 10, + 2 + ], + [ + 11, + 2 + ], + [ + 12, + 2 + ], + [ + 13, + 2 + ], + [ + 14, + 2 + ], + [ + 15, + 2 + ], + [ + 16, + 2 + ], + [ + 17, + 2 + ], + [ + 18, + 2 + ], + [ + 19, + 2 + ], + [ + 20, + 2 + ], + [ + 21, + 2 + ], + [ + 22, + 2 + ], + [ + 23, + 2 + ], + [ + 24, + 2 + ], + [ + 25, + 2 + ], + [ + 26, + 2 + ], + [ + 27, + 2 + ], + [ + 28, + 2 + ], + [ + 29, + 2 + ], + [ + 30, + 2 + ], + [ + 31, + 2 + ], + [ + 32, + 2 + ], + [ + 33, + 2 + ], + [ + 34, + 2 + ] + ], + "cost": 66, + "forward_peak": 4, + "reverse_peak": 4 + }, + { + "targets": 32, + "auxiliaries": 1, + "word": [ + [ + 0, + 1 + ], + [ + 3, + 0 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ], + [ + 7, + 0 + ], + [ + 8, + 0 + ], + [ + 9, + 0 + ], + [ + 10, + 0 + ], + [ + 11, + 0 + ], + [ + 12, + 0 + ], + [ + 13, + 0 + ], + [ + 14, + 0 + ], + [ + 15, + 0 + ], + [ + 16, + 0 + ], + [ + 17, + 0 + ], + [ + 18, + 0 + ], + [ + 19, + 0 + ], + [ + 20, + 0 + ], + [ + 21, + 0 + ], + [ + 22, + 0 + ], + [ + 23, + 0 + ], + [ + 24, + 0 + ], + [ + 25, + 0 + ], + [ + 26, + 0 + ], + [ + 27, + 0 + ], + [ + 28, + 0 + ], + [ + 29, + 0 + ], + [ + 30, + 0 + ], + [ + 31, + 0 + ], + [ + 32, + 0 + ], + [ + 33, + 0 + ], + [ + 34, + 0 + ], + [ + 0, + 1 + ], + [ + 3, + 2 + ], + [ + 4, + 2 + ], + [ + 5, + 2 + ], + [ + 6, + 2 + ], + [ + 7, + 2 + ], + [ + 8, + 2 + ], + [ + 9, + 2 + ], + [ + 10, + 2 + ], + [ + 11, + 2 + ], + [ + 12, + 2 + ], + [ + 13, + 2 + ], + [ + 14, + 2 + ], + [ + 15, + 2 + ], + [ + 16, + 2 + ], + [ + 17, + 2 + ], + [ + 18, + 2 + ], + [ + 19, + 2 + ], + [ + 20, + 2 + ], + [ + 21, + 2 + ], + [ + 22, + 2 + ], + [ + 23, + 2 + ], + [ + 24, + 2 + ], + [ + 25, + 2 + ], + [ + 26, + 2 + ], + [ + 27, + 2 + ], + [ + 28, + 2 + ], + [ + 29, + 2 + ], + [ + 30, + 2 + ], + [ + 31, + 2 + ], + [ + 32, + 2 + ], + [ + 33, + 2 + ], + [ + 34, + 2 + ] + ], + "cost": 66, + "forward_peak": 4, + "reverse_peak": 4 + }, + { + "targets": 32, + "auxiliaries": 5, + "word": [ + [ + 0, + 1 + ], + [ + 3, + 0 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ], + [ + 7, + 0 + ], + [ + 8, + 0 + ], + [ + 9, + 0 + ], + [ + 10, + 0 + ], + [ + 11, + 0 + ], + [ + 12, + 0 + ], + [ + 13, + 0 + ], + [ + 14, + 0 + ], + [ + 15, + 0 + ], + [ + 16, + 0 + ], + [ + 17, + 0 + ], + [ + 18, + 0 + ], + [ + 19, + 0 + ], + [ + 20, + 0 + ], + [ + 21, + 0 + ], + [ + 22, + 0 + ], + [ + 23, + 0 + ], + [ + 24, + 0 + ], + [ + 25, + 0 + ], + [ + 26, + 0 + ], + [ + 27, + 0 + ], + [ + 28, + 0 + ], + [ + 29, + 0 + ], + [ + 30, + 0 + ], + [ + 31, + 0 + ], + [ + 32, + 0 + ], + [ + 33, + 0 + ], + [ + 34, + 0 + ], + [ + 0, + 1 + ], + [ + 3, + 2 + ], + [ + 4, + 2 + ], + [ + 5, + 2 + ], + [ + 6, + 2 + ], + [ + 7, + 2 + ], + [ + 8, + 2 + ], + [ + 9, + 2 + ], + [ + 10, + 2 + ], + [ + 11, + 2 + ], + [ + 12, + 2 + ], + [ + 13, + 2 + ], + [ + 14, + 2 + ], + [ + 15, + 2 + ], + [ + 16, + 2 + ], + [ + 17, + 2 + ], + [ + 18, + 2 + ], + [ + 19, + 2 + ], + [ + 20, + 2 + ], + [ + 21, + 2 + ], + [ + 22, + 2 + ], + [ + 23, + 2 + ], + [ + 24, + 2 + ], + [ + 25, + 2 + ], + [ + 26, + 2 + ], + [ + 27, + 2 + ], + [ + 28, + 2 + ], + [ + 29, + 2 + ], + [ + 30, + 2 + ], + [ + 31, + 2 + ], + [ + 32, + 2 + ], + [ + 33, + 2 + ], + [ + 34, + 2 + ] + ], + "cost": 66, + "forward_peak": 4, + "reverse_peak": 4 + }, + { + "targets": 64, + "auxiliaries": 0, + "word": [ + [ + 0, + 1 + ], + [ + 3, + 0 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ], + [ + 7, + 0 + ], + [ + 8, + 0 + ], + [ + 9, + 0 + ], + [ + 10, + 0 + ], + [ + 11, + 0 + ], + [ + 12, + 0 + ], + [ + 13, + 0 + ], + [ + 14, + 0 + ], + [ + 15, + 0 + ], + [ + 16, + 0 + ], + [ + 17, + 0 + ], + [ + 18, + 0 + ], + [ + 19, + 0 + ], + [ + 20, + 0 + ], + [ + 21, + 0 + ], + [ + 22, + 0 + ], + [ + 23, + 0 + ], + [ + 24, + 0 + ], + [ + 25, + 0 + ], + [ + 26, + 0 + ], + [ + 27, + 0 + ], + [ + 28, + 0 + ], + [ + 29, + 0 + ], + [ + 30, + 0 + ], + [ + 31, + 0 + ], + [ + 32, + 0 + ], + [ + 33, + 0 + ], + [ + 34, + 0 + ], + [ + 35, + 0 + ], + [ + 36, + 0 + ], + [ + 37, + 0 + ], + [ + 38, + 0 + ], + [ + 39, + 0 + ], + [ + 40, + 0 + ], + [ + 41, + 0 + ], + [ + 42, + 0 + ], + [ + 43, + 0 + ], + [ + 44, + 0 + ], + [ + 45, + 0 + ], + [ + 46, + 0 + ], + [ + 47, + 0 + ], + [ + 48, + 0 + ], + [ + 49, + 0 + ], + [ + 50, + 0 + ], + [ + 51, + 0 + ], + [ + 52, + 0 + ], + [ + 53, + 0 + ], + [ + 54, + 0 + ], + [ + 55, + 0 + ], + [ + 56, + 0 + ], + [ + 57, + 0 + ], + [ + 58, + 0 + ], + [ + 59, + 0 + ], + [ + 60, + 0 + ], + [ + 61, + 0 + ], + [ + 62, + 0 + ], + [ + 63, + 0 + ], + [ + 64, + 0 + ], + [ + 65, + 0 + ], + [ + 66, + 0 + ], + [ + 0, + 1 + ], + [ + 3, + 2 + ], + [ + 4, + 2 + ], + [ + 5, + 2 + ], + [ + 6, + 2 + ], + [ + 7, + 2 + ], + [ + 8, + 2 + ], + [ + 9, + 2 + ], + [ + 10, + 2 + ], + [ + 11, + 2 + ], + [ + 12, + 2 + ], + [ + 13, + 2 + ], + [ + 14, + 2 + ], + [ + 15, + 2 + ], + [ + 16, + 2 + ], + [ + 17, + 2 + ], + [ + 18, + 2 + ], + [ + 19, + 2 + ], + [ + 20, + 2 + ], + [ + 21, + 2 + ], + [ + 22, + 2 + ], + [ + 23, + 2 + ], + [ + 24, + 2 + ], + [ + 25, + 2 + ], + [ + 26, + 2 + ], + [ + 27, + 2 + ], + [ + 28, + 2 + ], + [ + 29, + 2 + ], + [ + 30, + 2 + ], + [ + 31, + 2 + ], + [ + 32, + 2 + ], + [ + 33, + 2 + ], + [ + 34, + 2 + ], + [ + 35, + 2 + ], + [ + 36, + 2 + ], + [ + 37, + 2 + ], + [ + 38, + 2 + ], + [ + 39, + 2 + ], + [ + 40, + 2 + ], + [ + 41, + 2 + ], + [ + 42, + 2 + ], + [ + 43, + 2 + ], + [ + 44, + 2 + ], + [ + 45, + 2 + ], + [ + 46, + 2 + ], + [ + 47, + 2 + ], + [ + 48, + 2 + ], + [ + 49, + 2 + ], + [ + 50, + 2 + ], + [ + 51, + 2 + ], + [ + 52, + 2 + ], + [ + 53, + 2 + ], + [ + 54, + 2 + ], + [ + 55, + 2 + ], + [ + 56, + 2 + ], + [ + 57, + 2 + ], + [ + 58, + 2 + ], + [ + 59, + 2 + ], + [ + 60, + 2 + ], + [ + 61, + 2 + ], + [ + 62, + 2 + ], + [ + 63, + 2 + ], + [ + 64, + 2 + ], + [ + 65, + 2 + ], + [ + 66, + 2 + ] + ], + "cost": 130, + "forward_peak": 4, + "reverse_peak": 4 + }, + { + "targets": 64, + "auxiliaries": 1, + "word": [ + [ + 0, + 1 + ], + [ + 3, + 0 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ], + [ + 7, + 0 + ], + [ + 8, + 0 + ], + [ + 9, + 0 + ], + [ + 10, + 0 + ], + [ + 11, + 0 + ], + [ + 12, + 0 + ], + [ + 13, + 0 + ], + [ + 14, + 0 + ], + [ + 15, + 0 + ], + [ + 16, + 0 + ], + [ + 17, + 0 + ], + [ + 18, + 0 + ], + [ + 19, + 0 + ], + [ + 20, + 0 + ], + [ + 21, + 0 + ], + [ + 22, + 0 + ], + [ + 23, + 0 + ], + [ + 24, + 0 + ], + [ + 25, + 0 + ], + [ + 26, + 0 + ], + [ + 27, + 0 + ], + [ + 28, + 0 + ], + [ + 29, + 0 + ], + [ + 30, + 0 + ], + [ + 31, + 0 + ], + [ + 32, + 0 + ], + [ + 33, + 0 + ], + [ + 34, + 0 + ], + [ + 35, + 0 + ], + [ + 36, + 0 + ], + [ + 37, + 0 + ], + [ + 38, + 0 + ], + [ + 39, + 0 + ], + [ + 40, + 0 + ], + [ + 41, + 0 + ], + [ + 42, + 0 + ], + [ + 43, + 0 + ], + [ + 44, + 0 + ], + [ + 45, + 0 + ], + [ + 46, + 0 + ], + [ + 47, + 0 + ], + [ + 48, + 0 + ], + [ + 49, + 0 + ], + [ + 50, + 0 + ], + [ + 51, + 0 + ], + [ + 52, + 0 + ], + [ + 53, + 0 + ], + [ + 54, + 0 + ], + [ + 55, + 0 + ], + [ + 56, + 0 + ], + [ + 57, + 0 + ], + [ + 58, + 0 + ], + [ + 59, + 0 + ], + [ + 60, + 0 + ], + [ + 61, + 0 + ], + [ + 62, + 0 + ], + [ + 63, + 0 + ], + [ + 64, + 0 + ], + [ + 65, + 0 + ], + [ + 66, + 0 + ], + [ + 0, + 1 + ], + [ + 3, + 2 + ], + [ + 4, + 2 + ], + [ + 5, + 2 + ], + [ + 6, + 2 + ], + [ + 7, + 2 + ], + [ + 8, + 2 + ], + [ + 9, + 2 + ], + [ + 10, + 2 + ], + [ + 11, + 2 + ], + [ + 12, + 2 + ], + [ + 13, + 2 + ], + [ + 14, + 2 + ], + [ + 15, + 2 + ], + [ + 16, + 2 + ], + [ + 17, + 2 + ], + [ + 18, + 2 + ], + [ + 19, + 2 + ], + [ + 20, + 2 + ], + [ + 21, + 2 + ], + [ + 22, + 2 + ], + [ + 23, + 2 + ], + [ + 24, + 2 + ], + [ + 25, + 2 + ], + [ + 26, + 2 + ], + [ + 27, + 2 + ], + [ + 28, + 2 + ], + [ + 29, + 2 + ], + [ + 30, + 2 + ], + [ + 31, + 2 + ], + [ + 32, + 2 + ], + [ + 33, + 2 + ], + [ + 34, + 2 + ], + [ + 35, + 2 + ], + [ + 36, + 2 + ], + [ + 37, + 2 + ], + [ + 38, + 2 + ], + [ + 39, + 2 + ], + [ + 40, + 2 + ], + [ + 41, + 2 + ], + [ + 42, + 2 + ], + [ + 43, + 2 + ], + [ + 44, + 2 + ], + [ + 45, + 2 + ], + [ + 46, + 2 + ], + [ + 47, + 2 + ], + [ + 48, + 2 + ], + [ + 49, + 2 + ], + [ + 50, + 2 + ], + [ + 51, + 2 + ], + [ + 52, + 2 + ], + [ + 53, + 2 + ], + [ + 54, + 2 + ], + [ + 55, + 2 + ], + [ + 56, + 2 + ], + [ + 57, + 2 + ], + [ + 58, + 2 + ], + [ + 59, + 2 + ], + [ + 60, + 2 + ], + [ + 61, + 2 + ], + [ + 62, + 2 + ], + [ + 63, + 2 + ], + [ + 64, + 2 + ], + [ + 65, + 2 + ], + [ + 66, + 2 + ] + ], + "cost": 130, + "forward_peak": 4, + "reverse_peak": 4 + }, + { + "targets": 64, + "auxiliaries": 5, + "word": [ + [ + 0, + 1 + ], + [ + 3, + 0 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ], + [ + 7, + 0 + ], + [ + 8, + 0 + ], + [ + 9, + 0 + ], + [ + 10, + 0 + ], + [ + 11, + 0 + ], + [ + 12, + 0 + ], + [ + 13, + 0 + ], + [ + 14, + 0 + ], + [ + 15, + 0 + ], + [ + 16, + 0 + ], + [ + 17, + 0 + ], + [ + 18, + 0 + ], + [ + 19, + 0 + ], + [ + 20, + 0 + ], + [ + 21, + 0 + ], + [ + 22, + 0 + ], + [ + 23, + 0 + ], + [ + 24, + 0 + ], + [ + 25, + 0 + ], + [ + 26, + 0 + ], + [ + 27, + 0 + ], + [ + 28, + 0 + ], + [ + 29, + 0 + ], + [ + 30, + 0 + ], + [ + 31, + 0 + ], + [ + 32, + 0 + ], + [ + 33, + 0 + ], + [ + 34, + 0 + ], + [ + 35, + 0 + ], + [ + 36, + 0 + ], + [ + 37, + 0 + ], + [ + 38, + 0 + ], + [ + 39, + 0 + ], + [ + 40, + 0 + ], + [ + 41, + 0 + ], + [ + 42, + 0 + ], + [ + 43, + 0 + ], + [ + 44, + 0 + ], + [ + 45, + 0 + ], + [ + 46, + 0 + ], + [ + 47, + 0 + ], + [ + 48, + 0 + ], + [ + 49, + 0 + ], + [ + 50, + 0 + ], + [ + 51, + 0 + ], + [ + 52, + 0 + ], + [ + 53, + 0 + ], + [ + 54, + 0 + ], + [ + 55, + 0 + ], + [ + 56, + 0 + ], + [ + 57, + 0 + ], + [ + 58, + 0 + ], + [ + 59, + 0 + ], + [ + 60, + 0 + ], + [ + 61, + 0 + ], + [ + 62, + 0 + ], + [ + 63, + 0 + ], + [ + 64, + 0 + ], + [ + 65, + 0 + ], + [ + 66, + 0 + ], + [ + 0, + 1 + ], + [ + 3, + 2 + ], + [ + 4, + 2 + ], + [ + 5, + 2 + ], + [ + 6, + 2 + ], + [ + 7, + 2 + ], + [ + 8, + 2 + ], + [ + 9, + 2 + ], + [ + 10, + 2 + ], + [ + 11, + 2 + ], + [ + 12, + 2 + ], + [ + 13, + 2 + ], + [ + 14, + 2 + ], + [ + 15, + 2 + ], + [ + 16, + 2 + ], + [ + 17, + 2 + ], + [ + 18, + 2 + ], + [ + 19, + 2 + ], + [ + 20, + 2 + ], + [ + 21, + 2 + ], + [ + 22, + 2 + ], + [ + 23, + 2 + ], + [ + 24, + 2 + ], + [ + 25, + 2 + ], + [ + 26, + 2 + ], + [ + 27, + 2 + ], + [ + 28, + 2 + ], + [ + 29, + 2 + ], + [ + 30, + 2 + ], + [ + 31, + 2 + ], + [ + 32, + 2 + ], + [ + 33, + 2 + ], + [ + 34, + 2 + ], + [ + 35, + 2 + ], + [ + 36, + 2 + ], + [ + 37, + 2 + ], + [ + 38, + 2 + ], + [ + 39, + 2 + ], + [ + 40, + 2 + ], + [ + 41, + 2 + ], + [ + 42, + 2 + ], + [ + 43, + 2 + ], + [ + 44, + 2 + ], + [ + 45, + 2 + ], + [ + 46, + 2 + ], + [ + 47, + 2 + ], + [ + 48, + 2 + ], + [ + 49, + 2 + ], + [ + 50, + 2 + ], + [ + 51, + 2 + ], + [ + 52, + 2 + ], + [ + 53, + 2 + ], + [ + 54, + 2 + ], + [ + 55, + 2 + ], + [ + 56, + 2 + ], + [ + 57, + 2 + ], + [ + 58, + 2 + ], + [ + 59, + 2 + ], + [ + 60, + 2 + ], + [ + 61, + 2 + ], + [ + 62, + 2 + ], + [ + 63, + 2 + ], + [ + 64, + 2 + ], + [ + 65, + 2 + ], + [ + 66, + 2 + ] + ], + "cost": 130, + "forward_peak": 4, + "reverse_peak": 4 + }, + { + "targets": 128, + "auxiliaries": 0, + "word": [ + [ + 0, + 1 + ], + [ + 3, + 0 + ], + [ + 4, + 0 + ], + [ + 5, + 0 + ], + [ + 6, + 0 + ], + [ + 7, + 0 + ], + [ + 8, + 0 + ], + [ + 9, + 0 + ], + [ + 10, + 0 + ], + [ + 11, + 0 + ], + [ + 12, + 0 + ], + [ + 13, + 0 + ], + [ + 14, + 0 + ], + [ + 15, + 0 + ], + [ + 16, + 0 + ], + [ + 17, + 0 + ], + [ + 18, + 0 + ], + [ + 19, + 0 + ], + [ + 20, + 0 + ], + [ + 21, + 0 + ], + [ + 22, + 0 + ], + [ + 23, + 0 + ], + [ + 24, + 0 + ], + [ + 25, + 0 + ], + [ + 26, + 0 + ], + [ + 27, + 0 + ], + [ + 28, + 0 + ], + [ + 29, + 0 + ], + [ + 30, + 0 + ], + [ + 31, + 0 + ], + [ + 32, + 0 + ], + [ + 33, + 0 + ], + [ + 34, + 0 + ], + [ + 35, + 0 + ], + [ + 36, + 0 + ], + [ + 37, + 0 + ], + [ + 38, + 0 + ], + [ + 39, + 0 + ], + [ + 40, + 0 + ], + [ + 41, + 0 + ], + [ + 42, + 0 + ], + [ + 43, + 0 + ], + [ + 44, + 0 + ], + [ + 45, + 0 + ], + [ + 46, + 0 + ], + [ + 47, + 0 + ], + [ + 48, + 0 + ], + [ + 49, + 0 + ], + [ + 50, + 0 + ], + [ + 51, + 0 + ], + [ + 52, + 0 + ], + [ + 53, + 0 + ], + [ + 54, + 0 + ], + [ + 55, + 0 + ], + [ + 56, + 0 + ], + [ + 57, + 0 + ], + [ + 58, + 0 + ], + [ + 59, + 0 + ], + [ + 60, + 0 + ], + [ + 61, + 0 + ], + [ + 62, + 0 + ], + [ + 63, + 0 + ], + [ + 64, + 0 + ], + [ + 65, + 0 + ], + [ + 66, + 0 + ], + [ + 67, + 0 + ], + [ + 68, + 0 + ], + [ + 69, + 0 + ], + [ + 70, + 0 + ], + [ + 71, + 0 + ], + [ + 72, + 0 + ], + [ + 73, + 0 + ], + [ + 74, + 0 + ], + [ + 75, + 0 + ], + [ + 76, + 0 + ], + [ + 77, + 0 + ], + [ + 78, + 0 + ], + [ + 79, + 0 + ], + [ + 80, + 0 + ], + [ + 81, + 0 + ], + [ + 82, + 0 + ], + [ + 83, + 0 + ], + [ + 84, + 0 + ], + [ + 85, + 0 + ], + [ + 86, + 0 + ], + [ + 87, + 0 + ], + [ + 88, + 0 + ], + [ + 89, + 0 + ], + [ + 90, + 0 + ], + [ + 91, + 0 + ], + [ + 92, + 0 + ], + [ + 93, + 0 + ], + [ + 94, + 0 + ], + [ + 95, + 0 + ], + [ + 96, + 0 + ], + [ + 97, + 0 + ], + [ + 98, + 0 + ], + [ + 99, + 0 + ], + [ + 100, + 0 + ], + [ + 101, + 0 + ], + [ + 102, + 0 + ], + [ + 103, + 0 + ], + [ + 104, + 0 + ], + [ + 105, + 0 + ], + [ + 106, + 0 + ], + [ + 107, + 0 + ], + [ + 108, + 0 + ], + [ + 109, + 0 + ], + [ + 110, + 0 + ], + [ + 111, + 0 + ], + [ + 112, + 0 + ], + [ + 113, + 0 + ], + [ + 114, + 0 + ], + [ + 115, + 0 + ], + [ + 116, + 0 + ], + [ + 117, + 0 + ], + [ + 118, + 0 + ], + [ + 119, + 0 + ], + [ + 120, + 0 + ], + [ + 121, + 0 + ], + [ + 122, + 0 + ], + [ + 123, + 0 + ], + [ + 124, + 0 + ], + [ + 125, + 0 + ], + [ + 126, + 0 + ], + [ + 127, + 0 + ], + [ + 128, + 0 + ], + [ + 129, + 0 + ], + [ + 130, + 0 + ], + [ + 0, + 1 + ], + [ + 3, + 2 + ], + [ + 4, + 2 + ], + [ + 5, + 2 + ], + [ + 6, + 2 + ], + [ + 7, + 2 + ], + [ + 8, + 2 + ], + [ + 9, + 2 + ], + [ + 10, + 2 + ], + [ + 11, + 2 + ], + [ + 12, + 2 + ], + [ + 13, + 2 + ], + [ + 14, + 2 + ], + [ + 15, + 2 + ], + [ + 16, + 2 + ], + [ + 17, + 2 + ], + [ + 18, + 2 + ], + [ + 19, + 2 + ], + [ + 20, + 2 + ], + [ + 21, + 2 + ], + [ + 22, + 2 + ], + [ + 23, + 2 + ], + [ + 24, + 2 + ], + [ + 25, + 2 + ], + [ + 26, + 2 + ], + [ + 27, + 2 + ], + [ + 28, + 2 + ], + [ + 29, + 2 + ], + [ + 30, + 2 + ], + [ + 31, + 2 + ], + [ + 32, + 2 + ], + [ + 33, + 2 + ], + [ + 34, + 2 + ], + [ + 35, + 2 + ], + [ + 36, + 2 + ], + [ + 37, + 2 + ], + [ + 38, + 2 + ], + [ + 39, + 2 + ], + [ + 40, + 2 + ], + [ + 41, + 2 + ], + [ + 42, + 2 + ], + [ + 43, + 2 + ], + [ + 44, + 2 + ], + [ + 45, + 2 + ], + [ + 46, + 2 + ], + [ + 47, + 2 + ], + [ + 48, + 2 + ], + [ + 49, + 2 + ], + [ + 50, + 2 + ], + [ + 51, + 2 + ], + [ + 52, + 2 + ], + [ + 53, + 2 + ], + [ + 54, + 2 + ], + [ + 55, + 2 + ], + [ + 56, + 2 + ], + [ + 57, + 2 + ], + [ + 58, + 2 + ], + [ + 59, + 2 + ], + [ + 60, + 2 + ], + [ + 61, + 2 + ], + [ + 62, + 2 + ], + [ + 63, + 2 + ], + [ + 64, + 2 + ], + [ + 65, + 2 + ], + [ + 66, + 2 + ], + [ + 67, + 2 + ], + [ + 68, + 2 + ], + [ + 69, + 2 + ], + [ + 70, + 2 + ], + [ + 71, + 2 + ], + [ + 72, + 2 + ], + [ + 73, + 2 + ], + [ + 74, + 2 + ], + [ + 75, + 2 + ], + [ + 76, + 2 + ], + [ + 77, + 2 + ], + [ + 78, + 2 + ], + [ + 79, + 2 + ], + [ + 80, + 2 + ], + [ + 81, + 2 + ], + [ + 82, + 2 + ], + [ + 83, + 2 + ], + [ + 84, + 2 + ], + [ + 85, + 2 + ], + [ + 86, + 2 + ], + [ + 87, + 2 + ], + [ + 88, + 2 + ], + [ + 89, + 2 + ], + [ + 90, + 2 + ], + [ + 91, + 2 + ], + [ + 92, + 2 + ], + [ + 93, + 2 + ], + [ + 94, + 2 + ], + [ + 95, + 2 + ], + [ + 96, + 2 + ], + [ + 97, + 2 + ], + [ + 98, + 2 + ], + [ + 99, + 2 + ], + [ + 100, + 2 + ], + [ + 101, + 2 + ], + [ + 102, + 2 + ], + [ + 103, + 2 + ], + [ + 104, + 2 + ], + [ + 105, + 2 + ], + [ + 106, + 2 + ], + [ + 107, + 2 + ], + [ + 108, + 2 + ], + [ + 109, + 2 + ], + [ + 110, + 2 + ], + [ + 111, + 2 + ], + [ + 112, + 2 + ], + [ + 113, + 2 + ], + [ + 114, + 2 + ], + [ + 115, + 2 + ], + [ + 116, + 2 + ], + [ + 117, + 2 + ], + [ + 118, + 2 + ], + [ + 119, + 2 + ], + [ + 120, + 2 + ], + [ + 121, + 2 + ], + [ + 122, + 2 + ], + [ + 123, + 2 + ], + [ + 124, + 2 + ], + [ + 125, + 2 + ], + [ + 126, + 2 + ], + [ + 127, + 2 + ], + [ + 128, + 2 + ], + [ + 129, + 2 + ], + [ + 130, + 2 + ] + ], + "cost": 258, + "forward_peak": 4, + "reverse_peak": 4 + } + ] +} diff --git a/research/three-source-envelope-floor/README.md b/research/three-source-envelope-floor/README.md new file mode 100644 index 0000000000..0273ccbcb9 --- /dev/null +++ b/research/three-source-envelope-floor/README.md @@ -0,0 +1,154 @@ +# Exact cost of minimum-envelope three-source XOR fanout + +**Scoped uniform theorem; no new supplier or kappa.** For every `n >= 2`, +adding the parity of three restored helpers to `n` dirty targets requires +exactly **`2n+2` unit XORs** when the forward positive envelope is at most four. +This remains true with any finite number of additional dirty auxiliaries, +arbitrary target feedback and arbitrary circuit length. The attaining word +also has reverse envelope four. + +PR [#1520](https://github.com/CrocSwap/integer-mult-bounds/pull/1520), by +Hanson Sun (@bbMisk), already gave the eight-gate, peak-four construction for +three targets and the complete six-register cost/precision frontier. We +generalize its construction and replace its shortest-word census as the +peak-four lower-bound argument with a structural proof valid for all target +counts and extra dirty registers. We do not claim a new unconstrained XOR +minimum or repeat the finite 3x4 census in PR1557. + +## Model and theorem + +There are helpers `h0,h1,h2`, targets `y0,...,y(n-1)`, and any finite number of +auxiliaries. Initially every register is arbitrary and independent over F2 +(equivalently any F2 module). The complete endpoint restores every helper +and auxiliary and maps each target to `y_j + h0 + h1 + h2`. + +Every gate is an ordered `r_d ^= r_s`, with `d != s`, charged one unit. There +are no free permutations, basis changes, clean roles, COPY/ERASE operations, +recursive calls or frame changes. All roles use one common zero frame. +The positive lift replaces each XOR by integer row addition, starting from +the identity matrix. Thus every initial bound is one; the envelope `F` is +the maximum row sum over every prefix. All entries are nonnegative and +monotone, so the final maximum is also the prefix maximum. `B` is the same +quantity for the reversed word. This is a local majorant, not word size. + +**Theorem.** For `n >= 2`, the minimum gate count among these circuits with +`F <= 4` is `2n+2`. Every such endpoint has `F >= 4` and `B >= 4`. The minimum +with `B <= 4`, or with both envelopes at most four, is also `2n+2`. + +### Lower bound + +Let `P` denote the nonnegative integer transfer matrix at a prefix. Reduction +modulo two is exactly that prefix's binary transfer. Each row retains its own +initial diagonal entry at least one, and every entry can only increase. + +1. A final target row has four required odd entries: its own target column + and all three helper columns. If `F <= 4`, those four entries must each + equal one and every other entry must be zero. This also proves `F >= 4`. +2. A gate into a target cannot use another target or auxiliary as source. + The source row contains its own original column with positive coefficient, + which would permanently pollute the destination's final row. A helper + source contaminated by any nonhelper column is likewise unusable: if that + column is the destination's own, its already-present diagonal one would + become at least two; otherwise a forbidden column becomes positive. + Therefore every target gate uses a helper row containing only helper + columns, and its contributions must fit within the three unit entries. +3. No helper row can ever contain all three helper columns positively. + At the restored endpoint its own helper column is odd and at least one, + while the two other columns must be even. If both had ever been positive, + monotonicity would make each at least two at the end, giving row sum at + least five, contrary to `F <= 4`. Consequently no single incoming gate + can supply all three helper columns to any target. Each target needs at + least two incoming gates, for at least `2n` target-destination gates. +4. If any helper is written, at least two helper-destination gates occur. + Exactly one would change that helper by a nonzero binary source row; + all prefix matrices are invertible because the allowed gates are + invertible, so no source row is zero. With no later write to that helper, + restoration would fail. These helper gates are distinct from target + gates, giving at least `2n+2` total. +5. If no helper is written, every usable helper stays a single original + basis row. Each target then needs at least three incoming gates, giving + `3n >= 2n+2` for `n >= 2`. Auxiliary gates can only add to either count. + +This proves the lower bound for arbitrary words; it is not inferred from the +finite checks below. In particular, extra dirty storage and target feedback +do not evade the positive-row obstruction. + +### Attainment and reverse direction + +Use the following paid word, leaving auxiliaries untouched: + +```text +h0 ^= h1 +for each j: y_j ^= h0 +h0 ^= h1 +for each j: y_j ^= h2 +``` + +It restores the helper, adds all three original helper values to every target, +and costs `1+n+1+n = 2n+2`. Its final positive helper bounds are `(3,1,1)`; +each target bound is four and every auxiliary bound remains one. Reversing +the word gives the same final bounds. The endpoint is an involution, so +reversing any admissible word preserves its contract and gate count while +exchanging `F` and `B`. The forward theorem therefore gives the reverse and +simultaneous claims. For the excluded case `n=1`, three direct gates suffice; +the stated formula four would be false. + +For four targets this proves the peak-four cost is ten. The familiar +eight-gate gather/fanout/restore word has both peaks five. Its unconstrained +minimality on exactly seven registers is prior finite evidence in PR1557, +not a new claim or an assumption of this theorem. No unconstrained minimum +with additional auxiliaries is asserted here. + +## Reproduce and validation boundary + +```sh +python3.12 -I -B scripts/research_package.py --package research/three-source-envelope-floor +``` + +The registered standard-library checks reconstruct the witnesses and their +exact binary endpoints and integer lifts, verify both directions on several +target/auxiliary counts, and independently enumerate full dirty truth tables +for small instances. Controls reject missing restoration, missing target +updates, incorrect cost/peak claims, malformed gates and the `n=1` extension. +Historical source pins identify the predecessor descriptions used for +attribution; those descriptions are not runtime proof inputs. These finite +checks support the construction and illustrate the +proof's hypotheses; they do not turn the prose uniform proof into a formal +kernel theorem. No full supplier replay or precision guard admission is claimed. + +## Provenance, usefulness and limits + +The base is `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`, priority revision four. +The task nonce is `54ac0d737844a7825d9d6cbcee723dd8`; the prescribed PR1062 +star verifier passed. `TASK.json` records the changed scope from the already +covered semantic H2/K repair to a positive-envelope interface bound. The +claim is [on PR1520](https://github.com/CrocSwap/integer-mult-bounds/pull/1520#issuecomment-6196577531). +`SOURCES.json` records exact predecessor byte identities and heads. + +The theorem provides a stopping rule for searching peak-four parity fanout: +allowing more dirty helper space cannot beat the displayed cost in this +model. Unequal incoming bounds, clean initialized roles, nonmonotone bounds, +COPY/ERASE and nonzero frames are outside the theorem. The selected complex +supplier remains binding; this result neither admits a new bit supplier nor +changes the selected kappa. A hosted replacement must pay all surrounding +costs and pass its own chronological, native and precision checks. + +## Open next questions + +Can an actual native hosted occurrence benefit from replacing a peak-five +gather/fanout/restore word with the peak-four word after paying the extra +XORs? First locate a pinned occurrence with its real incoming bounds and +interior observations, then replay the complete surrounding word. No such +occurrence or completed invoice is established here. For unequal positive +bounds, the simple all-ones exact floor need not describe the correct objective. + +## Credit and license + +Credit Hanson Sun (@bbMisk) for PR1520's three-target precision frontier and +construction; @commdata2338 for PR1306's zero-frame feedback model and +substitution lemma; PR1557 for the seven-register finite census; and the +PR1062/PR555/PR589 contributors for the bit-supplier and positive-envelope +lineage. No priority is claimed for elementary monotone matrix arguments. +Prepared for @ywz65 with substantial OpenAI Codex assistance in proof, +implementation, testing and writing; no independent human review. New work +is Apache-2.0. diff --git a/research/three-source-envelope-floor/SOURCES.json b/research/three-source-envelope-floor/SOURCES.json new file mode 100644 index 0000000000..f494cda5d6 --- /dev/null +++ b/research/three-source-envelope-floor/SOURCES.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "research/bit-j3-precision-seed11/README.md", + "usage": "provenance", + "main_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "predecessor_pr": 1520, + "predecessor_head": "69e353410ae1e6f0555b5add9720f3e691a762b9", + "git_blob": "3b6e3fd2c2ad6cc6902061147b0d5eae4635aa90", + "sha256": "6cfdf4cd2fa60fec60b06d22cc460911d000f8855fe0b7502bf548a277e7f836" + }, + { + "path": "research/bit-zero-frame-feedback-3x4/README.md", + "usage": "provenance", + "main_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "predecessor_pr": 1557, + "predecessor_head": "15e0987e5fa88d1c15699215ac0cd70b47a535a6", + "git_blob": "3aa2cecc9316bc21ef8cbad5729bd9bc781a3dc3", + "sha256": "6bd8092ec2dfb673a338a78803b4f66f9d8867749d1b7af85b67438f0dcac64b" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + } + ], + "limits": "Proof and witness checks are self-contained; earlier unrestricted minima are credited context, not newly replayed claims." +} diff --git a/research/three-source-envelope-floor/TASK.json b/research/three-source-envelope-floor/TASK.json new file mode 100644 index 0000000000..09f0ffa2f3 --- /dev/null +++ b/research/three-source-envelope-floor/TASK.json @@ -0,0 +1,93 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "assignment_nonce": "54ac0d737844a7825d9d6cbcee723dd8", + "original_card": { + "id": "bit-helper-contract", + "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?", + "starting_points": [ + "research/r439-bsection-stars-seed01/README.md", + "research/r439-copy-path-sharing-barrier/README.md" + ], + "methods": [ + "Derive a replacement interface lemma and price its implementation.", + "Seek an exact dirty-input or chronological-cut counterexample to the proposed replacement." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient.", + "first_step": { + "command": [ + "python3", + "-B", + "research/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.", + "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.", + "allowed_variations": [ + "Choose one helper-star or quartet instance; narrow to one boundary implication." + ], + "scope_change_triggers": [ + "Changing only source count or scalar addition count without an interface argument." + ], + "overlap_terms": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D", + "helper-star" + ] + }, + "scope_status": "changed", + "actual_scope": "Uniform peak-four gate minimum for three-helper parity fanout, arbitrary n>=2 and finite dirty auxiliaries.", + "scope_change_reason": "Semantic H2/K repair and finite XOR censuses already covered. New structural proof removes target-count and dirty-auxiliary restrictions from the peak-four lower bound.", + "bottleneck_link": "Bit-side local precision/cost stopping rule; selected complex supplier still binds and no hosted admission follows.", + "budget_minutes": 60, + "stop_rule": "Prove the uniform row-majorant bound, replay attaining words and hypothesis controls; no wider search.", + "outcome": "completed", + "evidence": "README uniform proof; CERTIFICATE/verify/independent witness checks.", + "first_step": "PASS_R439_BSECTION_STARS blocks=10 gates=388->254 ADDs=11783->11515->11500 guard_rejections=24->0 columns=661 controls=8 no_new_kappa", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1520#issuecomment-6196577531", + "overlap": { + "coverage": { + "open_prs": { + "fetched_at": "2026-10-15T16:13:42.723564+00:00", + "complete_pagination": true, + "records": 804 + }, + "discussions": { + "fetched_at": "2026-10-15T15:22:22.047084+00:00", + "complete_pagination": true, + "records": 1239 + } + }, + "queries": [ + "2n+2", + "fanout envelope", + "three helpers positive", + "dirty auxiliaries fanout" + ], + "limitations": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "warnings": [ + "open_prs: offline; cached data may miss current changes", + "discussions: offline; cached data may miss current changes" + ] + }, + "author": "ywz65", + "ai_assistance": "Substantial OpenAI Codex assistance; independent agent prose review, no human review.", + "open_questions": [ + { + "question": "Does a native hosted occurrence benefit after paying the extra XORs?", + "why_it_matters": "A local envelope improvement alone does not admit a supplier.", + "first_step": "Locate one pinned occurrence with incoming bounds/interior observers and replay its complete word.", + "blocked_by": "No hosted occurrence or complete invoice established." + } + ], + "pre_submission_refresh": { + "main": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "utc": "2026-10-15T16:13:42Z", + "predecessor_heads": "PR1520 and PR1557 unchanged" + } +} diff --git a/research/three-source-envelope-floor/VERIFY.json b/research/three-source-envelope-floor/VERIFY.json new file mode 100644 index 0000000000..eab4d1fb76 --- /dev/null +++ b/research/three-source-envelope-floor/VERIFY.json @@ -0,0 +1,31 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact endpoints, positive lifts, cost accounting and eight scope/certificate controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Column-oriented positive lifts and full small-instance dirty truth tables without primary imports." + } + ] +} diff --git a/research/three-source-envelope-floor/independent.py b/research/three-source-envelope-floor/independent.py new file mode 100644 index 0000000000..41374f18a0 --- /dev/null +++ b/research/three-source-envelope-floor/independent.py @@ -0,0 +1,64 @@ +"""Independent full truth tables and column-oriented positive replay; no primary imports.""" +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent + + +def need(value, message): + if not value: + raise ValueError(message) + + +def columns(n, auxiliary, gates): + m = 3+n+auxiliary + totals = [0]*m + for basis in range(m): + vector = [int(i == basis) for i in range(m)] + for destination, source in gates: + need(type(destination) is int and type(source) is int and 0 <= destination < m and 0 <= source < m and destination != source, 'gate') + vector[destination] += vector[source] + for output, value in enumerate(vector): + expected = int(output == basis) ^ int(3 <= output < 3+n and basis < 3) + need(value % 2 == expected, 'basis endpoint') + totals[output] += value + return max(totals) + + +def truth(n, auxiliary, gates): + m = 3+n+auxiliary + for original in range(1 << m): + values = [(original >> i) & 1 for i in range(m)] + parity = values[0] ^ values[1] ^ values[2] + expected = [v ^ (parity if 3 <= i < 3+n else 0) for i, v in enumerate(values)] + for destination, source in gates: + values[destination] ^= values[source] + need(values == expected, 'dirty truth table') + return 1 << m + + +def main(): + data = json.loads((HERE/'CERTIFICATE.json').read_text(encoding='utf-8')) + need(data['claim'] == 'minimum_peak_four_cost_2n_plus_2', 'claim') + need([(c['targets'], c['auxiliaries']) for c in data['cases']] == [(n, a) for n in (2, 3, 4, 8, 16, 32, 64) for a in (0, 1, 5)]+[(128, 0)], 'inventory') + truth_inputs = 0 + for c in data['cases']: + n, a, gates = c['targets'], c['auxiliaries'], c['word'] + need(c['cost'] == len(gates) == 2*n+2, 'cost') + for word, label in ((gates, 'forward'), (gates[::-1], 'reverse')): + need(columns(n, a, word) == c[label+'_peak'] == 4, 'positive column envelope') + if n <= 4: + truth_inputs += truth(n, a, word) + # Endpoint-only replay with clean helpers would miss omitted restoration. + bad = [[0, 1]] + [[3+j, 0] for j in range(4)] + [[3+j, 2] for j in range(4)] + try: + truth(4, 1, bad) + except ValueError: + pass + else: + raise ValueError('missing-restoration control accepted') + print(f'PASS_INDEPENDENT_ENVELOPE cases={len(data["cases"])} dirty_inputs={truth_inputs} control=1') + + +if __name__ == '__main__': + main() diff --git a/research/three-source-envelope-floor/verify.py b/research/three-source-envelope-floor/verify.py new file mode 100644 index 0000000000..df46365f36 --- /dev/null +++ b/research/three-source-envelope-floor/verify.py @@ -0,0 +1,79 @@ +"""Exact witness replay; the uniform lower bound is the proof in README.md.""" +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent + + +def require(value, message): + if not value: + raise ValueError(message) + + +def witness(n): + return [[0, 1]] + [[3+j, 0] for j in range(n)] + [[0, 1]] + [[3+j, 2] for j in range(n)] + + +def replay(n, auxiliary, word): + size = 3+n+auxiliary + rows = [[int(i == j) for j in range(size)] for i in range(size)] + binary = [1 << i for i in range(size)] + peak = 1 + for gate in word: + require(isinstance(gate, list) and len(gate) == 2, 'gate shape') + d, s = gate + require(type(d) is int and type(s) is int and 0 <= d < size and 0 <= s < size and d != s, 'gate indices') + binary[d] ^= binary[s] + rows[d] = [a+b for a, b in zip(rows[d], rows[s])] + peak = max(peak, sum(rows[d])) + expected = [(1 << i) ^ (7 if 3 <= i < 3+n else 0) for i in range(size)] + require(binary == expected, 'complete dirty endpoint') + require([sum((v % 2) << j for j, v in enumerate(row)) for row in rows] == binary, 'integer/binary reduction') + return peak, rows + + +def validate(certificate): + require(certificate['schema_version'] == 1 and certificate['claim'] == 'minimum_peak_four_cost_2n_plus_2', 'claim') + expected_cases = [(n, a) for n in (2, 3, 4, 8, 16, 32, 64) for a in (0, 1, 5)] + [(128, 0)] + require([(c['targets'], c['auxiliaries']) for c in certificate['cases']] == expected_cases, 'case inventory') + for c in certificate['cases']: + n, a, word = c['targets'], c['auxiliaries'], c['word'] + require(word == witness(n), 'attaining word') + require(c['cost'] == len(word) == 2*n+2, 'cost') + for actual, direction in ((word, 'forward'), (list(reversed(word)), 'reverse')): + peak, rows = replay(n, a, actual) + require(c[direction+'_peak'] == peak == 4, 'peak') + require(rows[0][1] == 2 and sum(rows[0]) == 3, 'helper positive restoration bill') + return len(certificate['cases']) + + +def rejected(fn): + try: + fn() + except (ValueError, KeyError, TypeError): + return + raise ValueError('negative control accepted') + + +def main(): + certificate = json.loads((HERE/'CERTIFICATE.json').read_text(encoding='utf-8')) + count = validate(certificate) + rejected(lambda: replay(4, 1, witness(4)[1:])) + rejected(lambda: replay(4, 1, witness(4)[:-1])) + rejected(lambda: replay(4, 1, witness(4)+[[0, 0]])) + for field, value in [('cost', 9), ('forward_peak', 3), ('reverse_peak', 5)]: + mutant = json.loads(json.dumps(certificate)) + mutant['cases'][6][field] = value + rejected(lambda: validate(mutant)) + gather = [[0, 1], [0, 2]] + [[j, 0] for j in range(3, 7)] + [[0, 2], [0, 1]] + require(replay(4, 0, gather)[0] == 5, 'eight-gate control must have peak five') + direct = [[3, 0], [3, 1], [3, 2]] + require(replay(1, 0, direct)[0] == 4 and len(direct) < 2*1+2, 'n=1 restriction') + # Finite illustration of the restored helper parity obstruction. + restored = [(x, y, z) for x in range(1, 5, 2) for y in range(0, 5, 2) for z in range(0, 5, 2) if x+y+z <= 4] + require(all(not (x and y and z) for x, y, z in restored), 'restored helper support floor') + print(f'PASS_THREE_SOURCE_ENVELOPE cases={count} directions={2*count} controls=8 uniform_proof=README no_new_kappa') + + +if __name__ == '__main__': + main()