From 19a139b0f6de2ecf2cd3d931d7193f85ec4023ab Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Mon, 2 Nov 2026 22:23:43 +0000 Subject: [PATCH] feat(research): prove exact fixed-weight borrowed-source tours --- research/fixed-weight-borrowed-tours/PROOF.md | 125 ++++++++ .../fixed-weight-borrowed-tours/README.md | 124 ++++++++ .../fixed-weight-borrowed-tours/SOURCES.json | 25 ++ .../fixed-weight-borrowed-tours/TASK.json | 120 ++++++++ .../fixed-weight-borrowed-tours/VERIFY.json | 34 +++ .../fixed-weight-borrowed-tours/verify.py | 278 ++++++++++++++++++ 6 files changed, 706 insertions(+) create mode 100644 research/fixed-weight-borrowed-tours/PROOF.md create mode 100644 research/fixed-weight-borrowed-tours/README.md create mode 100644 research/fixed-weight-borrowed-tours/SOURCES.json create mode 100644 research/fixed-weight-borrowed-tours/TASK.json create mode 100644 research/fixed-weight-borrowed-tours/VERIFY.json create mode 100644 research/fixed-weight-borrowed-tours/verify.py diff --git a/research/fixed-weight-borrowed-tours/PROOF.md b/research/fixed-weight-borrowed-tours/PROOF.md new file mode 100644 index 0000000000..6bb0b1f805 --- /dev/null +++ b/research/fixed-weight-borrowed-tours/PROOF.md @@ -0,0 +1,125 @@ +# Exact restored tours through one mask layer + +This scoped proof was produced by Nick Petalas. Apache-2.0. + +## Boundary and charged alphabet + +Fix n>=1 and 0<=k<=n. There is one borrowed anchor A, source rows +B_1,...,B_n, and arbitrary target rows X_(S,j). Every row is an arbitrary +element of F_2^L, for any L>=1. There is at least one target for each +k-element subset S of {1,...,n}; its multiplicity r_S is a positive integer. +The required map is + + X_(S,j) <- X_(S,j) + A + sum_(i in S) B_i. + +All source rows, including A, must return to their exact input values. +Let R=sum_S r_S and N=binomial(n,k). + +The permitted word toggles A by one unchanged B_i and writes each target +exactly once by adding the current A. No other mixing or workspace is +allowed. Every toggle and every write costs one row ADD. Intermediate +anchor masks and repeated visits are unrestricted. In particular the +anchor is arbitrary dirty data, not a zero-initialized accumulator. + +The target identities are quantified over all input rows. Thus a write +to X_(S,j) must occur when A's source mask is exactly S. Equality at a +particular numerical input would not suffice. The independent coefficient +of A stays one throughout the permitted word. + +## Theorem + +For 1<=k<=n, the minimum number of anchor toggles is + + T(n,k) = 2 binomial(n,k) + 2k - 2. + +The minimum complete row-ADD count in this alphabet is R+T(n,k). +For k=0 the corresponding counts are zero toggles and R writes. +No optimum over unrestricted CNOT circuits is claimed. + +The application to every k>=3 is the new part of the fixed-weight-layer +tariff here. The k=2 specialization, including unequal positive prices, +is already covered by Nick Petalas / PR4899. The k=1 and k=n endpoint +cases are elementary and included to state the uniform formula. + +## Lower bound, including arbitrary repeated visits + +View the anchor mask as a vertex of the n-cube. Each toggle crosses one +cube edge. The word is a walk starting and ending at the empty mask and +visiting all N required masks. + +Order the required masks by their first visits, S_1,...,S_N. The part of +the walk up to S_1 has length at least k. Each disjoint segment from the +first visit to S_i to the first visit to S_(i+1) has length at least two, +since distinct masks of the same weight have Hamming distance at least +two. The remaining segment from the first visit to S_N to the final empty +mask has length at least k. These segments partition the entire walk. +Consequently its length is at least + + k + 2(N-1) + k = 2N+2k-2. + +The argument permits every off-layer excursion, every repeated mask and +any ordering of target writes. The exactly R target writes add R to the +bound. For k=0, the unmodified anchor already has the required parity. + +## An attaining fixed-weight listing + +For completeness the classical reflected Gray construction is proved here. +Let G(n,k) be the binary reflected Gray list on n bits, with all entries +of weights other than k deleted. In integer notation the unfiltered list +is i XOR floor(i/2), for i=0,...,2^n-1. Its reflected definition gives + + G(n,k) = G(n-1,k), then 2^(n-1) + reverse(G(n-1,k-1)), + +where out-of-range lists are empty. For k=0 or k=n there is a single +entry. The recurrence lists every weight-k mask exactly once. + +For 1<=k<=n its first entry is 2^k-1 and its last entry is +2^(n-1)+2^(k-1)-1. This follows by induction from the two blocks; +the singleton k=n case has the same endpoints. + +For 1<=k=1 +and 1<=k<=n, a borrowed arbitrary source row can visit every weight-k mask +of n unchanged source rows and return to its input with exactly + + 2 binomial(n,k) + 2k - 2 + +source toggles. This is optimal among closed one-anchor schedules, even +with arbitrary intermediate masks and repeated visits. If the targets +number R, each requiring the anchor plus its designated source parity, +their complete cost is R plus this transition count. Every target is +written once and all source rows are restored. The k=0 cost is R. + +For n=5, k=3 and one target per mask, the complete circuit costs **34 row +ADDs versus 40 direct ADDs**. The six-ADD reduction includes preparation +and restoration. At row width L these are 34L versus 40L bit XORs. +[PROOF.md](PROOF.md) gives the exact boundary, lower bound and constructor. +This is a local row-register result, with no new kappa or supplier admission. + +## Predecessors and new scope + +Cinna Davis / [PR2271](https://github.com/CrocSwap/integer-mult-bounds/pull/2271) +introduced the borrowed-source multi-mask interface and asked in Open next +question 2 for shortest tours through higher-dimensional mask families. +This result answers that question for every complete fixed-weight layer. +The application to k>=3 is the new contribution here. Nick Petalas / +[PR4899](https://github.com/CrocSwap/integer-mult-bounds/pull/4899) already +proves the k=2 case with unequal positive source prices; that specialization +is credited rather than claimed as new. The reflected Gray construction +and Hamming-distance tools are classical and are proved here for completeness. + +Ali Romman / [PR5372](https://github.com/CrocSwap/integer-mult-bounds/pull/5372) +proves an all-nonempty-mask optimum with a paid clean-row contract. The +present masks all have one fixed weight, and the anchor is an arbitrary +borrowed source. No predecessor scientific verifier is imported or replayed. +The source question and original card are pinned as historical provenance +in [SOURCES.json](SOURCES.json); the standalone verifier has no live input +outside this six-file package. + +The `bit-helper-contract` card changes scope from a selected G20 helper +trajectory to this explicit row-register side result. It supplies neither +a G20 target split nor a complete BIT moment. Native frames, physical +access, storage, tape movement, an actual caller and recursive charges +remain unknown. The selected PR6030 conditional kappa stays 0.003125804. +The source-binding baseline passed; its scientific cold replay was not run. + +## Reproduce + +From the repository root, with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/fixed-weight-borrowed-tours/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/fixed-weight-borrowed-tours/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/fixed-weight-borrowed-tours +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/fixed-weight-borrowed-tours --check-source-history --check-modes +``` + +Another CPython 3.12 path may replace the displayed interpreter. The last +command requires committed package bytes and full Git history. Direct +verification also works in a Git-free export and writes no file. Its stdout +is a generated receipt bound to the SHA256 of all six package files. +Expected status is `PASS_FIXED_WEIGHT_BORROWED_TOURS_NO_NEW_KAPPA`. +Both registered modes use explicit guards that stay active under `-O`. + +Exact evidence covers 90 layers and 8,190 required masks through n=12; +20 independent full-cube covering-walk optima through n=5; 132 complete +arbitrary-input circuits through n=8, with one to three targets per mask; +301,288 coefficient positions; 532 dirty-data cases, including 400 +exhaustive one-bit states and 132 wide-row fixtures; and 132 inverse +executions. Eighteen rejection controls cover malformed domains, missing +masks, failed restoration, illegal gates, excess costs and an equal-length +semantic mutation. The 20 BFS runs discover 58,616 states in total, counting +each run's distinct state set separately. These finite checks corroborate +the written proof; they do not establish its unbounded quantifiers. + +## Open next questions + +1. Find a source-pinned caller that needs one complete fixed-weight parity + layer at an aligned cut. Begin with the exact source and target demands, + then price native frames, storage, references, routing and restoration. + A caller is the missing link to a supplier consequence. +2. For a specified caller with unequal source prices and k>=3, determine + its exact restored tariff. Begin with the small weighted covering-walk + instance. The unweighted Gray listing is not asserted to be optimal + for those prices. No physical price vector is supplied here. + +The structured relevance, first steps and blockers are in [TASK.json](TASK.json). +Neither follow-on question is reserved by this contribution. + +## Limits, overlap and implementation constraints + +Base is canonical main `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority +revision 8. The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19361665) +preceded substantial work. Live open PRs, recent account contributions, +active Discussions, local target locks, main README terms and merged +fixed-weight/mask-tour searches were checked. Sparse local notes and +unpublished work limit overlap coverage; these searches do not establish +global literature priority. The package gives a self-contained proof. + +The theorem requires exactly this one-anchor, one-write-per-target alphabet. +It is not an unrestricted CNOT minimum, a physical tape tariff, a native +implementation, supplier admission or a complete multiplication theorem. +Independent human and formal proof-kernel review are unclaimed. Lean, +Docker, full selected replay and all-size implementation checks were not run. + +The verifier retains a deterministic constructor, an independent shortest-walk +oracle, full dirty coefficient-map checks and inverse execution. +Its eighteen functions are at most 38 physical lines. There is no subprocess, +network, dynamic code, callback dispatch or file-write path. Loops are bounded +by n<=12 for listings, n<=5 for BFS and n<=8 with multiplicity<=3 for circuits. +The BFS has at most 32,768 states, circuits at most 219 rows and 356 gates, +and receipts read six files with a 128-KiB limit each. + +Power of Ten rule 3 deviation applies to `verify.py`: CPython allocates +managed integers and containers during execution. Fixed domains, explicit +state/circuit capacities and bounded receipt reads limit live collections; +this is not a fixed-allocation implementation. A fixed-allocation port +would be needed before embedded or real-time use. All remaining contracts +use explicit exceptions. Warning-strict normal and optimized replay plus +in-memory AST compilation provide the available interpreter diagnostics; +no external static analyzer or formal kernel was run. diff --git a/research/fixed-weight-borrowed-tours/SOURCES.json b/research/fixed-weight-borrowed-tours/SOURCES.json new file mode 100644 index 0000000000..fdb2051fc4 --- /dev/null +++ b/research/fixed-weight-borrowed-tours/SOURCES.json @@ -0,0 +1,25 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/borrowed-source-gray-mask-fanout-seed9b2fe133/README.md", + "usage": "provenance", + "git_blob": "32c2ea04e8e25c5a199861d8e0906127ffd9a5ce", + "sha256": "fb81510e09747ea2917318d23b667edaca28e09535b9a833e221672b9910f8f4" + } + ], + "notes": "PR2271 README and its exact open question are historical provenance only. No predecessor scientific verifier is imported or replayed." +} diff --git a/research/fixed-weight-borrowed-tours/TASK.json b/research/fixed-weight-borrowed-tours/TASK.json new file mode 100644 index 0000000000..9485c66597 --- /dev/null +++ b/research/fixed-weight-borrowed-tours/TASK.json @@ -0,0 +1,120 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "bit-helper-contract", + "question": "Can a changed G20 helper path or independent-target split improve the complete BIT moment without losing its physical endpoint?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "research/g20-helper-split/README.md", + "research/g20-conjugation-admission/README.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "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", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "First read #5679/#5708 and their audits as pending component proposals. Choose one uncovered helper group/cut on an exact word; compare arbitrary-input native action, targets, owned storage, both orientations and full signed bill. Stop if the gain is only a scalar count or repaid by lost targets. Do not rerun the frozen #5609 common-frame domain without changing its hypothesis.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "G20", + "helper split", + "5679", + "5708", + "independent target" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact restored one-anchor Hamming-tour tariff for every fixed-weight source-mask layer, with arbitrary dirty rows and one designated anchor write per target.", + "scope_change_reason": "Take PR2271 Open next question 2 instead of extending the selected G20 word. This is a local row-register side result and supplies no G20 physical split or complete BIT moment.", + "bottleneck_link": "Side result for shared parity delivery with exact dirty-source restoration. A caller, native frames, physical access and recursive price remain unknown; no selected assumption is discharged.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved and boundedly checked exact tariff; package it without extending to unequal prices or new mask families.", + "outcome": "completed", + "evidence": "PROOF.md gives the all-n, all-k proof; verify.py independently checks unrestricted hypercube walks through n=5, exact coefficient circuits, dirty data and rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a source-pinned caller use a complete fixed-weight parity layer at one aligned cut?", + "why_it_matters": "Only an actual caller and full invoice could turn this row-register tariff into a supplier consequence.", + "first_step": "Identify its source/target demand and bind all input/output rows and frames before pricing native operations, storage, routing and restoration.", + "blocked_by": "No such source-bound caller or physical cost law is supplied here." + }, + { + "question": "What is the exact restored tariff for a specified nonuniform source-price vector and a fixed-weight layer k>=3?", + "why_it_matters": "The Hamming-distance lower bound does not price which coordinates toggle.", + "first_step": "Start with an actual caller price vector and solve its bounded weighted covering-walk instance; do not assume the unweighted Gray listing is optimal.", + "blocked_by": "A specified caller and its positive physical source prices." + } + ], + "claim_type": "Scoped mathematical proof with exact finite corroboration.", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19361665", + "playbook": "Autonomous local run", + "environment": { + "interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12", + "python_version": "3.12.15", + "dependencies": "standard library only" + }, + "predecessors": [ + { + "pr": 2271, + "author": "1337isnot1337", + "contribution": "Borrowed-source mask-tour interface, restoration contract and Open next question 2." + }, + { + "pr": 4899, + "author": "petalas", + "contribution": "Earlier exact positive weighted pair-layer tariff; its k=2 specialization is credited, not new." + }, + { + "pr": 5372, + "author": "aliromman", + "contribution": "Related all-nonempty-mask optimum under a different paid clean-row contract; not used as a proof premise." + } + ], + "overlap": { + "upstream_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "priority_revision": 8, + "checked_at": "2026-11-02T22:23:28.732951+00:00", + "cached_open_prs": 371, + "cached_discussion_records": 6295, + "remote_pagination_complete": true, + "local_notes_complete": false, + "source": "PR2271 Open next question 2", + "new_scope": "fixed-weight layers k>=3; k=2 is credited to PR4899", + "recent_related_pr": "PR6393 uses separate dirty borrowed rows and multilinear evaluation, rather than this linear one-anchor ADD boundary." + } +} diff --git a/research/fixed-weight-borrowed-tours/VERIFY.json b/research/fixed-weight-borrowed-tours/VERIFY.json new file mode 100644 index 0000000000..52f6d0239f --- /dev/null +++ b/research/fixed-weight-borrowed-tours/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact fixed-weight layer and tariff checks, independent full hypercube shortest walks, arbitrary-dirty linear circuits, domain and semantic rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same exact checks with assertions disabled; explicit mathematical guards must remain active." + } + ] +} diff --git a/research/fixed-weight-borrowed-tours/verify.py b/research/fixed-weight-borrowed-tours/verify.py new file mode 100644 index 0000000000..b4bf680649 --- /dev/null +++ b/research/fixed-weight-borrowed-tours/verify.py @@ -0,0 +1,278 @@ +#!/usr/bin/env python3 +"""Exact finite evidence for fixed-weight tours. Produced by Nick Petalas. + +Apache-2.0. Standard library only. Universal claims rest on PROOF.md. +""" + +from collections import deque +from hashlib import sha256 +from itertools import combinations +import json +from math import comb +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def domain(n, k, limit=12): + require(type(n) is int and type(k) is int, "integer dimensions required") + require(1 <= n <= limit and 0 <= k <= n, "dimension outside finite domain") + + +def tariff(n, k): + domain(n, k) + return 0 if k == 0 else 2 * comb(n, k) + 2 * k - 2 + + +def gray_layer(n, k): + domain(n, k) + return tuple(i ^ (i >> 1) for i in range(1 << n) + if (i ^ (i >> 1)).bit_count() == k) + + +def layer_set(n, k): + domain(n, k) + return {sum(1 << j for j in positions) + for positions in combinations(range(n), k)} + + +def expand_walk(n, k, listing): + domain(n, k) + require(len(listing) == comb(n, k), "wrong layer size") + require(set(listing) == layer_set(n, k), "wrong layer masks") + current = 0 + walk = [0] + for target in (*listing, 0): + difference = current ^ target + for bit in range(n): + if difference & (1 << bit): + current ^= 1 << bit + walk.append(current) + return tuple(walk) + + +def check_walk(n, k, walk): + domain(n, k) + require(1 <= len(walk) <= n * (comb(n, k) + 1) + 1, "walk capacity") + require(walk[0] == walk[-1] == 0, "anchor must return") + require(all(type(x) is int and 0 <= x < (1 << n) for x in walk), "invalid mask") + require(all((a ^ b).bit_count() == 1 for a, b in zip(walk, walk[1:])), + "each step must toggle one source") + require(layer_set(n, k) <= set(walk), "missing required mask") + require(len(walk) - 1 == tariff(n, k), "nonoptimal transition count") + + +def shortest_cover(n, k): + """BFS permits every cube step, arbitrary repeats and off-layer states.""" + domain(n, k, limit=5) + goals = {mask: i for i, mask in enumerate(sorted(layer_set(n, k)))} + complete = (1 << len(goals)) - 1 + initial = 1 << goals[0] if 0 in goals else 0 + queue = deque([(0, initial, 0)]) + seen = {(0, initial)} + capacity = 1 << (n + len(goals)) + for _ in range(capacity): + require(bool(queue), "covering walk must exist") + position, visited, distance = queue.popleft() + if position == 0 and visited == complete: + return distance, len(seen) + for bit in range(n): + neighbor = position ^ (1 << bit) + following = visited | (1 << goals[neighbor] if neighbor in goals else 0) + state = (neighbor, following) + if state not in seen: + seen.add(state) + queue.append((neighbor, following, distance + 1)) + require(len(seen) <= capacity, "BFS state capacity") + raise ValueError("finite state space exhausted without a covering walk") + + +def compile_word(n, k, copies): + domain(n, k, limit=8) + require(type(copies) is int and 1 <= copies <= 3, "copy multiplicity") + gates = [] + current = 0 + for index, mask in enumerate(gray_layer(n, k)): + difference = current ^ mask + for bit in range(n): + if difference & (1 << bit): + gates.append((0, bit + 1)) + current = mask + for copy in range(copies): + gates.append((n + 1 + index * copies + copy, 0)) + for bit in range(n): + if current & (1 << bit): + gates.append((0, bit + 1)) + return tuple(gates) + + +def apply_word(rows, gates): + require(1 <= len(rows) <= 219 and len(gates) <= 356, "circuit capacity") + result = list(rows) + for destination, source in gates: + require(type(destination) is int and type(source) is int, + "integer row references required") + require(0 <= destination < len(rows) and 0 <= source < len(rows), + "row reference outside boundary") + require(destination != source, "self ADD is outside the alphabet") + result[destination] ^= result[source] + return tuple(result) + + +def expected_rows(n, k, copies, rows): + result = list(rows) + for index, mask in enumerate(gray_layer(n, k)): + parity = rows[0] + for bit in range(n): + if mask & (1 << bit): + parity ^= rows[bit + 1] + for copy in range(copies): + target = n + 1 + index * copies + copy + result[target] ^= parity + return tuple(result) + + +def check_word(n, k, copies, gates): + domain(n, k, limit=8) + require(type(copies) is int and 1 <= copies <= 3, "copy multiplicity") + count = n + 1 + copies * comb(n, k) + require(len(gates) == copies * comb(n, k) + tariff(n, k), "full row invoice") + writes = [0] * count + for destination, source in gates: + require((destination == 0 and 1 <= source <= n) + or (n < destination < count and source == 0), "gate alphabet") + writes[destination] += 1 + require(all(writes[row] == 1 for row in range(n + 1, count)), + "each target must be written exactly once") + basis = tuple(1 << row for row in range(count)) + require(apply_word(basis, gates) == expected_rows(n, k, copies, basis), + "arbitrary-input coefficient map or source restoration") + return count + + +def check_layers(): + cases = 0 + vertices = 0 + for n in range(1, 13): + for k in range(n + 1): + listing = gray_layer(n, k) + require(len(listing) == len(set(listing)) == comb(n, k), "layer census") + require(set(listing) == layer_set(n, k), "independent combination census") + if k: + require(listing[0] == (1 << k) - 1, "first Gray mask") + require(listing[-1] == (1 << (n - 1)) + (1 << (k - 1)) - 1, + "last Gray mask") + require(all((a ^ b).bit_count() == 2 + for a, b in zip(listing, listing[1:])), "exchange adjacency") + check_walk(n, k, expand_walk(n, k, listing)) + cases += 1 + vertices += len(listing) + return {"layer_cases": cases, "required_masks": vertices} + + +def check_oracle(): + cases = [] + for n in range(1, 6): + for k in range(n + 1): + distance, states = shortest_cover(n, k) + require(distance == tariff(n, k), "independent shortest-walk mismatch") + cases.append({"n": n, "k": k, "distance": distance, "states": states}) + return cases + + +def check_circuits(): + cases = coefficients = dirty_cases = inverse_cases = 0 + for n in range(1, 9): + for k in range(n + 1): + for copies in range(1, 4): + gates = compile_word(n, k, copies) + count = check_word(n, k, copies, gates) + cases += 1 + coefficients += count * count + rows = tuple(((1 << 73) - 1) ^ (i * 0x13579BDF) for i in range(count)) + require(apply_word(rows, gates) == expected_rows(n, k, copies, rows), + "73-bit dirty rows") + require(apply_word(apply_word(rows, gates), tuple(reversed(gates))) == rows, + "inverse must restore every input") + dirty_cases += 1 + inverse_cases += 1 + if n <= 3 and copies == 1: + for bits in range(1 << count): + rows = tuple((bits >> i) & 1 for i in range(count)) + require(apply_word(rows, gates) == expected_rows(n, k, copies, rows), + "exhaustive arbitrary dirty data") + dirty_cases += 1 + gates = compile_word(5, 3, 1) + require(len(gates) == 34 and 4 * comb(5, 3) == 40, "attaining fixture") + return {"circuit_cases": cases, "coefficient_positions": coefficients, + "dirty_data_cases": dirty_cases, "inverse_cases": inverse_cases, + "fixture": {"n": 5, "k": 3, "targets": 10, "transitions": 24, + "complete_row_adds": len(gates), "direct_row_adds": 40}} + + +def check_rejections(): + controls = 0 + for n, k in [(0, 0), (13, 2), (4, -1), (4, 5), (True, 1), (3, 1.0)]: + try: + gray_layer(n, k) + except ValueError: + controls += 1 + else: + raise ValueError("invalid dimensions accepted") + walk = expand_walk(5, 3, gray_layer(5, 3)) + for changed in [walk[:-1], (0,), (*walk, 1, 0), (0, 32, 0)]: + try: + check_walk(5, 3, changed) + except ValueError: + controls += 1 + else: + raise ValueError("bad covering walk accepted") + gates = compile_word(5, 3, 1) + changed_words = [gates[:-1], gates[1:], gates + ((0, 1), (0, 1)), + ((6, 1),) + gates[1:]] + first = next(i for i, gate in enumerate(gates) if gate[0] == 0) + alternate = 1 if gates[first][1] != 1 else 2 + changed_words.append(gates[:first] + ((0, alternate),) + gates[first + 1:]) + for changed in changed_words: + try: + check_word(5, 3, 1, changed) + except ValueError: + controls += 1 + else: + raise ValueError("bad source restoration or target map accepted") + for copies in [0, 4, True]: + try: + compile_word(5, 3, copies) + except ValueError: + controls += 1 + else: + raise ValueError("invalid multiplicity accepted") + return controls + + +def source_hashes(): + root = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + hashes = {} + for name in names: + with (root / name).open("rb") as stream: + payload = stream.read(131073) + require(len(payload) <= 131072, "package file exceeds receipt capacity") + hashes[name] = sha256(payload).hexdigest() + return hashes + + +def main(): + result = {"claim_type": "scoped proof with finite corroboration", + "layers": check_layers(), "shortest_walks": check_oracle(), + "circuits": check_circuits(), "rejection_controls": check_rejections(), + "sha256": source_hashes(), + "status": "PASS_FIXED_WEIGHT_BORROWED_TOURS_NO_NEW_KAPPA"} + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()