Prove optimal weighted borrowed-source pair tours (no new κ)

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<j. The required map preserves A and every B_i and
+updates
+
+    X_ij,k <- X_ij,k + A_initial + B_i + B_j.
+
+The permitted gates are anchor toggles A <- A+B_i, at price c_i, and a
+single write from A to each assigned target, at a fixed target-specific
+price. A target may be written only when A contains its required parity.
+There are no other gates. Target prices therefore add the same constant
+F to every schedule. We optimize the transition bill. Any mask of the B_i
+may be visited; visits and toggles may repeat; A must be restored. There
+is no clean-state assumption and no restriction to weight-two intermediate
+masks. In particular, this model is narrower than general CNOT synthesis.
+
+Relabel the sources so that c_1 >= ... >= 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.

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.

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

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

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