diff --git a/research/dyadic-query-runs/CERTIFICATE.json b/research/dyadic-query-runs/CERTIFICATE.json new file mode 100644 index 0000000000..eedfb963e2 --- /dev/null +++ b/research/dyadic-query-runs/CERTIFICATE.json @@ -0,0 +1,87 @@ +{ + "assignment_seed": 55, + "domain": {"indices": [0, 1, 2, 3, 4, 5], "masks": [1, 63]}, + "format": "dyadic-query-runs-v1", + "instruction_format": "integer k: Q(k) on target; X: target XOR source", + "cases": [ + {"baseline": [-1, "X", 2, "X", -1], "baseline_invoice": {"affines": 18, "children": 3, "query_multiplicities": {"-1": 2, "2": 1}, "xor_scans": 2}, "indices": [0], "invoice": {"affines": 18, "children": 3, "query_multiplicities": {"-1": 2, "2": 1}, "xor_scans": 2}, "mask": 1, "word": [-1, "X", 2, "X", -1]}, + {"baseline": [-2, "X", 4, "X", -2], "baseline_invoice": {"affines": 18, "children": 3, "query_multiplicities": {"-2": 2, "4": 1}, "xor_scans": 2}, "indices": [1], "invoice": {"affines": 18, "children": 3, "query_multiplicities": {"-2": 2, "4": 1}, "xor_scans": 2}, "mask": 2, "word": [-2, "X", 4, "X", -2]}, + {"baseline": [-1, "X", 2, "X", -1, -2, "X", 4, "X", -2], "baseline_invoice": {"affines": 36, "children": 6, "query_multiplicities": {"-1": 2, "-2": 2, "2": 1, "4": 1}, "xor_scans": 4}, "indices": [0, 1], "invoice": {"affines": 30, "children": 5, "query_multiplicities": {"-2": 2, "1": 2, "2": 1}, "xor_scans": 4}, "mask": 3, "word": [-2, "X", 1, "X", 2, "X", 1, "X", -2]}, + {"baseline": [-4, "X", 8, "X", -4], "baseline_invoice": {"affines": 18, "children": 3, "query_multiplicities": {"-4": 2, "8": 1}, "xor_scans": 2}, "indices": [2], "invoice": {"affines": 18, "children": 3, "query_multiplicities": {"-4": 2, "8": 1}, "xor_scans": 2}, "mask": 4, "word": [-4, "X", 8, "X", -4]}, + {"baseline": [-1, "X", 2, "X", -1, -4, "X", 8, "X", -4], "baseline_invoice": {"affines": 36, "children": 6, "query_multiplicities": {"-1": 2, "-4": 2, "2": 1, "8": 1}, "xor_scans": 4}, "indices": [0, 2], "invoice": {"affines": 36, "children": 6, "query_multiplicities": {"-1": 2, "-4": 2, "2": 1, "8": 1}, "xor_scans": 4}, "mask": 5, "word": [-1, "X", 2, "X", -1, -4, "X", 8, "X", -4]}, + {"baseline": [-2, "X", 4, "X", -2, -4, "X", 8, "X", -4], "baseline_invoice": {"affines": 36, "children": 6, "query_multiplicities": {"-2": 2, "-4": 2, "4": 1, "8": 1}, "xor_scans": 4}, "indices": [1, 2], "invoice": {"affines": 30, "children": 5, "query_multiplicities": {"-4": 2, "2": 2, "4": 1}, "xor_scans": 4}, "mask": 6, "word": [-4, "X", 2, "X", 4, "X", 2, "X", -4]}, + {"baseline": [-1, "X", 2, "X", -1, -2, "X", 4, "X", -2, -4, "X", 8, "X", -4], "baseline_invoice": {"affines": 54, "children": 9, "query_multiplicities": {"-1": 2, "-2": 2, "-4": 2, "2": 1, "4": 1, "8": 1}, "xor_scans": 6}, "indices": [0, 1, 2], "invoice": {"affines": 42, "children": 7, "query_multiplicities": {"-4": 2, "1": 2, "2": 3}, "xor_scans": 6}, "mask": 7, "word": [-4, "X", 2, "X", 1, "X", 2, "X", 1, "X", 2, "X", -4]}, + {"baseline": [-8, "X", 16, "X", -8], "baseline_invoice": {"affines": 18, "children": 3, "query_multiplicities": {"-8": 2, "16": 1}, "xor_scans": 2}, "indices": [3], "invoice": {"affines": 18, "children": 3, "query_multiplicities": {"-8": 2, "16": 1}, "xor_scans": 2}, "mask": 8, "word": [-8, "X", 16, "X", -8]}, + {"baseline": [-1, "X", 2, "X", -1, -8, "X", 16, "X", -8], "baseline_invoice": {"affines": 36, "children": 6, "query_multiplicities": {"-1": 2, "-8": 2, "16": 1, "2": 1}, "xor_scans": 4}, "indices": [0, 3], "invoice": {"affines": 36, "children": 6, "query_multiplicities": {"-1": 2, "-8": 2, "16": 1, "2": 1}, "xor_scans": 4}, "mask": 9, "word": [-1, "X", 2, "X", -1, -8, "X", 16, "X", -8]}, + {"baseline": [-2, "X", 4, "X", -2, -8, "X", 16, "X", -8], "baseline_invoice": {"affines": 36, "children": 6, "query_multiplicities": {"-2": 2, "-8": 2, "16": 1, "4": 1}, "xor_scans": 4}, "indices": [1, 3], "invoice": {"affines": 36, "children": 6, "query_multiplicities": {"-2": 2, "-8": 2, "16": 1, "4": 1}, "xor_scans": 4}, "mask": 10, "word": [-2, "X", 4, "X", -2, -8, "X", 16, "X", -8]}, + {"baseline": [-1, "X", 2, "X", -1, -2, "X", 4, "X", -2, -8, "X", 16, "X", -8], "baseline_invoice": {"affines": 54, "children": 9, "query_multiplicities": {"-1": 2, "-2": 2, "-8": 2, "16": 1, "2": 1, "4": 1}, "xor_scans": 6}, "indices": [0, 1, 3], "invoice": {"affines": 48, "children": 8, "query_multiplicities": {"-2": 2, "-8": 2, "1": 2, "16": 1, "2": 1}, "xor_scans": 6}, "mask": 11, "word": [-2, "X", 1, "X", 2, "X", 1, "X", -2, -8, "X", 16, "X", -8]}, + {"baseline": [-4, "X", 8, "X", -4, -8, "X", 16, "X", -8], "baseline_invoice": {"affines": 36, "children": 6, "query_multiplicities": {"-4": 2, "-8": 2, "16": 1, "8": 1}, "xor_scans": 4}, "indices": [2, 3], "invoice": {"affines": 30, "children": 5, "query_multiplicities": {"-8": 2, "4": 2, "8": 1}, "xor_scans": 4}, "mask": 12, "word": [-8, "X", 4, "X", 8, "X", 4, "X", -8]}, + {"baseline": [-1, "X", 2, "X", -1, -4, "X", 8, "X", -4, -8, "X", 16, "X", -8], "baseline_invoice": {"affines": 54, "children": 9, "query_multiplicities": {"-1": 2, "-4": 2, "-8": 2, "16": 1, "2": 1, "8": 1}, "xor_scans": 6}, "indices": [0, 2, 3], "invoice": {"affines": 48, "children": 8, "query_multiplicities": {"-1": 2, "-8": 2, "2": 1, "4": 2, "8": 1}, "xor_scans": 6}, "mask": 13, "word": [-1, "X", 2, "X", -1, -8, "X", 4, "X", 8, "X", 4, "X", -8]}, + {"baseline": [-2, "X", 4, "X", -2, -4, "X", 8, "X", -4, -8, "X", 16, "X", -8], "baseline_invoice": {"affines": 54, "children": 9, "query_multiplicities": {"-2": 2, "-4": 2, "-8": 2, "16": 1, "4": 1, "8": 1}, "xor_scans": 6}, "indices": [1, 2, 3], "invoice": {"affines": 42, "children": 7, "query_multiplicities": {"-8": 2, "2": 2, "4": 3}, "xor_scans": 6}, "mask": 14, "word": [-8, "X", 4, "X", 2, "X", 4, "X", 2, "X", 4, "X", -8]}, + {"baseline": [-1, "X", 2, "X", -1, -2, "X", 4, "X", -2, -4, "X", 8, "X", -4, -8, "X", 16, "X", -8], "baseline_invoice": {"affines": 72, "children": 12, "query_multiplicities": {"-1": 2, "-2": 2, "-4": 2, "-8": 2, "16": 1, "2": 1, "4": 1, "8": 1}, "xor_scans": 8}, "indices": [0, 1, 2, 3], "invoice": {"affines": 54, "children": 9, "query_multiplicities": {"-8": 2, "1": 2, "2": 3, "4": 2}, "xor_scans": 8}, "mask": 15, "word": [-8, "X", 4, "X", 2, "X", 1, "X", 2, "X", 1, "X", 2, "X", 4, "X", -8]}, + {"baseline": [-16, "X", 32, "X", -16], "baseline_invoice": {"affines": 18, "children": 3, "query_multiplicities": {"-16": 2, "32": 1}, "xor_scans": 2}, "indices": [4], "invoice": {"affines": 18, "children": 3, "query_multiplicities": {"-16": 2, "32": 1}, "xor_scans": 2}, "mask": 16, "word": [-16, "X", 32, "X", -16]}, + {"baseline": [-1, "X", 2, "X", -1, -16, "X", 32, "X", -16], "baseline_invoice": {"affines": 36, "children": 6, "query_multiplicities": {"-1": 2, "-16": 2, "2": 1, "32": 1}, "xor_scans": 4}, "indices": [0, 4], "invoice": {"affines": 36, "children": 6, "query_multiplicities": {"-1": 2, "-16": 2, "2": 1, "32": 1}, "xor_scans": 4}, "mask": 17, "word": [-1, "X", 2, "X", -1, -16, "X", 32, "X", -16]}, + {"baseline": [-2, "X", 4, "X", -2, -16, "X", 32, "X", -16], "baseline_invoice": {"affines": 36, "children": 6, "query_multiplicities": {"-16": 2, "-2": 2, "32": 1, "4": 1}, "xor_scans": 4}, "indices": [1, 4], "invoice": {"affines": 36, "children": 6, "query_multiplicities": {"-16": 2, "-2": 2, "32": 1, "4": 1}, "xor_scans": 4}, "mask": 18, "word": [-2, "X", 4, "X", -2, -16, "X", 32, "X", -16]}, + {"baseline": [-1, "X", 2, "X", -1, -2, "X", 4, "X", -2, -16, "X", 32, "X", -16], "baseline_invoice": {"affines": 54, "children": 9, "query_multiplicities": {"-1": 2, "-16": 2, "-2": 2, "2": 1, "32": 1, "4": 1}, "xor_scans": 6}, "indices": [0, 1, 4], "invoice": {"affines": 48, "children": 8, "query_multiplicities": {"-16": 2, "-2": 2, "1": 2, "2": 1, "32": 1}, "xor_scans": 6}, "mask": 19, "word": [-2, "X", 1, "X", 2, "X", 1, "X", -2, -16, "X", 32, "X", -16]}, + {"baseline": [-4, "X", 8, "X", -4, -16, "X", 32, "X", -16], "baseline_invoice": {"affines": 36, "children": 6, "query_multiplicities": {"-16": 2, "-4": 2, "32": 1, "8": 1}, "xor_scans": 4}, "indices": [2, 4], "invoice": {"affines": 36, "children": 6, "query_multiplicities": {"-16": 2, "-4": 2, "32": 1, "8": 1}, "xor_scans": 4}, "mask": 20, "word": [-4, "X", 8, "X", -4, -16, "X", 32, "X", -16]}, + {"baseline": [-1, "X", 2, "X", -1, -4, "X", 8, "X", -4, -16, "X", 32, "X", -16], "baseline_invoice": {"affines": 54, "children": 9, "query_multiplicities": {"-1": 2, "-16": 2, "-4": 2, "2": 1, "32": 1, "8": 1}, "xor_scans": 6}, "indices": [0, 2, 4], "invoice": {"affines": 54, "children": 9, "query_multiplicities": {"-1": 2, "-16": 2, "-4": 2, "2": 1, "32": 1, "8": 1}, "xor_scans": 6}, "mask": 21, "word": [-1, "X", 2, "X", -1, -4, "X", 8, "X", -4, -16, "X", 32, "X", -16]}, + {"baseline": [-2, "X", 4, "X", -2, -4, "X", 8, "X", -4, -16, "X", 32, "X", -16], "baseline_invoice": {"affines": 54, "children": 9, "query_multiplicities": {"-16": 2, "-2": 2, "-4": 2, "32": 1, "4": 1, "8": 1}, "xor_scans": 6}, "indices": [1, 2, 4], "invoice": {"affines": 48, "children": 8, "query_multiplicities": {"-16": 2, "-4": 2, "2": 2, "32": 1, "4": 1}, "xor_scans": 6}, "mask": 22, "word": [-4, "X", 2, "X", 4, "X", 2, "X", -4, -16, "X", 32, "X", -16]}, + {"baseline": [-1, "X", 2, "X", -1, -2, "X", 4, "X", -2, -4, "X", 8, "X", -4, -16, "X", 32, "X", -16], "baseline_invoice": {"affines": 72, "children": 12, "query_multiplicities": {"-1": 2, "-16": 2, "-2": 2, "-4": 2, "2": 1, "32": 1, "4": 1, "8": 1}, "xor_scans": 8}, "indices": [0, 1, 2, 4], "invoice": {"affines": 60, "children": 10, "query_multiplicities": {"-16": 2, "-4": 2, "1": 2, "2": 3, "32": 1}, "xor_scans": 8}, "mask": 23, "word": [-4, "X", 2, "X", 1, "X", 2, "X", 1, "X", 2, "X", -4, -16, "X", 32, "X", -16]}, + {"baseline": [-8, "X", 16, "X", -8, -16, "X", 32, "X", -16], "baseline_invoice": {"affines": 36, "children": 6, "query_multiplicities": {"-16": 2, "-8": 2, "16": 1, "32": 1}, "xor_scans": 4}, "indices": [3, 4], "invoice": {"affines": 30, "children": 5, "query_multiplicities": {"-16": 2, "16": 1, "8": 2}, "xor_scans": 4}, "mask": 24, "word": [-16, "X", 8, "X", 16, "X", 8, "X", -16]}, + {"baseline": [-1, "X", 2, "X", -1, -8, "X", 16, "X", -8, -16, "X", 32, "X", -16], "baseline_invoice": {"affines": 54, "children": 9, "query_multiplicities": {"-1": 2, "-16": 2, "-8": 2, "16": 1, "2": 1, "32": 1}, "xor_scans": 6}, "indices": [0, 3, 4], "invoice": {"affines": 48, "children": 8, "query_multiplicities": {"-1": 2, "-16": 2, "16": 1, "2": 1, "8": 2}, "xor_scans": 6}, "mask": 25, "word": [-1, "X", 2, "X", -1, -16, "X", 8, "X", 16, "X", 8, "X", -16]}, + {"baseline": [-2, "X", 4, "X", -2, -8, "X", 16, "X", -8, -16, "X", 32, "X", -16], "baseline_invoice": {"affines": 54, "children": 9, "query_multiplicities": {"-16": 2, "-2": 2, "-8": 2, "16": 1, "32": 1, "4": 1}, "xor_scans": 6}, "indices": [1, 3, 4], "invoice": {"affines": 48, "children": 8, "query_multiplicities": {"-16": 2, "-2": 2, "16": 1, "4": 1, "8": 2}, "xor_scans": 6}, "mask": 26, "word": [-2, "X", 4, "X", -2, -16, "X", 8, "X", 16, "X", 8, "X", -16]}, + {"baseline": [-1, "X", 2, "X", -1, -2, "X", 4, "X", -2, -8, "X", 16, "X", -8, -16, "X", 32, "X", -16], "baseline_invoice": {"affines": 72, "children": 12, "query_multiplicities": {"-1": 2, "-16": 2, "-2": 2, "-8": 2, "16": 1, "2": 1, "32": 1, "4": 1}, "xor_scans": 8}, "indices": [0, 1, 3, 4], "invoice": {"affines": 60, "children": 10, "query_multiplicities": {"-16": 2, "-2": 2, "1": 2, "16": 1, "2": 1, "8": 2}, "xor_scans": 8}, "mask": 27, "word": [-2, "X", 1, "X", 2, "X", 1, "X", -2, -16, "X", 8, "X", 16, "X", 8, "X", -16]}, + {"baseline": [-4, "X", 8, "X", -4, -8, "X", 16, "X", -8, -16, "X", 32, "X", -16], "baseline_invoice": {"affines": 54, "children": 9, "query_multiplicities": {"-16": 2, "-4": 2, "-8": 2, "16": 1, "32": 1, "8": 1}, "xor_scans": 6}, "indices": [2, 3, 4], "invoice": {"affines": 42, "children": 7, "query_multiplicities": {"-16": 2, "4": 2, "8": 3}, "xor_scans": 6}, "mask": 28, "word": [-16, "X", 8, "X", 4, "X", 8, "X", 4, "X", 8, "X", -16]}, + {"baseline": [-1, "X", 2, "X", -1, -4, "X", 8, "X", -4, -8, "X", 16, "X", -8, -16, "X", 32, "X", -16], "baseline_invoice": {"affines": 72, "children": 12, "query_multiplicities": {"-1": 2, "-16": 2, "-4": 2, "-8": 2, "16": 1, "2": 1, "32": 1, "8": 1}, "xor_scans": 8}, "indices": [0, 2, 3, 4], "invoice": {"affines": 60, "children": 10, "query_multiplicities": {"-1": 2, "-16": 2, "2": 1, "4": 2, "8": 3}, "xor_scans": 8}, "mask": 29, "word": [-1, "X", 2, "X", -1, -16, "X", 8, "X", 4, "X", 8, "X", 4, "X", 8, "X", -16]}, + {"baseline": [-2, "X", 4, "X", -2, -4, "X", 8, "X", -4, -8, "X", 16, "X", -8, -16, "X", 32, "X", -16], "baseline_invoice": {"affines": 72, "children": 12, "query_multiplicities": {"-16": 2, "-2": 2, "-4": 2, "-8": 2, "16": 1, "32": 1, "4": 1, "8": 1}, "xor_scans": 8}, "indices": [1, 2, 3, 4], "invoice": {"affines": 54, "children": 9, "query_multiplicities": {"-16": 2, "2": 2, "4": 3, "8": 2}, "xor_scans": 8}, "mask": 30, "word": [-16, "X", 8, "X", 4, "X", 2, "X", 4, "X", 2, "X", 4, "X", 8, "X", -16]}, + {"baseline": [-1, "X", 2, "X", -1, -2, "X", 4, "X", -2, -4, "X", 8, "X", -4, -8, "X", 16, "X", -8, -16, "X", 32, "X", -16], "baseline_invoice": {"affines": 90, "children": 15, "query_multiplicities": {"-1": 2, "-16": 2, "-2": 2, "-4": 2, "-8": 2, "16": 1, "2": 1, "32": 1, "4": 1, "8": 1}, "xor_scans": 10}, "indices": [0, 1, 2, 3, 4], "invoice": {"affines": 66, "children": 11, "query_multiplicities": {"-16": 2, "1": 2, "2": 3, "4": 2, "8": 2}, "xor_scans": 10}, "mask": 31, "word": [-16, "X", 8, "X", 4, "X", 2, "X", 1, "X", 2, "X", 1, "X", 2, "X", 4, "X", 8, "X", -16]}, + {"baseline": [-32, "X", 64, "X", -32], "baseline_invoice": {"affines": 18, "children": 3, "query_multiplicities": {"-32": 2, "64": 1}, "xor_scans": 2}, "indices": [5], "invoice": {"affines": 18, "children": 3, "query_multiplicities": {"-32": 2, "64": 1}, "xor_scans": 2}, "mask": 32, "word": [-32, "X", 64, "X", -32]}, + {"baseline": [-1, "X", 2, "X", -1, -32, "X", 64, "X", -32], "baseline_invoice": {"affines": 36, "children": 6, "query_multiplicities": {"-1": 2, "-32": 2, "2": 1, "64": 1}, "xor_scans": 4}, "indices": [0, 5], "invoice": {"affines": 36, "children": 6, "query_multiplicities": {"-1": 2, "-32": 2, "2": 1, "64": 1}, "xor_scans": 4}, "mask": 33, "word": [-1, "X", 2, "X", -1, -32, "X", 64, "X", -32]}, + {"baseline": [-2, "X", 4, "X", -2, -32, "X", 64, "X", -32], "baseline_invoice": {"affines": 36, "children": 6, "query_multiplicities": {"-2": 2, "-32": 2, "4": 1, "64": 1}, "xor_scans": 4}, "indices": [1, 5], "invoice": {"affines": 36, "children": 6, "query_multiplicities": {"-2": 2, "-32": 2, "4": 1, "64": 1}, "xor_scans": 4}, "mask": 34, "word": [-2, "X", 4, "X", -2, -32, "X", 64, "X", -32]}, + {"baseline": [-1, "X", 2, "X", -1, -2, "X", 4, "X", -2, -32, "X", 64, "X", -32], "baseline_invoice": {"affines": 54, "children": 9, "query_multiplicities": {"-1": 2, "-2": 2, "-32": 2, "2": 1, "4": 1, "64": 1}, "xor_scans": 6}, "indices": [0, 1, 5], "invoice": {"affines": 48, "children": 8, "query_multiplicities": {"-2": 2, "-32": 2, "1": 2, "2": 1, "64": 1}, "xor_scans": 6}, "mask": 35, "word": [-2, "X", 1, "X", 2, "X", 1, "X", -2, -32, "X", 64, "X", -32]}, + {"baseline": [-4, "X", 8, "X", -4, -32, "X", 64, "X", -32], "baseline_invoice": {"affines": 36, "children": 6, "query_multiplicities": {"-32": 2, "-4": 2, "64": 1, "8": 1}, "xor_scans": 4}, "indices": [2, 5], "invoice": {"affines": 36, "children": 6, "query_multiplicities": {"-32": 2, "-4": 2, "64": 1, "8": 1}, "xor_scans": 4}, "mask": 36, "word": [-4, "X", 8, "X", -4, -32, "X", 64, "X", -32]}, + {"baseline": [-1, "X", 2, "X", -1, -4, "X", 8, "X", -4, -32, "X", 64, "X", -32], "baseline_invoice": {"affines": 54, "children": 9, "query_multiplicities": {"-1": 2, "-32": 2, "-4": 2, "2": 1, "64": 1, "8": 1}, "xor_scans": 6}, "indices": [0, 2, 5], "invoice": {"affines": 54, "children": 9, "query_multiplicities": {"-1": 2, "-32": 2, "-4": 2, "2": 1, "64": 1, "8": 1}, "xor_scans": 6}, "mask": 37, "word": [-1, "X", 2, "X", -1, -4, "X", 8, "X", -4, -32, "X", 64, "X", -32]}, + {"baseline": [-2, "X", 4, "X", -2, -4, "X", 8, "X", -4, -32, "X", 64, "X", -32], "baseline_invoice": {"affines": 54, "children": 9, "query_multiplicities": {"-2": 2, "-32": 2, "-4": 2, "4": 1, "64": 1, "8": 1}, "xor_scans": 6}, "indices": [1, 2, 5], "invoice": {"affines": 48, "children": 8, "query_multiplicities": {"-32": 2, "-4": 2, "2": 2, "4": 1, "64": 1}, "xor_scans": 6}, "mask": 38, "word": [-4, "X", 2, "X", 4, "X", 2, "X", -4, -32, "X", 64, "X", -32]}, + {"baseline": [-1, "X", 2, "X", -1, -2, "X", 4, "X", -2, -4, "X", 8, "X", -4, -32, "X", 64, "X", -32], "baseline_invoice": {"affines": 72, "children": 12, "query_multiplicities": {"-1": 2, "-2": 2, "-32": 2, "-4": 2, "2": 1, "4": 1, "64": 1, "8": 1}, "xor_scans": 8}, "indices": [0, 1, 2, 5], "invoice": {"affines": 60, "children": 10, "query_multiplicities": {"-32": 2, "-4": 2, "1": 2, "2": 3, "64": 1}, "xor_scans": 8}, "mask": 39, "word": [-4, "X", 2, "X", 1, "X", 2, "X", 1, "X", 2, "X", -4, -32, "X", 64, "X", -32]}, + {"baseline": [-8, "X", 16, "X", -8, -32, "X", 64, "X", -32], "baseline_invoice": {"affines": 36, "children": 6, "query_multiplicities": {"-32": 2, "-8": 2, "16": 1, "64": 1}, "xor_scans": 4}, "indices": [3, 5], "invoice": {"affines": 36, "children": 6, "query_multiplicities": {"-32": 2, "-8": 2, "16": 1, "64": 1}, "xor_scans": 4}, "mask": 40, "word": [-8, "X", 16, "X", -8, -32, "X", 64, "X", -32]}, + {"baseline": [-1, "X", 2, "X", -1, -8, "X", 16, "X", -8, -32, "X", 64, "X", -32], "baseline_invoice": {"affines": 54, "children": 9, "query_multiplicities": {"-1": 2, "-32": 2, "-8": 2, "16": 1, "2": 1, "64": 1}, "xor_scans": 6}, "indices": [0, 3, 5], "invoice": {"affines": 54, "children": 9, "query_multiplicities": {"-1": 2, "-32": 2, "-8": 2, "16": 1, "2": 1, "64": 1}, "xor_scans": 6}, "mask": 41, "word": [-1, "X", 2, "X", -1, -8, "X", 16, "X", -8, -32, "X", 64, "X", -32]}, + {"baseline": [-2, "X", 4, "X", -2, -8, "X", 16, "X", -8, -32, "X", 64, "X", -32], "baseline_invoice": {"affines": 54, "children": 9, "query_multiplicities": {"-2": 2, "-32": 2, "-8": 2, "16": 1, "4": 1, "64": 1}, "xor_scans": 6}, "indices": [1, 3, 5], "invoice": {"affines": 54, "children": 9, "query_multiplicities": {"-2": 2, "-32": 2, "-8": 2, "16": 1, "4": 1, "64": 1}, "xor_scans": 6}, "mask": 42, "word": [-2, "X", 4, "X", -2, -8, "X", 16, "X", -8, -32, "X", 64, "X", -32]}, + {"baseline": [-1, "X", 2, "X", -1, -2, "X", 4, "X", -2, -8, "X", 16, "X", -8, -32, "X", 64, "X", -32], "baseline_invoice": {"affines": 72, "children": 12, "query_multiplicities": {"-1": 2, "-2": 2, "-32": 2, "-8": 2, "16": 1, "2": 1, "4": 1, "64": 1}, "xor_scans": 8}, "indices": [0, 1, 3, 5], "invoice": {"affines": 66, "children": 11, "query_multiplicities": {"-2": 2, "-32": 2, "-8": 2, "1": 2, "16": 1, "2": 1, "64": 1}, "xor_scans": 8}, "mask": 43, "word": [-2, "X", 1, "X", 2, "X", 1, "X", -2, -8, "X", 16, "X", -8, -32, "X", 64, "X", -32]}, + {"baseline": [-4, "X", 8, "X", -4, -8, "X", 16, "X", -8, -32, "X", 64, "X", -32], "baseline_invoice": {"affines": 54, "children": 9, "query_multiplicities": {"-32": 2, "-4": 2, "-8": 2, "16": 1, "64": 1, "8": 1}, "xor_scans": 6}, "indices": [2, 3, 5], "invoice": {"affines": 48, "children": 8, "query_multiplicities": {"-32": 2, "-8": 2, "4": 2, "64": 1, "8": 1}, "xor_scans": 6}, "mask": 44, "word": [-8, "X", 4, "X", 8, "X", 4, "X", -8, -32, "X", 64, "X", -32]}, + {"baseline": [-1, "X", 2, "X", -1, -4, "X", 8, "X", -4, -8, "X", 16, "X", -8, -32, "X", 64, "X", -32], "baseline_invoice": {"affines": 72, "children": 12, "query_multiplicities": {"-1": 2, "-32": 2, "-4": 2, "-8": 2, "16": 1, "2": 1, "64": 1, "8": 1}, "xor_scans": 8}, "indices": [0, 2, 3, 5], "invoice": {"affines": 66, "children": 11, "query_multiplicities": {"-1": 2, "-32": 2, "-8": 2, "2": 1, "4": 2, "64": 1, "8": 1}, "xor_scans": 8}, "mask": 45, "word": [-1, "X", 2, "X", -1, -8, "X", 4, "X", 8, "X", 4, "X", -8, -32, "X", 64, "X", -32]}, + {"baseline": [-2, "X", 4, "X", -2, -4, "X", 8, "X", -4, -8, "X", 16, "X", -8, -32, "X", 64, "X", -32], "baseline_invoice": {"affines": 72, "children": 12, "query_multiplicities": {"-2": 2, "-32": 2, "-4": 2, "-8": 2, "16": 1, "4": 1, "64": 1, "8": 1}, "xor_scans": 8}, "indices": [1, 2, 3, 5], "invoice": {"affines": 60, "children": 10, "query_multiplicities": {"-32": 2, "-8": 2, "2": 2, "4": 3, "64": 1}, "xor_scans": 8}, "mask": 46, "word": [-8, "X", 4, "X", 2, "X", 4, "X", 2, "X", 4, "X", -8, -32, "X", 64, "X", -32]}, + {"baseline": [-1, "X", 2, "X", -1, -2, "X", 4, "X", -2, -4, "X", 8, "X", -4, -8, "X", 16, "X", -8, -32, "X", 64, "X", -32], "baseline_invoice": {"affines": 90, "children": 15, "query_multiplicities": {"-1": 2, "-2": 2, "-32": 2, "-4": 2, "-8": 2, "16": 1, "2": 1, "4": 1, "64": 1, "8": 1}, "xor_scans": 10}, "indices": [0, 1, 2, 3, 5], "invoice": {"affines": 72, "children": 12, "query_multiplicities": {"-32": 2, "-8": 2, "1": 2, "2": 3, "4": 2, "64": 1}, "xor_scans": 10}, "mask": 47, "word": [-8, "X", 4, "X", 2, "X", 1, "X", 2, "X", 1, "X", 2, "X", 4, "X", -8, -32, "X", 64, "X", -32]}, + {"baseline": [-16, "X", 32, "X", -16, -32, "X", 64, "X", -32], "baseline_invoice": {"affines": 36, "children": 6, "query_multiplicities": {"-16": 2, "-32": 2, "32": 1, "64": 1}, "xor_scans": 4}, "indices": [4, 5], "invoice": {"affines": 30, "children": 5, "query_multiplicities": {"-32": 2, "16": 2, "32": 1}, "xor_scans": 4}, "mask": 48, "word": [-32, "X", 16, "X", 32, "X", 16, "X", -32]}, + {"baseline": [-1, "X", 2, "X", -1, -16, "X", 32, "X", -16, -32, "X", 64, "X", -32], "baseline_invoice": {"affines": 54, "children": 9, "query_multiplicities": {"-1": 2, "-16": 2, "-32": 2, "2": 1, "32": 1, "64": 1}, "xor_scans": 6}, "indices": [0, 4, 5], "invoice": {"affines": 48, "children": 8, "query_multiplicities": {"-1": 2, "-32": 2, "16": 2, "2": 1, "32": 1}, "xor_scans": 6}, "mask": 49, "word": [-1, "X", 2, "X", -1, -32, "X", 16, "X", 32, "X", 16, "X", -32]}, + {"baseline": [-2, "X", 4, "X", -2, -16, "X", 32, "X", -16, -32, "X", 64, "X", -32], "baseline_invoice": {"affines": 54, "children": 9, "query_multiplicities": {"-16": 2, "-2": 2, "-32": 2, "32": 1, "4": 1, "64": 1}, "xor_scans": 6}, "indices": [1, 4, 5], "invoice": {"affines": 48, "children": 8, "query_multiplicities": {"-2": 2, "-32": 2, "16": 2, "32": 1, "4": 1}, "xor_scans": 6}, "mask": 50, "word": [-2, "X", 4, "X", -2, -32, "X", 16, "X", 32, "X", 16, "X", -32]}, + {"baseline": [-1, "X", 2, "X", -1, -2, "X", 4, "X", -2, -16, "X", 32, "X", -16, -32, "X", 64, "X", -32], "baseline_invoice": {"affines": 72, "children": 12, "query_multiplicities": {"-1": 2, "-16": 2, "-2": 2, "-32": 2, "2": 1, "32": 1, "4": 1, "64": 1}, "xor_scans": 8}, "indices": [0, 1, 4, 5], "invoice": {"affines": 60, "children": 10, "query_multiplicities": {"-2": 2, "-32": 2, "1": 2, "16": 2, "2": 1, "32": 1}, "xor_scans": 8}, "mask": 51, "word": [-2, "X", 1, "X", 2, "X", 1, "X", -2, -32, "X", 16, "X", 32, "X", 16, "X", -32]}, + {"baseline": [-4, "X", 8, "X", -4, -16, "X", 32, "X", -16, -32, "X", 64, "X", -32], "baseline_invoice": {"affines": 54, "children": 9, "query_multiplicities": {"-16": 2, "-32": 2, "-4": 2, "32": 1, "64": 1, "8": 1}, "xor_scans": 6}, "indices": [2, 4, 5], "invoice": {"affines": 48, "children": 8, "query_multiplicities": {"-32": 2, "-4": 2, "16": 2, "32": 1, "8": 1}, "xor_scans": 6}, "mask": 52, "word": [-4, "X", 8, "X", -4, -32, "X", 16, "X", 32, "X", 16, "X", -32]}, + {"baseline": [-1, "X", 2, "X", -1, -4, "X", 8, "X", -4, -16, "X", 32, "X", -16, -32, "X", 64, "X", -32], "baseline_invoice": {"affines": 72, "children": 12, "query_multiplicities": {"-1": 2, "-16": 2, "-32": 2, "-4": 2, "2": 1, "32": 1, "64": 1, "8": 1}, "xor_scans": 8}, "indices": [0, 2, 4, 5], "invoice": {"affines": 66, "children": 11, "query_multiplicities": {"-1": 2, "-32": 2, "-4": 2, "16": 2, "2": 1, "32": 1, "8": 1}, "xor_scans": 8}, "mask": 53, "word": [-1, "X", 2, "X", -1, -4, "X", 8, "X", -4, -32, "X", 16, "X", 32, "X", 16, "X", -32]}, + {"baseline": [-2, "X", 4, "X", -2, -4, "X", 8, "X", -4, -16, "X", 32, "X", -16, -32, "X", 64, "X", -32], "baseline_invoice": {"affines": 72, "children": 12, "query_multiplicities": {"-16": 2, "-2": 2, "-32": 2, "-4": 2, "32": 1, "4": 1, "64": 1, "8": 1}, "xor_scans": 8}, "indices": [1, 2, 4, 5], "invoice": {"affines": 60, "children": 10, "query_multiplicities": {"-32": 2, "-4": 2, "16": 2, "2": 2, "32": 1, "4": 1}, "xor_scans": 8}, "mask": 54, "word": [-4, "X", 2, "X", 4, "X", 2, "X", -4, -32, "X", 16, "X", 32, "X", 16, "X", -32]}, + {"baseline": [-1, "X", 2, "X", -1, -2, "X", 4, "X", -2, -4, "X", 8, "X", -4, -16, "X", 32, "X", -16, -32, "X", 64, "X", -32], "baseline_invoice": {"affines": 90, "children": 15, "query_multiplicities": {"-1": 2, "-16": 2, "-2": 2, "-32": 2, "-4": 2, "2": 1, "32": 1, "4": 1, "64": 1, "8": 1}, "xor_scans": 10}, "indices": [0, 1, 2, 4, 5], "invoice": {"affines": 72, "children": 12, "query_multiplicities": {"-32": 2, "-4": 2, "1": 2, "16": 2, "2": 3, "32": 1}, "xor_scans": 10}, "mask": 55, "word": [-4, "X", 2, "X", 1, "X", 2, "X", 1, "X", 2, "X", -4, -32, "X", 16, "X", 32, "X", 16, "X", -32]}, + {"baseline": [-8, "X", 16, "X", -8, -16, "X", 32, "X", -16, -32, "X", 64, "X", -32], "baseline_invoice": {"affines": 54, "children": 9, "query_multiplicities": {"-16": 2, "-32": 2, "-8": 2, "16": 1, "32": 1, "64": 1}, "xor_scans": 6}, "indices": [3, 4, 5], "invoice": {"affines": 42, "children": 7, "query_multiplicities": {"-32": 2, "16": 3, "8": 2}, "xor_scans": 6}, "mask": 56, "word": [-32, "X", 16, "X", 8, "X", 16, "X", 8, "X", 16, "X", -32]}, + {"baseline": [-1, "X", 2, "X", -1, -8, "X", 16, "X", -8, -16, "X", 32, "X", -16, -32, "X", 64, "X", -32], "baseline_invoice": {"affines": 72, "children": 12, "query_multiplicities": {"-1": 2, "-16": 2, "-32": 2, "-8": 2, "16": 1, "2": 1, "32": 1, "64": 1}, "xor_scans": 8}, "indices": [0, 3, 4, 5], "invoice": {"affines": 60, "children": 10, "query_multiplicities": {"-1": 2, "-32": 2, "16": 3, "2": 1, "8": 2}, "xor_scans": 8}, "mask": 57, "word": [-1, "X", 2, "X", -1, -32, "X", 16, "X", 8, "X", 16, "X", 8, "X", 16, "X", -32]}, + {"baseline": [-2, "X", 4, "X", -2, -8, "X", 16, "X", -8, -16, "X", 32, "X", -16, -32, "X", 64, "X", -32], "baseline_invoice": {"affines": 72, "children": 12, "query_multiplicities": {"-16": 2, "-2": 2, "-32": 2, "-8": 2, "16": 1, "32": 1, "4": 1, "64": 1}, "xor_scans": 8}, "indices": [1, 3, 4, 5], "invoice": {"affines": 60, "children": 10, "query_multiplicities": {"-2": 2, "-32": 2, "16": 3, "4": 1, "8": 2}, "xor_scans": 8}, "mask": 58, "word": [-2, "X", 4, "X", -2, -32, "X", 16, "X", 8, "X", 16, "X", 8, "X", 16, "X", -32]}, + {"baseline": [-1, "X", 2, "X", -1, -2, "X", 4, "X", -2, -8, "X", 16, "X", -8, -16, "X", 32, "X", -16, -32, "X", 64, "X", -32], "baseline_invoice": {"affines": 90, "children": 15, "query_multiplicities": {"-1": 2, "-16": 2, "-2": 2, "-32": 2, "-8": 2, "16": 1, "2": 1, "32": 1, "4": 1, "64": 1}, "xor_scans": 10}, "indices": [0, 1, 3, 4, 5], "invoice": {"affines": 72, "children": 12, "query_multiplicities": {"-2": 2, "-32": 2, "1": 2, "16": 3, "2": 1, "8": 2}, "xor_scans": 10}, "mask": 59, "word": [-2, "X", 1, "X", 2, "X", 1, "X", -2, -32, "X", 16, "X", 8, "X", 16, "X", 8, "X", 16, "X", -32]}, + {"baseline": [-4, "X", 8, "X", -4, -8, "X", 16, "X", -8, -16, "X", 32, "X", -16, -32, "X", 64, "X", -32], "baseline_invoice": {"affines": 72, "children": 12, "query_multiplicities": {"-16": 2, "-32": 2, "-4": 2, "-8": 2, "16": 1, "32": 1, "64": 1, "8": 1}, "xor_scans": 8}, "indices": [2, 3, 4, 5], "invoice": {"affines": 54, "children": 9, "query_multiplicities": {"-32": 2, "16": 2, "4": 2, "8": 3}, "xor_scans": 8}, "mask": 60, "word": [-32, "X", 16, "X", 8, "X", 4, "X", 8, "X", 4, "X", 8, "X", 16, "X", -32]}, + {"baseline": [-1, "X", 2, "X", -1, -4, "X", 8, "X", -4, -8, "X", 16, "X", -8, -16, "X", 32, "X", -16, -32, "X", 64, "X", -32], "baseline_invoice": {"affines": 90, "children": 15, "query_multiplicities": {"-1": 2, "-16": 2, "-32": 2, "-4": 2, "-8": 2, "16": 1, "2": 1, "32": 1, "64": 1, "8": 1}, "xor_scans": 10}, "indices": [0, 2, 3, 4, 5], "invoice": {"affines": 72, "children": 12, "query_multiplicities": {"-1": 2, "-32": 2, "16": 2, "2": 1, "4": 2, "8": 3}, "xor_scans": 10}, "mask": 61, "word": [-1, "X", 2, "X", -1, -32, "X", 16, "X", 8, "X", 4, "X", 8, "X", 4, "X", 8, "X", 16, "X", -32]}, + {"baseline": [-2, "X", 4, "X", -2, -4, "X", 8, "X", -4, -8, "X", 16, "X", -8, -16, "X", 32, "X", -16, -32, "X", 64, "X", -32], "baseline_invoice": {"affines": 90, "children": 15, "query_multiplicities": {"-16": 2, "-2": 2, "-32": 2, "-4": 2, "-8": 2, "16": 1, "32": 1, "4": 1, "64": 1, "8": 1}, "xor_scans": 10}, "indices": [1, 2, 3, 4, 5], "invoice": {"affines": 66, "children": 11, "query_multiplicities": {"-32": 2, "16": 2, "2": 2, "4": 3, "8": 2}, "xor_scans": 10}, "mask": 62, "word": [-32, "X", 16, "X", 8, "X", 4, "X", 2, "X", 4, "X", 2, "X", 4, "X", 8, "X", 16, "X", -32]}, + {"baseline": [-1, "X", 2, "X", -1, -2, "X", 4, "X", -2, -4, "X", 8, "X", -4, -8, "X", 16, "X", -8, -16, "X", 32, "X", -16, -32, "X", 64, "X", -32], "baseline_invoice": {"affines": 108, "children": 18, "query_multiplicities": {"-1": 2, "-16": 2, "-2": 2, "-32": 2, "-4": 2, "-8": 2, "16": 1, "2": 1, "32": 1, "4": 1, "64": 1, "8": 1}, "xor_scans": 12}, "indices": [0, 1, 2, 3, 4, 5], "invoice": {"affines": 78, "children": 13, "query_multiplicities": {"-32": 2, "1": 2, "16": 2, "2": 3, "4": 2, "8": 2}, "xor_scans": 12}, "mask": 63, "word": [-32, "X", 16, "X", 8, "X", 4, "X", 2, "X", 1, "X", 2, "X", 1, "X", 2, "X", 4, "X", 8, "X", 16, "X", -32]} + ], + "lowerings": { + "-64": [["A", 2, "1", [[0, "-1"]]], ["A", 3, "1", [[0, "1"]]], ["A", 5, "-16", [[0, "-15"], [2, "16"], [3, "16"]]], ["C", 0, 5], ["A", 2, "1", [[0, "1"]]], ["A", 3, "1", [[0, "-1"]]], ["A", 5, "1/16", [[0, "-17/16"], [2, "1"], [3, "1"]]]], + "-32": [["A", 2, "1", [[0, "-1"]]], ["A", 3, "1", [[0, "1"]]], ["A", 5, "-8", [[0, "-7"], [2, "8"], [3, "8"]]], ["C", 0, 5], ["A", 2, "1", [[0, "1"]]], ["A", 3, "1", [[0, "-1"]]], ["A", 5, "1/8", [[0, "-9/8"], [2, "1"], [3, "1"]]]], + "-16": [["A", 2, "1", [[0, "-1"]]], ["A", 3, "1", [[0, "1"]]], ["A", 5, "-4", [[0, "-3"], [2, "4"], [3, "4"]]], ["C", 0, 5], ["A", 2, "1", [[0, "1"]]], ["A", 3, "1", [[0, "-1"]]], ["A", 5, "1/4", [[0, "-5/4"], [2, "1"], [3, "1"]]]], + "-8": [["A", 2, "1", [[0, "-1"]]], ["A", 3, "1", [[0, "1"]]], ["A", 5, "-2", [[0, "-1"], [2, "2"], [3, "2"]]], ["C", 0, 5], ["A", 2, "1", [[0, "1"]]], ["A", 3, "1", [[0, "-1"]]], ["A", 5, "1/2", [[0, "-3/2"], [2, "1"], [3, "1"]]]], + "-4": [["A", 2, "1", [[0, "-1"]]], ["A", 3, "1", [[0, "1"]]], ["A", 5, "-1", [[0, "0"], [2, "1"], [3, "1"]]], ["C", 0, 5], ["A", 2, "1", [[0, "1"]]], ["A", 3, "1", [[0, "-1"]]], ["A", 5, "1", [[0, "-2"], [2, "1"], [3, "1"]]]], + "-2": [["A", 2, "1", [[0, "-1"]]], ["A", 3, "1", [[0, "1"]]], ["A", 5, "-1/2", [[0, "1/2"], [2, "1/2"], [3, "1/2"]]], ["C", 0, 5], ["A", 2, "1", [[0, "1"]]], ["A", 3, "1", [[0, "-1"]]], ["A", 5, "2", [[0, "-3"], [2, "1"], [3, "1"]]]], + "-1": [["A", 2, "1", [[0, "-1"]]], ["A", 3, "1", [[0, "1"]]], ["A", 5, "-1/4", [[0, "3/4"], [2, "1/4"], [3, "1/4"]]], ["C", 0, 5], ["A", 2, "1", [[0, "1"]]], ["A", 3, "1", [[0, "-1"]]], ["A", 5, "4", [[0, "-5"], [2, "1"], [3, "1"]]]], + "1": [["A", 2, "1", [[0, "-1"]]], ["A", 3, "1", [[0, "1"]]], ["A", 5, "1/4", [[0, "5/4"], [2, "-1/4"], [3, "-1/4"]]], ["C", 0, 5], ["A", 2, "1", [[0, "1"]]], ["A", 3, "1", [[0, "-1"]]], ["A", 5, "-4", [[0, "3"], [2, "1"], [3, "1"]]]], + "2": [["A", 2, "1", [[0, "-1"]]], ["A", 3, "1", [[0, "1"]]], ["A", 5, "1/2", [[0, "3/2"], [2, "-1/2"], [3, "-1/2"]]], ["C", 0, 5], ["A", 2, "1", [[0, "1"]]], ["A", 3, "1", [[0, "-1"]]], ["A", 5, "-2", [[0, "1"], [2, "1"], [3, "1"]]]], + "4": [["A", 2, "1", [[0, "-1"]]], ["A", 3, "1", [[0, "1"]]], ["A", 5, "1", [[0, "2"], [2, "-1"], [3, "-1"]]], ["C", 0, 5], ["A", 2, "1", [[0, "1"]]], ["A", 3, "1", [[0, "-1"]]], ["A", 5, "-1", [[0, "0"], [2, "1"], [3, "1"]]]], + "8": [["A", 2, "1", [[0, "-1"]]], ["A", 3, "1", [[0, "1"]]], ["A", 5, "2", [[0, "3"], [2, "-2"], [3, "-2"]]], ["C", 0, 5], ["A", 2, "1", [[0, "1"]]], ["A", 3, "1", [[0, "-1"]]], ["A", 5, "-1/2", [[0, "-1/2"], [2, "1"], [3, "1"]]]], + "16": [["A", 2, "1", [[0, "-1"]]], ["A", 3, "1", [[0, "1"]]], ["A", 5, "4", [[0, "5"], [2, "-4"], [3, "-4"]]], ["C", 0, 5], ["A", 2, "1", [[0, "1"]]], ["A", 3, "1", [[0, "-1"]]], ["A", 5, "-1/4", [[0, "-3/4"], [2, "1"], [3, "1"]]]], + "32": [["A", 2, "1", [[0, "-1"]]], ["A", 3, "1", [[0, "1"]]], ["A", 5, "8", [[0, "9"], [2, "-8"], [3, "-8"]]], ["C", 0, 5], ["A", 2, "1", [[0, "1"]]], ["A", 3, "1", [[0, "-1"]]], ["A", 5, "-1/8", [[0, "-7/8"], [2, "1"], [3, "1"]]]], + "64": [["A", 2, "1", [[0, "-1"]]], ["A", 3, "1", [[0, "1"]]], ["A", 5, "16", [[0, "17"], [2, "-16"], [3, "-16"]]], ["C", 0, 5], ["A", 2, "1", [[0, "1"]]], ["A", 3, "1", [[0, "-1"]]], ["A", 5, "-1/16", [[0, "-15/16"], [2, "1"], [3, "1"]]]] + } +} diff --git a/research/dyadic-query-runs/CLAIM.md b/research/dyadic-query-runs/CLAIM.md new file mode 100644 index 0000000000..1a8cf878aa --- /dev/null +++ b/research/dyadic-query-runs/CLAIM.md @@ -0,0 +1,68 @@ +# Sprint claim: dyadic query runs + +- Track: recursive interfaces. OS assignment seed **55**, drawn with + `secrets.randbelow(100)` at 2026-10-13 13:51:49 UTC (2026-10-14 Melbourne). +- Exact base: `47481c89fd30a43f8f882eb4b391e89c29273fd0`. +- Object: batches of PR840's centered native BIT shears on the **same** target + and unchanged source, with exponents `+/-2^j` for a finite index set J. +- Hypothesis: keeping the target in its intermediate ADDRESS layout across + adjacent powers eliminates repeated query boundaries. The candidate bill is + `2|J| + runs(J)` ordinary children instead of `3|J|`, with no private row. + Investigate exact optimality only in the target-query / source-XOR alphabet. +- Method/domain: written integer-walk argument, literal paid affine/child + lowering, independent Laurent and modular VALUE replay. Complete all 63 + nonempty subsets of indices 0 through 5; seed 55 selects the gapped set + `{0,1,2,4,5}`. No random search or new kappa claim. +- Deliverable: one standalone research construction with proof, complete + typed cost recurrence, exact certificates, source pins and adverse controls. +- Budget: approximately 60 minutes, orientation at most 12 minutes; + final 15 minutes reserved for verification and handoff. Expected finish + 2026-10-14 01:52 AEDT (2026-10-13 14:52 UTC). + +Three candidates were considered: (1) extend the dyadic DATA-target query +pair across a finite exponent set, (2) move clean checkpoints among recursive +subtrees, (3) share a dirty connector among product-shear outputs. Candidate 1 +was selected. PR714/788 already cover checkpoint placement; PR889/934/943 and +the newly visible PR944 cover the multi-source connector neighborhood. The +selected task extends PR840's single centered pair to a shared target batch; +it does not repeat its arbitrary-dirty-row three-query lower bound. + +Initial overlap inventory: 714 open PRs through #943. Immediate claim refresh +included #944 (signed connectors) and #945 (complex Horner). No pinned issues +exist; the two open issues #650/#913 are not sprint coordination issues, so +this claim is local. The review ledger marks PR521 unreviewed and has no +exact-head acceptance for PR677/840. They are pinned pending predecessors, +not accepted frontier dependencies. Prior fixed-menu and supplier-profile +negative results are not reopened: the query interface changes and the +selected supplier is not modified. + +At this base the selected conditional kappa is +`1661957774647029/1000000000000000000` (PR890). Its certificate, actual T21 +construction and maintainer review were followed. The first checkout read +saw the older PR799 snapshot while the fetch was running; that snapshot is +not used as the accepted result here. + +## Result update + +Completed contribution: [PR953](https://github.com/CrocSwap/integer-mult-bounds/pull/953), +**recursive-interface research construction; no new kappa**. The written +argument proves the `2|J|+runs(J)` query optimum in the declared uniform +target-only dyadic alphabet, including arbitrary off-support excursions. +The seed-55 batch uses 12 children and 72 affine events instead of 15 and 90, +with ten XOR scans and no extra full private row in both programs. Actual +coefficient-dependent work and all inherited implementation obligations remain +explicit in [the proof and recurrence](PROOF.md). + +All 63 literal cases, the separate 15-selection bounded walk census, 252 dirty +forward/inverse case pairs, 15 rejection controls and eight package faults +pass. The complete evidence agrees on Python 3.14.6 and 3.9.6; source Git +objects, relocation and regeneration pass. See [validation](VALIDATION.md) +for the exact domains and the incomplete root-suite boundary (missing SymPy). + +The full overlap refresh reached #947 and the immediate pre-submission check +reached #950, again with no pinned coordination issue. PR840's consumed head +remains unchanged. Main advanced to `007664306fff84fbb1c9a1b4053b69f439764034` +without changing the selected record. The mathematical implementation and +certificate were committed at `282eff4d60bacfe1d0018bc08b22a2e1bf8d5928`; +this result update adds publication metadata only. Verification and packaging +occupied the final part of the session, after implementation was frozen. diff --git a/research/dyadic-query-runs/EVIDENCE.json b/research/dyadic-query-runs/EVIDENCE.json new file mode 100644 index 0000000000..65fb2b7fd6 --- /dev/null +++ b/research/dyadic-query-runs/EVIDENCE.json @@ -0,0 +1,167 @@ +{ + "all_cases_baseline_queries": 576, + "all_cases_fused_queries": 496, + "ancestral_source_files": 7, + "cases": 63, + "dirty_execution_sha256": "3a6aa40fd16e230b40e9b0cd7f19afac8276b85947892a1193f93eada0ae9f46", + "dirty_forward_cases": 252, + "dirty_inverse_cases": 252, + "format": "dyadic-query-runs-evidence-v1", + "full_address_moduli": [ + 3, + 5 + ], + "graph_records_sha256": "3964f2b66ba03ade78eb7b96f0e2400932dcb4d6a35e85d152e31ae7e6bb3fe2", + "independent_bounded_walk_census": { + "completed_selections": [ + [ + 1, + 3 + ], + [ + 2, + 3 + ], + [ + 3, + 5 + ], + [ + 4, + 3 + ], + [ + 5, + 6 + ], + [ + 6, + 5 + ], + [ + 7, + 7 + ], + [ + 8, + 3 + ], + [ + 9, + 6 + ], + [ + 10, + 6 + ], + [ + 11, + 8 + ], + [ + 12, + 5 + ], + [ + 13, + 8 + ], + [ + 14, + 7 + ], + [ + 15, + 9 + ] + ], + "directed_edges_examined": 156672, + "indices": [ + 0, + 1, + 2, + 3 + ], + "max_dyadic_step": 64, + "position_interval": [ + -32, + 32 + ], + "reachable_states": 15616, + "scope": "Complete bounded walk census; universal bound is the written proof." + }, + "modular_columns": 756, + "native_address_comparisons": 228956, + "odd_moduli": [ + 3, + 5, + 7, + 9, + 15, + 25, + 27, + 49, + 81 + ], + "positive_scope_controls": [ + "nondyadic five-query endpoint", + "modulus-three zero target" + ], + "rational_columns": 84, + "rejection_controls": [ + "omitted final return", + "omitted source tap", + "wrong query sign", + "VALUE-address confusion", + "source query outside alphabet", + "unpaid children", + "unpaid affines", + "unpaid xor_scans", + "removed native child", + "control after target", + "nonunit at odd radix", + "scalar-valid wrong native sign", + "even radix admission", + "nondyadic shortcut", + "valid nonoptimal invoice" + ], + "seed_baseline_invoice": { + "affines": 90, + "children": 15, + "query_multiplicities": { + "-1": 2, + "-16": 2, + "-2": 2, + "-32": 2, + "-4": 2, + "2": 1, + "32": 1, + "4": 1, + "64": 1, + "8": 1 + }, + "xor_scans": 10 + }, + "seed_indices": [ + 0, + 1, + 2, + 4, + 5 + ], + "seed_invoice": { + "affines": 72, + "children": 12, + "query_multiplicities": { + "-32": 2, + "-4": 2, + "1": 2, + "16": 2, + "2": 3, + "32": 1 + }, + "xor_scans": 10 + }, + "source_files": 11, + "spectator_configurations_per_address": 4 +} diff --git a/research/dyadic-query-runs/NOTICE.md b/research/dyadic-query-runs/NOTICE.md new file mode 100644 index 0000000000..5e073127c6 --- /dev/null +++ b/research/dyadic-query-runs/NOTICE.md @@ -0,0 +1,42 @@ +# Attribution and assistance + +New material prepared by **Ross Richardson (@RossRichardson)** with substantial +**OpenAI Codex assistance** in mathematical derivation, implementation, +verification and writing. Licensed under the repository's Apache-2.0 license. +No independent human review, proof-assistant verification, official endorsement +or literature-priority claim is made. No delegated agents were used. + +- **Wentao Li / VictorLiwentao, PR840**, exact head + `da2cd0dd2229e08b61b174a8835a2c2bb99d2230`: centered dyadic DATA shear, + signed dyadic one-child lowering, three-query single-pair construction, + full target ownership contract and typed cost recurrence. Its proof, + notice, source manifest and license are retained byte for byte. The present + construction concatenates runs of dyadic indices; its lower bound is in + the narrower target-only alphabet, not PR840's arbitrary-row chart model. +- **Karl Appel / applecrusher, PR521**, head + `a190fdb39f31647fc6f651625353710624627348`: native unipotent ADDRESS map + and paid one-child lowering. The original proof and source pins are + retained unchanged through PR840's archive and checked against original + Git objects. +- **commdata2338, PR677**, head + `613c02b8b4411f991f108dcc1481b3f9100b996f`: completed first-difference + DATA-target shears, dirty-role contract and query-cost distinctions. The + original proof and notice are retained, including their predecessor + attribution to eumemic/PR288 and Ali Romman/PR468 and AI-assistance notices. +- **OpenAI's original integer-multiplication framework**, maintained here + by **Douglas Colkitt**: ordered affine streams, complete row volumes, + ordinary ADDRESS interchange and tape/head-return contracts. Full source + sections 02 and 04 and their license are retained unchanged at the original + revision pinned in PR840's source manifest. + +The selected PR890 construction by Chafik Boukhalfa builds on Jeremy Kothe, +Hao Yan, DreamingOfClouds, eumemic and the repository's cumulative contributors. +Its conditional exponent is context, not a result established by this package. +PR714/788 checkpoint work and PR889/929/934/938/940/943/944 were inspected for +overlap. Their different storage and query contracts are not consumed here. +The cross-family split obstruction and PR83 fixed-menu barrier remain intact: +no recursive child is split or repriced as a different operation. + +The graph-component counting argument and retained-layout scheduling are +elementary methods; no claim of new mathematics beyond this precise +repository interface and its finite implementation evidence is made. diff --git a/research/dyadic-query-runs/PROOF.md b/research/dyadic-query-runs/PROOF.md new file mode 100644 index 0000000000..83c08a1be3 --- /dev/null +++ b/research/dyadic-query-runs/PROOF.md @@ -0,0 +1,228 @@ +# Dyadic runs in a restored native BIT query batch + +This is a local recursive-interface construction and a query-count optimum +in an explicitly restricted alphabet. It does not change a supplier or kappa. +The one-query native lowering is credited to PR521 and its signed dyadic +extension to PR840; their original proofs and notices are in `vendor/`. + +## 1. Contract and alphabet + +Let `h` be the VALUE permutation induced by the ADDRESS **push** map + +``` +M(k) = I + (k/4) s r^T, +s = (1,0,1,-1,0,-1)^T, r = (1,0,-1,-1,0,1)^T. +``` + +The six selected fields have equal width b over `Z/(ell^b)`, with ell odd. +They are physically ordered; arbitrary intervening and exterior ADDRESS +fields and suffix VALUE records are spectators. Since `r^T s=0`, the query +`Q(k): x <- h^k x` has inverse `Q(-k)` and `M(k)M(l)=M(k+l)`. +The other instruction is `X: x <- x XOR y`. Only the target x is queried; +source y and all other dirty roles are never changed. Every query power must +be a nonzero **signed power of two**. Every full ordinary recursive child, +its affine wrappers and the full XOR scan are paid. + +For a finite nonempty index set `J subset Z_{>=0}`, define + +``` +D_J(x,y,z) = (x + sum_{j in J}(h^(2^j)+h^(-2^j)) y, y, z). +``` + +VALUE sums are in F2; ADDRESS arithmetic is not. The program is uniform over +all odd prime-power field moduli. The target is exclusively owned throughout +the batch: intermediate contents cannot be observed or used by other calls. +No clean, disposable or additional full private role is available. Role +mixing, queries on y or z, nondyadic queries and modulus-specific programs +are outside the optimization alphabet. PR840's more permissive single-pair +three-query lower bound is neither strengthened nor contradicted here. + +## 2. Retain the target layout across one run + +For an interval `[l,u]` of indices, follow this walk of cumulative powers: + +``` +0, -2^u, -2^(u-1), ..., -2^l, +2^l, ..., +2^(u-1), +2^u, 0. +``` + +Execute `Q(next-current)` at each edge and X at every nonzero listed vertex. +Every edge is dyadic: the two exterior edges are `-2^u`, each interior gap +on either side is a positive power of two, and the middle edge is `2^(l+1)`. +If the interval has t indices there are `2t+1` queries and `2t` XOR scans. + +An X at prefix power p contributes `h^(-p)y` at the endpoint, because the +total query power is zero. The visited powers are precisely `+/-2^j` for +the interval. Thus the endpoint is D for that interval on arbitrary dirty +inputs. Concatenate this word for all maximal consecutive runs of J. Each +word restores the target layout; the VALUE shears add and source/spectators +remain unchanged. If r is `|J|` and c is the number of runs, the complete +word uses + +``` +q(J) = 2r+c queries, 2r XOR scans. +``` + +The baseline concatenates PR840's optimal single-pair word +`Q(-a), X, Q(2a), X, Q(-a)` for every `a=2^j`, costing `3r` queries and +the same `2r` XOR scans. The saving is `r-c` full queries, without assuming +any previously restored boundary is free. Reversing all literal events, +inverting each Q and keeping X, gives the exact inverse. D itself is an +involution, but the inverse literal word need not equal the forward word. + +## 3. Exact optimum in this alphabet, including off-support excursions + +Consider any finite program in the alphabet, not just the run constructor. +On a full-order orbit the ADDRESS action is multiplication by t in +`F2[t,t^-1]/(t^m-1)`, m an odd prime power. Such an orbit exists: starting +at the first coordinate vector gives `e0 + k*s/4`, distinct for k modulo m. +Uniform equality for arbitrarily large m implies equality of the corresponding +finite Laurent polynomials. Choose m larger than their exponent span to see +that no nonzero finite difference can vanish in every quotient. + +Restoring arbitrary x therefore forces the total **integer** query power +to zero. At cumulative prefix p, an X adds `t^(-p)y` at the endpoint. +To produce D_J, the closed walk must visit every member of +`S={+/-2^j: j in J}` and tap it oddly; off-support taps must cancel evenly. +In particular it needs at least `2r` XOR scans. + +Join two distinct elements of S when their difference is a signed power of +two. For distinct magnitudes, same-sign vertices are joined exactly when +their indices differ by one: `2^b-2^a = 2^a(2^(b-a)-1)`. Opposite-sign +vertices of different magnitudes are not joined, since their sum has an odd +factor larger than one. The two signs of a single magnitude are joined. +Consequently this induced graph has exactly c components, the consecutive +runs of J. This is a graph property of the required vertices, not a ban on +off-support visits. + +Write a closed walk with q edges cyclically as its first q vertices (omit +the repeated endpoint). Let a count occurrences in S and b occurrences +outside S. Then `q=a+b` and `a>=2r`. The walk starts at 0, outside S, so +`b>=1`. Every block of S vertices between consecutive outside occurrences +lies within one component of the induced graph. There are at most b such +blocks. All c components must be visited, so `b>=c`. Thus + +``` +q >= 2r+c. +``` + +This also covers repeated vertices, untapped intermediate states, arbitrary +large dyadic jumps and off-support XOR cancellations. Section 2 attains the +bound. The empty set separately admits the empty word. This is a written +universal argument; the finite certificate is supporting evidence, not a +proof-assistant theorem. + +Two scope controls matter. For J={0,2}, allowing nondyadic jumps gives the +five-query walk `0,-4,-1,1,4,0`, beating the six-query restricted optimum. +For J={0,1} modulo 3, the four monomials cancel and the empty program works. +Neither is a counterexample to the uniform dyadic-alphabet theorem. + +## 4. Literal paid native lowering + +For each query k, set `a=k/4`. The retained PR840 chronological lowering is + +``` +z2 <- z2-z0 +z3 <- z3+z0 +z5 <- a*z5+(1+a)*z0-a*z2-a*z3 +CHILD_C(0,5) +z2 <- z2+z0 +z3 <- z3-z0 +z5 <- -(1/a)*z5+(1/a-1)*z0+z2+z3. +``` + +The child interchanges equal-width fields on the entire queried row. It +preserves all spectators and returns its own workspace. Every affine control +precedes its target. Each diagonal coefficient is a signed power of two, +and every coefficient denominator is a power of two. Hence these operations +and their literal inverses specialize to every odd modulus. Removing the +child or treating the ADDRESS coefficients as binary VALUE coefficients is +invalid. The exact certificate contains all seven events for each used k. +This lowering is inherited; the new contribution is the shared batch schedule +and its exact restricted optimum. + +## 5. Complete work and storage recurrence + +Use the same three genuine equal-volume roles as PR840. Let each full row +have volume U (including all spectators and VALUE bits), `V=3U`, `N=3b`. +Let `C(U,b)` pay one ordinary restored ADDRESS interchange. Let `L_k(U,b)` +pay all six affine events of the above lowering: coefficient preparation, +coefficient/source access, descriptors, counters, primitive temporary streams, +routing and head returns. Let `X(U)` pay one aligned XOR scan. Let `R_J` +pay all further schedule preparation/dispatch, full-row splitting/rejoining, +parking, source access and additional head returns, avoiding double counting +those already in L, C or X. J is supplied as a finite fixed program parameter. + +The literal invoices for the baseline B and fused run program F are + +``` +B_J(V,3b) <= 3r C(U,b) + + sum_{j in J} (2 L_{-2^j}(U,b) + L_{2^(j+1)}(U,b)) + + 2r X(U) + R_B(J,U,b), + +F_J(V,3b) <= (2r+c) C(U,b) + + sum_{[l,u] a run of J} + (2 L_{-2^u}(U,b) + L_{2^(l+1)}(U,b) + + 2 sum_{i=l}^{u-1} L_{2^i}(U,b)) + + 2r X(U) + R_F(J,U,b). +``` + +Each query has exactly one full-row child and six affine events. No copy, +clear, uncompute child or frame change is omitted: X reads unchanged y; +queries act only on x; all target-layout return edges are present; all +address-chart work is in the six-event lowerings. There are no extra full +private roles, copied sources or recursive product children. Any future +supplier adapter or incompatible frame must be separately charged, and is +not provided by this construction. The child interface is inherited, not +implemented by these finite replay arrays. + +For the two literal invoices, the saving is `(r-c)C + L_B-L_F + R_B-R_F`. +Different coefficient tables may change L, so no universal wall-clock or +finite total-work speedup is inferred from the counts. In particular the +seed-selected J={0,1,2,4,5} lowers 15 to 12 children and 90 to 72 affine +events, retaining ten XOR scans; its coefficient-aware inequality still +needs the actual implementation costs. + +The children execute sequentially on actual volume V/3 and width N/3. For +fixed J, the retained stream premises give `L_k,X,R=O_J(V)`, so the child +coefficient is `(2r+c)/3` instead of r. For growing J, retain all coefficient, +program-storage and dispatch dependence explicitly: coefficients have +`O(1+max J)` bits, but the inherited stream constants can depend on their +values. No polynomial dependence on max J is asserted. A safe peak bound is + +``` +W_F(V,3b) <= V + B_F(J,U,b) + W_C(U,b), +``` + +where B_F pays live coefficient/descriptor/counter state and the maximum +nonchild stream workspace retained across a child. This is not an exact +physical tape count. The target and source may not alias. + +F is a completed DATA shear and C an ADDRESS interchange. Substituting F for +C and solving a self-recurrence would require a compiler not supplied here. +Neither selected supplier nor any assembly inequality changes. Common labels, +mutable-source realization, frames/owners, full-row hosting, arbitrary widths, +all-size compilation, tape/precision and the outer analytic transfer remain +open. No new kappa follows from this result. + +At the pinned base the selected assembly explicitly reports `binding: complex`: +the complex lower endpoint is `1664724476433282815289/10^24`, below the bit +endpoint `1733427039589844234749/10^24`. Even an integrated improvement only +to this BIT interface would not by itself establish a stronger selected +exponent. No such integration or recomputed supplier moment is supplied here. + +## 6. Bounded evidence + +All 63 nonempty subsets of indices 0 through 5 are compiled. Seed 55 is the +six-bit mask choosing the gapped five-pair example. A separate verifier reads +literal words and lowerings without importing the constructor, independently +recounts graph components, and replays Laurent coefficients, rational and +modular ADDRESS columns and full-domain dirty VALUE executions. It checks +baselines, inverses, native spectators and obligation-specific faults. +An independent breadth-first traversal exhausts all walks represented by +`(position, visited-support-mask)` with position in `[-32,32]`, dyadic steps +through 64 and support indices 0 through 3. All 15 nonempty target selections +agree with the formula. This allows intermediate visits outside their support +but is still a bounded experiment, separate from section 3's unbounded proof. +The stopping rule is completion of these domains, with no adaptive search. +No exhaustive optimization over arbitrary circuits, new supplier invoice, +full multiplication proof or literature-priority claim is made. diff --git a/research/dyadic-query-runs/PUBLICATION-CONTEXT.json b/research/dyadic-query-runs/PUBLICATION-CONTEXT.json new file mode 100644 index 0000000000..a1ac6ea1b8 --- /dev/null +++ b/research/dyadic-query-runs/PUBLICATION-CONTEXT.json @@ -0,0 +1,91 @@ +{ + "base_commit": "47481c89fd30a43f8f882eb4b391e89c29273fd0", + "closest_prs": [ + { + "head": "a8dccef5736454993c7f428f17b23f60329847f1", + "number": 947, + "title": "Scoped negative result: exact constant-row center shear optimum (no new kappa)" + }, + { + "head": "b6e22dbf548d72f18b722ccb6c2ea8e3d9df6ac1", + "number": 946, + "title": "Tooling: cross-platform byte/codec reproducibility of the make verify surface (no new kappa)" + }, + { + "head": "a3245bf22fa2a2eb778b11128cbc605b130d737f", + "number": 945, + "title": "Finite construction: joint Horner saves 13,072 PR799 backward primitives (no new kappa)" + }, + { + "head": "5dbcfbc63f646de5a1354f6b9760ec03837233f0", + "number": 944, + "title": "Research: classify signed 3x3 connector obstructions and a 14-query repair (no new kappa)" + }, + { + "head": "cf360b4b09b7d0419decdd6ac85421fefed55bdd", + "number": 943, + "title": "Research: sharp four/five-source dirty-connector boundary (no new kappa)" + }, + { + "head": "f3100aec6ce6a7b061987875d5e9a8b93801ac0b", + "number": 934, + "title": "Research: optimal 3x3 binary connector queries (no new kappa)" + }, + { + "head": "da2cd0dd2229e08b61b174a8835a2c2bb99d2230", + "number": 840, + "title": "Research: fuse native BIT dyadic shear pairs with three children (no new kappa)" + }, + { + "head": "613c02b8b4411f991f108dcc1481b3f9100b996f", + "number": 677, + "title": "Research note: restored DATA-shear boundaries for PR #521's native BIT query (exact query costs, no new \u03ba)" + }, + { + "head": "a190fdb39f31647fc6f651625353710624627348", + "number": 521, + "title": "Native BIT ADDRESS fusion: two recursive queries to one" + } + ], + "distinct_contribution": "Batch several PR840 pairs on the same target; prove the optimum within the target-only dyadic query alphabet. No duplicate identified in the inspected queue.", + "immediate_submit_refresh": { + "max_pr": 950, + "new_prs_since_full_refresh": [ + { + "head": "5bafe2c91e045d10de207b9e5b21630dfebb9cd2", + "number": 950, + "title": "Tooling: 1.61x faster exact historical central-factor audit (no new kappa)" + }, + { + "head": "102ddfb47d11c8ad66121350907d4a2cc04cea8c", + "number": 949, + "title": "Scoped negative result: exact 73-primitive factory scale optimum (no new kappa)" + }, + { + "head": "eb11543094825c193c4bccece4857601fcd1620a", + "number": 948, + "title": "Independent verification: symbolic PR479 chirp state transitions (no new kappa)" + } + ], + "pinned_issue": null, + "recent_open_count": 40 + }, + "max_pr": 947, + "open_pr_count": 700, + "pinned_coordination_issue": null, + "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/953", + "refreshed_main": "007664306fff84fbb1c9a1b4053b69f439764034", + "search_terms": [ + "dyadic query", + "dyadic shear", + "query batching", + "Laurent", + "native BIT", + "query pair", + "query-run", + "dyadic-run" + ], + "selected_record_sha256": "41fb066ff0f43ce472323195e9088d6d888715c13c54eae7b42e357ed5bfc726", + "selected_record_unchanged": true, + "verified_mathematical_commit": "282eff4d60bacfe1d0018bc08b22a2e1bf8d5928" +} diff --git a/research/dyadic-query-runs/README.md b/research/dyadic-query-runs/README.md new file mode 100644 index 0000000000..620b2e8021 --- /dev/null +++ b/research/dyadic-query-runs/README.md @@ -0,0 +1,72 @@ +# Optimal dyadic-run BIT query batching + +Batching centered native BIT shears on the same target removes repeated +ADDRESS-layout restoration boundaries. For a finite set J of dyadic indices, +with r indices in c consecutive runs, the completed batch uses **2r+c ordinary +recursive children instead of 3r**, with unchanged source, arbitrary dirty +spectators and no extra full private row. This count is optimal in the +specified target-query/source-XOR alphabet, including off-support excursions. + +**Status: recursive-interface research construction; no new kappa.** The +selected PR890 result and `upstream/` are unchanged. This is not a new supplier, +a general circuit lower bound, a measured speedup or a formal multiplication +theorem. The complete coefficient-aware work/space recurrence and inherited +obligations are in [PROOF.md](PROOF.md), especially sections 1, 3 and 5. + +OS assignment seed **55** selects `J={0,1,2,4,5}`. Its two runs give: + +| Complete cost item | Separate PR840 pairs | Shared runs | +|---|---:|---:| +| Full ordinary recursive children | 15 | 12 | +| Ordered affine events | 90 | 72 | +| Full source-XOR scans | 10 | 10 | +| Additional full private rows | 0 | 0 | + +Every query is lowered to six explicit affine events and one separately paid +child, including all layout return edges. Coefficient preparation and stream +costs differ; the count saving does not guarantee a finite runtime saving. +For three isolated indices `{0,2,4}`, the exact count is nine and this +mechanism saves nothing. Allowing nondyadic queries or a modulus-specific +program can beat the restricted count; both boundaries have concrete controls. + +From the repository root, with Python 3.9+ and the standard library: + +```sh +python3 -I -O -B research/dyadic-query-runs/verify.py +python3 -I -O -B research/dyadic-query-runs/test_package.py +``` + +Expected first lines: + +``` +PASS_DYADIC_QUERY_RUNS cases=63 seed=55 children=15->12 affines=90->72 XOR=10 +PASS_DYADIC_QUERY_RUNS_PACKAGE relocation=1 regeneration=2 corruptions=8 +``` + +The verifier imports no constructor or predecessor implementation. It checks +all 63 nonempty subsets of indices 0 through 5, exact Laurent endpoints, +native rational/modular columns, both full ADDRESS domains modulo 3 and 5 +with two intervening binary spectator fields, and 252 dirty forward plus +252 inverse executions. A separate bounded shortest-walk census admits +off-support visits for all 15 nonempty subsets of indices 0 through 3. +Its finite coverage is distinct from the written universal proof. Fifteen +obligation-specific rejection controls and two positive scope controls pass. + +[CERTIFICATE.json](CERTIFICATE.json) contains every literal word, baseline, +native lowering and recounted invoice. [EVIDENCE.json](EVIDENCE.json) contains +the deterministic complete receipt. `build.py` regenerates only this package's +certificate; `verify.py --write-evidence` regenerates its receipt. Ordinary +verification is read-only. [SOURCES.json](SOURCES.json) pins the base, retained +predecessors and inspected PR heads; [VALIDATION.md](VALIDATION.md) records +executed checks and limits; [CLAIM.md](CLAIM.md) records selection and handoff. + +Exact base: `47481c89fd30a43f8f882eb4b391e89c29273fd0`. Direct predecessor: +[PR840](https://github.com/CrocSwap/integer-mult-bounds/pull/840) at +`da2cd0dd2229e08b61b174a8835a2c2bb99d2230`. The new result batches several of +its centered pairs, rather than reproving the single-pair theorem. It does +not consume or combine the dirty connector results in PR889/934/943/944. + +Prepared by **Ross Richardson (@RossRichardson)** with substantial **OpenAI +Codex assistance**, under Apache-2.0. Credit Wentao Li/PR840, Karl Appel/PR521, +commdata2338/PR677 and the retained OpenAI tape framework. Full attribution, +original notices and source licenses are in [NOTICE.md](NOTICE.md) and `vendor/`. diff --git a/research/dyadic-query-runs/SOURCES.json b/research/dyadic-query-runs/SOURCES.json new file mode 100644 index 0000000000..776d209482 --- /dev/null +++ b/research/dyadic-query-runs/SOURCES.json @@ -0,0 +1,185 @@ +{ + "assignment_seed": 55, + "base_commit": "47481c89fd30a43f8f882eb4b391e89c29273fd0", + "base_context": [ + { + "commit": "47481c89fd30a43f8f882eb4b391e89c29273fd0", + "path": "certificates/selected-result.json", + "sha256": "41fb066ff0f43ce472323195e9088d6d888715c13c54eae7b42e357ed5bfc726" + }, + { + "commit": "47481c89fd30a43f8f882eb4b391e89c29273fd0", + "path": "docs/research/current-status.md", + "sha256": "bc18a48072b15aa66b036df5901c0c209478458a39a650f1b514762ace3088ad" + }, + { + "commit": "47481c89fd30a43f8f882eb4b391e89c29273fd0", + "path": "docs/research/pr-ledger.md", + "sha256": "24d1b69d88b1975e32a3aebc08bba4970ca9c2f5b3e027889aee3a30188108bc" + }, + { + "commit": "47481c89fd30a43f8f882eb4b391e89c29273fd0", + "path": "docs/research/community-frontier890-review.md", + "sha256": "cd03b7c2c6c09db2cfa89ae40133ae44e1deb6e32ec5ddd23aacecc9c50f2fea" + }, + { + "commit": "47481c89fd30a43f8f882eb4b391e89c29273fd0", + "path": "research/complex-t21-owners/PROOF.md", + "sha256": "78721b32fceb34b21b8e77c95381c38c60276e72e6d9c2e9c6262cb347457def" + }, + { + "commit": "47481c89fd30a43f8f882eb4b391e89c29273fd0", + "path": "research/community-frontier890-audit/ASSEMBLY.json", + "sha256": "190110b509dc87d38b72ad37c3290efcc245ce26df4cae3d7e2d6dcf0bac2c43" + }, + { + "commit": "47481c89fd30a43f8f882eb4b391e89c29273fd0", + "path": "docs/research/community-round4-review.md", + "sha256": "8311c6aa2f4fa6ee6c99434c75e16e60b08533d065f65dcfcbdf88eab1c7a48d" + }, + { + "commit": "47481c89fd30a43f8f882eb4b391e89c29273fd0", + "path": "research/experiment-log/negative-searches/results.json", + "sha256": "8d7662f8c2569ec0423fbf916f7951a69dc56864e8bc02aa1261144730221d3d" + } + ], + "format": "dyadic-query-runs-sources-v1", + "immutable_inputs": [ + { + "commit": "da2cd0dd2229e08b61b174a8835a2c2bb99d2230", + "git_blob": "aaba3e501de1f761c783ec7f0dc9307ef45ab5d7", + "local": "vendor/pr840-PROOF.md", + "path": "research/dyadic-query-pair/PROOF.md", + "sha256": "9a5ce93b866371189c797fbe8837c6a0bd22c5cf71ed84d60b9ae1c22a5ec83a" + }, + { + "commit": "da2cd0dd2229e08b61b174a8835a2c2bb99d2230", + "git_blob": "d58769de46f8580697b2d079bc7368789101ee21", + "local": "vendor/pr840-NOTICE.md", + "path": "research/dyadic-query-pair/NOTICE.md", + "sha256": "7fe86c785bc9862577ee1cc359096bc8c2606c1d70c357a46339eee28c89643e" + }, + { + "commit": "da2cd0dd2229e08b61b174a8835a2c2bb99d2230", + "git_blob": "d535b797d18e86ef5688201d70f91fa308bb6647", + "local": "vendor/pr840-SOURCES.json", + "path": "research/dyadic-query-pair/SOURCES.json", + "sha256": "c67d77a86031af189ea145556e65cc379f25bb285407bfcf7c67b711f7ce1694" + }, + { + "commit": "da2cd0dd2229e08b61b174a8835a2c2bb99d2230", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", + "local": "vendor/pr840-LICENSE", + "path": "research/dyadic-query-pair/LICENSE", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4" + }, + { + "commit": "da2cd0dd2229e08b61b174a8835a2c2bb99d2230", + "git_blob": "c3f67fc807aa3bf32ba559d51ea0b7e7a424229d", + "local": "vendor/pr521-PROOF.md", + "path": "research/dyadic-query-pair/vendor/pr521-PROOF.md", + "sha256": "320ce5529c1543f9e6fceb9e7f8b563ed332f13923229e38d4e7edac98f30283" + }, + { + "commit": "da2cd0dd2229e08b61b174a8835a2c2bb99d2230", + "git_blob": "549b87c2d57eb00296301c90e090d2f49d475a57", + "local": "vendor/pr521-SOURCE-PINS.json", + "path": "research/dyadic-query-pair/vendor/pr521-SOURCE-PINS.json", + "sha256": "34f97e7a31deed0dd85474ece3709a55de495f9473a3619f84e991fdbd3bf732" + }, + { + "commit": "da2cd0dd2229e08b61b174a8835a2c2bb99d2230", + "git_blob": "47d9bf59a3e0d85bcc4930cd76a3d21a1e43c2fc", + "local": "vendor/pr677-PROOF.md", + "path": "research/dyadic-query-pair/vendor/pr677-PROOF.md", + "sha256": "4f281eb48b9662c03269717b3919b45b27f7c2655abb185249a1eea2a03af186" + }, + { + "commit": "da2cd0dd2229e08b61b174a8835a2c2bb99d2230", + "git_blob": "bbd90a76bb1f3c55393367e24afd9970b796dba2", + "local": "vendor/pr677-NOTICE.md", + "path": "research/dyadic-query-pair/vendor/pr677-NOTICE.md", + "sha256": "d79071e9dda5edc60305f80910572c1a61daf0b4601f5673b5ff874a6d487742" + }, + { + "commit": "da2cd0dd2229e08b61b174a8835a2c2bb99d2230", + "git_blob": "088fceea1867abc76271d7efe7532b779fee9039", + "local": "vendor/upstream-02-streams.tex", + "path": "research/dyadic-query-pair/vendor/upstream-02-streams.tex", + "sha256": "606c80db61cad13aa0c3b6060dc4b88dbbe7ac60cdd831aa93f28d908fd09dab" + }, + { + "commit": "da2cd0dd2229e08b61b174a8835a2c2bb99d2230", + "git_blob": "951e792b1768e6509561380b8bbfb1d1ccb64c08", + "local": "vendor/upstream-04-swap.tex", + "path": "research/dyadic-query-pair/vendor/upstream-04-swap.tex", + "sha256": "412b170ccaab38dba96e95e3cbfae09f4876a9818f8d278776a746b0f8044906" + }, + { + "commit": "da2cd0dd2229e08b61b174a8835a2c2bb99d2230", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", + "local": "vendor/upstream-LICENSE", + "path": "research/dyadic-query-pair/vendor/upstream-LICENSE", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4" + } + ], + "inspected_prs": [ + { + "head": "cf360b4b09b7d0419decdd6ac85421fefed55bdd", + "number": 943, + "title": "Research: sharp four/five-source dirty-connector boundary (no new kappa)" + }, + { + "head": "fccac36fa9bcc063c4fda733299a22349ce10e56", + "number": 940, + "title": "Research audit: exact scope of retained Fourier layout cancellation (no new kappa)" + }, + { + "head": "df645942469e6a739ec94010a6068c398f4a6c86", + "number": 938, + "title": "Independent verification: complete minimum-word census for dirty fanout stars (no new kappa)" + }, + { + "head": "f3100aec6ce6a7b061987875d5e9a8b93801ac0b", + "number": 934, + "title": "Research: optimal 3x3 binary connector queries (no new kappa)" + }, + { + "head": "85a1d11adbbd7610d269cfeb3e477cf7d457f2eb", + "number": 929, + "title": "Research: four grouped cyclic inverse calls with one dirty connector (no new kappa)" + }, + { + "head": "e2021d1c9e06948528cbc0a8fd7079b671da981d", + "number": 889, + "title": "Research: batch common-factor product shears with dirty restoration" + }, + { + "head": "da2cd0dd2229e08b61b174a8835a2c2bb99d2230", + "number": 840, + "title": "Research: fuse native BIT dyadic shear pairs with three children (no new kappa)" + }, + { + "head": "ff8251519e009a01ede6b27e3f5af703eaa70132", + "number": 788, + "title": "Research: reusable clean checkpoint lowers weighted binary leaf bill 20 to 16 (no new kappa)" + }, + { + "head": "efad8a40094ab453c0525efef0b0eff2a5d8b850", + "number": 714, + "title": "Research: optimal clean root checkpoint saves 25\u201340% of binary product-shear calls" + }, + { + "head": "613c02b8b4411f991f108dcc1481b3f9100b996f", + "number": 677, + "title": "Research note: restored DATA-shear boundaries for PR #521's native BIT query (exact query costs, no new \u03ba)" + }, + { + "head": "a190fdb39f31647fc6f651625353710624627348", + "number": 521, + "title": "Native BIT ADDRESS fusion: two recursive queries to one" + } + ], + "pinned_issue": null, + "repository": "CrocSwap/integer-mult-bounds" +} diff --git a/research/dyadic-query-runs/VALIDATION.md b/research/dyadic-query-runs/VALIDATION.md new file mode 100644 index 0000000000..07bd093554 --- /dev/null +++ b/research/dyadic-query-runs/VALIDATION.md @@ -0,0 +1,105 @@ +# Validation and limits + +Executed on macOS arm64 on **2026-10-14 AEDT**, with CPython **3.14.6** and +**3.9.6**. The program and mathematical certificate are identical across +interpreters. No Linux, hosted-CI or proof-assistant result is claimed. + +## Focused checks + +The normal 3.14.6 run generated the complete receipt. Isolated optimized +execution verified it unchanged on both interpreters: + +```sh +python3 -I -O -B research/dyadic-query-runs/verify.py +/usr/bin/python3 -I -O -B research/dyadic-query-runs/verify.py +python3 -I -O -B research/dyadic-query-runs/test_package.py +``` + +- All **63** declared nonempty index sets pass literal forward/inverse + Laurent replay, the independently reconstructed graph-component bound + and both complete native invoices. Their fused query counts total **496** + versus **576** for the separate-pair baseline. These are finite census + totals, not an asymptotic or runtime measure. +- All **14** signed native query lowerings pass **84 rational** and **756 + modular** basis columns, literal inverse checks and ordered/unit admission. + Modular checks use 3, 5, 7, 9, 15, 25, 27, 49 and 81; modulus 15 is an + additional non-prime-power odd-ring control. +- **228,956** native address comparisons cover the complete six-field + domains modulo 3 and 5. Each is lifted over all four configurations of + two physically intervening binary spectator fields. The VALUE replay + includes three arbitrary dirty roles, **252 forward** and **252 inverse** + executions. Its complete deterministic output digest is in EVIDENCE.json. +- The independent finite shortest-walk traversal exhausts **15,616 states** + and **156,672 directed edges**, with position restricted to `[-32,32]` and + dyadic steps at most 64. All **15** nonempty subsets of indices 0 through + 3 match the theorem. This finite traversal is not the unbounded proof. +- **15** obligation-specific rejection controls and **two positive scope + controls** distinguish wrong endpoints, invalid operations, unpaid work, + legal nonoptimal words, nondyadic shortcuts and small-modulus cancellation. +- The package test passes standalone relocation in a path with spaces, + byte-exact certificate/evidence regeneration and **eight on-disk faults**. + It checks the expected failure reason, not just a nonzero exit code. +- Every retained source's SHA256 and Git blob digest agrees. All seven + transitive original source files also match their fetched original Git + objects at the commits recorded in `vendor/pr840-SOURCES.json`. + +The explicit stopping rule was completion of the declared certificate and +bounded-walk domains; neither used adaptive search. The assignment seed 55 +selects the five-index example and deterministic dirty inputs. The universal +query optimum is the written argument in PROOF.md, not an extrapolation of +this finite evidence or a machine-checked theorem. + +## Repository context + +Exact development base: `47481c89fd30a43f8f882eb4b391e89c29273fd0`. + +```sh +make selected-record-check +python3 -B -m unittest discover -s tests -p 'test_selected_result.py' +git diff --check +``` + +The selected-record check and all **five** existing selected-result tests pass. +The selected certificate still records PR890 at +`1661957774647029/1000000000000000000`. Only this new research directory is +added; existing sources, `upstream/` and the selected frontier are unchanged. + +Publication refresh reached main +`007664306fff84fbb1c9a1b4053b69f439764034`: its eighteen-contribution batch +does not change the selected record. The refreshed queue contains 700 open +PRs through #947; the closest dependency PR840 remains at the exact consumed +head. Its current discussion has no review or comment introducing a changed +contract. PUBLICATION-CONTEXT.json records the overlap scope and heads. +The immediate pre-submission refresh checked 40 recent open PRs through #950 +and again found no pinned coordination issue. The complete optimized replay +and selected-record/five-test checks pass at mathematical commit +`282eff4d60bacfe1d0018bc08b22a2e1bf8d5928`. The subsequent claim/publication +update changes documentation and context metadata only. + +The required root `make verify` was launched once in an untouched archive of +the exact base, so unrelated regeneration cannot enter this contribution. +Six historical groups completed: community, producers, partial-gauge, +three-stage-cover, paired-cube and recycled-bit. The recycled-bit replay also +passed its three tests. The run was deliberately terminated during the next +entrance-bank group (exit 143) after a direct check of the later mandatory +`make gen4-bank-verify` target established its missing dependency: + +``` +ModuleNotFoundError: No module named 'sympy' +make: *** [gen4-bank-verify] Error 1 +``` + +That direct gate exited 2. Its selected-record prerequisite passed. The +interpreter also lacks NumPy/SciPy, but no further missing-dependency failure +is inferred. The root suite is **incomplete**, not passed; no dependency +installation or further repository-wide replay was attempted. The standalone +contribution requires only the standard library and its complete checks pass. + +## Remaining obligations + +No selected-supplier cold replay is claimed, because no selected construction +is changed. No physical selected-supplier integration, common-label compiler, +new frame/owner invoice, bit-precision theorem, all-size tape implementation, +outer analytic improvement or measured runtime is established. The actual +ordinary child and ordered affine stream implementations remain inherited +contracts. Coefficient-dependent work is kept explicit in the recurrence. diff --git a/research/dyadic-query-runs/build.py b/research/dyadic-query-runs/build.py new file mode 100644 index 0000000000..44e8ca7357 --- /dev/null +++ b/research/dyadic-query-runs/build.py @@ -0,0 +1,97 @@ +#!/usr/bin/env python3 +"""Emit the finite dyadic-run schedules; verification is in a separate file.""" +from fractions import Fraction +from pathlib import Path +import json + +ROOT = Path(__file__).resolve().parent + + +def runs(indices): + out = [] + for j in indices: + if out and out[-1][-1] + 1 == j: + out[-1].append(j) + else: + out.append([j]) + return out + + +def schedule(indices): + word = [] + for run in runs(indices): + vertices = [-(1 << j) for j in reversed(run)] + [1 << j for j in run] + previous = 0 + for vertex in vertices: + word.extend([vertex - previous, "X"]) + previous = vertex + word.append(-previous) + return word + + +def lowering(k): + a = Fraction(k, 4) + + def affine(target, diagonal, controls): + return ["A", target, str(diagonal), [[i, str(v)] for i, v in controls]] + + return [ + affine(2, 1, [(0, -1)]), + affine(3, 1, [(0, 1)]), + affine(5, a, [(0, 1+a), (2, -a), (3, -a)]), + ["C", 0, 5], + affine(2, 1, [(0, 1)]), + affine(3, 1, [(0, -1)]), + affine(5, -1/a, [(0, 1/a-1), (2, 1), (3, 1)]), + ] + + +def invoice(word): + powers = sorted(set(k for k in word if type(k) is int)) + queries = sum(type(k) is int for k in word) + return {"children": queries, "affines": 6*queries, + "xor_scans": word.count("X"), + "query_multiplicities": {str(k): word.count(k) for k in powers}} + + +def certificate(): + cases = [] + for mask in range(1, 64): + indices = [j for j in range(6) if mask & (1 << j)] + fused = schedule(indices) + baseline = [op for j in indices for op in [-(1 << j), "X", 2 << j, "X", -(1 << j)]] + cases.append({"mask": mask, "indices": indices, "word": fused, + "baseline": baseline, "invoice": invoice(fused), + "baseline_invoice": invoice(baseline)}) + powers = {k for case in cases for name in ["word", "baseline"] + for k in case[name] if type(k) is int} + powers |= {-k for k in powers} + return {"format": "dyadic-query-runs-v1", "assignment_seed": 55, + "domain": {"indices": list(range(6)), "masks": [1, 63]}, + "instruction_format": "integer k: Q(k) on target; X: target XOR source", + "cases": cases, + "lowerings": {str(k): lowering(k) for k in sorted(powers)}} + + +def encode(data): + # One case per line keeps the literal finite schedule easy to inspect. + compact = lambda x: json.dumps(x, sort_keys=True) + lines = ["{"] + for key in sorted(set(data) - {"cases", "lowerings"}): + lines.append(" " + compact(key) + ": " + compact(data[key]) + ",") + lines.append(' "cases": [') + lines.extend(" " + compact(case) + ("," if i+1 < len(data["cases"]) else "") + for i, case in enumerate(data["cases"])) + lines.append(" ],") + lines.append(' "lowerings": {') + items = list(data["lowerings"].items()) + lines.extend(" " + compact(key) + ": " + compact(value) + + ("," if i+1 < len(items) else "") + for i, (key, value) in enumerate(items)) + lines.extend([" }", "}"]) + return "\n".join(lines) + "\n" + + +if __name__ == "__main__": + (ROOT / "CERTIFICATE.json").write_text(encode(certificate()), encoding="utf-8") + print("WROTE_DYADIC_QUERY_RUNS cases=63 seed=55") diff --git a/research/dyadic-query-runs/test_package.py b/research/dyadic-query-runs/test_package.py new file mode 100644 index 0000000000..67c59b72b5 --- /dev/null +++ b/research/dyadic-query-runs/test_package.py @@ -0,0 +1,75 @@ +#!/usr/bin/env python3 +"""Relocate, regenerate and corrupt disposable copies of the complete package.""" +from pathlib import Path +import json +import shutil +import subprocess +import sys +import tempfile + +ROOT = Path(__file__).resolve().parent + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def run(root, script, *args): + return subprocess.run([sys.executable, "-I", "-O", "-B", str(root/script), *args], + cwd=root.parent, capture_output=True, text=True, timeout=120) + + +def edit_json(path, change): + data = json.loads(path.read_text()) + change(data) + path.write_text(json.dumps(data)) + + +def main(): + with tempfile.TemporaryDirectory(prefix="dyadic runs package ") as tmp: + root = Path(tmp)/"offline package with spaces" + shutil.copytree(ROOT, root, ignore=shutil.ignore_patterns("__pycache__")) + certificate = (root/"CERTIFICATE.json").read_bytes() + evidence = (root/"EVIDENCE.json").read_bytes() + result = run(root, "build.py") + need(result.returncode == 0 and (root/"CERTIFICATE.json").read_bytes() == certificate, + "exact certificate regeneration: " + result.stderr) + result = run(root, "verify.py") + need(result.returncode == 0 and "PASS_DYADIC_QUERY_RUNS" in result.stdout, + "isolated relocated replay: " + result.stderr) + result = run(root, "verify.py", "--write-evidence") + need(result.returncode == 0 and (root/"EVIDENCE.json").read_bytes() == evidence, + "complete evidence regeneration: " + result.stderr) + faults = [ + ("source", "SOURCES.json", lambda d: d["immutable_inputs"][0].update(sha256="0"*64), + "source SHA256"), + ("return", "CERTIFICATE.json", lambda d: d["cases"][54]["word"].pop(), + "Laurent endpoint/restoration"), + ("unpaid child", "CERTIFICATE.json", lambda d: d["cases"][54]["invoice"].update(children=11), + "literal complete invoice"), + ("removed child", "CERTIFICATE.json", lambda d: d["lowerings"]["1"].pop(3), + "six affines and one paid child"), + ("missing case", "CERTIFICATE.json", lambda d: d["cases"].pop(), + "every declared mask once"), + ("bool count", "CERTIFICATE.json", lambda d: d["cases"][0]["invoice"]["query_multiplicities"].update({"2": True}), + "multiplicity integer type"), + ("nonoptimal", "CERTIFICATE.json", lambda d: d["cases"][54].update( + word=d["cases"][54]["baseline"], invoice=d["cases"][54]["baseline_invoice"]), + "graph lower bound attained"), + ("receipt", "EVIDENCE.json", lambda d: d.update(all_cases_fused_queries=495), + "complete evidence receipt mismatch"), + ] + for name, filename, change, error in faults: + path = root/filename + old = path.read_bytes() + edit_json(path, change) + result = run(root, "verify.py") + need(result.returncode != 0 and error in result.stderr, + "fault did not reject for the expected obligation: " + name + "\n" + result.stderr) + path.write_bytes(old) + print("PASS_DYADIC_QUERY_RUNS_PACKAGE relocation=1 regeneration=2 corruptions=8") + + +if __name__ == "__main__": + main() diff --git a/research/dyadic-query-runs/vendor/pr521-PROOF.md b/research/dyadic-query-runs/vendor/pr521-PROOF.md new file mode 100644 index 0000000000..c3f67fc807 --- /dev/null +++ b/research/dyadic-query-runs/vendor/pr521-PROOF.md @@ -0,0 +1,183 @@ +# Exact local fusion and paid implementation + +The tape-operation premises come from the original +[ordered affine streams lemma](https://github.com/CrocSwap/integer-mult-bounds/blob/5996e33ecad6a0ccd578aec58831457829d75575/upstream/build/sections/02-streams.tex) +and [address interchange construction](https://github.com/CrocSwap/integer-mult-bounds/blob/5996e33ecad6a0ccd578aec58831457829d75575/upstream/build/sections/04-swap.tex) +of CrocSwap/integer-mult-bounds, pinned at the displayed revision. +The general rank-one lowering, selected unipotent operator and dirty +shared-chart fusion in this packet are a separate contribution. +Source pins distinguish that contribution from the borrowed tape contracts. + +## ADDRESS operator + +Use six physically ordered fields `(H0,H1,H2,D0,D1,D2)`, each of width +`b=N/3`. Each coordinate lies in the true residue ring `Z/(ell^b)`, where +ell is any odd prime. Unnamed ADDRESS fields may occur between or outside +these fields and remain spectators. Set + +``` +u = (1,0,1), t = (1,0,-1), t^T u = 0, +g = I3 + (1/2) u t^T, +g^-1 = I3 - (1/2) u t^T, +s = (u,-u), r = (t,-t), +Phi(g) = I6 + (1/4) s r^T. +``` + +The lift preserves H+D and applies g to H-D; H1 and D1 are fixed. +Since `(u t^T)^2=0`, the displayed inverse is exact. The map is not an +involution over the rationals or any odd residue ring. These are rational +ADDRESS operations specializing to residue rings, not signed arithmetic +on stored VALUE bits. + +The following chronological seven-event word equals Phi(g): + +``` +z2 <- z2-z0 +z3 <- z3+z0 +z5 <- (z5+5*z0-z2-z3)/4 +CHILD_C(0,5) +z2 <- z2+z0 +z3 <- z3-z0 +z5 <- -4*z5+3*z0+z2+z3 +``` + +Every affine control precedes its target. `CHILD_C(0,5)` is one ordinary +recursive interchange of the selected equal-width fields on the COMPLETE +private BIT stream; it preserves all other ADDRESS fields. It is a +contract invocation, not an implementation of the recursive supplier in +this packet. The affine operations use the original ordered-stream +contract, including its work tapes and head returns. Subject to those +contracts and their row/stack hypotheses, this is a fixed all-b local +implementation with six affine scans, one child and O(V) additional work. +There is no exponential array enumeration in the implementation. + +For completeness, the lowering formula is independently checked. For +`M=I+s v^T`, let `D=1+v^T s` and `a=s0*vlast`, both nonzero. Subtract +`(si/s0)z0` from each middle coordinate. Then set + +``` +zlast <- a*zlast+(D-slast*vlast)*z0+sum_middle s0*vi*zi, +swap(z0,zlast), +zi <- zi+(si/s0)*z0 for each middle coordinate, +zlast <- (-D/a)*zlast+((D-s0*v0)/a)*z0 + -sum_middle (vi/vlast)*zi. +``` + +Substitution gives M on every input coordinate. Here `v=r/4`, D=1 and +a=1/4, and only middle indices 2 and 3 need updates. Thus the formula +emits exactly the word above. The checker derives it afresh and verifies +its rational matrix. The literal reverse inverts each affine unit and +uses the same involutive child; its matrix is Phi(g^-1), not Phi(g). + +The denominators and affine diagonal numerators exclude only prime 2. +For example, a control coefficient vanishing modulo 5 does not make a +diagonal singular. This proves specialization for every odd ell and b, +including composite rings such as Z/25 and Z/49. Removing only the child +while retaining the affine wrappers changes the operator. + +## Exact comparison and native dirty chart + +Let `P=u*(1/2,0,1/2)` and `Q=u*(3/4,0,1/4)` denote outer products. +Both row pairings with u are 1, so P and Q are idempotents; Q need not be +orthogonal. Write `R_P=I-2P` and `R_Q=I-2Q`. Since PQ=Q, + +``` +R_P R_Q = I+2(Q-P) = g. +``` + +Chronologically apply Q first, then P. `PROGRAM.json` gives a separate +six-affine/one-child word for each lifted reflection. Their full matrix +product, including spectator coordinates, equals the fused word. + +For three genuine BIT DATA rows `(x1,x2,x3)` and retained private row q, +all with the same full ADDRESS domain, use this fixed chart: + +``` +q XOR= x2 +x1 XOR= q +h(q) # array permutation induced by Phi(h) +x1 XOR= q +q XOR= x2 +``` + +Write its complete linear BIT operator as H(h). Its endpoint on arbitrary +dirty inputs is + +``` +x1' = x1 XOR q XOR x2 XOR h(q) XOR h(x2), +q' = h(q) XOR x2 XOR h(x2), +x2' = x2, x3' = x3. +``` + +Equivalently, with `E=(e1+eq)(e2^T+eq^T)` over F2, E^2=E and +`H(h)=I+E tensor(h-I)`. Hence H(h2)H(h1)=H(h2 h1) for arbitrary arrays, +and in particular `H(R_P)H(R_Q)=H(g)`, including arbitrary initial q. +This proof does not assume a clean private row. There is no F9 codec, +padding promise or signed integer VALUE lift. + +The adjacent decoder and encoder in the specified two-reflection baseline +cancel exactly. That baseline already has FOUR XOR scans around its two +ADDRESS queries. The fused word also has four. The verified improvement +is two specified recursive children reduced to one; there is no separate +XOR saving. Twelve baseline affine events is its literal serialized +count before possible affine simplification. Neither affine nor child +optimality is claimed against other possible implementations. + +## Orientation, spectators and recovery controls + +For modulus m=ell^b and seed e_H0, the orbit is +`z_k=e_H0+(k/4)s`, indexed by Z/m. It has exactly m points because 1/4 +and a component of s are units. Phi(g) pushes address index k to k+1; +its array permutation reads old VALUE index k-1. The inverse reads k+1. +The reflection address maps are Q: `k -> -3-k` and P: `k -> -2-k`. +Their chronological composition pushes k to k+1, as required. + +The checker applies the actual words to these actual addresses at m=5, +25,7,49. It verifies all six ADDRESS basis columns and unchanged exterior +spectators, as well as H1/D1. On these orbits it checks all 4m dirty BIT +basis columns, 344 total, plus m VALUE spectator columns, 86 total. Each +dirty column agrees with the formula, the full two-stage word and the +chart-cancelled baseline; the literal inverse restores its input. +BIT linearity gives all assignments on each tested orbit, while the +algebraic operator identity above covers arbitrary arrays on the full +ADDRESS domain. Fixed points and their 16 four-role BIT assignments are +also checked. Replacing the WHOLE query by identity gives H(I)=I; +this differs from removing only the recursive child. + +At m=5 start with x2 a delta at index 0 and x1=x3=q=0. The forward module +gives `x1=q=[1,1,0,0,0]`. Its proper retained-q inverse restores all rows. +If q is wiped first, that inverse instead gives +`x1=[0,1,0,0,1]`, `q=[1,0,0,0,1]`: DATA is lost. Using g again as the +inverse also fails. These are explicit negative controls, not a claim +that private state can be reset between uses. + +## Paid state and limits + +Take V as the productive volume of the three genuine DATA streams. +Private q has full volume V/3, including all spectator ADDRESS ranges. +Persistent stock is 4V/3 before evaluator routing, parking, work-tape or +recursion scratch. Initially zeroing fresh q costs V/3. Each fused module +pays one separate child of actual volume V/3 and width N/3, six ordered +ADDRESS affine events, four native XOR scans, setup and head-return work. +The specified cancelled baseline pays two such children and the same +four XOR scans. Each actual separate child call must remain separately +charged in a future supplier recurrence. + +The component identity is valid with dirty q, but an enclosing DATA +construction starting from clean q must allocate and initialize it. +Its state is retained through every future use and recovery. A once-only +final wipe costs V/3 and is eligible only after a separately verified +completed DATA endpoint and the last read of q. This unfinished module +boundary does not license that wipe. No DATA row is cleared for free. + +The half-integral g is outside an odd-denominator mod-4 generator grammar; +the old rho4 construction is undefined on it. This does not invalidate +that construction on its own alphabet and cannot be priced by extending +it without a new proof. + +The packet supplies one exact local query fusion. It does not produce a +complete three-DATA cyclic-interchange c word, a complex C supplier, a +common cover/owner schedule or an all-size weighted-row compiler. Those +missing endpoints and schedules, both suppliers, all separate calls, +movement, dirty recovery and paid stock must be verified before deriving +an integer-multiplication exponent. No kappa improvement is asserted. diff --git a/research/dyadic-query-runs/vendor/pr521-SOURCE-PINS.json b/research/dyadic-query-runs/vendor/pr521-SOURCE-PINS.json new file mode 100644 index 0000000000..549b87c2d5 --- /dev/null +++ b/research/dyadic-query-runs/vendor/pr521-SOURCE-PINS.json @@ -0,0 +1,31 @@ +{ + "public_contract_sources": [ + { + "repository": "CrocSwap/integer-mult-bounds", + "revision": "5996e33ecad6a0ccd578aec58831457829d75575", + "path": "upstream/build/sections/02-streams.tex", + "git_blob": "088fceea1867abc76271d7efe7532b779fee9039", + "sha256": "606c80db61cad13aa0c3b6060dc4b88dbbe7ac60cdd831aa93f28d908fd09dab", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/5996e33ecad6a0ccd578aec58831457829d75575/upstream/build/sections/02-streams.tex", + "used_contract": "Ordered affine streams with earlier controls, rational units, spectator fields and paid tape preparation/head returns." + }, + { + "repository": "CrocSwap/integer-mult-bounds", + "revision": "5996e33ecad6a0ccd578aec58831457829d75575", + "path": "upstream/build/sections/04-swap.tex", + "git_blob": "951e792b1768e6509561380b8bbfb1d1ccb64c08", + "sha256": "412b170ccaab38dba96e95e3cbfae09f4876a9818f8d278776a746b0f8044906", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/5996e33ecad6a0ccd578aec58831457829d75575/upstream/build/sections/04-swap.tex", + "used_contract": "One ordinary equal-width recursive ADDRESS interchange preserves spectators; each actual invocation is separately paid under its row/stack hypotheses." + } + ], + "source_readback": "Public source excerpts and exact Git blob identities read through the GitHub connector at the pinned revision; full SHA256 values independently match the local pinned source copies.", + "contribution": "Selected rational rank-one unipotent lowering and full-dirty native shared-chart fusion of the specified reflection pair; no complete supplier or exponent claim.", + "prior_exact_verification_provenance": { + "description": "Before this standalone extraction, separate exact algebra, physical-program and paid-cost checks agreed. The opaque hashes below identify that prior verification, but its internal files are neither distributed nor dependencies. This packet checks all admitted claims from its own public files.", + "independent_algebra_checkpoint_sha256": "4fa63459e3fc7b48daf1b6cbdbccbe5d09951da39e6805ce697a95455594e1b8", + "independent_fusion_gate_sha256": "2c47e97c62e169161b126e1faf4757759cf2b159f0d88e0e654ba9a6814c6d5e", + "physical_program_checkpoint_sha256": "408f22a6669ebad10f433c448cc01dcdac281177d35a4f7f82c7450c1066bd9d", + "paid_cost_checkpoint_sha256": "5532473f8094d6c0ddda273a865387c5b64582429e279face9ccf1e2ce27c628" + } +} diff --git a/research/dyadic-query-runs/vendor/pr677-NOTICE.md b/research/dyadic-query-runs/vendor/pr677-NOTICE.md new file mode 100644 index 0000000000..bbd90a76bb --- /dev/null +++ b/research/dyadic-query-runs/vendor/pr677-NOTICE.md @@ -0,0 +1,39 @@ +# Attribution, license, and scope + +New prose and checker code in this packet are contributed under the +repository's Apache-2.0 license. The repository's LICENSE and NOTICE remain +unchanged. Submitted by @commdata2338. Prepared with substantial AI assistance: +OpenAI Codex (GPT-6-Astra) wrote the analysis, proof and checker, and +Claude Code (Claude Opus 5.5) packaged the submission. No independent +human peer review is claimed. + +- **Karl Appel / applecrusher, PR #521**, head + `a190fdb39f31647fc6f651625353710624627348`: the rank-one unipotent ADDRESS + map, its seven-event lowering, the reflected-query comparison, and the + dirty shared-chart operator. The ADDRESS word in PROGRAM.json is an + attributed transcription. The completed shear contracts, two-query + classification, cost comparison and fresh checker are this contribution. +- **OpenAI #109 / the imported upstream framework**: ordered-affine streams, + complete-range ordinary ADDRESS interchange, tape/stack and head-return + contracts. The two original sources at revision + `5996e33ecad6a0ccd578aec58831457829d75575` match the files in this base; + exact URLs and SHA-256 values are recorded in SOURCES.json. Their licenses + and repository notices are retained, and their interfaces remain premises. +- **eumemic, PR #288**, head + `475a088b5862f75f0b10596cfd6842d19531a5ec`, and **Ali Romman, PR #468**, + the in-tree `research/bit-three-register-lower-bound` package: the binary + scalar-projector/group-algebra model used for other interchange targets. + This packet credits that model and does not repeat the nine-call search. +- **Joseph Demarest, PR #83**, head + `183077b7b3ae12e96eb3a87c1dc08023e6494dca`: the scoped fixed-menu adaptive + recursion barrier, inspected when selecting this task. We do not claim + that rescheduling complete supplier profiles changes their best exponent. +- The selected #626/#622/#623 construction, #543 bit supplier, and cumulative + community authors retain their attribution. Their selected artifacts are + neither changed nor re-certified by this local note. + +No priority claim is made for the elementary compute/uncompute identities, +matrix determinant lemma, or Laurent-polynomial methods. The useful output +is the pinned component's explicit restored-boundary alternatives, their +precise model restrictions and paid recurrence, and exact reproducible +evidence for review. diff --git a/research/dyadic-query-runs/vendor/pr677-PROOF.md b/research/dyadic-query-runs/vendor/pr677-PROOF.md new file mode 100644 index 0000000000..47d9bf59a3 --- /dev/null +++ b/research/dyadic-query-runs/vendor/pr677-PROOF.md @@ -0,0 +1,383 @@ +# Restored boundaries for one native unipotent BIT query + +This is a local interface result, conditional on the cited ordinary ADDRESS +interchange and ordered-stream primitives. It supplies no complete interchange +supplier and no multiplication exponent. The algebra below proves the stated +identities and scoped query bounds; the finite checker is corroboration, not a +formal proof of a full multiplication theorem. + +## 1. Object, predecessor, and boundary contracts + +Karl Appel / applecrusher's [PR #521](https://github.com/CrocSwap/integer-mult-bounds/pull/521), +pinned at `a190fdb39f31647fc6f651625353710624627348`, replaces two particular +reflected queries by one unipotent query. Its complete dirty operator retains +a private BIT row. It explicitly does not complete a DATA interchange or +authorize erasure of that row at an unfinished boundary. Its result is not +contradicted here. + +We choose a different, modest completed endpoint. For three genuine DATA rows +`(x,y,z)` and one fixed ADDRESS permutation `h`, let + + S_h(x,y,z) = (x + (h+I)y, y, z). (1) + +All VALUE additions in this note are XOR, over F2. ADDRESS arithmetic below +is rational arithmetic specialized to odd prime-power residue rings; these +two coefficient systems must not be conflated. Equation (1) is a shear, +not the three-DATA interchange. It satisfies `S_h^2 = I`, even though +`h^2 != I`. + +The contribution is an explicit comparison of three ways to complete (1): + +| Contract | Queries `h` or `h^-1` | Additional full row | Endpoint for that row | +|---|---:|---:|---| +| Query the DATA target | 2 | none | All other dirty rows untouched | +| Queries remain on one private row, with triangular source/target XORs | 4 | one | Arbitrary initial private contents restored | +| Caller owns disposable private storage | 1 | one | Explicit copy initialization and final zeroing | + +The first count is optimal in the fixed-`h` query/XOR model of section 4. +The second is optimal in the narrower private-row model of section 5 for +a uniform all-width program. These are **not** lower bounds for arbitrary +ordinary-interchange programs with different free ADDRESS operations. +The third changes the workspace contract: discarding someone else's dirty +row is not allowed. Its successful DATA endpoint makes its *own* final clear +legitimate. It is not evidence that clearing PR #521's private row is safe +inside an arbitrary surrounding construction. + +## 2. The retained query, with its actual recursive child + +Fix an odd prime `ell`, `b >= 1`, and `m = ell^b`. Use six ordered ADDRESS +fields `(H0,H1,H2,D0,D1,D2)`, all of width `b`, and all complete spectator +ranges. Define + + s = (1,0,1,-1,0,-1)^T, + r = (1,0,-1,-1,0,1)^T, + M = I6 + s r^T / 4, M^-1 = I6 - s r^T / 4. + +Here `r^T s = 0`. The permutation `h` moves the BIT at ADDRESS `a` to `M a`; +its action on values reads the inverse ADDRESS image. PR #521's literal +lowering, transcribed in `PROGRAM.json`, is + + a2 -= a0 + a3 += a0 + a5 = (a5 + 5*a0 - a2 - a3)/4 + CHILD_C(a0,a5) + a2 += a0 + a3 -= a0 + a5 = -4*a5 + 3*a0 + a2 + a3. (2) + +Substitution gives `M`. Reversing (2) and inverting each scalar event gives +`M^-1`. The child is an ordinary interchange of two `b`-digit ADDRESS fields +on the **entire selected BIT row**, including all other ADDRESS fields. +It is not a pointwise VALUE swap or an uncharged oracle. + +All six affine events read only earlier fields. Their diagonal numerators +and denominators are powers of two up to sign; denominators of controls are +also powers of two. Thus every event is well defined for every odd `ell`. +The cited ordered-stream lemma pays the finite coefficient preparation, +counter work, complete spectator scans, temporary work and head returns. +It does not assume unit-cost arithmetic on growing integers. + +The same implementation works on a DATA row or a private row: the ADDRESS +primitive's contract is for arbitrary BIT contents and is insensitive to +the role's name. Calls must be sequential and have exclusive access to the +queried row until its completed boundary. No source chart or current supplier +schedule is asserted to provide that permission automatically. + +For `a0 = e_H0`, the addresses `a_k = e_H0 + k*s/4`, `k in Z/m`, are distinct +and satisfy `M a_k = a_(k+1)`. Hence on their VALUE array, `(h y)_k = y_(k-1)`. +This supplies a nontrivial orbit of order `m`, as well as a direct finite +check on push/read orientation. There are also fixed points and shorter +orbits at nonunit initial scales; these are included in the replay. + +## 3. Three complete programs + +### 3.1 No full private row + +Apply, chronologically, + + x <- h^-1 x + x += y + x <- h x + x += y. (3) + +The output is `x + h y + y`; `y,z` and every unrelated row are untouched. +No row is assumed zero, copied, or erased. A pre-existing private row is +an untouched spectator. Source `y` is never modified, even temporarily. +The queried target may be permuted temporarily, so callers may not inspect +it between events. This is a restored boundary, not a concurrently readable +intermediate representation. + +### 3.2 Queries only on a restored dirty private row + +For arbitrary initial `q=q0`, use + + q += y + q <- h q + x += q + q <- h^-1 q + q += y + q <- h q + x += q + q <- h^-1 q + x += y. (4) + +The two contributions read into `x` are `h(q0+y)` and `h q0`. Their sum is +`h y`. The last XOR supplies `y`; both query/inverse pairs restore their +own input, and the two source XORs restore `q0`. Thus (4) implements (1) +on DATA and the identity on arbitrary private input. It has four queries +and five XORs, not four queries plus an implicit cleanup. + +### 3.3 An owned, disposable private row + +Allocate or reserve one owned full row `q`, whose incoming contents may be +discarded, and use + + q <- copy(y) + x += y + q <- h q + x += q + q <- 0. (5) + +The copy overwrites every private cell and pays source access and +initialization in one scan. Just before the last line, DATA already equals +(1), and `q=h y` is redundant with retained `y`. No later step reads `q`. +The final full-row clear therefore returns owned work storage to zero. +All five events are charged. There is no assumption that unknown dirty +caller state can be thrown away. + +Reapplying the *completed* program (5) implements `S_h^2=I` on DATA. This is +different from applying the inverse of PR #521's unfinished dirty module +after clearing its private row; that inverse generally fails. Both facts +are checked, including arbitrary DATA inputs and explicit private-input +rejection when (5) is falsely labeled a dirty-restoring program. + +The normal form of PR #521's dirty module is +`H(h)=I+E(h-I)`, `E=(e_x+e_q)(e_y+e_q)^T`. It directly explains the +tradeoff: for initial `q=0`, its DATA output is already (1), but its private +output is `(h+I)y`. Once (1) is declared and verified as the desired complete +endpoint, terminal operations needed solely for later dirty-module recovery +can be removed. Program (5) is the simpler paid copy implementation of that +completed endpoint. It changes neither the predecessor's two-reflection +identity nor its warning about other unfinished endpoints. + +## 4. Sharp two-query classification with arbitrary dirty spectators + +The model permits any number `d >= 2` of arbitrary dirty rows. Free algebraic +operations are invertible, address-independent XOR maps of the row roles; +actual implementations still pay for these scans. A query applies `h` or +`h^-1` to one row. No other nontrivial ADDRESS map, copying into clean storage, +or erasure is free in this lower-bound model. + +Represent `h` by `t`. Work over `F2[t,t^-1]`, or over +`F2[t,t^-1]/(t^m-1)` for an odd orbit length `m >= 3`. In the latter ring, +zero divisors cause no problem: the proof uses determinants and comparison +of distinct basis coefficients, not division or a fraction field. + +On an `m`-cycle, identify a BIT row with `sum_k value_k t^k`. The query is +multiplication by `t` on the regular module of the cyclic ring. Thus equality +of these row operators is equivalent to entrywise equality of their matrices +over that ring. The determinant below is taken **in this ring**, not the +ordinary F2 determinant of the expanded bit matrix. Restricting a complete +array to the full-order orbit in section 2 gives a necessary condition for +any claimed full-array identity. + +After conjugation by an invertible binary row map, one query is + + D_P(t^e) = I + (t^e-1) P, e in {+1,-1}, + P = u v^T, v^T u = 1. (6) + +These are precisely binary rank-one idempotents. Any arbitrary interleaving +of free XOR maps normalizes to a product of such factors: commute the +constant maps to the left, conjugating each projector as they pass. +At `t=1`, the desired endpoint is `I`, so the remaining constant factor +must be `I`. Thus allowing arbitrary endpoint XOR maps does not omit a +one-query or two-query solution from this model. + +Let `N=a b^T` be a nonzero rank-one nilpotent, `b^T a=0`; the desired shear is + + T_N(t) = I + (t-1) N. (7) + +The determinant lemma, valid over each stated commutative ring, gives +`det D_P(t^e)=t^e` and `det T_N(t)=1`. Zero queries cannot give the nonconstant +(7). One query has the wrong determinant. Two queries of the same sign also +have the wrong determinant, since `t^2 != 1` on an odd orbit of length at +least three. Therefore any two-query solution has opposite signs. + +For left sign `+1`, expand the product *in operator order*: + + D_P(t) D_Q(t^-1) + = I+P+Q + t(P+PQ) + t^-1(Q+PQ). (8) + +The coefficients of `1,t,t^-1` are independent in either ring, so (8) +equals (7) **if and only if** + + PQ=Q, P+Q=N. (9) + +For the other sign order the exact conditions are + + PQ=P, P+Q=N. (10) + +This is an exhaustive classification, not just a necessary filter. In (9), +the two rank-one images coincide and equal the image of `N`. Consequently + + P=a c^T, Q=a(c+b)^T, c^T a=1. (11) + +In (10), the two row spaces coincide and equal the row space of `N`, giving + + P=(c+a)b^T, Q=c b^T, b^T c=1. (12) + +Conversely, (11) or (12) directly verifies the corresponding conditions. +Over F2 there is no nontrivial scalar rescaling of a rank-one decomposition. +Each family has `2^(d-1)` choices, so every nonzero rank-one nilpotent target +has exactly `2^d` ordered, signed two-query factorizations. Program (3) +realizes one of them for `N=e_x e_y^T`, proving the two-query minimum. + +For any private index `q` distinct from `x,y`, all these factorizations have +`P_qq=Q_qq=0`: in (11) the image is `e_x`, and in (12) the row space is +`e_y^T`. This observation separates the unrestricted dirty-row model from +the private-only contract below. + +The scalar-projector/group-algebra method is established predecessor work: +eumemic's PR #288 and Ali Romman's in-tree `bit-three-register-lower-bound` +package (PR #468) use it for different diagonal interchange targets. We do +not claim that method as new. The present two-query classification targets +one off-diagonal restored shear and includes finite cyclic rings explicitly. + +## 5. Why the private-only dirty boundary costs four queries + +Here queries are restricted to `q`; the allowed pointwise gates are +`q += y`, `x += q`, and `x += y`. Source `y` and spectator rows remain +unchanged. A free-gate prefix has the triangular form + + K(x,y,q) = (x + a q + b y, y, q + c y). + +Both `K` and `K^-1` have `qq` entry one. A normalized query projector +`K^-1 e_q e_q^T K` therefore has `P_qq=1`. Section 4 shows that no +two-query factorization of (1) can have that property. A one-query program +is already excluded. A three-query program has determinant `t^j` for +`j in {-3,-1,1,3}`, so cannot have determinant one in the Laurent model, +or on an odd orbit of length at least five. Thus a uniform all-width +program needs at least four queries. Program (4) attains four. + +This proof does not assert a separate three-query exclusion for one isolated +order-three quotient from the determinant alone. The formal finite-word +check below is over Laurent coefficients, not modulo three. The uniform +claim has no gap: for example the actual order-eleven orbit already gives +the stated lower bound, and the program must work at that width too. + +Arbitrary XOR maps that swap a DATA role with `q`, arbitrary alternate +ADDRESS maps, non-restored private state, and clean/disposable storage are +outside this private-only restriction. Removing any of those restrictions +requires a new analysis; program (3) deliberately changes the first one. + +## 6. Complete typed costs and workspace + +Let each genuine DATA row have logical BIT volume `U`, including the full +ADDRESS domain and all spectators. Productive volume is `V=3U`, and nominal +chunk width is `N=3b`. Let: + +- `C(U,b)` be the cost of one ordinary interchange of the selected two + `b`-digit fields on a complete row of volume `U`, with restored child work; +- `A(U,b)` bound each fixed ordered-affine event of (2), including coefficient + preparation, its source access, temporary work, and head returns; +- `X(U)`, `P(U)`, and `Z(U)` bound one aligned XOR, full copy, and full clear; +- `R_j(V,b)` include row split/merge, routing to the fixed evaluator tapes, + descriptor setup, parking and recovery, allocation if needed, and head + returns not already charged in a primitive. Each `R_j=O(V)` under the + inherited complete-range, fixed-number-of-rows, and stack contract. + +The complete local recurrences/charges are + + S_data(V,3b) <= 2 C(U,b) + 12 A(U,b) + 2 X(U) + R_data(V,b), + S_dirty(V,3b) <= 4 C(U,b) + 24 A(U,b) + 5 X(U) + R_dirty(V,b), + S_owned(V,3b) <= C(U,b) + 6 A(U,b) + 2 X(U) + + P(U) + Z(U) + R_owned(V,b). (13) + +Every query is lowered using (2), so there are exactly 2, 4, and 1 ordinary +recursive children respectively, all of actual volume `V/3` and width `N/3`. +There is no dropped recovery child, additional live query, or implicit +source-copy oracle. All children run sequentially and reuse restored child +workspace. Primitive affine work may itself use temporary streams; those +are covered by `A`, not claimed absent by the phrase "no private row." + +Under the cited streaming contracts, the non-child terms of (13) are `O(V)`. +If `c(b)` uniformly bounds `C(U,b)/U`, then + + s_data(3b) <= (2/3)c(b) + O(1), + s_dirty(3b) <= (4/3)c(b) + O(1), + s_owned(3b) <= (1/3)c(b) + O(1). (14) + +The constants are independent of `b,U`, for a fixed permitted radix and +the fixed literal program. Fractions count the **actual child stream +volumes**, not the persistent stock. Persistent role storage is `V` for +(3), and `4V/3` for (4) and (5), before primitive/evaluator/recursive scratch. +For peak workspace, let `B_j(V,b)` include the fixed streaming and parking +workspace and `W_C(U,b)` child workspace. A safe bound is + + W_j(V,3b) <= persistent_j(V) + B_j(V,b) + W_C(U,b), + persistent_data=V, persistent_dirty=persistent_owned=4V/3. + +`B_j=O(V)` under the same tape primitives; the bound pays their temporary +streams and does not claim an exact number of physical tapes or total cells. +Private-row allocation is not normalized away. In the owned case the initial +copy and final clear are charged on every invocation, even if a later caller +could establish safe reuse. + +These are **typed** recurrences: the left side is a DATA shear and `C` is +ordinary ADDRESS interchange. Substituting `S_data` for `C` and solving a +self-recursion would be circular without a separate compiler. No such +compiler, arbitrary-width padding, common-frame schedule, or assembled +supplier is provided. For `N` not divisible by three this packet specifies +no reduction. The old all-size, row/stack, precision and analytic assumptions +are not discharged. In particular none of (13) or (14) is a new κ certificate. + +## 7. Reproducible evidence and exact limits + +`check.py --check` uses only Python's standard library and this directory. +It does not import the predecessor's checker or any supplier implementation. + +1. Enumerate all binary matrices at dimensions 2, 3 and 4; select rank-one + idempotents by independent rank and square tests; compare against the + outer-product catalogue. The sizes are 6, 28 and 120. +2. Multiply all **60,880 ordered signed pairs** as matrix Laurent polynomials. + Check (9)/(10) against the literal polynomial result for every pair and + every nonzero rank-one nilpotent target encountered. Every target has + `2^d` factorizations; none for a DATA coordinate shear has both private + diagonals one. +3. Exhaust all four native triangular charts + `(e_q+a e_x)(e_q+b e_y)^T`, `a,b in F2`, with both query signs, through + length four. The full **4,681-word** domain is completed: counts of + successes by length are `0,0,0,0,24`. This is a finite corroboration of + the specified model, not a search over arbitrary circuits or frames. +4. Verify (2) and its inverse on all rational ADDRESS basis columns and + modulo `3,9,27,11,121`, including two additional ADDRESS spectators. + Check full and shorter orbits from nonunit initial scales, plus fixed + points. These rings differ from PR #521's `5,25,7,49` replay. +5. Propagate all independent BIT basis columns simultaneously as distinct + integer bits, so every XOR-column cancellation is exact. Check all three + literal programs, their completed DATA involution, and the separate + owned-versus-dirty workspace contracts. No VALUE assignment is sampled. +6. Reject omissions of every recursive query, a wrong inverse, missing XORs, + missing owned initialization or clear, unpaid ADDRESS children, and the + false inference that owned clearing restores arbitrary dirty state. + A concrete order-two, same-sign factorization rejects extending the + opposite-sign classification to a domain where `t=t^-1`. + +The separate `full_domain_check.py` imports no main-checker code. It applies +the literal ADDRESS program to all **729 addresses in `(Z/3)^6`**, including +all 243 fixed addresses, and compares a separately written coordinate +formula. It then tracks individual sparse sets of nonzero BIT positions, +rather than packed symbolic columns, for **2,916 independent inputs per +program**. This covers every row and every address, not just a selected +orbit. Endpoints and completed inverses give **17,496 cases** across the +three programs. The private input is discarded only in the explicitly +owned-storage contract. This second finite method is included in the +single reproduction command. + +Assignment seed 57 selects candidate `57 mod 3 = 0` in `CLAIM.md`. The +algebraic domains and stopping rule above were fixed before implementing +the verifier; there is no random search whose losing trials are omitted. +The source pins and original attribution are in `SOURCES.json` and +`NOTICE.md`. `EXPECTED.json` records deterministic finite evidence. The +universal proof in sections 3–5 is a written argument open to review; +neither the exhaustive small-dimensional checks nor a PASS string replace it. diff --git a/research/dyadic-query-runs/vendor/pr840-LICENSE b/research/dyadic-query-runs/vendor/pr840-LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/dyadic-query-runs/vendor/pr840-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/dyadic-query-runs/vendor/pr840-NOTICE.md b/research/dyadic-query-runs/vendor/pr840-NOTICE.md new file mode 100644 index 0000000000..d58769de46 --- /dev/null +++ b/research/dyadic-query-runs/vendor/pr840-NOTICE.md @@ -0,0 +1,52 @@ +# Attribution, license and scope + +New compiler, checker, proof, certificate and documentation prepared for +**Wentao Li**, with substantial **OpenAI Codex (GPT-6.1 Sol) assistance** in +analysis, derivation, implementation, testing and writing. Contributor profiles: +[GitHub: VictorLiwentao](https://github.com/VictorLiwentao) and +[X: @Is__Victor](https://x.com/Is__Victor). Apache-2.0; the repository license +is copied unchanged to LICENSE. No sub-agents, independent human peer review, +proof-assistant verification or literature-priority claim. + +- **Karl Appel / applecrusher, PR521**, exact head + `a190fdb39f31647fc6f651625353710624627348`: native rank-one unipotent ADDRESS + map, one-child ordered lowering at k=1, shared-chart comparison and stated + tape premises. His proof and source-pin record are retained unchanged. +- **commdata2338, PR677**, exact head + `613c02b8b4411f991f108dcc1481b3f9100b996f`: completed first-difference DATA + shear, DATA-target querying permission, two-query model/classification, + private-storage distinctions and typed costs. The original proof and full + notice remain unchanged in vendor/. That notice retains the disclosed + OpenAI Codex / Claude Code assistance and predecessor attribution. Its + two-query first-difference theorem is preserved. +- **OpenAI, Integer multiplication below n log n, September 23, 2026**: + ordered affine streams, ordinary equal-width ADDRESS interchange, + complete spectators, tape/stack and head-return contracts. The two full + source sections and their Apache-2.0 license are copied byte for byte from + CrocSwap/integer-mult-bounds revision + `5996e33ecad6a0ccd578aec58831457829d75575`. Their source identity and the + imported framework maintained by **Douglas Colkitt** remain credited. +- The binary projector / group-algebra lineage is credited through PR677's + retained notice to **eumemic (PR288)** and **Ali Romman (PR468)**. No code + or nine-call search from those packages is imported here. +- Concurrent dirty/clean echo work by **FanPUYen, Sagar Thakrar, Ali Romman, + Koroffstrogov, Alexander Schwartzman and nightangelflowerwin-ops** was + inspected to avoid overlap. It is context, not a dependency. PR481's + Gaussian boundary batching by **Chafik Boukhalfa / chafreaky** was also + inspected and supplies no code or analytic claim here. +- Later context checks read **Jeremy Diviney / PR800** (formal Clifford + path valuations), **shhxera / PR822** (dirty connector reuse) and + **Paul Chan / PR829** (two clean checkpoints). Those objects and query/ + storage alphabets differ from this centered native ADDRESS shear. No + code, certificate or theorem from these three PRs is consumed. +- PR741 at the task base and the refreshed PR799 construction retain + their existing repository attribution. Their certificates, suppliers and + inherited conditions are not changed or re-certified by this local result. + +This package adds the dyadic lowering extension, fusion of the completed +centered shear pair, precise three-query bound and new finite evidence relative +to the pinned repository context. Elementary compute/uncompute, determinant +and Laurent methods are not claimed as new literature discoveries. PR756 and +PR805 are explicitly excluded from the consumed construction and verification. +This is not an official OpenAI release or endorsement. Exact source hashes and +inspected context heads are in SOURCES.json. diff --git a/research/dyadic-query-runs/vendor/pr840-PROOF.md b/research/dyadic-query-runs/vendor/pr840-PROOF.md new file mode 100644 index 0000000000..aaba3e501d --- /dev/null +++ b/research/dyadic-query-runs/vendor/pr840-PROOF.md @@ -0,0 +1,204 @@ +# Three queries for a centered dyadic native BIT shear + +This is a local recursive-interface construction and a scoped query lower +bound. Ordinary ADDRESS interchange and ordered affine tape streams remain +premises. There is no new supplier, kappa, or formal multiplication proof. + +## Object and predecessor contracts + +Karl Appel / applecrusher's PR521 gives the native unipotent query below and +its one-child lowering at `k=1`. PR677 by commdata2338 completes the shear +`S_h(x,y,z)=(x+(h+I)y,y,z)` using two queries on the DATA target. Its source +remains untouched, and no full private row is required. VALUE addition is +over F2; ADDRESS arithmetic is rational arithmetic specialized to an odd +residue ring. The contribution here combines **two completed shears**, +extends the literal lowering to signed dyadic powers, and changes the +intermediate query to `h^(2a)`. It is not PR521's unfinished dirty chart. + +Use six physically ordered equal-width ADDRESS fields +`(H0,H1,H2,D0,D1,D2)`, each ranging over `Z/(ell^b)`, `b>=1`, `ell` odd. +Arbitrary intervening/exterior spectator fields and suffix VALUE records +are retained. Define column vectors + + s=(1,0,1,-1,0,-1)^T, r=(1,0,-1,-1,0,1)^T, + M(k)=I6+(k/4)s r^T. + +Since `r^T s=0`, `M(k)M(l)=M(k+l)` and `M(k)^-1=M(-k)`. +Let `h` be the array permutation induced by the ADDRESS **push** map `M(1)`. +Thus a VALUE moves from address `z` to `M(1)z`, and the value at a new address +is read from its inverse image. The full-array operator for `M(k)` is `h^k`. + +For each fixed integer `j>=0`, let `a=+/-2^j`. The desired completed endpoint is + + F_a(x,y,z)=(x+(h^a+h^-a)y,y,z). (1) + +Every additional arbitrary dirty row is unchanged. Source `y` is never +modified. The target requires exclusive access until the completed boundary; +the caller may not read its temporarily permuted representation mid-program. +This is the same target permission needed by PR677's DATA-target program. + +## One-child lowering of every signed dyadic power + +Put `c=k/4`, for `k=+/-2^j`. Apply, chronologically, + + z2 <- z2-z0 + z3 <- z3+z0 + z5 <- c*z5+(1+c)*z0-c*z2-c*z3 + CHILD_C(0,5) + z2 <- z2+z0 + z3 <- z3-z0 + z5 <- -(1/c)*z5+(1/c-1)*z0+z2+z3. (2) + +Every control precedes its target. The child swaps exactly two `b`-digit +fields on the complete queried BIT row, preserving every spectator. All six +affine events are charged, including their preparation, temporary tapes, +source access, counter work and head returns. The child uses its own restored +workspace; it is not an uncharged VALUE swap. + +To check (2), write incoming coordinates as `A,B,C,D,E,F` and +`d=A-C-D+F`. Just before the child, the later field is `A+c*d`, and the +middle fields are `C-A,D+A`. After the child and the next two events, +the first field is `A+c*d`, and the middle fields are `C+c*d,D-c*d`. +The final line gives `F-c*d`. Coordinates 1 and 4 stay fixed. This is +exactly `z+(k/4)s(r^T z)=M(k)z`. The literal reverse of (2), inverting +each affine event and using the same involutive child, implements `M(-k)`. + +The only diagonal units are `1,c,-1/c`. All numerator and denominator +factors of these units are powers of two, up to sign. Every control +denominator is also a power of two. Therefore (2) and its inverse +specialize to **every odd modulus**, including every odd prime-power +width. A control numerator may vanish modulo ell without invalidating a +diagonal. An arbitrary non-dyadic k would introduce prime exclusions into +this particular lowering; no such all-odd-radix claim is made. + +At k=1 this is exactly PR521's attributed word. The extension changes its +coefficients, not its tape/child contracts. For a fixed j, the finite +coefficient table is compiled into the machine description. Its size and +streaming constants depend on j. A growing j is separately priced below. + +## Completed pair fusion + +Two successive applications of PR677's completed DATA-target program, +for `h^a` and `h^-a`, produce (1): the two identity contributions cancel +over F2. This literal baseline has four queries and four XOR scans. + +Instead apply, chronologically, + + x <- h^-a x + x += y + x <- h^(2a) x + x += y + x <- h^-a x. (3) + +Following x gives `h^-a x+y`, then `h^a x+h^(2a)y`, then +`h^a x+h^(2a)y+y`, finally `x+h^a y+h^-a y`. The three target +permutations multiply to the identity. The unchanged source and spectators +can be arbitrarily dirty. No private row is initialized, borrowed, copied +or cleared. Because (1) is a VALUE shear, `F_a^2=I` despite `h^a` being +noninvolutive. Reversing and inverting the literal events restores all data. + +Lowering all queries by (2) gives **three separately paid ordinary children, +eighteen affine events and two XOR scans**, versus four children, +twenty-four affine events and four XOR scans for the completed pair. +This is a count comparison for this baseline; physical speed is not measured. + +## Three queries are necessary in the stated model + +Allow d>=2 arbitrary dirty F2-valued rows, invertible address-independent +linear XOR maps between row roles, and queries `h^e` on one row for any +integer e. All other ADDRESS maps, clean/disposable storage, erasure, +nonlinear VALUE gates and intermediate observations lie outside this model. +The lower bound counts queries, even when a non-dyadic power would need a +different physical lowering. It is not a lower bound on all tape programs. + +Restrict the complete ADDRESS domain to the orbit of `e_H0` under h. +Its addresses are `e_H0+k*s/4`, indexed by `Z/m`, `m=ell^b`. They are +distinct because a component of s and 1/4 are units. Hence h is multiplication +by t on the regular module of `R=F2[t,t^-1]/(t^m-1)`. Basis monomials +`1,t,...,t^(m-1)` are independent; zero divisors in R do not affect the +following determinant and coefficient arguments. The same proof works +over the Laurent ring for a uniform symbolic identity. +The determinants are those of d-by-d row matrices over R, not of the +expanded F2 matrix of all individual BIT positions. + +Move all constant row maps to the left, conjugating queries. At t=1, +the target `I+(t^a+t^-a)N`, `N=e_x e_y^T`, is I, so the remaining +constant map is I. A normalized query has the form + + D_P(t^e)=I+(t^e+1)P, P=u v^T, v^T u=1, + det D_P(t^e)=t^e. (4) + +The determinant of the target is one. Zero queries cannot produce its +nonzero off-diagonal entry: a is a unit modulo odd m and `t^a!=t^-a`. +One query either is the identity (e=0 modulo m) or has the wrong determinant. +For two queries, the determinant forces opposite exponents modulo m, +and their product is + + I+P+Q+t^e(P+PQ)+t^-e(Q+PQ). (5) + +If e=0 modulo m, both are identity. Otherwise, as m is odd, `1,t^e,t^-e` +are distinct basis monomials. The target's constant coefficient is I. +Comparing constant coefficients in (5) therefore forces P=Q. Then +`P^2=P` cancels both other coefficients and (5) is I, a contradiction. +Thus no two-query program implements (1), even with arbitrary dirty +spectator rows and arbitrary integer-power queries. Program (3) attains +three. This is a written algebraic proof, not an inference from finite tests. + +PR677's different first-difference target has constant coefficient `I+N` +and attains two queries. Its theorem is preserved. Allowing `h^(2a)` here +changes the physical query alphabet: substituting two `h^a` calls would +restore the four-child bill. At an even orbit a centered target can vanish; +the odd full-order hypothesis is necessary for this formulation. + +## Complete typed costs and workspace + +Let each genuine DATA row have full logical BIT volume U, including every +spectator range; V=3U and N=3b. Let C(U,b) pay one ordinary ADDRESS +interchange with restored child workspace. Let L_k(U,b) be the sum of the +six actual ordered-affine charges in (2), **including** finite coefficient +preparation, source access, counter work, temporary tapes and their returns. +Let X(U) pay one aligned XOR scan. Let R_f,R_b pay row split/merge, evaluator +routing, descriptors, parking and all additional head returns. Then + + B_a(V,3b) <= 4 C(U,b)+2 L_a(U,b)+2 L_-a(U,b)+4 X(U)+R_b, + F_a(V,3b) <= 3 C(U,b)+2 L_-a(U,b)+L_2a(U,b)+2 X(U)+R_f. (6) + +The new middle lowering has a different coefficient table. Equation (6) +does not assume equal costs for it. Relative to these literal invoices, +the saving is `C+2 L_a-L_2a+2 X+R_b-R_f`; this is not asserted positive +for every finite implementation. Under the retained tape contracts and +**fixed j**, L_k, X and R are O_j(V), giving normalized recursive-child +coefficients 4/3 and 1 respectively. The three children are sequential, +each on actual volume V/3 and width N/3. Persistent genuine-role storage is +V in both programs, with no additional full private role. A safe peak bound is + + W_f(V,3b) <= V+B_f(V,b,j)+W_C(U,b), + +where B_f pays streaming, counter/coefficient and evaluator parking workspace. +No exact physical tape count or scratch-cell saving is claimed. + +For growing j, table entries have O(j+1) numerator/denominator bits and +modular preparations and all primitive costs must retain their j dependence. +In particular the original direct multiplication stream can have a number +of pieces depending on a fixed large integer. No polynomial-in-j runtime +or uniform O(V) constant is inferred from (2). The `j=54` fixture is exact +coefficient evidence, not a practical performance demonstration. + +The left sides of (6) are a centered DATA shear; C is ordinary ADDRESS +interchange. Replacing C by F_a and solving a self-recursion would require +a separate compiler and would be circular here. Arbitrary-width padding, +common-label construction, scalar/frame/owner schedules, both supplier +invoices, precision/tape/hosting and analytic transfer remain obligations. +No supplier or assembly constraint is changed, so no new kappa follows. + +## Evidence boundary + +The checker compares (2) to an independently derived rational matrix and +modular formula, checks the VALUE endpoint over exact Laurent matrices, +and uses a separate sparse-set full-domain replay. Negative controls remove +children, change powers/directions, omit scans, destroy a dirty spectator, +and demonstrate the first-difference/even-orbit scope boundaries. +The recorded finite domains, fixed seed-selected coefficient and source pins +are in CERTIFICATE.json and SOURCES.json. No search outside those domains, +proof-assistant verification, complete supplier replay or runtime benchmark +is claimed. The universal argument above remains open to mathematical review. diff --git a/research/dyadic-query-runs/vendor/pr840-SOURCES.json b/research/dyadic-query-runs/vendor/pr840-SOURCES.json new file mode 100644 index 0000000000..d535b797d1 --- /dev/null +++ b/research/dyadic-query-runs/vendor/pr840-SOURCES.json @@ -0,0 +1,171 @@ +{ + "assignment_seed": 54, + "base_commit": "7ee02b7c96d85f22b38d28bd7ed49bb8c1aeb261", + "claim_overlap": { + "inspected": [ + { + "author": "chafreaky", + "head": "5f3db6a11198bab07d8effe8f0c9f5df9c3f2eb7", + "number": 481, + "title": "Batch Gaussian boundary right-hand sides to reduce their cost" + }, + { + "author": "applecrusher", + "head": "a190fdb39f31647fc6f651625353710624627348", + "number": 521, + "title": "Native BIT ADDRESS fusion: two recursive queries to one" + }, + { + "author": "commdata2338", + "head": "613c02b8b4411f991f108dcc1481b3f9100b996f", + "number": 677, + "title": "Research note: restored DATA-shear boundaries for PR #521's native BIT query (exact query costs, no new \u03ba)" + }, + { + "author": "FanPUYen", + "head": "efad8a40094ab453c0525efef0b0eff2a5d8b850", + "number": 714, + "title": "Research: optimal clean root checkpoint saves 25\u201340% of binary product-shear calls" + }, + { + "author": "thakrarsagar", + "head": "d222e348179cc02a54d6d26dbd2838944f62c6e5", + "number": 730, + "title": "Research: optimize ordered dirty echoes at fixed scratch (no new kappa)" + }, + { + "author": "aliromman", + "head": "302383e0c1ec71c50860362d3f394f85664c2445", + "number": 744, + "title": "Independent verification: fixed-space ternary echo minima and rounded leaves" + }, + { + "author": "Koroffstrogov", + "head": "a164f06263e438ead570b169e5b7103aa45bf228", + "number": 758, + "title": "Research: higher-arity dirty echoes use 152 calls at five-array cap (no new kappa)" + }, + { + "author": "AlexS-scale", + "head": "548e42022b37a300f8bf745e848c38baccbce056", + "number": 784, + "title": "Research theorem: sharp scratch-dependent call bound for dirty echoes" + }, + { + "author": "nightangelflowerwin-ops", + "head": "ff8251519e009a01ede6b27e3f5af703eaa70132", + "number": 788, + "title": "Research: reusable clean checkpoint lowers weighted binary leaf bill 20 to 16 (no new kappa)" + }, + { + "author": "VictorLiwentao", + "head": "4fad623a1e4ca06959f4326e221c2f8d9125c269", + "number": 756, + "title": "Tooling: replay balanced Fano 2.91\u00d7 faster with identical exhaustive streams" + }, + { + "author": "VictorLiwentao", + "head": "ef34bd5b32fcf2d5640dae90b5b8f28488738d5a", + "number": 805, + "title": "Research: determinant-balanced cyclic leaves with exact dirty restoration (no new kappa)" + }, + { + "author": "shiftybitshiftr", + "head": "d91c5152b314391406b0ec792b6765a5cf0af2f1", + "number": 814, + "title": "Research: Eisenstein nonlinear message copy floor 22b under explicit width pricing" + } + ], + "max_pr": 814, + "open_count": 627, + "pinned_issue": null + }, + "format": "dyadic-native-query-pair-sources-v1", + "immutable_inputs": [ + { + "commit": "5996e33ecad6a0ccd578aec58831457829d75575", + "git_blob": "088fceea1867abc76271d7efe7532b779fee9039", + "local": "vendor/upstream-02-streams.tex", + "path": "upstream/build/sections/02-streams.tex", + "repository": "CrocSwap/integer-mult-bounds", + "sha256": "606c80db61cad13aa0c3b6060dc4b88dbbe7ac60cdd831aa93f28d908fd09dab", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/5996e33ecad6a0ccd578aec58831457829d75575/upstream/build/sections/02-streams.tex" + }, + { + "commit": "5996e33ecad6a0ccd578aec58831457829d75575", + "git_blob": "951e792b1768e6509561380b8bbfb1d1ccb64c08", + "local": "vendor/upstream-04-swap.tex", + "path": "upstream/build/sections/04-swap.tex", + "repository": "CrocSwap/integer-mult-bounds", + "sha256": "412b170ccaab38dba96e95e3cbfae09f4876a9818f8d278776a746b0f8044906", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/5996e33ecad6a0ccd578aec58831457829d75575/upstream/build/sections/04-swap.tex" + }, + { + "commit": "5996e33ecad6a0ccd578aec58831457829d75575", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", + "local": "vendor/upstream-LICENSE", + "path": "upstream/LICENSE", + "repository": "CrocSwap/integer-mult-bounds", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/5996e33ecad6a0ccd578aec58831457829d75575/upstream/LICENSE" + }, + { + "commit": "a190fdb39f31647fc6f651625353710624627348", + "git_blob": "c3f67fc807aa3bf32ba559d51ea0b7e7a424229d", + "local": "vendor/pr521-PROOF.md", + "path": "research/native-unipotent-fusion/PROOF.md", + "repository": "CrocSwap/integer-mult-bounds", + "sha256": "320ce5529c1543f9e6fceb9e7f8b563ed332f13923229e38d4e7edac98f30283", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/a190fdb39f31647fc6f651625353710624627348/research/native-unipotent-fusion/PROOF.md" + }, + { + "commit": "a190fdb39f31647fc6f651625353710624627348", + "git_blob": "549b87c2d57eb00296301c90e090d2f49d475a57", + "local": "vendor/pr521-SOURCE-PINS.json", + "path": "research/native-unipotent-fusion/SOURCE-PINS.json", + "repository": "CrocSwap/integer-mult-bounds", + "sha256": "34f97e7a31deed0dd85474ece3709a55de495f9473a3619f84e991fdbd3bf732", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/a190fdb39f31647fc6f651625353710624627348/research/native-unipotent-fusion/SOURCE-PINS.json" + }, + { + "commit": "613c02b8b4411f991f108dcc1481b3f9100b996f", + "git_blob": "47d9bf59a3e0d85bcc4930cd76a3d21a1e43c2fc", + "local": "vendor/pr677-PROOF.md", + "path": "research/native-fusion-restored-shear/PROOF.md", + "repository": "CrocSwap/integer-mult-bounds", + "sha256": "4f281eb48b9662c03269717b3919b45b27f7c2655abb185249a1eea2a03af186", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/613c02b8b4411f991f108dcc1481b3f9100b996f/research/native-fusion-restored-shear/PROOF.md" + }, + { + "commit": "613c02b8b4411f991f108dcc1481b3f9100b996f", + "git_blob": "bbd90a76bb1f3c55393367e24afd9970b796dba2", + "local": "vendor/pr677-NOTICE.md", + "path": "research/native-fusion-restored-shear/NOTICE.md", + "repository": "CrocSwap/integer-mult-bounds", + "sha256": "d79071e9dda5edc60305f80910572c1a61daf0b4601f5673b5ff874a6d487742", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/613c02b8b4411f991f108dcc1481b3f9100b996f/research/native-fusion-restored-shear/NOTICE.md" + } + ], + "selected_context": [ + { + "commit": "7ee02b7c96d85f22b38d28bd7ed49bb8c1aeb261", + "path": "certificates/selected-result.json", + "sha256": "8f2bfbf11609194654d4da145866223d4c546c5418727cae056bfb9968cabcac" + }, + { + "commit": "7ee02b7c96d85f22b38d28bd7ed49bb8c1aeb261", + "path": "docs/research/community-frontier741-review.md", + "sha256": "4634694fa75ea9e749ecf19d3db3e4d82effe3b61a2efdf08ac5a97275fb676a" + }, + { + "commit": "7ee02b7c96d85f22b38d28bd7ed49bb8c1aeb261", + "path": "research/complex-sw4-frame8/PROOF.md", + "sha256": "21d8ef267f9ee4c837bcbab0f659e5a8bbf16e0ee1e79e7775342d39c8c8dd7b" + }, + { + "commit": "7ee02b7c96d85f22b38d28bd7ed49bb8c1aeb261", + "path": "docs/research/pr-ledger.json", + "sha256": "b7bf4514786dbd591a5579851871da12a5c235f925ddb465b4b93930493eb52b" + } + ] +} diff --git a/research/dyadic-query-runs/vendor/upstream-02-streams.tex b/research/dyadic-query-runs/vendor/upstream-02-streams.tex new file mode 100644 index 0000000000..088fceea18 --- /dev/null +++ b/research/dyadic-query-runs/vendor/upstream-02-streams.tex @@ -0,0 +1,208 @@ +\section{The machine model and elementary streams} +\label{sec:streams} + +A machine has one fixed finite alphabet and one fixed finite number of +one-dimensional tapes. A step reads and writes at most one cell on each +tape and moves each head by at most one cell. Fixed tracks and finitely +many work tapes change time by a fixed factor. We distinguish moving one +digit in a fixed radix, which needs a bounded number of scans, from +interchanging fields whose numbers of digits grow. The latter permutation +will be realized in Section~\ref{sec:tape-interchange} by computing XOR +combinations of intermediate data streams. The present section supplies +the elementary scans it uses. Every scan includes its counters and the +return of its tape heads. + +\subsection{Array order and elementary scans} + +For a positive integer $a$ write $[a]=\{0,\ldots,a-1\}$. +An array with address set $[a_1]\times\cdots\times[a_t]$ is stored in +lexicographic order, with the first coordinate most significant. Its +entries are bits unless a record width is specified. A trailing record +of $B$ bits can equivalently be regarded as a final address field $[B]$. +An address is implicit in an entry's position in this ordered stream; it +is not stored beside every data bit. +The \emph{logical volume} $V$ is the number of stored data bits. Work +tapes and duplicate streams are charged in time but do not increase $V$ +in recurrences. All the fields discussed below are nonempty. A call +with an empty array is handled directly. + +An address permutation $f$ moves the entry at $x$ to $f(x)$. Thus its +action on an array $A$ is $(fA)(f(x))=A(x)$. Adjacent fields which are +irrelevant to an operation may be replaced by a single field whose length +is their product. In particular, the elementary procedures below have a +fixed number of formal address fields even when a surrounding algorithm +has a growing list of coordinates. Lengths and positions are supplied in +canonical binary on descriptor tapes; no additional tape head is attached to an +address coordinate. Each elementary call receives a fixed number of +collapsed canonical lengths. Constructing them from a longer surrounding +list is work of the caller; recursive calls below construct their own +collapsed descriptors within their stated bounds. + +When one address field is designated as a row field, collapse the fields +before it to a prefix $[P]$ and those after it to a suffix $[B]$. If the +row field has range $[R]$, a \emph{row} at prefix $p$ and row index $r$ +is the complete consecutive block $\{p\}\times\{r\}\times[B]$. +Every row therefore contains $B$ bits in the same suffix order. + +For headers that concatenate a list of positive integer parameters, we use +the self-delimiting code +\begin{equation} + b_v=\lfloor\log_2v\rfloor+1,\qquad + \Gamma(v)=0^{b_v-1}\operatorname{bin}_{b_v}(v),\qquad + |\Gamma(v)|=2b_v-1\quad(v\ge1). + \label{eq:integer-descriptor-code} +\end{equation} +The initial zeroes specify how many further bits follow the first one, +so concatenated codes can be read in order. We use this code when an +interface specifies a header; elementary calls still receive the fixed +number of canonical binary lengths described above. + +\begin{lemma}[Elementary stream operations] +\label{lem:elementary-streams} +Fix a radix $q\ge2$. Each of the following operations on an array of +volume $V$ takes $O(V)$ steps on a fixed number of one-dimensional tapes: +\begin{enumerate} +\item any fixed permutation of the pair of digit values at two specified +radix-$q$ positions, whether or not the positions are adjacent; +\item moving one specified radix-$q$ digit to another position, preserving +the order of the intervening positions; +\item splitting on a specified radix-$q$ digit, applying a fixed +pointwise map to aligned streams, and merging them back; +\item for positive integers $P,R,B$, within each prefix of an array on +$[P]\times[R]\times[B]$, splitting +whole rows cyclically into a fixed number $W$ of streams, and, when $W$ +divides $R$, merging those streams in any fixed order of the row classes. +\end{enumerate} +The bounds include shape preparation, counter initialization and resets, +and returning or clearing the visited portions of work tapes. Their +constants may depend on the fixed radix, the fixed pointwise map, and the +fixed number of row classes. +\end{lemma} + +\begin{proof} +For the first operation split into $q^2$ streams according to the two +specified digits. With these digits fixed, the order of all remaining +digits is unchanged by the permutation. Enumerate output addresses in +their required order and read the stream prescribed by the two preimage +digits. For a digit move use $q$ streams instead. The same observation +shows that splitting on one digit gives streams with the same remaining +address set in the same order. Scan their aligned entries, apply the +fixed pointwise map, and merge according to the output digit; this proves +the third operation. For the fourth, write $r=Wg+w$, where +$0\le w0$, write each chunk as $m$ +consecutive $b=e/m$ digit fields, giving vectors $H,D$ over +$\mathbb Z/q^b\mathbb Z$. We first construct the shear $H\leftarrow H+D$. + +Split whole rows cyclically into $W$ role streams within each prefix +preceding the row field. Write the original row number as +$r=Wg+(w-1)$ with $1\le w\le W$; stream $w$ has row number $g$. +These streams have exactly the same remaining shape, including the +full ranges of $H$ and $D$. Each has +logical volume $V/W$, and its row count is divisible by $W^{k-1}$. + +For a rational matrix $M$, let $\Phi_M$ act on an array by moving its +entry at address $(H,D)$ to $(H+MD,D)$, with every spectator unchanged. +Thus $\Phi_M$ is the array permutation induced by that address map. +Its inverse is $\Phi_{-M}$ and +$\Phi_{M'}\Phi_M=\Phi_{M'+M}$. On every circuit edge apply +$\Phi_{A_e}$ to that role stream; implement it by +Lemma~\ref{lem:matrix-shear}, recursively interchanging each pivot pair +of $b$-digit fields. Execute each circuit gate pointwise at matching +addresses of its role streams. + +The row split supplies the common address set used in the +frame identity~\eqref{eq:common-frame-identity}. Here the frame at a +vertex with matrix $M$ is the address permutation $\Phi_M$, and every +edge changes it by $\Phi_{M'-M}$. The same invariant proof applies +because a common address permutation commutes with every pointwise +bit gate. For the physical input arrays $f_w$, the logical arrays are +$g_w=\Phi_{-M_{\mathrm{in}(w)}}f_w$; this only specifies their +interpretation, with no initial tape operation. The logical circuit +routes $g_w$ to role $\rho(w)$. Thus its physical output satisfies +\[ + f'_{\rho(w)} + =\Phi_{M_{\mathrm{out}(\rho(w))}} + \Phi_{-M_{\mathrm{in}(w)}}f_w + =\Phi_{I_m}f_w, +\] +by~\eqref{eq:finite-shear-contract}. Merge by returning row $g$ of +output role $\rho(w)$ to the original row $Wg+(w-1)$ within the same +preceding prefix. This undoes $\rho$ and restores row order. The result +is $H\leftarrow H+D$ on every original row, including rows assigned +to scratch roles, whose initial values were arbitrary. + +To interchange the two full chunks, perform +\[ + D\leftarrow D-H,\qquad H\leftarrow H+D,\qquad D\leftarrow H-D, +\] +componentwise. Only the middle shear uses the circuit. The other two +updates target the later group and have linear cost. The transformation +sends $(H,D)$ to $(D,H)$. + +The number of recursive calls is the sum of the edge ranks, exactly $s$. +Each acts on one role stream of volume $V/W$, retaining all other +fields as spectators. Splitting, +merging, gates, and triangular operations have total cost $O(V)$ because +their number is fixed. Below we verify that scheduling the recursive +calls on fixed tapes also costs $O(V)$ at this node. Thus if $F_k$ is a +uniform upper bound for time divided by logical volume, then +\begin{equation} +\label{eq:swap-recurrence} + F_0=O(1),\qquad F_k\le(s/W)F_{k-1}+O(1). +\end{equation} +For $a=s/W1$, it is $O(a^k)$. +Hence $F_k=O(e^\tau)$. + +\paragraph{A fixed-tape depth-first schedule.} +Here we complete the implementation assertion used in +\eqref{eq:swap-recurrence}. Reserve $W$ role tapes, a fixed set of +I/O and elementary-operation work tapes, one parking stack tape, and a +separate descriptor stack. Although $W$ is large, it is fixed. +At a call boundary all reusable work tapes, other than the current I/O +and local descriptor, are empty and their heads are at their origins. +The parking and descriptor heads are at the tops of their stacks. + +Before a recursive call, append the $W-1$ inactive role streams to the +parking stack in a fixed order, with separators. Copy the active stream +to the child I/O area, and erase the parent role tapes while traversing +their current contents. Push the parent descriptor and its finite +program counter to the descriptor stack. The role and work tapes are +now available to the child, using the same tapes at every depth. +On return, copy the child output into the designated active role. +Pop the inactive streams in reverse order. To recover a stream in its +original direction, prepare its destination to the known length and +write the popped symbols from the destination's right end toward its +left end. Erase the popped stack cells as they are left. This uses +linear time and ends with the parking head at the previously saved top. +No scan passes through a parked ancestor. Cleanup is always limited to +the region visited by the current call; a reused tape is not swept to +the largest position ever visited by an ancestor. + +Each push, pop, copy, positioning operation, or erasure moves $O(V)$ +symbols at a parent node. There are only the fixed number $s$ of child +calls. This gives precisely the additional $O(V)$ term claimed above, +even though each child itself has volume $V/W$. Temporary storage is +therefore not substituted for logical volume in the factor $s/W$. + +For completeness, descriptor processing also fits this term when the +payload is one bit. Let $V_0$ be the volume at the root of one +power-width call with width $e_0=m^{k_0}$, and $V_j=V_0/W^j$ the volume +of any depth-$j$ child. Here $j\le k_0=\log_m e_0$. The root row +count is at least $W^{k_0}$, so at depth $j$ it is still at least one. +Both original chunk ranges remain present: digits outside the current +subchunks become spectators rather than being removed. Hence +\[ + V_j\ge q^{2e_0},\qquad + j\log W\le(\log_m e_0)\log W=O(e_0)=O(\log V_j). +\] +It follows that +$\log V_0=\log V_j+j\log W=O(\log(2V_j))$. +A local descriptor lists the row field, at most the current $m+m$ +fields, and a fixed number of intervals formed from intervening +spectator fields. Computing products of their lengths, subdividing +target fields, copying lengths, and storing the current instruction take +$(\log(2V_0))^{O(1)}=O(V_j)$ time at that child, since every fixed +power of $\log(2V_j)$ is $O(V_j)$. Before descending, +construct the child's descriptor by retaining its two target fields and +combining each consecutive group of spectator fields into one interval. +The ancestor's subdivision need not remain active in the child. Stack entries contain +finite instructions and binary integers, not new alphabet symbols. +These observations establish one finite machine for every recursion +depth and every choice of spectator lengths. + +\end{proof} + + +We use the rational value $\tau=1-2^{-50}$ established in +\eqref{eq:explicit-motif-exponents}. Its verification uses fixed integer +comparisons and the displayed exponential inequality; it needs no +real-arithmetic oracle. + + +\subsection{Removing width and row restrictions} + +We have proved the fast operation for power widths with enough rows. +Rows for a general array can be supplied by a few of its own high digits. +Their movement will cost less than the final bound. + +\begin{lemma}[Arbitrary-width interchange] +\label{lem:chunk-swap} +There exist fixed $0<\tau<1$ and one fixed finite-alphabet multitape +procedure with the following property. For positive integers $P,G,B$ +and $u\ge1$, it transforms an arbitrary bit array on +\[ + [P]\times[2^u]\times[G]\times[2^u]\times[B] +\] +by the address permutation +\[ + (p,h,g,d,z)\longmapsto(p,d,g,h,z) +\] +in $O(Vu^\tau)$ steps, where $V=PG B\,2^{2u}$. +The integers specifying the shape are part of the input. The time +includes their processing, all padding and unpadding, and fixed-tape +workspace cleanup. In particular, $B=1$ is allowed. +\end{lemma} + +\begin{proof} +First suppose the two ranges are $[q^e]$, where $q$ is the fixed prime +already chosen. Set +\[ + k=\lceil\log_m e\rceil,\qquad + \rho=\left\lceil\frac{k\log W}{2\log q}\right\rceil. +\] +For all sufficiently large $e$, $1\le\rho= 3 and modulus % 2 == 1, + "odd ADDRESS modulus") + + def coefficient(s): + a = F(s) + return a if modulus is None else a.numerator * pow(a.denominator, -1, modulus) % modulus + + out = [] + for op in reversed(events) if inverse else events: + if op[0] == "C": + out.append(tuple(op)) + else: + _, t, diagonal, controls = op + d = F(diagonal) + cs = [(i, F(v)) for i, v in controls] + if inverse: + cs = [(i, -v/d) for i, v in cs] + d = 1/d + out.append(("A", t, coefficient(d), [(i, coefficient(v)) for i, v in cs])) + return out + + +def native(events, z, modulus=None): + z = list(z) + for op in events: + if op[0] == "C": + _, i, j = op + z[i], z[j] = z[j], z[i] + else: + _, t, d, cs = op + z[t] = d*z[t] + sum(v*z[i] for i, v in cs) + if modulus is not None: + z[t] %= modulus + return tuple(z) + + +def formula(k, z, modulus=None): + a = F(k, 4) if modulus is None else k*pow(4, -1, modulus) % modulus + dot = sum(v*w for v, w in zip(R, z)) + out = tuple(v+a*s*dot for v, s in zip(z, S)) + return out if modulus is None else tuple(v % modulus for v in out) + + +def invoice_check(word, invoice, lowerings): + word_check(word) + actual = Counter() + powers = Counter() + for op in word: + if op == "X": + actual["xor_scans"] += 1 + else: + need(str(op) in lowerings, "missing native lowering") + powers[str(op)] += 1 + for event in lowerings[str(op)]: + actual["children" if event[0] == "C" else "affines"] += 1 + expected = dict(actual, query_multiplicities=dict(powers)) + need(invoice == expected, "literal complete invoice") + for name in ["children", "affines", "xor_scans"]: + need(type(invoice[name]) is int, "invoice integer type") + need(all(type(v) is int for v in invoice["query_multiplicities"].values()), + "multiplicity integer type") + + +def source_check(): + sources = json.loads((ROOT / "SOURCES.json").read_text()) + need(sources["format"] == "dyadic-query-runs-sources-v1", "source format") + need(sources["base_commit"] == BASE and sources["assignment_seed"] == 55, + "base and assignment") + need(len(sources["immutable_inputs"]) == 11, "complete retained source inventory") + seen = set() + for item in sources["immutable_inputs"]: + need(item["commit"] == PREDECESSOR, "predecessor head") + local = item["local"] + need(local.startswith("vendor/") and ".." not in Path(local).parts and local not in seen, + "source path/inventory") + seen.add(local) + data = (ROOT / local).read_bytes() + need(hashlib.sha256(data).hexdigest() == item["sha256"], "source SHA256: " + local) + blob = b"blob " + str(len(data)).encode() + b"\0" + data + need(hashlib.sha1(blob).hexdigest() == item["git_blob"], "source Git blob: " + local) + # The predecessor's retained source manifest also binds its original + # transitive inputs to their actual original commits and byte digests. + ancestor = json.loads((ROOT / "vendor/pr840-SOURCES.json").read_text()) + for item in ancestor["immutable_inputs"]: + data = (ROOT / item["local"]).read_bytes() + need(hashlib.sha256(data).hexdigest() == item["sha256"], "ancestral source digest") + return len(seen), len(ancestor["immutable_inputs"]) + + +def invert_word(word): + return ["X" if op == "X" else -op for op in reversed(word)] + + +def pack(coords, radices): + result = 0 + for v, m in zip(coords, radices): + result = result*m+v + return result + + +def full_permutations(modulus, lowerings): + # Physical order (H0, spectator, H1,H2,D0, spectator,D1,D2), + # with two binary spectator fields. Every address is enumerated. + coords = list(product(range(modulus), repeat=6)) + radices = (modulus, 2, modulus, modulus, modulus, 2, modulus, modulus) + slots = [[pack((z[0], a, z[1], z[2], z[3], b, z[4], z[5]), radices) + for a, b in product(range(2), repeat=2)] for z in coords] + U = 4*len(coords) + literal, direct = {}, {} + comparisons = 0 + for key, events in lowerings.items(): + p, ref = [0]*U, [0]*U + ops = prepared(events, modulus) + for i, z in enumerate(coords): + got = native(ops, z, modulus) + expected = formula(int(key), z, modulus) + need(got == expected, "full ADDRESS push map") + comparisons += 1 + j = pack(got, (modulus,)*6) + e = pack(expected, (modulus,)*6) + for src, dst, correct in zip(slots[i], slots[j], slots[e]): + p[src], ref[src] = dst, correct + need(len(set(p)) == U, "native permutation is bijective") + literal[int(key)], direct[int(key)] = p, ref + return U, literal, direct, comparisons + + +def push(data, permutation): + out = bytearray(len(data)) + for src, dst in enumerate(permutation): + out[dst] = data[src] + return out + + +def xor(a, b): + return bytearray(x ^ y for x, y in zip(a, b)) + + +def execute(word, state, permutations): + x, y, z = (bytearray(row) for row in state) + for op in word: + x = xor(x, y) if op == "X" else push(x, permutations[op]) + return x, y, z + + +def adverse_controls(data): + import copy + controls = [] + + def rejects(name, fn): + try: + fn() + except ValueError: + controls.append(name) + return + raise ValueError("negative control accepted: " + name) + + case = data["cases"][54] + word, indices = case["word"], case["indices"] + rejects("omitted final return", lambda: endpoint_check(word[:-1], indices)) + missing = list(word) + missing.remove("X") + rejects("omitted source tap", lambda: endpoint_check(missing, indices)) + changed = list(word) + changed[0] *= -1 + rejects("wrong query sign", lambda: endpoint_check(changed, indices)) + rejects("VALUE-address confusion", lambda: endpoint_check([True, "X", -1], [0])) + rejects("source query outside alphabet", lambda: word_check(["QY"])) + for field in ["children", "affines", "xor_scans"]: + bill = copy.deepcopy(case["invoice"]) + bill[field] -= 1 + rejects("unpaid " + field, lambda bill=bill: invoice_check(word, bill, data["lowerings"])) + table = copy.deepcopy(data["lowerings"]) + table["1"] = [op for op in table["1"] if op[0] != "C"] + rejects("removed native child", lambda: lowerings_check(table)) + table = copy.deepcopy(data["lowerings"]) + table["1"][0][3][0][0] = 5 + rejects("control after target", lambda: lowerings_check(table)) + table = copy.deepcopy(data["lowerings"]) + table["1"][0][2] = "3" + rejects("nonunit at odd radix", lambda: lowerings_check(table)) + bad_events = copy.deepcopy(data["lowerings"]["1"]) + bad_events[0][3][0][1] = "1" + basis = (1, 0, 0, 0, 0, 0) + rejects("scalar-valid wrong native sign", lambda: need( + native(prepared(bad_events), basis) == formula(1, basis), "native endpoint")) + rejects("even radix admission", lambda: prepared(data["lowerings"]["1"], 4)) + + # Two positive scope controls: the endpoint is valid but the lower-bound + # hypothesis changes. They must not be reported as failed constructions. + unrestricted = [-4, "X", 3, "X", 2, "X", 3, "X", -4] + need(symbolic(unrestricted) == ({0}, {-4, -1, 1, 4}), "nondyadic scope endpoint") + need(sum(type(op) is int for op in unrestricted) == 5, "nondyadic query count") + rejects("nondyadic shortcut", lambda: word_check(unrestricted)) + aliased = set() + for e in [-2, -1, 1, 2]: + aliased.symmetric_difference_update({e % 3}) + need(not aliased, "modulus-three cancellation scope control") + # A legal but longer construction is evidence of correctness, not + # evidence of optimality: the separate-pair seed baseline has 15 queries. + endpoint_check(case["baseline"], indices) + rejects("valid nonoptimal invoice", lambda: need( + case["baseline_invoice"]["children"] == 2*len(indices)+len(components(indices)), + "restricted optimum")) + return controls, ["nondyadic five-query endpoint", "modulus-three zero target"] + + +def finite_walk_census(): + # A separate shortest-walk experiment, not the universal proof: allow + # every dyadic edge with both endpoints in [-32,32], and any off-support + # visits. Track all eight possible required vertices simultaneously. + bound = 32 + width = 2*bound+1 + required = sorted(sign*(1 << j) for j in range(4) for sign in [-1, 1]) + bits = {v: 1 << i for i, v in enumerate(required)} + steps = [sign*(1 << j) for j in range(7) for sign in [-1, 1]] + distances = array("i", [-1])*(width*(1 << len(required))) + distances[bound] = 0 + todo = deque([bound]) + states = edges = 0 + while todo: + key = todo.popleft() + mask, offset = divmod(key, width) + position = offset-bound + states += 1 + for step in steps: + target = position+step + if -bound <= target <= bound: + edges += 1 + newmask = mask | bits.get(target, 0) + nxt = newmask*width+target+bound + if distances[nxt] == -1: + distances[nxt] = distances[key]+1 + todo.append(nxt) + minima = [] + for selection in range(1, 16): + indices = [j for j in range(4) if selection & (1 << j)] + required_mask = sum(bits[sign*(1 << j)] for j in indices for sign in [-1, 1]) + candidates = [distances[mask*width+bound] for mask in range(256) + if mask & required_mask == required_mask and distances[mask*width+bound] >= 0] + best = min(candidates) + need(best == 2*len(indices)+len(components(indices)), "independent finite walk minimum") + minima.append([selection, best]) + return {"position_interval": [-bound, bound], "max_dyadic_step": 64, + "indices": list(range(4)), "reachable_states": states, + "directed_edges_examined": edges, "completed_selections": minima, + "scope": "Complete bounded walk census; universal bound is the written proof."} + + +def verify(): + source_count, ancestor_count = source_check() + data = json.loads((ROOT / "CERTIFICATE.json").read_text()) + need(data["format"] == "dyadic-query-runs-v1" and data["assignment_seed"] == 55, + "certificate identity") + need(data["domain"] == {"indices": list(range(6)), "masks": [1, 63]}, "complete domain") + cases = data["cases"] + need([case["mask"] for case in cases] == list(range(1, 64)), "every declared mask once") + lowerings_check(data["lowerings"]) + query_total = baseline_total = 0 + graph_records = [] + for case in cases: + expected_indices = [j for j in range(6) if case["mask"] & (1 << j)] + need(case["indices"] == expected_indices, "mask/indices binding") + groups = components(expected_indices) + for name, bill in [("word", "invoice"), ("baseline", "baseline_invoice")]: + word = case[name] + endpoint_check(word, expected_indices) + endpoint_check(invert_word(word), expected_indices) + invoice_check(word, case[bill], data["lowerings"]) + optimum = 2*len(expected_indices)+len(groups) + need(case["invoice"]["children"] == optimum, "graph lower bound attained") + need(case["invoice"]["xor_scans"] == 2*len(expected_indices), "tap lower bound attained") + need(case["baseline_invoice"]["children"] == 3*len(expected_indices), "pair baseline count") + query_total += optimum + baseline_total += case["baseline_invoice"]["children"] + graph_records.append([case["mask"], groups, optimum]) + rational = modular = 0 + moduli = [3, 5, 7, 9, 15, 25, 27, 49, 81] + for key, events in data["lowerings"].items(): + for modulus in [None]+moduli: + fwd = prepared(events, modulus) + inv = prepared(events, modulus, inverse=True) + for column in range(6): + basis = tuple(int(i == column) for i in range(6)) + result = native(fwd, basis, modulus) + need(result == formula(int(key), basis, modulus), "native matrix column") + need(native(inv, result, modulus) == basis, "literal native inverse") + need(native(inv, basis, modulus) == formula(-int(key), basis, modulus), + "inverse push direction") + if modulus is None: + rational += 1 + else: + modular += 1 + negative, positive = adverse_controls(data) + walk_census = finite_walk_census() + rng = random.Random(55) + full_cases = address_points = 0 + stream_hash = hashlib.sha256() + for modulus in [3, 5]: + U, literal, direct, checked = full_permutations(modulus, data["lowerings"]) + address_points += checked + for case in cases: + state = tuple(bytearray(rng.getrandbits(1) for _ in range(U)) for _ in range(3)) + expected = bytearray(state[0]) + for j in case["indices"]: + for sign in [-1, 1]: + expected = xor(expected, push(state[1], direct[sign*(1 << j)])) + for name in ["word", "baseline"]: + out = execute(case[name], state, literal) + need(out == (expected, state[1], state[2]), "full dirty VALUE endpoint") + restored = execute(invert_word(case[name]), out, literal) + need(restored == state, "full dirty inverse restoration") + for row in out+restored: + stream_hash.update(row) + full_cases += 1 + seed = cases[54] + return {"format": "dyadic-query-runs-evidence-v1", "cases": len(cases), + "rational_columns": rational, "modular_columns": modular, + "odd_moduli": moduli, "full_address_moduli": [3, 5], + "native_address_comparisons": address_points, + "spectator_configurations_per_address": 4, + "dirty_forward_cases": full_cases, "dirty_inverse_cases": full_cases, + "dirty_execution_sha256": stream_hash.hexdigest(), + "graph_records_sha256": hashlib.sha256(json.dumps(graph_records).encode()).hexdigest(), + "all_cases_fused_queries": query_total, "all_cases_baseline_queries": baseline_total, + "seed_indices": seed["indices"], "seed_invoice": seed["invoice"], + "seed_baseline_invoice": seed["baseline_invoice"], + "rejection_controls": negative, "positive_scope_controls": positive, + "independent_bounded_walk_census": walk_census, + "source_files": source_count, "ancestral_source_files": ancestor_count} + + +if __name__ == "__main__": + parser = argparse.ArgumentParser() + parser.add_argument("--write-evidence", action="store_true") + args = parser.parse_args() + result = verify() + evidence = ROOT / "EVIDENCE.json" + if args.write_evidence: + evidence.write_text(json.dumps(result, indent=2, sort_keys=True)+"\n", encoding="utf-8") + else: + need(result == json.loads(evidence.read_text()), "complete evidence receipt mismatch") + print("PASS_DYADIC_QUERY_RUNS cases=63 seed=55 children=15->12 affines=90->72 XOR=10") + print("dirty_forward={dirty_forward_cases} dirty_inverse={dirty_inverse_cases} " + "rational_columns={rational_columns} modular_columns={modular_columns}".format(**result))