diff --git a/research/weighted-pair-mask-tour/PROOF.md b/research/weighted-pair-mask-tour/PROOF.md new file mode 100644 index 0000000000..c092d1de18 --- /dev/null +++ b/research/weighted-pair-mask-tour/PROOF.md @@ -0,0 +1,141 @@ +# Exact weighted all-pair tours + +This proof and construction are produced by Nick Petalas. Apache-2.0. + +## Boundary and permitted schedules + +Fix an integer n >= 2 and positive real toggle prices c_1,...,c_n. All rows +are arbitrary elements of F2^L for any L >= 1. There is one anchor A, n +unchanged source rows B_i, and m_ij >= 1 independent dirty targets X_ij,k +for each unordered pair i= ... >= c_n > 0. Ties can be resolved +arbitrarily. The exact minimum transition cost is + + C = 2 c_1 + 2 sum_(i=2)^n (i-1)c_i. (1) + +The proof permits real prices. The executable accepts exact rational prices +for 2 <= n <= 64 and emits the schedule without numerical rounding. + +## Lower bound for every closed walk + +Represent the anchor by its mask in F2^n. Toggling bit i has price c_i, so +the shortest distance between masks x,y is their weighted Hamming distance + + d(x,y) = sum_i c_i [x_i != y_i]. + +Take any legal closed walk from zero. List the N=binom(n,2) required pair +masks in the order of their first designated target visit. Shortcut the +segments between these visits, including the initial and final segments, +by shortest Hamming paths. The triangle inequality gives a tour through +this permutation with cost no greater than the original walk. Extra mask +visits and early visits without a target write do not affect this argument. +Thus it suffices to lower-bound every permutation p_1,...,p_N of the pairs, +with zero before and after it. + +For each i let a_i count consecutive pairs p_t,p_(t+1) that both contain i. +Each pair containing i contributes c_i upon entry and c_i upon exit except +that two consecutive such pairs save 2c_i. There are n-1 pairs containing i, +so the shortcut tour costs exactly + + 2(n-1) sum_i c_i - 2 sum_i c_i a_i. (2) + +This identity includes disjoint consecutive pairs and both zero endpoints. + +For 1 <= k <= n let S_k={1,...,k}, and let V_k be the pair masks containing +at least one member of S_k. Their number is + + v_k = binom(n,2) - binom(n-k,2). + +Draw the path with vertices p_1,...,p_N and its N-1 consecutive edges. The +edges counted by sum_(i<=k) a_i lie in the subgraph on V_k. No edge is +counted twice, since two distinct two-element sets share at most one +coordinate. A subgraph of a path is a forest. Since v_k >= 1, it has at +most v_k-1 edges. Hence + + A_k := sum_(i<=k) a_i <= v_k-1. (3) + +Define b_1=n-2 and b_i=n-i for 2 <= i <= n. Direct summation gives +sum_(i<=k) b_i=v_k-1 for every k, including k=n. Put c_(n+1)=0. +Summation by parts and c_k-c_(k+1)>=0 give + + sum_i c_i a_i + = sum_(k=1)^n (c_k-c_(k+1)) A_k + <= sum_(k=1)^n (c_k-c_(k+1)) sum_(i<=k) b_i + = sum_i c_i b_i. + +Substituting into (2) yields (1). This is a bound on every original walk, +including those that repeat required masks or leave the weight-two layer. + +## An attaining schedule + +In sorted source order, visit pairs in this order: + + {1,n}, {1,n-1}, ..., {1,2}, + {2,n}, {2,n-1}, ..., {2,3}, + ..., + {n-1,n}. + +Use a shortest bit-toggle path between each consecutive pair, from zero to +the first pair, and from the last pair back to zero. At each designated +pair, write its anchor value once to each assigned target. The schedule +visits every pair exactly once as a designated visit. Intervening masks +need not be pairs. + +The first row of pairs has n-2 adjacent edges sharing coordinate 1. +For i>=2, the row with first coordinate i has n-i-1 internal edges, when +that number is nonnegative, and one incoming edge from the preceding row. +Thus the consecutive-pair counts are exactly + + (a_1,...,a_n) = (n-2,n-2,n-3,...,1,0) = (b_1,...,b_n). + +For n=2 there is one pair and no consecutive edge, giving (0,0) directly. +The lower bound is attained in all cases. Each target receives its +prescribed original-source parity. No B_i changes, and the final mask zero +restores the arbitrary initial A. This proves the full row map for every L. + +## Unit-price example and cost limits + +When every c_i=1, formula (1) is n(n-1)+2=2N+2. With t targets per pair, +the complete row ADD count is + + t N + n(n-1)+2. + +For n=4,t=2 this is 12+14=26. A direct implementation uses three source +ADDs per target, totaling 36. Separately preparing each pair on the anchor +and restoring it costs four transitions per pair plus the same 12 target +writes, also 36. The constructed local improvement is ten row ADDs, with +all source restoration included. At row width L these are 26L versus 36L +bit XORs and 26 versus 36 source-row reads and destination updates. Tape head travel and +frame conversion are outside this aligned row-register tariff. + +For prices (7,3,2,1), the exact transition optimum is 34. Independent +prepare/write/restore visits instead cost 2(n-1)sum_i c_i=78 in transitions. +Target prices are additional and identical in both schedules. + +## Evidence and obligations + +The written forest argument proves the quantified theorem. Independent +Held-Karp permutation optimization and literal hypercube-state Dijkstra +corroborate small rational/integer cases. Complete dirty-state enumeration, +full linear-map columns and wide-row executions corroborate the emitted +circuit. These finite computations do not substitute for the proof. + +The general weighted metric and forest inequalities are elementary tools, +not claimed as new methods. The contribution is the exact optimum and +attaining dirty-source circuit in the specified repository interface. +No source-pinned multiplier caller, legal physical layout, native frame +schedule, recursive invoice, supplier admission or multiplication theorem +is supplied. No independent human or formal proof-kernel review is claimed. diff --git a/research/weighted-pair-mask-tour/README.md b/research/weighted-pair-mask-tour/README.md new file mode 100644 index 0000000000..3a5f809fc9 --- /dev/null +++ b/research/weighted-pair-mask-tour/README.md @@ -0,0 +1,100 @@ +# Exact weighted borrowed-source pair tours + +Scoped proof with finite corroboration. For n >= 2 toggle sources and +positive prices sorted c1 >= ... >= cn, the minimum closed anchor tour +through every pair mask is + + 2c1 + 2 sum_(i=2)^n (i-1)ci. + +The optimum permits arbitrary intermediate masks and repeated visits. A +simple pair ordering attains it. Each dirty target is written once from the +borrowed source at its designated parity; all source rows are restored. +The [proof](PROOF.md) states the exact operation alphabet and lower bound. +This contribution is produced by Nick Petalas. + +For four toggle sources, unit prices and two targets per pair, the complete +map takes **26 row ADDs versus 36 direct ADDs**. This includes 14 anchor +toggles and 12 target writes. At row width L, it costs 26L rather than 36L +bit XORs. Unequal prices (7,3,2,1) give an exact transition cost of 34. +The optimization is within one-anchor schedules, with no other source +mixing and one write per target. It is not a global CNOT optimum. + +## Relation to prior work + +Cinna Davis's merged [PR #2271](https://github.com/CrocSwap/integer-mult-bounds/pull/2271) +introduced the borrowed-source mask-tour boundary, shared transitions, +exact restoration and a four-edge square example. Its Open next question 2 +asks for shortest tours through larger specified mask families. This result +answers that question for all two-element masks, with positive unequal +prices and an all-n minimum. The predecessor's example and verifier are +not replayed or claimed as new work. Its README is pinned as provenance +in [SOURCES.json](SOURCES.json). No predecessor code is imported. + +The `bit-helper-contract` assignment changes scope from R439 H2/K to this +explicit local row-register interface. This is a side result for shared +parity delivery. It does not discharge an R439 replacement lemma. Selected +κ=0.00302015 and all frontier files are unchanged. Native realization, +frames, actual caller occurrence, hosting, tape movement and recursive +charges remain unknown. No supplier or κ improvement is claimed. + +## Reproduce + +From the repository root with CPython 3.12 and standard library only: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/weighted-pair-mask-tour +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -B research/weighted-pair-mask-tour/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -O -B research/weighted-pair-mask-tour/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/weighted-pair-mask-tour --check-source-history +``` + +Expected direct status is `PASS_WEIGHTED_PAIR_MASK_TOUR`. The independent +permutation oracle and the literal hypercube-state oracle optimize different +state spaces. The latter permits off-layer masks and repeated visits. +Exact basis columns, complete one-bit dirty states and 73-bit row fixtures +check the output map and restoration. Controls reject bad prices, incomplete +tours, wrong visits, malformed row references and altered circuits; a legal +expensive order distinguishes price priority from feasibility. Every runtime +check remains active under Python optimization. + +The optional `--receipt NEW_PATH` creates a generated receipt after success, +bound to SHA256 hashes of the package files. It refuses an occupied path. +Normal verification writes no file and requires no Git, network or external +package. The mathematical theorem permits all n and positive real prices; +the constructor is bounded to n<=64 and rational prices, the full circuit to +at most eight targets per pair. Finite oracle domains are explicit in code. + +## Open next questions + +- Find one actual aligned caller requiring all pair parities at the same + cut. Begin with its exact source/target demand and frames, then price + references, restoration, physical storage and tape movement. Without a + caller there is no claimed supplier consequence. +- If a caller needs only a subset of pairs, determine its weighted optimum. + Start with that actual demand graph. The complete-pair forest bounds used + here need not be sharp after pairs are deleted. + +## Scope and credit + +The base is canonical main `624de9dc66858af0945e5f8a0942488d62280d43`, +priority revision 7. The advance [CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19134289) +records the exact question. Open PR bodies, recent account contributions, +current handoffs, main README terms and merged PR searches were consulted. +The cached scan covered 412 open PRs and 3,928 Discussion records at about +23:07 UTC on October 22, 2026. Sparse local-note coverage was incomplete; +main Git searches supplied separate object/formula checks. These searches +exclude unpublished work and do not prove novelty. + +Cinna Davis retains credit for PR2271 and its predecessor lineage. General +weighted Hamming metrics, shortcutting, forest edge bounds and dynamic +programming are standard tools. The new theorem, constructor, written proof +and independent finite oracles are produced by Nick Petalas. Independent +human and formal proof-kernel review are unclaimed. Apache-2.0. + +The Python code uses bounded source/gate domains, finite oracle state spaces, +explicit exceptions and direct calls without recursion. Python and its exact +arithmetic libraries allocate dynamically; the bounded verifier is not a +fixed-allocation implementation. Large-number bit complexity is not bounded +by the row-count limits. Warning-strict normal and optimized replay provide +the available interpreter diagnostics; no whole-repository linter or formal +kernel check is claimed. diff --git a/research/weighted-pair-mask-tour/SOURCES.json b/research/weighted-pair-mask-tour/SOURCES.json new file mode 100644 index 0000000000..5a267e5703 --- /dev/null +++ b/research/weighted-pair-mask-tour/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/borrowed-source-gray-mask-fanout-seed9b2fe133/README.md", + "usage": "provenance", + "git_blob": "32c2ea04e8e25c5a199861d8e0906127ffd9a5ce", + "sha256": "fb81510e09747ea2917318d23b667edaca28e09535b9a833e221672b9910f8f4" + } + ] +} diff --git a/research/weighted-pair-mask-tour/TASK.json b/research/weighted-pair-mask-tour/TASK.json new file mode 100644 index 0000000000..12ccef6422 --- /dev/null +++ b/research/weighted-pair-mask-tour/TASK.json @@ -0,0 +1,67 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "original_card": { + "id": "bit-helper-contract", + "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/r439-bsection-stars-seed01/README.md", + "research/r439-copy-path-sharing-barrier/README.md" + ], + "methods": [ + "Derive a replacement interface lemma and price its implementation.", + "Seek an exact dirty-input or chronological-cut counterexample to the proposed replacement." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.", + "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.", + "allowed_variations": [ + "Choose one helper-star or quartet instance; narrow to one boundary implication." + ], + "scope_change_triggers": [ + "Changing only source count or scalar addition count without an interface argument." + ], + "overlap_terms": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D", + "helper-star" + ] + }, + "scope_status": "changed", + "actual_scope": "Exact minimum weighted closed borrowed-anchor tour through all pair masks, with arbitrary intermediate masks and exact dirty-source restoration.", + "scope_change_reason": "Take Cinna Davis PR2271 Open next question 2 as a local row-register side result rather than an R439 H2/K replacement lemma.", + "bottleneck_link": "Shared transitions reduce a completely restored parity-delivery word; actual caller, physical frames, tape costs and recursive admission remain unknown.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved original optimum; package it without extending the mask family.", + "outcome": "completed", + "evidence": "PROOF.md; tour.py; verify.py independent optimization and full dirty-boundary checks.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does an actual aligned caller require this complete pair-mask family?", + "why_it_matters": "Only a priced actual caller can establish supplier relevance.", + "first_step": "Pin one caller and extract its source/target parity demands and frames.", + "blocked_by": "No caller occurrence or physical cost contract is supplied." + }, + { + "question": "What is the exact weighted optimum for a caller-specific incomplete pair family?", + "why_it_matters": "A sparse demand graph could change the useful transition sharing.", + "first_step": "Extract the actual required pair graph, then compare exact small tours with forest bounds.", + "blocked_by": "A concrete caller demand and legal transition prices are needed." + } + ] +} diff --git a/research/weighted-pair-mask-tour/VERIFY.json b/research/weighted-pair-mask-tour/VERIFY.json new file mode 100644 index 0000000000..1685d931b7 --- /dev/null +++ b/research/weighted-pair-mask-tour/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact weighted oracles, complete dirty-state/basis maps, restoration and rejection controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat all scientific checks with Python assertions disabled." + } + ] +} diff --git a/research/weighted-pair-mask-tour/tour.py b/research/weighted-pair-mask-tour/tour.py new file mode 100644 index 0000000000..fb301c4410 --- /dev/null +++ b/research/weighted-pair-mask-tour/tour.py @@ -0,0 +1,112 @@ +"""Exact weighted borrowed-anchor pair tours. Produced by Nick Petalas; Apache-2.0.""" +from fractions import Fraction +from itertools import combinations + +MAX_SOURCES = 64 +MAX_COPIES = 8 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def prices(values): + require(isinstance(values, (list, tuple)), "prices must be a list or tuple") + require(2 <= len(values) <= MAX_SOURCES, "source count must be in [2,64]") + require(all(type(x) is int or type(x) is Fraction for x in values), + "prices must be exact integers or Fractions, excluding booleans") + require(all(x > 0 for x in values), "prices must be positive") + return tuple(Fraction(x) for x in values) + + +def minimum_cost(values): + weights = sorted(prices(values), reverse=True) + return 2 * weights[0] + 2 * sum( + i * weight for i, weight in enumerate(weights[1:], 1)) + + +def pair_order(values): + weights = prices(values) + order = sorted(range(len(weights)), key=lambda i: (-weights[i], i)) + return tuple((order[i], order[j]) for i in range(len(order) - 1) + for j in range(len(order) - 1, i, -1)) + + +def transitions(start, end, n): + """Shortest mask path; each returned integer selects one toggle source.""" + return tuple(i for i in range(n) if ((start ^ end) >> i) & 1) + + +def tour_events(values): + """Events are ('toggle', source index) or ('visit', two-bit mask).""" + weights = prices(values) + current = 0 + events = [] + for i, j in pair_order(weights): + target = (1 << i) | (1 << j) + events.extend(("toggle", k) for k in transitions(current, target, len(weights))) + events.append(("visit", target)) + current = target + events.extend(("toggle", k) for k in transitions(current, 0, len(weights))) + return tuple(events) + + +def checked_tour_cost(values, events): + """Validate a complete possibly nonminimal tour and return its literal bill.""" + weights = prices(values) + require(isinstance(events, (list, tuple)) and len(events) <= 100_000, + "events must be a bounded sequence") + required = {(1 << i) | (1 << j) for i, j in combinations(range(len(weights)), 2)} + visited = set() + current = 0 + cost = Fraction(0) + for event in events: + require(isinstance(event, tuple) and len(event) == 2, "bad event") + kind, value = event + require(type(value) is int, "event value must be an integer") + if kind == "toggle": + require(0 <= value < len(weights), "unknown toggle source") + current ^= 1 << value + cost += weights[value] + else: + require(kind == "visit" and value == current and value in required, + "visit is not its required current pair mask") + visited.add(value) + require(current == 0, "anchor not restored") + require(visited == required, "missing pair mask") + return cost + + +def circuit(values, copies=2): + """A is row 0, B_i is row i+1; targets follow in lexicographic pair order.""" + weights = prices(values) + require(type(copies) is int and 1 <= copies <= MAX_COPIES, + "copies must be an integer in [1,8]") + pairs = tuple(combinations(range(len(weights)), 2)) + targets = {(1 << i) | (1 << j): tuple( + len(weights) + 1 + p * copies + k for k in range(copies)) + for p, (i, j) in enumerate(pairs)} + gates = [] + for kind, value in tour_events(weights): + if kind == "toggle": + gates.append((0, value + 1)) + else: + gates.extend((target, 0) for target in targets[value]) + return tuple(gates), len(weights) + 1 + copies * len(pairs) + + +def execute(gates, rows): + """Literal XOR execution on arbitrary-width dirty row values.""" + require(isinstance(rows, (list, tuple)) and 1 <= len(rows) <= 17_000, + "bad row bank") + require(all(type(x) is int and x >= 0 for x in rows), "rows must be unsigned integers") + require(isinstance(gates, (list, tuple)) and len(gates) <= 100_000, "bad gate count") + state = list(rows) + for gate in gates: + require(isinstance(gate, tuple) and len(gate) == 2, "bad gate") + dst, src = gate + require(type(dst) is int and type(src) is int and dst != src + and 0 <= dst < len(state) and 0 <= src < len(state), "bad row reference") + state[dst] ^= state[src] + return tuple(state) diff --git a/research/weighted-pair-mask-tour/verify.py b/research/weighted-pair-mask-tour/verify.py new file mode 100644 index 0000000000..661d163d2a --- /dev/null +++ b/research/weighted-pair-mask-tour/verify.py @@ -0,0 +1,211 @@ +#!/usr/bin/env python3 +"""Standalone exact corroboration. Produced by Nick Petalas; Apache-2.0.""" +import argparse +from fractions import Fraction +import hashlib +from heapq import heappop, heappush +from itertools import combinations, product +import json +from pathlib import Path +import sys + +# Script-local imports also work under -I and in a Git-free export. +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from tour import checked_tour_cost, circuit, execute, minimum_cost, tour_events + + +def check(condition, message): + if not condition: + raise ValueError(message) + + +def distance(a, b, weights): + return sum(weight for i, weight in enumerate(weights) if ((a ^ b) >> i) & 1) + + +def permutation_oracle(weights): + """Held-Karp over pair masks, independent of the claimed formula/order.""" + check(2 <= len(weights) <= 5, "oracle source bound") + masks = tuple((1 << i) | (1 << j) for i, j in combinations(range(len(weights)), 2)) + size = len(masks) + table = {(1 << i, i): distance(0, mask, weights) for i, mask in enumerate(masks)} + for seen in range(1, 1 << size): + for last in range(size): + previous = table.get((seen, last)) + if previous is None: + continue + for nxt in range(size): + if (seen >> nxt) & 1: + continue + key = (seen | (1 << nxt), nxt) + cost = previous + distance(masks[last], masks[nxt], weights) + if key not in table or cost < table[key]: + table[key] = cost + return min(table[(1 << size) - 1, last] + distance(mask, 0, weights) + for last, mask in enumerate(masks)) + + +def cube_oracle(weights): + """Dijkstra on (actual anchor mask, masks seen), including off-layer states.""" + n = len(weights) + check(2 <= n <= 4, "cube oracle source bound") + required = tuple((1 << i) | (1 << j) for i, j in combinations(range(n), 2)) + marked = {mask: 1 << i for i, mask in enumerate(required)} + done = (1 << len(required)) - 1 + queue = [(0, 0, 0)] + best = {(0, 0): 0} + maximum_pops = 1 + n * (1 << n) * (1 << len(required)) + for _ in range(maximum_pops): + check(bool(queue), "shortest-path queue unexpectedly exhausted") + cost, mask, seen = heappop(queue) + if best.get((mask, seen)) != cost: + continue + if mask == 0 and seen == done: + return cost + for i in range(n): + nxt = mask ^ (1 << i) + key = (nxt, seen | marked.get(nxt, 0)) + candidate = cost + weights[i] + if key not in best or candidate < best[key]: + best[key] = candidate + heappush(queue, (candidate, *key)) + raise ValueError("Dijkstra exceeded its finite edge-relaxation bound") + + +def weighted_checks(): + counts = {"permutation_oracles": 0, "literal_cube_oracles": 0, "large_tours": 0} + for n in range(2, 5): + for weights in product(range(1, 4), repeat=n): + predicted = minimum_cost(weights) + check(permutation_oracle(weights) == predicted, "permutation minimum disagrees") + check(cube_oracle(weights) == predicted, "arbitrary-mask minimum disagrees") + check(checked_tour_cost(weights, tour_events(weights)) == predicted, "tour bill") + counts["permutation_oracles"] += 1 + counts["literal_cube_oracles"] += 1 + for weights in [(1, 1, 1, 1, 1), (9, 2, 7, 1, 3), (1, 3, 2, 5, 4), + (Fraction(1, 3), Fraction(7, 2), Fraction(2, 5), Fraction(1, 7), 2)]: + check(permutation_oracle(weights) == minimum_cost(weights), "five-source oracle") + counts["permutation_oracles"] += 1 + for n in range(2, 65): + families = [tuple(1 for _ in range(n)), tuple(range(1, n + 1)), + tuple(Fraction(1 + (7 * i) % 13, 1 + i % 5) for i in range(n))] + for weights in families: + events = tour_events(weights) + check(checked_tour_cost(weights, events) == minimum_cost(weights), "large bill") + check(sum(kind == "toggle" for kind, _ in events) == n * (n - 1) + 2, + "wrong complete toggle count") + counts["large_tours"] += 1 + return counts + + +def reference(rows, n, copies): + """Requested simultaneous boundary, using the original input rows only.""" + expected = list(rows) + for p, (i, j) in enumerate(combinations(range(n), 2)): + for k in range(copies): + target = n + 1 + p * copies + k + expected[target] ^= rows[0] ^ rows[i + 1] ^ rows[j + 1] + return tuple(expected) + + +def circuit_checks(): + counts = {"basis_columns": 0, "complete_dirty_states": 0, "wide_dirty_states": 0} + for n in range(2, 9): + for copies in range(1, 4): + weights = tuple(1 + (3 * i) % 7 for i in range(n)) + gates, size = circuit(weights, copies) + for column in range(size): + rows = tuple(int(i == column) for i in range(size)) + result = execute(gates, rows) + check(result == reference(rows, n, copies), "full boundary column") + check(execute(tuple(reversed(gates)), result) == rows, "inverse column") + counts["basis_columns"] += 1 + for seed in range(8): + rows = tuple(((i + 11) * (seed + 37) * 0x123456789ABCDEF) % (1 << 73) + for i in range(size)) + check(execute(gates, rows) == reference(rows, n, copies), "wide dirty boundary") + counts["wide_dirty_states"] += 1 + for n, copies in [(2, 2), (3, 2), (4, 2)]: + gates, size = circuit((1,) * n, copies) + for bits in range(1 << size): + rows = tuple((bits >> i) & 1 for i in range(size)) + check(execute(gates, rows) == reference(rows, n, copies), "exhaustive dirty boundary") + counts["complete_dirty_states"] += 1 + gates, _ = circuit((1, 1, 1, 1), 2) + check(len(gates) == 26, "four-source invoice") + direct = tuple((5 + 2 * p + k, source) + for p, (i, j) in enumerate(combinations(range(4), 2)) + for k in range(2) for source in (0, i + 1, j + 1)) + check(len(direct) == 36, "direct invoice") + for column in range(17): + rows = tuple(int(i == column) for i in range(17)) + check(execute(direct, rows) == reference(rows, 4, 2), "direct baseline boundary") + check(minimum_cost((7, 3, 2, 1)) == 34, "weighted example") + return counts + + +def rejection_checks(): + cases = [lambda: minimum_cost((1,)), lambda: minimum_cost((1,) * 65), + lambda: minimum_cost((1, 0)), lambda: minimum_cost((1, -1)), + lambda: minimum_cost((True, 1)), lambda: minimum_cost((1.0, 1)), + lambda: minimum_cost("12"), lambda: circuit((1, 1), True), + lambda: circuit((1, 1), 0), lambda: circuit((1, 1), 9), + lambda: execute(((0, 0),), (1, 0)), + lambda: execute(((2, 0),), (1, 0)), + lambda: execute(((0, 1),), (True, 0))] + for case in cases: + try: + case() + except ValueError: + continue + raise ValueError("invalid-input control did not reject") + events = tour_events((7, 3, 2, 1)) + mutants = [events[:-1], tuple(event for event in events if event != ("visit", 3)), + (("visit", 3),) + events, (("toggle", 4),) + events] + for mutant in mutants: + try: + checked_tour_cost((7, 3, 2, 1), mutant) + except ValueError: + continue + raise ValueError("corrupted-tour control did not reject") + gates, size = circuit((1, 1, 1, 1), 2) + for mutant in [gates[:-1], gates[1:], tuple(g for g in gates if g != (5, 0))]: + check(any(execute(mutant, tuple(int(i == c) for i in range(size))) + != reference(tuple(int(i == c) for i in range(size)), 4, 2) + for c in range(size)), "faulty circuit escaped the boundary oracle") + # Reversed price priority is a legal tour but strictly worse for these prices. + bad = tour_events((1, 2, 3, 7)) + check(checked_tour_cost((7, 3, 2, 1), bad) > minimum_cost((7, 3, 2, 1)), + "price-order control") + return {"invalid_inputs": len(cases), "tour_corruptions": len(mutants), + "circuit_corruptions": 3, "suboptimal_price_order": 1} + + +def run(): + result = {"status": "PASS_WEIGHTED_PAIR_MASK_TOUR", "claim_type": "scoped proof with finite corroboration", + **weighted_checks(), **circuit_checks(), **rejection_checks(), + "unit_example": {"sources": 4, "targets_per_pair": 2, "transition_adds": 14, + "target_adds": 12, "complete_adds": 26, "direct_adds": 36}, + "weighted_example_cost": "34"} + return result + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path, help="write a new source-bound receipt after success") + args = parser.parse_args() + result = run() + if args.receipt is not None: + root = Path(__file__).resolve().parent + names = ("PROOF.md", "README.md", "SOURCES.json", "TASK.json", "VERIFY.json", + "tour.py", "verify.py") + hashes = {name: hashlib.sha256((root / name).read_bytes()).hexdigest() + for name in names} + receipt = {"schema": "weighted-pair-mask-tour/1", "files_sha256": hashes, "result": result} + with args.receipt.open("x", encoding="utf-8") as output: + output.write(json.dumps(receipt, indent=2, sort_keys=True) + "\n") + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()