Prove exact restored fixed-weight parity tours (no κ)

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<n, adjacent entries inside either block differ in exactly two
+bits by induction. At the junction, when k=1 the masks are 2^(n-2)
+and 2^(n-1), so they differ in two bits. For 2<=k<n, the junction masks
+are
+
+    2^(n-2) + 2^(k-1) - 1,
+    2^(n-1) + 2^(n-2) + 2^(k-2) - 1.
+
+The second removes bit k-2 and adds bit n-1 relative to the first.
+They also differ in exactly two bits. This proves the adjacency assertion
+in all cases, including k=n-1, where the first block is a singleton.
+
+Start at the empty mask, toggle its k coordinates to reach the first
+listing entry, and write its designated targets. Move between consecutive
+listing entries by their two differing coordinates, writing the targets
+at each entry. Finally toggle the k coordinates of the last entry to
+restore A. Each B_i is unchanged and each target receives exactly its
+specified parity. The transition count is k+2(N-1)+k, attaining the lower
+bound. The order of the two toggles within an exchange is immaterial.
+
+## One complete improvement fixture
+
+For n=5, k=3 and one target per mask, N=R=10. The new exact tour needs
+24 anchor toggles and ten target writes, or 34 row ADDs. Applying the
+four required source rows directly to each target needs 40 row ADDs.
+The six-ADD reduction includes anchor preparation and full restoration.
+At width L this is 34L versus 40L bit XORs. It does not include tape-head
+movement, which is absent from the declared model.
+
+## Scope and credit
+
+Cinna Davis / PR2271 supplied the borrowed-source multi-mask contract,
+its square example and the explicit higher-dimensional tour question.
+The reflected Gray listing and cube distances are classical. The new
+contribution is their exact restored fixed-weight-layer tariff and its
+arbitrary-dirty row-circuit realization in this contract, beyond the
+previously covered pair layer. Ali Romman / PR5372 treats a separate
+all-nonempty-mask, paid clean-row contract. Those scientific verifiers
+are neither imported nor replayed here.
+
+The finite replay corroborates the theorem on its declared bounded
+domains; the universal quantifiers rest on this written proof. A physical
+caller, native frames and implementation, ownership/hosting, routing,
+precision, recursive pricing and a complete supplier remain open.
+No selected framework assumption or complete multiplication theorem is
+proved. Independent human and formal proof-kernel review are unclaimed.

research/fixed-weight-borrowed-tours/README.md

@@ -0,0 +1,124 @@
+# Exact restored fixed-weight parity tours
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Scoped mathematical proof with exact finite corroboration. For every n>=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.

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."
+}