Prove optimal dyadic rotation switch tariffs (no new κ)

research/dyadic-rotation-switch-tariff/PROOF.md

@@ -0,0 +1,118 @@
+# Optimal edge-switch routing of a dyadic rotation
+
+This is a scoped combinatorial proof. It counts active swaps, with unit price
+per swap of two occupied addresses that differ in exactly one binary bit.
+There are N=2^h addresses, h>=1, and no additional addresses. Tokens may be
+arbitrary distinct records. A routing network must send the token initially
+at x to x+c modulo N, where 0<=c<N. A switch can use any hypercube edge;
+there is no restriction on the order, number of layers or repeated dimensions
+in the lower bound.
+
+Write d_k(c)=min(r,2^k-r), where r=c mod 2^k. Then the exact minimum is
+
+    S_h(c) = sum_{k=1}^h 2^(h-k) d_k(c).
+
+The maximum of this minimum over all c is
+
+    M_h = ((3h+1)2^h - (-1)^h)/9.
+
+The only maximizing offsets are a_h and 2^h-a_h, where
+
+    a_h = (2^h-(-1)^h)/3.
+
+For h=1 these two offsets coincide. For h>=2 they are distinct.
+
+## An explicit h-layer circuit
+
+Process bits i=h-1,h-2,...,0. Put b=2^i, r=c mod b, and c_i=floor(c/b) mod 2.
+For every edge (x,x+b) with x_i=0, swap that edge precisely when
+
+    c_i XOR [ (x mod b)+r >= b ] = 1.
+
+Each layer consists of disjoint edges. Its predicate is independent of bit i,
+so the two endpoints agree on whether to swap. At entry to layer i, the lower
+bits and bit i of any token's current address still equal those of its
+original address. Only higher bits have changed. The displayed predicate is
+exactly the change to bit i in addition of c modulo 2^h. Induction down the
+bits proves the required endpoint for every token, with no empty workspace
+and with arbitrary payloads preserved.
+
+There are 2^(h-i-1) copies of each lower-bit value. If c_i=0, exactly r of
+the b lower-bit values cause a swap. If c_i=1, exactly b-r do. Thus the number
+of active edges in this layer is
+
+    2^(h-i-1) min(c mod 2^(i+1), 2^(i+1)-(c mod 2^(i+1))).
+
+Summing gives S_h(c). Each token crosses each bit dimension at most once.
+
+## Global optimality in the stated swap model
+
+For any current token placement, sum the Hamming distances from every token
+to its required destination. One hypercube-edge swap changes the sum by at
+most two, since each of its two tokens changes one bit. Every routing needs
+at least half the initial distance sum. This is the standard token-swapping
+distance bound, for example Lemma 4 in Miltzow, Narins, Okamoto, Rote, Thomas
+and Uno, *Approximation and Hardness for Token Swapping*:
+https://page.mi.fu-berlin.de/rote/Papers/pdf/Approximation%2Band%2Bhardness%2Bfor%2Btoken%2Bswapping.pdf
+
+The circuit above moves each token in a bit dimension at most once and ends
+at its destination. Consequently each token moves exactly its original
+Hamming distance. Its S_h(c) swaps therefore meet the lower bound. This
+proves optimality against arbitrary edge-swap sequences, rather than only
+against circuits in the chosen layer order. The standard distance bound and
+binary carry rule are not claimed as new.
+
+## Sharp maximum and equality
+
+Let q_k=(c mod 2^k)/2^k, t_k=min(q_k,1-q_k), and t_0=0. Reading successive
+bits of c from least significant to most significant gives
+
+    q_(k+1) = (q_k+epsilon_k)/2,  epsilon_k in {0,1}.
+
+The possible next distances are t_k/2 and (1-t_k)/2. Every choice is
+realizable by a next bit, and the two choices coincide only at t_k=1/2.
+Also S_h(c)/2^h=sum_{k=1}^h t_k.
+
+For n>=1, let H_n(t) be the largest sum over n consecutive distances,
+including the present distance t in [0,1/2]. Then H_1(t)=t and
+
+    H_n(t) = t + max(H_(n-1)(t/2), H_(n-1)((1-t)/2)).
+
+Inductively H_n is affine with strictly positive slope A_n. Since t/2 is
+at most (1-t)/2, its maximum branch is always the second one. The slope
+recurrence is A_1=1 and A_n=1-A_(n-1)/2, which keeps 1/2<=A_n<=1.
+Thus every optimal path chooses
+
+    t_(k+1)=(1-t_k)/2.
+
+Starting at zero this gives t_k=(1-(-1/2)^k)/3. Therefore
+
+    sum_{k=1}^h t_k = h/3 + (1-(-1/2)^h)/9.
+
+Multiplication by 2^h proves the displayed M_h. All maximizing choices are
+strict except the one following t_1=1/2. For h>=2 there are exactly two
+maximizing bit strings. Their final q_h values are t_h and 1-t_h, so their
+offsets are exactly (2^h-(-1)^h)/3 and its complement. For h=1 the unique
+maximizer is c=1. This also proves the formula's integrality.
+
+## The first fixture
+
+For h=3,c=3, descending bit layers have 3,2,4 active switches. Their total
+is 9 and the initial Hamming-distance sum is 18. Both c=3 and c=5 attain
+M_3=9. A full eight-wire Beneš layout has 20 available switch sites, while
+this circuit has three layers and uses nine active sites. Available sites
+and active swaps are different quantities; no physical time ratio follows.
+
+## Scope at the CRT caller
+
+Cinna Davis's CRT.md section 2 in PR #4100 requires rotations on x<s that
+fix padded addresses x>=s. The present theorem covers s=2^h. It does not
+supply the strict s<2^h prime-modulus rotations used there. Unpaidmoon's
+PR #4377 prices generic Beneš reconstruction in that larger setting.
+This theorem adds an exact optimal tariff for a changed dyadic routing
+premise. It does not replace either predecessor's full evaluator argument.
+
+Control computation, table generation, the cost to access or swap a record
+on a sequential tape, scanner ownership, physical head motion, CRT repair,
+stock, the ordinary callee and all-size multiplication remain external.
+A smaller logical switch count alone gives no new kappa.

research/dyadic-rotation-switch-tariff/README.md

@@ -0,0 +1,104 @@
+# Exact optimal switch tariff for dyadic rotations
+
+For N=2^h occupied binary addresses, rotating x to x+c modulo N requires
+exactly
+
+    S_h(c) = sum_{k=1}^h 2^(h-k) dist(c, 2^k Z)
+
+hypercube-edge swaps, for every h>=1 and 0<=c<N. An explicit circuit attains
+this minimum in h descending bit layers. The sharp worst-case tariff is
+
+    max_c S_h(c) = ((3h+1)2^h-(-1)^h)/9,
+
+attained only at c=(2^h-(-1)^h)/3 and its complement modulo N. They coincide
+at h=1. For h=3,c=3 the layer counts are 3,2,4, giving 9 swaps.
+
+This is a scoped combinatorial proof with exact finite corroboration.
+[PROOF.md](PROOF.md) gives the construction, the standard Hamming-distance
+lower bound, and the maximum/equality proof. The contribution is the exact
+rotation tariff and sharp extremal law in this model. Binary carry logic
+and the token-swapping distance bound are credited standard ingredients.
+No claim of priority over the full routing literature is made.
+
+## Connection and limits
+
+Cinna Davis's [PR #4100](https://github.com/CrocSwap/integer-mult-bounds/pull/4100)
+uses bounded-bit switch networks for CRT rotations. Unpaidmoon's merged
+[PR #4377](https://github.com/CrocSwap/integer-mult-bounds/pull/4377)
+prices generic Beneš compilation and CRT reconstruction. Their statements
+are cited context, not replayed deliverables. The present circuit changes
+the modulus premise to a full dyadic cycle. It does not implement the
+strictly smaller prime-modulus cycle with fixed padded addresses.
+
+The count charges active logical edge swaps. It supplies no sequential-tape
+access bound, control-generation tariff, payload-movement bound, CRT repair,
+ordinary callee, supplier admission, new kappa or selected-frontier change.
+No spare address is available. Longer paths and repeated edge dimensions
+are allowed in the optimality comparison. Arbitrary records are routed by
+permutation, so the endpoint does not assume zero or clean payloads.
+
+## Reproduce
+
+From the repository root with CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B research/dyadic-rotation-switch-tariff/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/dyadic-rotation-switch-tariff
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/dyadic-rotation-switch-tariff --check-source-history
+```
+
+Expected final line is `PASS_DYADIC_ROTATION_SWITCH_TARIFF`. Normal and
+optimized runs perform the same checks, with explicit exceptions rather
+than removable assertions. The verifier checks all 510 rotations through
+h=8, independently computes each initial Hamming-distance sum, enumerates
+all offsets through h=12 for the maximum and equality cases, and compares
+against an independent full token-permutation BFS through h=3. The BFS
+visits 2, 24 and 40,320 states. Eight controls reject omitted switches,
+reversed layer order and invalid parameter values. These finite checks
+corroborate the universal written proof; they are not its replacement.
+
+`--receipt /absolute/scratch/path.json` writes a generated evidence report
+bound to the six package-file SHA256 hashes. No receipt is hand-authored.
+The two VERIFY.json commands are bounded to 120 seconds each. The checker
+caps widths at 12, direct execution at 8 and BFS at 3. Python allocation is
+a documented Power-of-Ten deviation with a factorial state cap of 40,320;
+there is no recursion or unbounded queue drain. No Lean or physical tape
+replay was run.
+
+## Provenance and overlap
+
+Scientific base is canonical main
+`624de9dc66858af0945e5f8a0942488d62280d43`, priority revision 7.
+The `uniform-transfer-audit` card is changed from audit to a new exact
+routing result under a dyadic modulus premise. The card's historical
+`research_baseline.py` command fails with `KeyError: 'bit_lower'` under the
+selected schema; the current `research_selected_baseline.py` passes its
+source-binding-only check. No selected replay is implied.
+
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19134021)
+records scope and overlap. The initial remote cache covers 395 open PRs and
+3,888 Discussion records at 22:39 UTC on October 22, 2026. Sparse local
+cache coverage is incomplete; a separate `git grep` covers all main-tree
+top-level research READMEs. Merged PR and exact-term searches found no
+same-scope result within that coverage. These searches do not prove novelty.
+SOURCES.json pins predecessor prose as historical provenance. The verifier
+has no external mathematical input or imported predecessor implementation.
+
+## Open next questions
+
+1. Determine the exact edge-switch tariff of a rotation on x<s<2^h that
+   fixes the padded addresses. This reaches the actual CRT modulus premise.
+   Start with s=3 at h=2 and compare the Hamming lower bound with an exact
+   token-swap search. The full-cycle triangular construction does not apply.
+2. Price the dyadic circuit's control generation and record access on one
+   fixed tape layout. Start with the h=3,c=3 circuit and count all control,
+   scan and payload operations. A logical swap count is not that tariff.
+
+## Credit
+
+This contribution was produced by Nick Petalas. Cinna Davis supplies the
+CRT routing context and unpaidmoon the generic evaluator predecessor.
+The Hamming-distance lower bound is standard; PROOF.md cites Miltzow,
+Narins, Okamoto, Rote, Thomas and Uno. No predecessor source is copied or
+rechecked here. Independent human and formal proof-kernel review are
+unclaimed. Apache-2.0.

research/dyadic-rotation-switch-tariff/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "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/unconditional-batched-crt/CRT.md",
+      "usage": "provenance",
+      "git_blob": "d98dd8e368431cac33d5fc1c8c336696663641d6",
+      "sha256": "02c3a1e38cbee25aefe2640cc72676da62ba10eb7519fbcb9adb9d48b74eff2b"
+    },
+    {
+      "path": "research/crt-uniform-evaluator/README.md",
+      "usage": "provenance",
+      "git_blob": "5b28a48bdc2ab7c9bb5e1103601ac0e9ff00ef14",
+      "sha256": "2328dd323a39f9b88677426c82ac538638ae3e40943fe3ca4c348d5c087a6aec"
+    }
+  ]
+}

research/dyadic-rotation-switch-tariff/TASK.json

@@ -0,0 +1,80 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Prove one missing implication with explicit quantified hypotheses.",
+      "Find an exact counterexample at the claimed interface boundary."
+    ],
+    "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.",
+    "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.",
+    "allowed_variations": [
+      "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller."
+    ],
+    "scope_change_triggers": [
+      "Replacing a quantified obligation with another finite smoke test.",
+      "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses."
+    ],
+    "overlap_terms": [
+      "uniform transfer",
+      "all-size",
+      "precision",
+      "4100",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Exact optimal hypercube-edge swap count and sharp maximum for every full dyadic rotation.",
+  "scope_change_reason": "The audit card is changed to an original scoped routing theorem under a full dyadic modulus, distinct from the strict non-dyadic padded CRT caller.",
+  "bottleneck_link": "Exact logical switch tariff for a changed CRT routing premise; tape and control costs remain external.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the first proved exact tariff and sharp maximum with bounded independent endpoint and BFS corroboration.",
+  "outcome": "completed",
+  "evidence": "PROOF.md and verify.py; generated hash-bound report on request.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "What is the optimal tariff for padded non-dyadic rotations?",
+      "why_it_matters": "This is the actual CRT prime-modulus premise.",
+      "first_step": "Compare s=3,h=2 with exact token-swap search.",
+      "blocked_by": "The dyadic triangular circuit does not preserve the padded domain."
+    },
+    {
+      "question": "What is the complete fixed-tape cost of the dyadic circuit?",
+      "why_it_matters": "Logical swaps do not price controls or sequential record access.",
+      "first_step": "Execute h=3,c=3 with all control and payload operations metered.",
+      "blocked_by": "No physical tape adapter is supplied."
+    }
+  ]
+}

research/dyadic-rotation-switch-tariff/VERIFY.json

@@ -0,0 +1,32 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact routes, Hamming equality, maximum/equality, full small BFS and eight fault/boundary controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Same explicit checks under optimized Python."
+    }
+  ]
+}