From 6d3af7bd7eb49b0adf34b7a144df8d17095b02c4 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 11 Nov 2026 13:30:21 +0000 Subject: [PATCH] feat(research): prove sharp four-demand Boolean restoration cost --- .../four-orthogonal-one-insertion/PROOF.md | 171 +++++++++++++ .../four-orthogonal-one-insertion/README.md | 136 +++++++++++ .../SOURCES.json | 30 +++ .../four-orthogonal-one-insertion/TASK.json | 89 +++++++ .../four-orthogonal-one-insertion/VERIFY.json | 34 +++ .../four-orthogonal-one-insertion/verify.py | 230 ++++++++++++++++++ 6 files changed, 690 insertions(+) create mode 100644 research/four-orthogonal-one-insertion/PROOF.md create mode 100644 research/four-orthogonal-one-insertion/README.md create mode 100644 research/four-orthogonal-one-insertion/SOURCES.json create mode 100644 research/four-orthogonal-one-insertion/TASK.json create mode 100644 research/four-orthogonal-one-insertion/VERIFY.json create mode 100644 research/four-orthogonal-one-insertion/verify.py diff --git a/research/four-orthogonal-one-insertion/PROOF.md b/research/four-orthogonal-one-insertion/PROOF.md new file mode 100644 index 0000000000..d03bc74646 --- /dev/null +++ b/research/four-orthogonal-one-insertion/PROOF.md @@ -0,0 +1,171 @@ +# Four orthogonal demands with one insertion + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Contract and claim type + +Let R be a commutative unital Boolean ring. Thus every x in R satisfies +x squared = x, the characteristic is two, and every elementary row addition +is its own inverse. Let lambda_0,...,lambda_3 be nonzero, pairwise orthogonal +elements, and put g = lambda_0+...+lambda_3. There are exactly four arbitrary +dirty rows a_0,...,a_3 and a disjoint preserved source p. The required map is + + a_j -> a_j + lambda_j p, j = 0,...,3. + +The gates are P_i(beta), adding beta p to row i, and E_ij(alpha), adding +alpha times row j to row i for distinct i,j. Every coefficient belongs to R. +A word is fixed and finite. All four original dirty columns must return +exactly. There are no extra rows, free scalar maps, erasures, clean fields, +intermediate readouts or input-dependent choices. + +We restrict to exactly one nonzero P gate. Each E has a common price c > 0; +an insertion at row i has price mu_i > 0, independent of its coefficient. + +**Result.** For each insertion row i, the exact minimum is twelve ADDs and +one insertion, costing mu_i+12c. Across insertion rows it is min_i(mu_i)+12c. + +The six-ADD column lower bound is an exact finite certificate over F2^4. +The argument below lifts it to every R in the stated contract. The upper +word is a written identity. This combination is a computer-assisted scoped +proof, not a proof-kernel verification or a multiplication theorem. + +## 1. The insertion coefficient is forced + +Write M for the ADD-only prefix matrix and L for the ADD-only suffix matrix. +The full dirty endpoint requires LM=I, so M=L inverse. The source endpoint +requires L(beta e_i)=lambda. Consequently every lambda_j is a multiple of +beta, and beta is a linear combination of the lambda_j, by applying L inverse. +In a Boolean ring, g generates exactly the ideal generated by the lambda_j: +g lambda_j=lambda_j and g is their sum. Thus (beta)=(g). + +An idempotent has a unique generator of its principal ideal. Indeed, if +beta=xg and g=y beta, then beta g=beta and beta g=g, respectively. Hence +beta=g. This is the same ideal invariant used in lee-phys's #5514 triple +contract. The number of rows does not change this argument. + +Both the suffix L and the inverse prefix M inverse therefore send g e_i +to lambda. Inverting an ADD word preserves its number of gates. A column +lower bound of six gives six ADDs on each side of the insertion. + +## 2. Finite component quotient + +For a proposed finite word, take the Boolean subring generated by its finitely +many coefficients, the lambdas and 1. This subring is finite: if generated by +m elements, every element is a sum of the at most 2^m products formed by +choosing each generator or its complement. The nonzero such products are +pairwise orthogonal atoms summing to 1. Every generator, and hence every +subring element, is constant zero or one on each atom. + +Each nonzero lambda_j contains at least one atom. Choose an atom under each +lambda_j; the four are distinct by orthogonality. Restricting to these four +components gives a ring homomorphism into F2^4, sending the lambdas to +(1,0,0,0),...,(0,0,0,1) and g to (1,1,1,1). A word with fewer gates would +give a word with at most that many gates after projection. Projected zero +coefficients are harmless no-ops. + +It therefore suffices to exclude a column word of length at most five over +F2^4. This reduction uses only the finite coefficient subring of the proposed +word. It does not assume that the whole Boolean ring is finite or that +lambda_0+...+lambda_3 equals 1. + +## 3. Complete finite distance certificate + +Represent a source column over F2^4 by four row masks v_0,...,v_3 in +{0,...,15}. Every atomic component must have a nonzero binary column: +elementary row additions are invertible on each component. Equivalently, + + v_0 OR v_1 OR v_2 OR v_3 = 15. + +There are exactly (2^4-1)^4 = 50,625 such states, choosing independently +one nonzero four-bit column for each of the four components. There are +65,536 possible packed four-nibble indices including invalid states. + +For root zero the starting state is (15,0,0,0), and the target is (1,2,4,8). +An ADD from row j to distinct row i replaces + + v_i by v_i XOR (alpha AND v_j), alpha = 0,...,15. + +All other row masks stay fixed. This is exactly the stated gate alphabet. + +The verifier first computes distances by breadth-first search, enumerating +nonempty subsets of the donor mask. These are all distinct nontrivial changes; +no-op gates cannot improve a shortest path. The queue has capacity 50,625, +and a state is enqueued only once. + +It then certifies the labels in a different representation. The four nibbles +now store the four independent binary component columns. For each of the +50,625 vertices, each of the twelve ordered distinct row pairs and each of +the sixteen component coefficient patterns, it applies the binary row update +component by component. For all 9,720,000 transitions, including no-ops, +it checks that the successor stays in the domain and that + + abs(potential(successor)-potential(vertex)) <= 1. + +The starting potential is zero, and the target potential is six. Telescoping +along any finite gate word gives length at least six. This local inequality +certificate does not require trusting the discovery search's shortest-path +claim. Its separately encoded transition scan covers every coefficient and +every state in the exact finite quotient. The verifier also checks the domain +of every one of the 65,536 indices and the coordinate conversion. + +Permuting row indices gives the same lower bound for every insertion root; +the target permutes by relabeling its four atomic demands. The verifier checks +an attaining word for each root. The distance array is generated deterministically, +and its SHA256 is printed in the receipt. Use --write-distances PATH to export +its 65,536 bytes, with 255 marking invalid states. No distance labels or +receipts are handwritten. + +## 4. Six-ADD column attainer and complete restoration + +Fix the insertion row i. In any Boolean ring, execute the column word C: + + E_ji(lambda_j), for each j != i in increasing order; + E_ij(lambda_j), for each j != i in increasing order. + +It has six ADDs. On g e_i, the first three give lambda_j in each other row, +because lambda_j g=lambda_j. The last three change row i to + + g + sum_(j != i) lambda_j squared = lambda_i. + +Thus C(g e_i)=lambda. The complete chronological word is + + C inverse; P_i(g); C. + +It has one insertion and twelve ADDs. Its dirty matrix is C C inverse=I, +and its source column is C(g e_i)=lambda. Every other source column is +unchanged, including the preserved p. This proves the upper bound and the +claimed exact single-insertion price. + +Formal endpoint checks use the universal five-atom Boolean ring F2^5, with +lambda_j encoded by 1< None: + if not condition: + raise ValueError(message) + + +def distances() -> tuple[bytearray, dict[str, object]]: + """Rows are four nibbles; a gate toggles a subset of its donor nibble.""" + labels = bytearray([UNSEEN]) * SIZE + queue = array('I', [0]) * VALID_STATES + queue[0] = 15 + labels[15] = 0 + tail = 1 + edges = 0 + subsets = tuple(tuple(k for k in range(1, 16) if k & ~v == 0) + for v in range(16)) + for head in range(VALID_STATES): + if head == tail: + break + state = queue[head] + depth = labels[state] + for donor in range(4): + value = state >> (4 * donor) & 15 + for change in subsets[value]: + for destination in range(4): + if destination == donor: + continue + edges += 1 + following = state ^ (change << (4 * destination)) + if labels[following] != UNSEEN: + continue + require(tail < VALID_STATES, 'BFS capacity exceeded') + labels[following] = depth + 1 + queue[tail] = following + tail += 1 + require(tail == VALID_STATES, 'incomplete reachable graph') + counts = Counter(v for v in labels if v != UNSEEN) + return labels, {'states': tail, 'effective_edges': edges, + 'layers': dict(sorted(counts.items()))} + + +def transpose(code: int) -> int: + result = 0 + for row in range(4): + for column in range(4): + result |= ((code >> (4 * row + column)) & 1) << (4 * column + row) + return result + + +def check_potential(labels: bytearray) -> dict[str, int]: + """Check all coefficients using four independent binary component columns.""" + potential = bytearray([UNSEEN]) * SIZE + valid = 0 + for code in range(SIZE): + columns = tuple((code >> (4 * atom)) & 15 for atom in range(4)) + value = labels[transpose(code)] + require((value != UNSEEN) == all(columns), 'wrong state domain') + require(transpose(transpose(code)) == code, 'invalid coordinate conversion') + potential[code] = value + valid += int(all(columns)) + require(valid == VALID_STATES, 'wrong vertex count') + toggles = tuple(tuple(sum(((pattern >> atom) & 1) << (4 * atom + row) + for atom in range(4)) for pattern in range(16)) + for row in range(4)) + checked = 0 + for code in range(SIZE): + value = potential[code] + if value == UNSEEN: + continue + for donor in range(4): + active = sum(((code >> (4 * atom + donor)) & 1) << atom + for atom in range(4)) + for destination in range(4): + if donor == destination: + continue + for coefficient in range(16): + following = code ^ toggles[destination][active & coefficient] + other = potential[following] + require(other != UNSEEN, 'gate left primitive-column domain') + require(abs(value - other) <= 1, 'invalid edge potential') + checked += 1 + require(potential[0x1111] == 0, 'wrong start potential') + require(potential[0x8421] == 6, 'wrong target potential') + return {'bellman_edges_with_noops': checked, 'target_distance': 6} + + +def column_word(root: int) -> list[tuple[int, int, int]]: + require(0 <= root < 4, 'root outside four rows') + others = [j for j in range(4) if j != root] + return ([(j, root, 1 << j) for j in others] + + [(root, j, 1 << j) for j in others]) + + +def full_word(root: int) -> list[tuple[int, int, int]]: + suffix = column_word(root) + return list(reversed(suffix)) + [(root, -1, 15)] + suffix + + +def formal_endpoint(word: list[tuple[int, int, int]]) -> list[list[int]]: + """Five atoms include the unused complement; column four is the source.""" + rows = [[31 * int(i == j) for j in range(4)] + [0] for i in range(4)] + for destination, donor, coefficient in word: + require(0 <= destination < 4 and 0 < coefficient < 32, 'invalid gate') + if donor == -1: + rows[destination][4] ^= coefficient + else: + require(0 <= donor < 4 and donor != destination, 'invalid ADD') + rows[destination] = [a ^ (coefficient & b) + for a, b in zip(rows[destination], rows[donor], strict=True)] + return rows + + +def is_target(rows: list[list[int]]) -> bool: + return rows == [[31 * int(i == j) for j in range(4)] + [1 << i] + for i in range(4)] + + +def literal_checks(word: list[tuple[int, int, int]]) -> int: + """An independent bit interpreter covers every input on each atom.""" + count = 0 + for atom in range(5): + for bits in range(32): + data = [(bits >> j) & 1 for j in range(5)] + original = data[:] + for destination, donor, coefficient in word: + factor = (coefficient >> atom) & 1 + source = data[4] if donor == -1 else data[donor] + data[destination] = (data[destination] + factor * source) % 2 + wanted = original[:] + if atom < 4: + wanted[atom] ^= original[4] + require(data == wanted, 'literal dirty endpoint mismatch') + count += 1 + return count + + +def check_attainers(labels: bytearray) -> dict[str, int]: + literal = 0 + omitted = 0 + for root in range(4): + start = tuple(15 if row == root else 0 for row in range(4)) + state = list(start) + for destination, donor, coefficient in column_word(root): + state[destination] ^= state[donor] & coefficient + require(state == [1, 2, 4, 8], 'six-ADD column attainer failed') + require(labels[15] == 0 and labels[0x8421] == 6, 'wrong BFS endpoints') + word = full_word(root) + require(len(word) == 13, 'wrong complete word length') + require(is_target(formal_endpoint(word)), 'formal dirty restoration failed') + require(is_target(formal_endpoint(list(reversed(word)))), 'inverse failed') + literal += literal_checks(word) + literal_checks(list(reversed(word))) + for position in range(len(word)): + mutant = word[:position] + word[position + 1:] + require(not is_target(formal_endpoint(mutant)), 'omitted call accepted') + omitted += 1 + without_prefix = word[6:] + rows = formal_endpoint(without_prefix) + require([row[4] for row in rows] == [1, 2, 4, 8], 'source control failed') + require(not is_target(rows), 'unrestored dirt accepted') + wrong_generator = word[:] + wrong_generator[6] = (root, -1, 31) + require(not is_target(formal_endpoint(wrong_generator)), 'complement leak accepted') + return {'roots': 4, 'literal_atom_inputs': literal, 'omission_controls': omitted, + 'dirty_controls': 4, 'complement_controls': 4} + + +def corruption_controls(labels: bytearray) -> int: + for index, value, message in ((0x8421, 7, 'invalid edge potential'), + (0, 0, 'wrong state domain')): + corrupted = labels[:] + corrupted[index] = value + try: + check_potential(corrupted) + except ValueError as error: + require(str(error) == message, 'unexpected certificate failure') + else: + raise ValueError('corrupted certificate accepted') + try: + column_word(4) + except ValueError as error: + require(str(error) == 'root outside four rows', 'unexpected boundary failure') + else: + raise ValueError('invalid root accepted') + return 3 + + +def main() -> None: + output = None + if len(sys.argv) == 3 and sys.argv[1] == '--write-distances': + output = Path(sys.argv[2]).resolve() + repository = Path(__file__).resolve().parents[2] + require(not output.is_relative_to(repository), 'export must be outside checkout') + else: + require(len(sys.argv) == 1, 'usage: verify.py [--write-distances PATH]') + labels, graph = distances() + proof = check_potential(labels) + attainers = check_attainers(labels) + controls = corruption_controls(labels) + package = Path(__file__).resolve().parent + paths = ('README.md', 'PROOF.md', 'SOURCES.json', 'TASK.json', 'VERIFY.json', 'verify.py') + hashes = {name: hashlib.sha256((package / name).read_bytes()).hexdigest() for name in paths} + receipt = {'status': 'PASS_FOUR_ORTHOGONAL_ONE_INSERTION', 'graph': graph, + 'certificate': proof, 'attainers': attainers, 'other_controls': controls, + 'distance_sha256': hashlib.sha256(labels).hexdigest(), 'sources_sha256': hashes} + if output is not None: + with output.open('xb') as stream: + require(stream.write(labels) == SIZE, 'incomplete certificate export') + print(json.dumps(receipt, sort_keys=True)) + + +if __name__ == '__main__': + main()