From 8584e3cbe9b98761eac8cfb52bc72acbf5f21e06 Mon Sep 17 00:00:00 2001 From: JoyboyBrian Date: Thu, 22 Oct 2026 20:15:02 -0700 Subject: [PATCH 1/4] Write the reservoir exchange as six BIT ordinary calls and locate the wrapper branch at H = r_max G --- .../crt-reservoir-interchange-bill/PROOF.md | 244 ++++++++++++ .../crt-reservoir-interchange-bill/README.md | 35 ++ .../SOURCES.json | 42 ++ .../crt-reservoir-interchange-bill/TASK.json | 74 ++++ .../VERIFY.json | 23 ++ .../crt-reservoir-interchange-bill/verify.py | 371 ++++++++++++++++++ 6 files changed, 789 insertions(+) create mode 100644 research/crt-reservoir-interchange-bill/PROOF.md create mode 100644 research/crt-reservoir-interchange-bill/README.md create mode 100644 research/crt-reservoir-interchange-bill/SOURCES.json create mode 100644 research/crt-reservoir-interchange-bill/TASK.json create mode 100644 research/crt-reservoir-interchange-bill/VERIFY.json create mode 100644 research/crt-reservoir-interchange-bill/verify.py diff --git a/research/crt-reservoir-interchange-bill/PROOF.md b/research/crt-reservoir-interchange-bill/PROOF.md new file mode 100644 index 0000000000..1cdf902570 --- /dev/null +++ b/research/crt-reservoir-interchange-bill/PROOF.md @@ -0,0 +1,244 @@ +# The #4174 reservoir exchange as ordinary H-bit interchange calls + +**Scoped counting proof, conditional on BIT.md's ordinary-interchange +theorem as stated. No new κ.** The selected conditional exponent stays +60403/20000000. + +## 0. What CRT.md bills, and which callee it means + +CRT.md (#4100, Cinna Davis) prices its reservoir and switch gadget with +"an already completed ordinary interchange", costing `O(V h^(1-a))`. The +same file says this interchange "is supplied by BIT.md". BIT.md's statement +is the following. A fixed finite-tape machine + +> exchanges two complete equal e-bit binary address fields, with arbitrary +> complete preceding, intervening and following fields, in O(V e^(1-a2)) +> time and O(V) visited space. + +It "preserves its borrowed input, returns a distinct owned output, fixes +every spectator, erases its work and returns its heads". Its constants +depend on `q = 2^89 - 1` and the fixed source, not on `e` or the payload. +Here `a = a2 = c(1-c^2)` with `c = 8667/5000000`, so `a2 < 1/500`. + +BIT.md §4 builds that machine as a wrapper: + +1. Embed each `2^e` binary field into `q^E` with `E = ceil(log_q 2^e)`. + This multiplies the volume by less than `q^2`. +2. At the root, set `w = ceil(E^c)`. Compute `stock = K(w)^{D(E)}` and the + least `k` with `q^k >= stock`. Here + `K(w) = 269241600 N q^{4096(w-1)}`, `N = |GL_64(F_q)|`, and + `D(n) = 0` for `n < 64`, otherwise `D(n) = 1 + D(42 floor(n/64))`. +3. If `2k >= E`, or the body width `n = floor((E-k)/w)` is below 64, + run the elementary algorithm. That is BIT.md §3's stage `a = 0`, + "elementary q-digit swaps", which costs `O(V E)`. Otherwise run the + body word. + +**Reading used here.** The "original radix width `e`" of BIT.md §4 is the +radix width `E` of the embedded field, and `w` and `D` are evaluated at +that root call. Remark 4 below gives a bound that does not depend on the +exact `D`. + +CRT.md §3 sets `G = 64(ell + ceil(log2(p+2)))`, `r_max = floor(L/(100G))` +and `H = r_max G`. It moves three borrowed `H`-bit fields "using a fixed +number of paid equal-H interchanges" and undoes them at the end of the +batch. PR #4174 (Hiroki KUMAZAKI) constructs these fields. Its PROOF.md +§4 gives destinations `U = [0,H)`, `T = [H,2H)`, `B = [L-H,L)` and +sources `S_0, S_1, S_2` inside the unused interval. All six blocks are +pairwise disjoint. It also states the invoice "at most six width-`H` +ordinary exchanges per batch" and leaves the callee open. + +`V` denotes the payload volume, that is `2^L` addresses times the record +length. + +## 1. Proposition + +Let `(p, ell, widths)` be any layout accepted by the #4174 `Layout` +constructor. Let `π` be any of its plans, with placement `P`. Put +`a = a2`. + +**(i) Calls.** For `k = 0, 1, 2`, let `X_k` exchange `S_k` with the `k`th +destination (`U`, `T`, `B`), bit for bit in order. Then +`P = X_0 X_1 X_2` in every order of the factors, and `P^{-1} = P`. Each +`X_k` is one BIT.md call with `e = H`. Its spectators are the other +`L - 2H` address bits and the record. So placement plus restoration is +exactly **six ordinary calls of width `H`**. No other payload action is +needed. Recomputing positions touches only the #4174 descriptor, which +has at most `d + 12` fragments. + +**(ii) Bill.** Assume BIT.md's theorem as stated, with constant `C_BIT`. +Placement plus restoration then costs at most + +``` +6 C_BIT V H^{1-a} + 6 c_own V, +``` + +where `c_own V` charges for using the owned output in place of the +borrowed input (one copy and one erase). This is CRT.md's +`O(V H^{1-a} + V)` with multiplicity 6 per batch. With #4174's bound of +25,600 batches per synchronized switch layer, a layer pays at most 153,600 +such calls. + +**(iii) Branch at the actual width.** For `1 <= H < 89·2^88`, the wrapper +runs at `E(H) = floor(H/89) + 1`. It takes the elementary branch for every +`H < H* = 27,706,412`, and the body branch at `H = H*`. Since +`H <= L/100`, every accepted layout with `L < 2,770,641,200` runs all six +calls on the elementary branch. So do the twelve width-`H` shuttles of +CRT.md §4. In particular: + +| layout | `H` | `E` | `w` | `D(E)` | `k` | branch | +|---|---|---|---|---|---|---| +| minimal, `p = 1310720`, `ell = 21`, widths 20 | 10752 | 121 | 2 | 1 | 8193 | elementary | +| #4174 production, `p = 9240576`, `ell = 24` | 15360 | 173 | 2 | 2 | 16385 | elementary | +| first body width | 27706412 | 311309 | 2 | 19 | 155654 | body | + +**(iv) The elementary branch meets the bill.** For `1 <= H < H*`, +`E(H) <= H^{1-a}`. So each elementary call costs at most +`C_0 q^2 V H^{1-a}` plus the `O(q^2 V)` embedding. Here `C_0` is the +per-digit constant of stage `a = 0`. On this range `H^{a} < 2^{1/20}`, +so the saving `H^{-a}` is numerically absent. + +**Answer to #4938's open question.** Yes. One #4174 three-field exchange +is three ordinary width-`H` calls, and its restoration is the same three +calls. Their cost fits `O(V H^{1-a} + V)` with multiplicity 6. At the +minimal layout, and at every layout with `L < 2,770,641,200`, the bill is +met by BIT.md's elementary fallback alone. The body word and the +`a2` saving play no part there. + +## 2. Proof of (i) + +By #4174 PROOF.md §4, `S_0, S_1, S_2, U, T, B` are pairwise disjoint +intervals of length `H`. `P` maps bit `S_k[0] + t` to `D_k[0] + t` and +back, for `0 <= t < H`, and fixes every other bit. Define `X_k` as the +same translation on the single pair `(S_k, D_k)`. The `X_k` have disjoint +supports, so they commute. Each is an involution, and their product is +`P`. Hence `P^{-1} = P = X_0 X_1 X_2` in any order. + +Fix `k`. The bits outside `S_k ∪ D_k` form at most three contiguous +spectator fields: before, between and after the pair. The other four +blocks lie inside these fields. `D_k` precedes `S_k` when `k = 0, 1`, +since `S_k ⊂ [2H, L-H)`, and follows it when `k = 2`. An exchange of two +fields is symmetric. So `X_k` is exactly the operation in BIT.md's +statement, with `e = H` and "arbitrary complete preceding, intervening +and following fields". The record payload is carried with its address. +The call fixes every spectator, so it moves the record at address `x` to +`X_k(x)` for every `x`. This includes invalid padded addresses and dirty +borrowed values. Three calls realize `P`, and three more realize +`P^{-1}`. The endpoint is the identity on every address. + +The transported controls `f'_i = f_i ∘ P^{-1}` and the split-axis +descriptors are #4174 PROOF.md §5. They are metadata, not payload +actions. ∎ + +## 3. Proof of (ii) + +By (i) and BIT.md, the six calls cost at most `6 C_BIT V H^{1-a}`. BIT.md +returns a distinct owned output and preserves its borrowed input. To keep +a fixed inventory, the caller copies the output back and erases it, or +swaps tape roles and erases the old input. Either costs at most +`c_own V`. The batch bound is #4174's. ∎ + +## 4. Proof of (iii) + +**Lemma R (radix width).** For `1 <= H < 89·2^88`, the least `E` with +`q^E >= 2^H` is `floor(H/89) + 1`. + +*Proof.* `q^E < 2^{89E}`. By Bernoulli, `q^E = 2^{89E}(1-2^{-89})^E >= +2^{89E}(1 - E 2^{-89}) >= 2^{89E-1}` when `E <= 2^88`. So `q^E >= 2^H` +holds if `H <= 89E - 1` and fails if `H >= 89E`. The least such `E` is +`ceil((H+1)/89) = floor(H/89) + 1`. ∎ + +**Lemma W.** For `2 <= E < 2^576`, `w = ceil(E^c) = 2`. + +*Proof.* `E^c > 1`. Also `E^{8667} < 2^{576·8667} = 2^{4992192} <= +2^{5000000}`, so `E^c <= 2`. ∎ + +**Lemma S (stock digits).** If `w = 2` and `D >= 1`, then +`k = 8192 D + j(D)`, where `j(D)` is the least `j` with +`q^j >= 269241600^D`. The values are +`j = 1, 1, 1, 2, 2, 2, 3, 3, 3, 4, 4, 4, 5, 5, 5, 6, 6, 6, 6` for +`D = 1, …, 19`. + +*Proof.* `N = ∏_{i<64}(q^64 - q^i) = q^{4096} ν` with +`ν = ∏(1 - q^{i-64})`. Then `1 - 2/q < 1 - Σ_{m>=1} q^{-m} <= ν < 1`. +So `K(2)^D = q^{8192 D}(269241600 ν)^D`. Let `j*` be the least `j` with +`q^j >= 269241600^D`. Then `q^{j*} > (269241600 ν)^D`. For the listed `D`, +the exact integer check `q^{j*-1+D} < (269241600 (q-2))^D` gives +`q^{j*-1} < (269241600 (1-2/q))^D < (269241600 ν)^D`. So `j(D) = j*`. ∎ + +**Lemma B (branch).** `D(E) = 0` exactly for `E < 64`, and then `k = 0` +and `n = floor(E/w) < 64`, so the branch is elementary. For `D >= 1`, +`D` is constant on blocks `[T_D, T_{D+1})`: + +| D | block | `2k` | +|---|---|---| +| 1 | 64–127 | 16386 | +| 2 | 128–255 | 32770 | +| 3 | 256–447 | 49154 | +| … | … | … | +| 17 | 114496–174527 | 278540 | +| 18 | 174528–265983 | 294924 | +| 19 | 265984–405311 | 311308 | + +For `D <= 18`, each block ends below `2k(D)`, so `2k >= E` and the branch +is elementary. In block 19 the branch is elementary iff +`E <= 311308`. At `E = 311309`, `2k = 311308 < E` and +`n = floor((311309 - 155654)/2) = 77827 >= 64`, so the branch is body. +The verifier evaluates all `E <= 311309` directly. ∎ + +By Lemma R, `E(H) <= 311308` iff `floor(H/89) <= 311307`, that is +`H <= 27,706,411`. Finally, `r_max <= L/(100G)` gives `H <= L/100`. So +`L < 2,770,641,200` forces `H < H*`. The CRT.md §4 shuttles exchange the +`t` field `[H,2H)` with the back field `[L-H,L)`. They are also width-`H` +ordinary calls, so the same branch applies. The two table rows follow +from Lemmas R, W, S and the definition of `D`. ∎ + +**Remark 4 (robust to the reading of `D`).** For `64 <= E <= 16386`, +any reading with stock at least `K(w)` and `w >= 2` gives +`k >= 8193`, so `2k >= 16386 >= E`. So `H <= 1,458,353` is elementary +whatever `D` is, provided `D >= 1`. Both table layouts are far below. + +## 5. Proof of (iv) + +If `H < 89`, then `E = 1 <= H^{1-a}`. If `89 <= H < H*`, then +`E <= H/89 + 1 <= 2H/89`. Also `H* < 2^25` and `a < 1/500`, so +`H^{a} < 2^{1/20}`. Since `2^{1/20} < 89/2`, we get +`E H^{a} <= (2H/89)(89/2) = H`. In both cases `E <= H^{1-a}`. + +Stage `a = 0` exchanges two `E`-digit fields with `E` single-digit swaps +on the embedded volume `V' < q^2 V`. Each swap costs `C_0 V'`. So one call +costs at most `C_0 q^2 V E <= C_0 q^2 V H^{1-a}`, plus the embedding and +its restriction, which are `O(q^2 V)`. ∎ + +## 6. Not proved here + +- BIT.md's theorem, including stage `a = 0`, its constant `C_0` and its + fixed-tape realization. AUDIT.md in #4100 records that its physical + suites are not all passing. This package uses the statement as written. +- The fixed-tape cost of the binary-to-radix embedding. BIT.md states it. +- The rest of the CRT.md §4 gadget: the guard scan, the sparse sort and + reinsertion, the last-`K` branch, and #4377's evaluator model. +- Whether `D` is meant at the radix width `E`. Remark 4 covers the two + table layouts under any `D >= 1`. +- Any κ change or selected-frontier change. + +## 7. Verification + +`verify.py` checks the following: + +- Input pins and the quoted phrases. +- **A.** On two `Placement` fixtures with dirty payloads, three literal + field-exchange calls realize `P` in all six orders, and the same three + calls restore every record. +- **B.** Every plan on the minimal layout (131,072 plans, 786,432 calls) + and on the production layout (104,864 plans, 629,184 calls) satisfies + the hypotheses of (i). +- **C.** The exact `N = |GL_64(F_q)|` bounds, the `j(D)` table, the branch + at every `E <= 311309`, Lemma R on `H < 3000` and the table widths, + and the `H*` edge. +- **D.** The inequality of (iv). + +Its rejection controls are: a dropped restoration call, a bit-reversing +exchange, a source overlapping `T`, the body branch one digit or one bit +early, the stock without `269241600 N`, `D(173) = 1`, `N >= q^{4096}`, +and `j(D)` dropped. Each must fail. The finite checks corroborate the +written argument; they do not replace it. diff --git a/research/crt-reservoir-interchange-bill/README.md b/research/crt-reservoir-interchange-bill/README.md new file mode 100644 index 0000000000..58b05b40dd --- /dev/null +++ b/research/crt-reservoir-interchange-bill/README.md @@ -0,0 +1,35 @@ +# crt-reservoir-interchange-bill + +**Draft; no new bound claimed.** + +## Scope and evidence + +Original card: `uniform-transfer-audit`. Complete [TASK.json](TASK.json), including any scope +change and its connection to the bottleneck. Explain the result and limitations here. +Source commits, Git blobs and SHA256 pins are in [SOURCES.json](SOURCES.json). +The selected record and catalogue are historical provenance, so later priority +updates do not invalidate this package. Explicit --source files are live inputs +and must match their pins. Full Git history is needed to resolve provenance. + +## Reproduce + +After completing the verifier and marking VERIFY.json ready, from repo root: + +```sh +python3 scripts/research_package.py --package research/crt-reservoir-interchange-bill --check-only +python3.12 scripts/research_package.py --package research/crt-reservoir-interchange-bill +``` + +Declare all external inputs and pinned dependencies in VERIFY.json. The generic +hook is bounded; native/Lean or long replays need an explicit dedicated workflow. + +## Open next questions + +Complete the structured `open_questions` list in TASK.json and explain it here: +the question, why it matters, a feasible first step and any blocker. If no next +question is justified, say so rather than inventing one. + +## Credit + +Prepared by JoyboyBrian. Retain predecessor attribution and source-specific notices. +New work is Apache-2.0. Disclose substantial AI assistance in TASK.json. diff --git a/research/crt-reservoir-interchange-bill/SOURCES.json b/research/crt-reservoir-interchange-bill/SOURCES.json new file mode 100644 index 0000000000..5d0191a495 --- /dev/null +++ b/research/crt-reservoir-interchange-bill/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "cef4b52f2a59009865bf8eabde1be3f159063703", + "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/crt-reservoir-placement/PROOF.md", + "usage": "input", + "git_blob": "087ab4462282fc68d6f5b8b1f17167383e77df7c", + "sha256": "cea5eec3d4ec1008293e98213f519bdbf88dcd9aa801bff516eaee24340efa68" + }, + { + "path": "research/crt-reservoir-placement/allocator.py", + "usage": "input", + "git_blob": "4b3ad89652a28f7d142248d1b5747272e696493c", + "sha256": "b764195fc6291e3c8fa8297b1f4ceaefc119d5664d8ff348b49eac8a2e79c688" + }, + { + "path": "research/unconditional-batched-crt/BIT.md", + "usage": "input", + "git_blob": "2aa2544fa61259ac48b936b8c906ec9d31d813fa", + "sha256": "83a0cc082e52219a5f142becc8b5b92019e091cb3ede6c5bccbd8508993fc4da" + }, + { + "path": "research/unconditional-batched-crt/CRT.md", + "usage": "input", + "git_blob": "d98dd8e368431cac33d5fc1c8c336696663641d6", + "sha256": "02c3a1e38cbee25aefe2640cc72676da62ba10eb7519fbcb9adb9d48b74eff2b" + } + ] +} diff --git a/research/crt-reservoir-interchange-bill/TASK.json b/research/crt-reservoir-interchange-bill/TASK.json new file mode 100644 index 0000000000..d5ee192b94 --- /dev/null +++ b/research/crt-reservoir-interchange-bill/TASK.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "cef4b52f2a59009865bf8eabde1be3f159063703", + "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": "unchanged", + "actual_scope": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "scope_change_reason": null, + "bottleneck_link": "TODO: explain the causal connection or label this as a side result", + "budget_minutes": 90, + "stop_rule": "TODO", + "outcome": "in-progress", + "evidence": "TODO", + "author": "JoyboyBrian", + "ai_assistance": "TODO: disclose tools used", + "open_questions": [ + { + "question": "TODO", + "why_it_matters": "TODO", + "first_step": "TODO", + "blocked_by": "TODO" + } + ] +} diff --git a/research/crt-reservoir-interchange-bill/VERIFY.json b/research/crt-reservoir-interchange-bill/VERIFY.json new file mode 100644 index 0000000000..b4bb11f568 --- /dev/null +++ b/research/crt-reservoir-interchange-bill/VERIFY.json @@ -0,0 +1,23 @@ +{ + "schema_version": 1, + "status": "draft", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/crt-reservoir-placement/PROOF.md", + "research/crt-reservoir-placement/allocator.py", + "research/unconditional-batched-crt/BIT.md", + "research/unconditional-batched-crt/CRT.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "TODO: identity, positive fixture and failure controls" + } + ] +} diff --git a/research/crt-reservoir-interchange-bill/verify.py b/research/crt-reservoir-interchange-bill/verify.py new file mode 100644 index 0000000000..49953bcdf2 --- /dev/null +++ b/research/crt-reservoir-interchange-bill/verify.py @@ -0,0 +1,371 @@ +#!/usr/bin/env python3 +"""Price the #4174 reservoir exchange with the #4100 BIT.md ordinary callee. + +PROOF.md is the argument. This script checks its finite facts: + +A. On small Placement fixtures, three literal field-exchange calls realize + the #4174 placement permutation in every order, and the same three calls + restore every dirty record. Payload is moved, not just positions. +B. Every #4174 plan on the minimal layout (p = 1310720, ell = 21) and on the + production layout (p = 9240576, ell = 24) is three disjoint width-H pairs + inside the reservoir, so placement plus restoration is six width-H calls. +C. BIT.md section 4's wrapper, evaluated exactly at radix width E: every + E < 311309 takes the elementary branch and E = 311309 takes the body. + In binary this is H < 27706412. Both layouts are elementary. +D. On that elementary range, E <= H^(1-a2), so the CRT.md per-call bill + V H^(1-a) is met by the elementary stage alone. + +Rejection controls check that mutated claims fail. No new kappa is claimed. +""" + +from __future__ import annotations + +import hashlib +import itertools +import json +import sys +import types +from fractions import Fraction +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = ROOT / "research" / "crt-reservoir-interchange-bill" +ALLOCATOR = "research/crt-reservoir-placement/allocator.py" + +Q = 2 ** 89 - 1 +M = 269241600 # the integer factor of K(w) +C = Fraction(8667, 5000000) +A2 = C * (1 - C * C) # BIT.md a2 +E_MIN = 311309 # first radix width on the body branch +H_MIN = 27706412 # first binary width on the body branch +J = (0, 1, 1, 1, 2, 2, 2, 3, 3, 3, 4, 4, 4, 5, 5, 5, 6, 6, 6, 6) # j(D), D <= 19 + +PHRASES = { + "research/unconditional-batched-crt/BIT.md": ( + "exchanges two complete equal e-bit binary address fields, with arbitrary " + "complete preceding, intervening and following fields, in O(V e^(1-a2)) " + "time and O(V) visited space.", + "It preserves its borrowed input, returns a distinct owned output, fixes " + "every spectator, erases its work and returns its heads.", + "q=2^89-1,", + "c=8667/5000000,", + "a2=c(1-c^2)=0.001733394791695384296.", + "Let W=28416, N=|GL_64(F_q)| and", + "K(w)=269241600 N q^(4096(w-1)),", + "D(n)=0 (n<64), D(n)=1+D(42 floor(n/64)) (n>=64).", + "At a root choose w=ceil(e^c)", + "On original radix width e compute stock=K(w)^D(e) and the least k with " + "q^k>=stock before removing borrowed digits. If 2k>=e or the body width " + "is below64, use the elementary algorithm.", + "Otherwise write e=k+nw+ell with 0<=ell None: + if not condition: + raise SystemExit("FAIL: " + message) + + +def must_fail(thunk, message: str) -> None: + """A rejection control: the mutated claim must raise or return False.""" + try: + result = thunk() + except (ValueError, SystemExit): + return + need(result is False, "control accepted: " + message) + + +def pins_and_phrases() -> dict[str, bytes]: + sources = json.loads((PACKAGE / "SOURCES.json").read_text(encoding="utf-8")) + data = {} + for row in sources["files"]: + if row["usage"] == "input": + raw = (ROOT / row["path"]).read_bytes() + need(hashlib.sha256(raw).hexdigest() == row["sha256"], "pin " + row["path"]) + data[row["path"]] = raw + for path, phrases in PHRASES.items(): + text = " ".join(data[path].decode("utf-8").split()) + for phrase in phrases: + need(phrase in text, f"{path}: {phrase[:60]}") + return data + + +def load_allocator(raw: bytes): + """Execute the authenticated bytes, never a cached module.""" + module = types.ModuleType("crt_reservoir_allocator") + module.__file__ = str(ROOT / ALLOCATOR) + sys.modules[module.__name__] = module + exec(compile(raw, module.__file__, "exec"), module.__dict__) + return module + + +# ---------------------------------------------------------------- part A + +def interchange(payload: list[int], length: int, first, second, reverse=False) -> list[int]: + """One ordinary call: exchange two equal complete address fields. + + Physical position v is integer bit length-1-v (#4174 convention). The + record at address x moves to the address with the two fields swapped, + bit for bit in order. All other fields are spectators. + """ + width = first[1] - first[0] + need(width == second[1] - second[0], "unequal fields") + pairs = [] + for t in range(width): + u = first[0] + (width - 1 - t if reverse else t) + pairs.append((length - 1 - u, length - 1 - (second[0] + t))) + out = [0] * len(payload) + for x, record in enumerate(payload): + y = x + for bu, bv in pairs: + if ((x >> bu) ^ (x >> bv)) & 1: + y ^= (1 << bu) | (1 << bv) + out[y] = record + return out + + +def placement_permutation(placement, length: int) -> list[int]: + """Address map induced by Placement.map_position (bit at v moves to P(v)).""" + image = [] + for x in range(1 << length): + y = 0 + for v in range(length): + if (x >> (length - 1 - v)) & 1: + y |= 1 << (length - 1 - placement.map_position(v)) + image.append(y) + return image + + +def dirty(length: int) -> list[int]: + return [(x * 0x9E3779B1 + 12345) % 1000003 for x in range(1 << length)] + + +def part_a(allocator) -> int: + # Adjacent aligned sources as #4174 builds them, and scattered sources. + fixtures = ((12, 2, ((4, 6), (6, 8), (8, 10))), + (14, 2, ((8, 10), (4, 6), (10, 12)))) + checked = 0 + for length, width, sources in fixtures: + placement = allocator.Placement(length, width, sources) + need(len(placement.swaps) == 3, "three swaps") + start = dirty(length) + target = placement_permutation(placement, length) + expected = [0] * len(start) + for x, record in enumerate(start): + expected[target[x]] = record + for order in itertools.permutations(placement.swaps): + state = start + for first, second in order: # placement: three calls + state = interchange(state, length, first, second) + need(state == expected, "three calls realize P in every order") + for first, second in order: # restoration: same three calls + state = interchange(state, length, first, second) + need(state == start, "six calls restore every dirty record") + checked += 1 + # Controls: a dropped restoration call, or a reversing exchange, fail. + def dropped(): + state = start + for first, second in placement.swaps: + state = interchange(state, length, first, second) + for first, second in placement.swaps[:2]: + state = interchange(state, length, first, second) + return state == start + must_fail(dropped, "five calls restore") + def reversed_call(): + state = start + for first, second in placement.swaps: + state = interchange(state, length, first, second, reverse=True) + return state == expected + must_fail(reversed_call, "bit-reversing exchange realizes P") + must_fail(lambda: allocator.Placement(12, 2, ((2, 4), (6, 8), (8, 10))), + "a source overlapping destination T") + return checked + + +# ---------------------------------------------------------------- part B + +def disjoint(a, b) -> bool: + return a[1] <= b[0] or b[1] <= a[0] + + +def part_b(allocator, p: int, ell: int, widths) -> tuple: + layout = allocator.Layout(p, ell, widths) + L, H = layout.L, layout.H + plans = calls = 0 + for plan in allocator.iter_plans(layout): + swaps = plan.swaps + need(len(swaps) == 3, "three pairs") + need(tuple(d for _, d in swaps) == ((0, H), (H, 2 * H), (L - H, L)), + "destinations u, t, b") + blocks = [b for pair in swaps for b in pair] + need(all(b[1] - b[0] == H for b in blocks), "every field has width H") + need(all(disjoint(x, y) for x, y in itertools.combinations(blocks, 2)), + "six blocks pairwise disjoint") + lo, hi = plan.reservoir_interval + for source, _ in swaps: + need(lo <= source[0] and source[1] <= hi, "source inside reservoir") + for dep in plan.dependencies: + need(disjoint(source, dep.own_interval) + and disjoint(source, dep.left_interval), "source omitted by controls") + for v in plan.cuts: + for u in (v - 1, v): + if 0 <= u < L: + need(plan.map_position(plan.map_position(u)) == u, "involution") + plans += 1 + calls += 2 * len(swaps) + return layout, plans, calls + + +# ---------------------------------------------------------------- part C + +def depth(n: int) -> int: + return 0 if n < 64 else 1 + depth(42 * (n // 64)) + + +def gl_order() -> int: + q64 = Q ** 64 + order = 1 + power = 1 + for _ in range(64): + order *= q64 - power + power *= Q + return order + + +def stock_digits(dep: int) -> int: + """j(D): least j with q^j >= (269241600 N / q^4096)^D.""" + j = 0 + while Q ** j < M ** dep: + j += 1 + # (M (1 - 2/q))^D < (M N/q^4096)^D, so q^(j-1) is still too small. + need(j == 0 or Q ** (j - 1 + dep) < (M * (Q - 2)) ** dep, f"j({dep}) is exact") + return j + + +def wrapper(E: int, table) -> tuple[int, int, int, str]: + """Return (w, D, k, branch) for BIT.md section 4 at radix width E.""" + need(1 <= E < 1 << 576, "w formula range") + w = 1 if E == 1 else 2 # E^c in (1, 2] for 2 <= E < 2^576 + dep = depth(E) + k = (4096 * w * dep + table[dep]) if dep else 0 + if 2 * k >= E or (E - k) // w < 64: + return w, dep, k, "elementary" + return w, dep, k, "body" + + +def radix_width(H: int) -> int: + """Least E with q^E >= 2^H, for 1 <= H < 89 * 2^88 (PROOF.md lemma).""" + need(1 <= H < 89 << 88, "radix lemma range") + return H // 89 + 1 + + +def part_c() -> dict: + N = gl_order() + q4096 = Q ** 4096 + need(N < q4096 and N * Q > q4096 * (Q - 2), "1 - 2/q < N/q^4096 < 1") + need(1 < M < Q and M * (Q - 2) > Q, "4096 < log_q(269241600 N) < 4097") + table = tuple(stock_digits(dep) for dep in range(20)) + need(table == J, "j(D) table") + need(576 * 8667 <= 5000000, "E < 2^576 gives E^c <= 2, so w = 2") + branches = [wrapper(E, table)[3] for E in range(1, E_MIN + 1)] + need(all(b == "elementary" for b in branches[:-1]), "every E < 311309 elementary") + need(branches[-1] == "body", "E = 311309 is body") + need(wrapper(E_MIN, table)[:3] == (2, 19, 155654), "body entry values") + need(all(depth(E) >= 1 for E in range(64, 16387)), "D >= 1 on [64, 16386]") + for H in list(range(1, 3000)) + [10752, 15360]: + E = radix_width(H) + need(Q ** E >= 2 ** H and Q ** (E - 1) < 2 ** H, f"radix width at H={H}") + need(radix_width(H_MIN - 1) == E_MIN - 1 and radix_width(H_MIN) == E_MIN, "H_MIN") + need(radix_width(1458353) == 16386 and radix_width(1458354) == 16387, "robust edge") + return {"table": table} + + +def layout_branch(layout, table) -> tuple: + E = radix_width(layout.H) + return (E,) + wrapper(E, table) + + +# ---------------------------------------------------------------- part D + +def part_d() -> None: + need(A2 < Fraction(1, 500), "a2 < 1/500") + need(H_MIN < 2 ** 25, "H_MIN < 2^25") + # For 89 <= H < 2^25: E <= 2H/89 and H^a2 < 2^(25/500) <= 89/2. + need(Fraction(89, 2) ** 500 > 2 ** 25, "2^(1/20) < 89/2") + for H in range(1, 89): + need(radix_width(H) == 1, "E = 1 below 89") + for H in range(89, 20000): + need(89 * radix_width(H) <= 2 * H, "E <= 2H/89") + # Floating sanity only; the inequality above is the proof. + need(radix_width(10752) <= 10752 ** float(1 - A2), "minimal layout ratio") + + +# ---------------------------------------------------------------- main + +def controls(table) -> int: + count = 0 + for thunk, message in ( + (lambda: wrapper(E_MIN - 1, table)[3] == "body", "body one digit early"), + (lambda: radix_width(H_MIN - 1) >= E_MIN, "binary body one bit early"), + (lambda: wrapper(121, table)[2] == 8192, "stock without the 269241600 N factor"), + (lambda: wrapper(173, table)[1] == 1, "D(173) = 1"), + (lambda: gl_order() >= Q ** 4096, "N >= q^4096"), + ): + must_fail(thunk, message) + count += 1 + # Dropping j(D) moves the first body width, so the sharp claim depends on it. + first = next(E for E in range(1, E_MIN + 1) + if wrapper(E, (0,) * 20)[3] == "body") + need(first != E_MIN, "j(D) matters for E_MIN") + return count + 1 + + +def main() -> None: + data = pins_and_phrases() + allocator = load_allocator(data[ALLOCATOR]) + orders = part_a(allocator) + minimal, m_plans, m_calls = part_b(allocator, 1310720, 21, (20,) * 65536) + need((minimal.L, minimal.G, minimal.r_max, minimal.H) == (1310720, 2688, 4, 10752), + "minimal layout") + need((m_plans, m_calls) == (131072, 786432), "minimal plan and call counts") + widths = tuple(24 - (i % 2) for i in range(65536)) + production, p_plans, p_calls = part_b(allocator, 6 * sum(widths), 24, widths) + need((production.p, production.H, p_plans, p_calls) == (9240576, 15360, 104864, 629184), + "production layout") + table = part_c()["table"] + need(layout_branch(minimal, table) == (121, 2, 1, 8193, "elementary"), "minimal branch") + need(layout_branch(production, table) == (173, 2, 2, 16385, "elementary"), + "production branch") + need(100 * H_MIN == 2770641200 and minimal.H <= minimal.L // 100, "caller threshold") + part_d() + count = controls(table) + print(f"PASS_CRT_RESERVOIR_INTERCHANGE_BILL orders={orders} " + f"minimal_plans={m_plans} minimal_calls={m_calls} " + f"production_plans={p_plans} E_min={E_MIN} H_min={H_MIN} " + f"minimal=(H=10752,E=121,k=8193,elementary) controls={count + 5}") + + +if __name__ == "__main__": + main() From c88a655a8b5702f32873eab294c75a7d948615f5 Mon Sep 17 00:00:00 2001 From: JoyboyBrian Date: Thu, 22 Oct 2026 20:15:32 -0700 Subject: [PATCH 2/4] Bound the binary-to-radix padding of the literal callee at both layouts --- .../crt-reservoir-interchange-bill/PROOF.md | 19 +++++++++++++- .../crt-reservoir-interchange-bill/verify.py | 26 +++++++++++++++++-- 2 files changed, 42 insertions(+), 3 deletions(-) diff --git a/research/crt-reservoir-interchange-bill/PROOF.md b/research/crt-reservoir-interchange-bill/PROOF.md index 1cdf902570..f9109a58f0 100644 --- a/research/crt-reservoir-interchange-bill/PROOF.md +++ b/research/crt-reservoir-interchange-bill/PROOF.md @@ -97,6 +97,14 @@ CRT.md §4. In particular: per-digit constant of stage `a = 0`. On this range `H^{a} < 2^{1/20}`, so the saving `H^{-a}` is numerically absent. +**(v) Padding at the actual width.** The literal BIT.md call embeds both +`H`-bit fields into `q^E`. This multiplies the volume by +`(q^E/2^H)^2`, which lies in `(2^{33}, 2^{34})` at the minimal layout +and in `(2^{73}, 2^{74})` at the production layout. So the `q^2` factor +in (iv) is mostly realized, not slack. A direct binary exchange, made of +`H` single-bit swaps, would avoid the padding. That routine is not +BIT.md's machine, and its fixed-tape cost is not proved here. + **Answer to #4938's open question.** Yes. One #4174 three-field exchange is three ordinary width-`H` calls, and its restoration is the same three calls. Their cost fits `O(V H^{1-a} + V)` with multiplicity 6. At the @@ -209,6 +217,14 @@ on the embedded volume `V' < q^2 V`. Each swap costs `C_0 V'`. So one call costs at most `C_0 q^2 V E <= C_0 q^2 V H^{1-a}`, plus the embedding and its restriction, which are `O(q^2 V)`. ∎ +## 5a. Proof of (v) + +By Lemma R, `E = floor(H/89) + 1`. At `H = 10752`, `E = 121` and +`89E - H = 17`. The exact integer check +`2^{33 + 2·10752} < q^{242} < 2^{34 + 2·10752}` gives the first range. At +`H = 15360`, `E = 173` and `89E - H = 37`. The same check with exponents +73 and 74 gives the second range. ∎ + ## 6. Not proved here - BIT.md's theorem, including stage `a = 0`, its constant `C_0` and its @@ -236,9 +252,10 @@ its restriction, which are `O(q^2 V)`. ∎ at every `E <= 311309`, Lemma R on `H < 3000` and the table widths, and the `H*` edge. - **D.** The inequality of (iv). +- **E.** The two padding ranges of (v). Its rejection controls are: a dropped restoration call, a bit-reversing exchange, a source overlapping `T`, the body branch one digit or one bit early, the stock without `269241600 N`, `D(173) = 1`, `N >= q^{4096}`, -and `j(D)` dropped. Each must fail. The finite checks corroborate the +`j(D)` dropped, and padding below `2^{33}` or `2^{73}`. Each must fail. The finite checks corroborate the written argument; they do not replace it. diff --git a/research/crt-reservoir-interchange-bill/verify.py b/research/crt-reservoir-interchange-bill/verify.py index 49953bcdf2..0629f995c5 100644 --- a/research/crt-reservoir-interchange-bill/verify.py +++ b/research/crt-reservoir-interchange-bill/verify.py @@ -14,6 +14,8 @@ In binary this is H < 27706412. Both layouts are elementary. D. On that elementary range, E <= H^(1-a2), so the CRT.md per-call bill V H^(1-a) is met by the elementary stage alone. +E. The literal call pads the volume by (q^E/2^H)^2: in (2^33, 2^34) at the + minimal layout and in (2^73, 2^74) at the production layout. Rejection controls check that mutated claims fail. No new kappa is claimed. """ @@ -322,6 +324,24 @@ def part_d() -> None: need(radix_width(10752) <= 10752 ** float(1 - A2), "minimal layout ratio") +# ---------------------------------------------------------------- part E + +def padding_bits(H: int) -> tuple[int, int]: + """(lo, hi) with 2^lo < (q^E / 2^H)^2 < 2^hi for the literal BIT call.""" + E = radix_width(H) + square = Q ** (2 * E) + lo = 2 * (89 * E - H) - 1 + need(2 ** (lo + 2 * H) < square < 2 ** (lo + 1 + 2 * H), f"padding at H={H}") + return lo, lo + 1 + + +def part_e() -> None: + need(padding_bits(10752) == (33, 34), "minimal padding (2^33, 2^34)") + need(padding_bits(15360) == (73, 74), "production padding (2^73, 2^74)") + must_fail(lambda: 2 ** (33 + 2 * 10752) >= Q ** 242, "minimal padding below 2^33") + must_fail(lambda: 2 ** (73 + 2 * 15360) >= Q ** 346, "production padding below 2^73") + + # ---------------------------------------------------------------- main def controls(table) -> int: @@ -360,11 +380,13 @@ def main() -> None: "production branch") need(100 * H_MIN == 2770641200 and minimal.H <= minimal.L // 100, "caller threshold") part_d() - count = controls(table) + part_e() + count = controls(table) + 2 print(f"PASS_CRT_RESERVOIR_INTERCHANGE_BILL orders={orders} " f"minimal_plans={m_plans} minimal_calls={m_calls} " f"production_plans={p_plans} E_min={E_MIN} H_min={H_MIN} " - f"minimal=(H=10752,E=121,k=8193,elementary) controls={count + 5}") + f"minimal=(H=10752,E=121,k=8193,elementary,pad=2^33..2^34) " + f"controls={count + 5}") if __name__ == "__main__": From c53232e44c0d078dce2a732650012f735d08b35a Mon Sep 17 00:00:00 2001 From: JoyboyBrian Date: Thu, 22 Oct 2026 20:18:38 -0700 Subject: [PATCH 3/4] Document scope, evidence, open questions and replay commands for the interchange bill --- .../crt-reservoir-interchange-bill/README.md | 130 +++++++++++++++--- .../crt-reservoir-interchange-bill/TASK.json | 30 ++-- .../VERIFY.json | 14 +- 3 files changed, 142 insertions(+), 32 deletions(-) diff --git a/research/crt-reservoir-interchange-bill/README.md b/research/crt-reservoir-interchange-bill/README.md index 58b05b40dd..5f76c4c117 100644 --- a/research/crt-reservoir-interchange-bill/README.md +++ b/research/crt-reservoir-interchange-bill/README.md @@ -1,35 +1,129 @@ -# crt-reservoir-interchange-bill +# The #4174 reservoir exchange against the ordinary-interchange bill -**Draft; no new bound claimed.** +**Scoped counting proof, conditional on BIT.md's ordinary interchange as +stated. No new κ.** The selected conditional exponent stays +60403/20000000. This does not accept PR #4100. -## Scope and evidence +## Result -Original card: `uniform-transfer-audit`. Complete [TASK.json](TASK.json), including any scope -change and its connection to the bottleneck. Explain the result and limitations here. -Source commits, Git blobs and SHA256 pins are in [SOURCES.json](SOURCES.json). -The selected record and catalogue are historical provenance, so later priority -updates do not invalidate this package. Explicit --source files are live inputs -and must match their pins. Full Git history is needed to resolve provenance. +Pending PR #4938 asked whether one ordinary H-bit interchange of +`research/unconditional-batched-crt/CRT.md` §3–§4 fits its bill +`O(V H^{1-a} + V)` at the actual #4174 width `H = r_max G`. The callee is +BIT.md's machine. It "exchanges two complete equal e-bit binary address +fields, with arbitrary complete preceding, intervening and following +fields" in `O(V e^(1-a2))`, through a wrapper that falls back to +elementary q-digit swaps (`q = 2^89 - 1`) at small widths. + +[PROOF.md](PROOF.md) proves the following for every layout accepted by the +#4174 constructor, with `a = a2`. + +| Part | Statement | +|---|---| +| (i) | One `Plan.placement` (three sources to front `u`, front `t`, back `b`) is three ordinary calls of width exactly `H`, in any order. Restoration is the same three calls. That is six calls per batch, and every dirty record is restored. | +| (ii) | Given BIT.md's theorem, these cost at most `6 C_BIT V H^{1-a} + 6 c_own V`, which is CRT.md's bill with multiplicity 6. | +| (iii) | BIT.md's wrapper runs at radix width `E = floor(H/89) + 1`. It is elementary for every `H < 27,706,412` and body at `H = 27,706,412` (`E = 311309`, `D = 19`, `k = 155654`). Since `H <= L/100`, every layout with `L < 2,770,641,200` runs all six calls, and all twelve §4 shuttles, on the elementary branch. | +| (iv) | On that range `E <= H^{1-a}`, so the elementary stage alone meets the bill, with constant `C_0 q^2`. Also `H^{a} < 2^{1/20}`, so the `a2` saving is numerically absent. | +| (v) | The literal call pads the volume by `(q^E/2^H)^2`. This is in `(2^{33}, 2^{34})` at the minimal layout and `(2^{73}, 2^{74})` at production. | + +At the minimal layout `p = 1310720`, `ell = 21`, `d = 2^16`, widths 20 +(`G = 2688`, `r_max = 4`, `H = 10752`), we get `E = 121`, `w = 2`, +`D = 1` and `k = 8193`. Since `2k >= E`, every call is elementary. The +production layout `p = 9240576`, `ell = 24` (`H = 15360`) gives +`E = 173`, `D = 2`, `k = 16385`, also elementary. These two layout +results do not depend on the exact `D`. Any `D >= 1` makes +`H <= 1,458,353` elementary. + +**Answer.** Yes, the bill fits, with multiplicity 6. At these widths it +is met by BIT.md's elementary fallback, not by its body word. The constant +includes a real padding factor of up to `2^{34}` (minimal) or `2^{74}` +(production) per call. + +Not proved: BIT.md's theorem itself (used as stated; #4100 AUDIT.md +records that its physical suites are not all passing), the stage-0 +constant and embedding on fixed tapes, the rest of the §4 gadget, and the +reading of `D(e)` at radix width `E`. Remark 4 of the proof covers the +last for both layouts. + +## Evidence + +[verify.py](verify.py) authenticates its four input pins and the quoted +source phrases. It then executes the #4174 allocator bytes it has just +authenticated, and checks the following: + +- **A.** Two `Placement` fixtures with dirty payloads (4,096 and 16,384 + addresses). Three literal field-exchange calls realize `P` in all six + orders, and the same three calls restore every record. +- **B.** All 131,072 minimal-layout plans (786,432 calls) and all 104,864 + production plans (629,184 calls). Each has three disjoint width-`H` + pairs inside the reservoir, sources omitted by every dependency, and the + `u`, `t`, `b` destinations. +- **C.** The exact bounds `1 - 2/q < N/q^4096 < 1` with `N = |GL_64(F_q)|`, + the `j(D)` table, the wrapper branch at every `E <= 311309`, the radix + lemma, and the `H*` and robust edges. +- **D, E.** The inequality `E <= H^{1-a}` and both padding ranges. +- **Controls.** Thirteen rejection controls: a dropped restoration call, + a bit-reversing exchange, an overlapping source, the body branch one + digit or one bit early, the stock without `269241600 N`, `D(173) = 1`, + `N >= q^4096`, `j(D)` dropped, and both padding floors. Each must fail. + +Ten source mutations of sharp claims (for example `E_MIN`, `H_MIN`, the +`j` table, the radix formula, the call count and the padding range) all +make the verifier fail. The finite checks corroborate the written proof; +they do not replace it. + +## Scope + +Card `uniform-transfer-audit`, scope **refined** to the reservoir +placement's ordinary-callee bill. Canonical main fetched 2026-10-23 at +`cef4b52f2a59009865bf8eabde1be3f159063703`, priority revision 7. Source +pins are in [SOURCES.json](SOURCES.json). This answers open question 1 +of pending #4938 and the reservoir remainder of open question 2 in #4377 +and #4650. ## Reproduce -After completing the verifier and marking VERIFY.json ready, from repo root: +Python 3.12, standard library only, from the repository root: ```sh python3 scripts/research_package.py --package research/crt-reservoir-interchange-bill --check-only -python3.12 scripts/research_package.py --package research/crt-reservoir-interchange-bill +python3.12 -B scripts/research_package.py --package research/crt-reservoir-interchange-bill ``` -Declare all external inputs and pinned dependencies in VERIFY.json. The generic -hook is bounded; native/Lean or long replays need an explicit dedicated workflow. +The direct command `python3.12 -B research/crt-reservoir-interchange-bill/verify.py` +prints `PASS_CRT_RESERVOIR_INTERCHANGE_BILL` in about 8 seconds. ## Open next questions -Complete the structured `open_questions` list in TASK.json and explain it here: -the question, why it matters, a feasible first step and any blocker. If no next -question is justified, say so rather than inventing one. +The [structured list](TASK.json) has the same entries. + +1. **Does a direct binary exchange of `H` single-bit swaps meet the same + bill on fixed tapes without the `(q^E/2^H)^2` padding?** + - *Why it matters:* at the actual widths the literal BIT.md call pays + up to `2^{34}` (minimal) or `2^{74}` (production) extra volume per + call, and the `a2` saving is absent anyway. + - *First step:* write one bit swap at positions `i < j` as one fixed-tape + pass with a bounded buffer, and count its tape actions per record. + - *Blocked by:* nothing. It needs a tape model, not new mathematics. +2. **What is the stage-0 constant `C_0` of BIT.md's elementary q-digit + swap?** + - *Why it matters:* by (iii)–(iv) it is the whole callee constant at + every CRT layout with `L < 2.77 × 10^9`. + - *First step:* bound one q-digit transposition of two radix-q fields + with intervening fields on a fixed tape inventory. + - *Blocked by:* BIT.md does not state the elementary algorithm in + detail. ## Credit -Prepared by JoyboyBrian. Retain predecessor attribution and source-specific notices. -New work is Apache-2.0. Disclose substantial AI assistance in TASK.json. +Cinna Davis, PR #4100, for the CRT construction, BIT.md's ordinary +interchange and its wrapper. Hiroki KUMAZAKI (@kumagi), PR #4174, for the +reservoir constructor, the disjoint-exchange geometry and the six-exchange +invoice. unpaidmoon, PRs #4377 and #4650, for the evaluator bills and the +open question 2 this continues. Nick Petalas, PR #4845, for the full-batch +arena bill. +PR #4938 (JoyboyBrian, pending) for the layout binding and the question +answered here. + +Prepared by JoyboyBrian with substantial Anthropic Claude (Claude Code, +Opus 5.5) assistance. Apache-2.0. No independent human review and no +formal-kernel acceptance are claimed. diff --git a/research/crt-reservoir-interchange-bill/TASK.json b/research/crt-reservoir-interchange-bill/TASK.json index d5ee192b94..0853823c4d 100644 --- a/research/crt-reservoir-interchange-bill/TASK.json +++ b/research/crt-reservoir-interchange-bill/TASK.json @@ -53,22 +53,28 @@ } ] }, - "scope_status": "unchanged", - "actual_scope": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", - "scope_change_reason": null, - "bottleneck_link": "TODO: explain the causal connection or label this as a side result", + "scope_status": "refined", + "actual_scope": "Write one #4174 Plan.placement (three reservoir sources to front u, front t, back b) as calls of BIT.md's ordinary interchange, the callee CRT.md section 3-4 bills at O(V H^{1-a}+V). Count placement and restoration calls, and evaluate BIT.md section 4's wrapper branch at the actual width H = r_max G, starting with p = 1310720, ell = 21 (H = 10752) and the #4174 production layout.", + "scope_change_reason": "The card asks for one quantified #4100 step at its actual caller. This refines it to the reservoir side left open by #4377/#4650 open question 2 and pending #4938 open question 1: the ordinary-callee bill of the #4174 placement. BIT.md's theorem is used as stated, not reproved.", + "bottleneck_link": "Side result on the #4100 transfer obligations. It prices one inherited callee interface of the CRT route at its actual parameters. It does not change the selected exponent.", "budget_minutes": 90, - "stop_rule": "TODO", - "outcome": "in-progress", - "evidence": "TODO", + "stop_rule": "Stop after the six-call decomposition, the conditional bill, the exact wrapper branch threshold, the elementary-range inequality and the padding ranges at the two layouts. Do not reprove BIT.md, price the rest of the section 4 gadget, or claim a new kappa.", + "outcome": "completed", + "evidence": "PROOF.md proves (i)-(v). verify.py checks 12 exchange orders on dirty Placement fixtures, all 131072 minimal and 104864 production plans, the exact GL_64 order bounds and j(D) table, the wrapper branch at every E <= 311309, the radix lemma, the elementary inequality, the padding ranges and 13 rejection controls. It prints PASS_CRT_RESERVOIR_INTERCHANGE_BILL. Ten source mutations of sharp claims all fail.", "author": "JoyboyBrian", - "ai_assistance": "TODO: disclose tools used", + "ai_assistance": "Substantial assistance from Anthropic Claude (Claude Code, Opus 5.5)", "open_questions": [ { - "question": "TODO", - "why_it_matters": "TODO", - "first_step": "TODO", - "blocked_by": "TODO" + "question": "Does a direct binary exchange of H single-bit swaps meet the same bill on fixed tapes without the (q^E/2^H)^2 padding?", + "why_it_matters": "At the actual widths the literal BIT.md call pays up to 2^34 (minimal) or 2^74 (production) extra volume per call, and the a2 saving is absent anyway.", + "first_step": "Write one bit swap at positions i < j as one fixed-tape pass with a bounded buffer, and count its tape actions per record.", + "blocked_by": "Nothing; it needs a tape model, not new mathematics." + }, + { + "question": "What is the stage-0 constant C_0 of BIT.md's elementary q-digit swap?", + "why_it_matters": "By (iii)-(iv) it is the whole callee constant at every CRT layout with L < 2.77e9.", + "first_step": "Bound one q-digit transposition of two radix-q fields with intervening fields on a fixed tape inventory.", + "blocked_by": "BIT.md does not state the elementary algorithm in detail." } ] } diff --git a/research/crt-reservoir-interchange-bill/VERIFY.json b/research/crt-reservoir-interchange-bill/VERIFY.json index b4bb11f568..2282632c85 100644 --- a/research/crt-reservoir-interchange-bill/VERIFY.json +++ b/research/crt-reservoir-interchange-bill/VERIFY.json @@ -1,6 +1,6 @@ { "schema_version": 1, - "status": "draft", + "status": "ready", "python": "3.12", "requirements": [], "inputs": [ @@ -17,7 +17,17 @@ "{package}/verify.py" ], "timeout_seconds": 120, - "checks": "TODO: identity, positive fixture and failure controls" + "checks": "Six-call decomposition on dirty Placement fixtures (all orders, restoration, dropped-call and reversed-exchange controls); all minimal (p=1310720, ell=21) and production (p=9240576, ell=24) #4174 plans; exact BIT.md wrapper branch for every E <= 311309 (elementary below 311309, body at it; H* = 27706412); E <= H^(1-a2) on the elementary range; padding (2^33,2^34) and (2^73,2^74); 13 rejection controls." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same checks under -O; all checks use explicit exceptions." } ] } From f46ed7cafad5eee43223737f704521c79d6ba1ee Mon Sep 17 00:00:00 2001 From: JoyboyBrian Date: Thu, 22 Oct 2026 20:21:48 -0700 Subject: [PATCH 4/4] Cite #4942 for the wrapper-branch threshold and scope the new content to the six-call placement bill --- .../crt-reservoir-interchange-bill/PROOF.md | 19 ++++++-- .../crt-reservoir-interchange-bill/README.md | 45 ++++++++++++++----- .../crt-reservoir-interchange-bill/TASK.json | 4 +- 3 files changed, 51 insertions(+), 17 deletions(-) diff --git a/research/crt-reservoir-interchange-bill/PROOF.md b/research/crt-reservoir-interchange-bill/PROOF.md index f9109a58f0..7b5d72562a 100644 --- a/research/crt-reservoir-interchange-bill/PROOF.md +++ b/research/crt-reservoir-interchange-bill/PROOF.md @@ -4,6 +4,15 @@ theorem as stated. No new κ.** The selected conditional exponent stays 60403/20000000. +**Attribution of the parts.** Parts (i)–(ii) are this package's +contribution: the placement as ordinary calls and its call count. Parts +(iii)–(iv) were first obtained by James Reed in pending PR #4942 +(`research/crt-interchange-width-threshold`, head +`32fa3600a0e739d47dca98fdeb3abceda073f9f2`). #4942 also proves that every +width above the threshold is recursive, which is not needed here. Sections +4–5 below are an independent recomputation and agree with #4942. Part (v) +and Remark 4 are additional checks of this package. + ## 0. What CRT.md bills, and which callee it means CRT.md (#4100, Cinna Davis) prices its reservoir and switch gadget with @@ -78,7 +87,7 @@ borrowed input (one copy and one erase). This is CRT.md's 25,600 batches per synchronized switch layer, a layer pays at most 153,600 such calls. -**(iii) Branch at the actual width.** For `1 <= H < 89·2^88`, the wrapper +**(iii) Branch at the actual width (#4942; recomputed).** For `1 <= H < 89·2^88`, the wrapper runs at `E(H) = floor(H/89) + 1`. It takes the elementary branch for every `H < H* = 27,706,412`, and the body branch at `H = H*`. Since `H <= L/100`, every accepted layout with `L < 2,770,641,200` runs all six @@ -91,7 +100,7 @@ CRT.md §4. In particular: | #4174 production, `p = 9240576`, `ell = 24` | 15360 | 173 | 2 | 2 | 16385 | elementary | | first body width | 27706412 | 311309 | 2 | 19 | 155654 | body | -**(iv) The elementary branch meets the bill.** For `1 <= H < H*`, +**(iv) The elementary branch meets the bill (agrees with #4942).** For `1 <= H < H*`, `E(H) <= H^{1-a}`. So each elementary call costs at most `C_0 q^2 V H^{1-a}` plus the `O(q^2 V)` embedding. Here `C_0` is the per-digit constant of stage `a = 0`. On this range `H^{a} < 2^{1/20}`, @@ -145,7 +154,7 @@ a fixed inventory, the caller copies the output back and erases it, or swaps tape roles and erases the old input. Either costs at most `c_own V`. The batch bound is #4174's. ∎ -## 4. Proof of (iii) +## 4. Proof of (iii), recomputing #4942 **Lemma R (radix width).** For `1 <= H < 89·2^88`, the least `E` with `q^E >= 2^H` is `floor(H/89) + 1`. @@ -205,7 +214,7 @@ any reading with stock at least `K(w)` and `w >= 2` gives `k >= 8193`, so `2k >= 16386 >= E`. So `H <= 1,458,353` is elementary whatever `D` is, provided `D >= 1`. Both table layouts are far below. -## 5. Proof of (iv) +## 5. Proof of (iv), recomputing #4942 If `H < 89`, then `E = 1 <= H^{1-a}`. If `89 <= H < H*`, then `E <= H/89 + 1 <= 2H/89`. Also `H* < 2^25` and `a < 1/500`, so @@ -235,6 +244,8 @@ By Lemma R, `E = floor(H/89) + 1`. At `H = 10752`, `E = 121` and reinsertion, the last-`K` branch, and #4377's evaluator model. - Whether `D` is meant at the radix width `E`. Remark 4 covers the two table layouts under any `D >= 1`. +- That every width above `H*` is recursive. #4942 proves it; it is not + used here. - Any κ change or selected-frontier change. ## 7. Verification diff --git a/research/crt-reservoir-interchange-bill/README.md b/research/crt-reservoir-interchange-bill/README.md index 5f76c4c117..233a889083 100644 --- a/research/crt-reservoir-interchange-bill/README.md +++ b/research/crt-reservoir-interchange-bill/README.md @@ -14,6 +14,20 @@ fields, with arbitrary complete preceding, intervening and following fields" in `O(V e^(1-a2))`, through a wrapper that falls back to elementary q-digit swaps (`q = 2^89 - 1`) at small widths. +**Relation to #4942.** James Reed's PR #4942 (pending, head +`32fa3600a0e739d47dca98fdeb3abceda073f9f2`) was claimed a minute before this +package. It already evaluates BIT.md §4's wrapper branch at the reservoir +width: elementary exactly for q-ary `E <= 311308` (binary `h < 27706412`), +`D = 19`, `k = 155654`, `E = 121` at `H = 10752` and `E = 173` at +`H = 15360`. It also proves that every larger width is recursive. **#4942 is +the predecessor for parts (iii)–(iv) below.** This package recomputed them +independently and agrees; it claims no novelty for the threshold. + +**New here:** parts (i)–(ii), the write-up of one `Plan.placement` as +ordinary calls and the count of placement and restoration calls with the +resulting 6x bill. Also new: the padding ranges (v) and the +`D`-independent bound of Remark 4. + [PROOF.md](PROOF.md) proves the following for every layout accepted by the #4174 constructor, with `a = a2`. @@ -21,20 +35,21 @@ elementary q-digit swaps (`q = 2^89 - 1`) at small widths. |---|---| | (i) | One `Plan.placement` (three sources to front `u`, front `t`, back `b`) is three ordinary calls of width exactly `H`, in any order. Restoration is the same three calls. That is six calls per batch, and every dirty record is restored. | | (ii) | Given BIT.md's theorem, these cost at most `6 C_BIT V H^{1-a} + 6 c_own V`, which is CRT.md's bill with multiplicity 6. | -| (iii) | BIT.md's wrapper runs at radix width `E = floor(H/89) + 1`. It is elementary for every `H < 27,706,412` and body at `H = 27,706,412` (`E = 311309`, `D = 19`, `k = 155654`). Since `H <= L/100`, every layout with `L < 2,770,641,200` runs all six calls, and all twelve §4 shuttles, on the elementary branch. | -| (iv) | On that range `E <= H^{1-a}`, so the elementary stage alone meets the bill, with constant `C_0 q^2`. Also `H^{a} < 2^{1/20}`, so the `a2` saving is numerically absent. | +| (iii) | *Recomputation of #4942.* BIT.md's wrapper runs at radix width `E = floor(H/89) + 1`. It is elementary for every `H < 27,706,412` and body at `H = 27,706,412` (`E = 311309`, `D = 19`, `k = 155654`). Since `H <= L/100`, every layout with `L < 2,770,641,200` runs all six calls, and all twelve §4 shuttles, on the elementary branch. | +| (iv) | *Agrees with #4942's `E^{a2} < 2^{0.033}`.* On that range `E <= H^{1-a}`, so the elementary stage alone meets the bill, with constant `C_0 q^2`. Also `H^{a} < 2^{1/20}`, so the `a2` saving is numerically absent. | | (v) | The literal call pads the volume by `(q^E/2^H)^2`. This is in `(2^{33}, 2^{34})` at the minimal layout and `(2^{73}, 2^{74})` at production. | At the minimal layout `p = 1310720`, `ell = 21`, `d = 2^16`, widths 20 (`G = 2688`, `r_max = 4`, `H = 10752`), we get `E = 121`, `w = 2`, `D = 1` and `k = 8193`. Since `2k >= E`, every call is elementary. The production layout `p = 9240576`, `ell = 24` (`H = 15360`) gives -`E = 173`, `D = 2`, `k = 16385`, also elementary. These two layout -results do not depend on the exact `D`. Any `D >= 1` makes -`H <= 1,458,353` elementary. +`E = 173`, `D = 2`, `k = 16385`, also elementary. These values agree with +#4942. As an extra check of this package, the two layout results do not +depend on the exact `D`: any `D >= 1` makes `H <= 1,458,353` elementary. **Answer.** Yes, the bill fits, with multiplicity 6. At these widths it -is met by BIT.md's elementary fallback, not by its body word. The constant +is met by BIT.md's elementary fallback, not by its body word, as #4942 +also finds. The constant includes a real padding factor of up to `2^{34}` (minimal) or `2^{74}` (production) per call. @@ -57,7 +72,7 @@ authenticated, and checks the following: production plans (629,184 calls). Each has three disjoint width-`H` pairs inside the reservoir, sources omitted by every dependency, and the `u`, `t`, `b` destinations. -- **C.** The exact bounds `1 - 2/q < N/q^4096 < 1` with `N = |GL_64(F_q)|`, +- **C.** An independent recomputation of #4942's branch values: the exact bounds `1 - 2/q < N/q^4096 < 1` with `N = |GL_64(F_q)|`, the `j(D)` table, the wrapper branch at every `E <= 311309`, the radix lemma, and the `H*` and robust edges. - **D, E.** The inequality `E <= H^{1-a}` and both padding ranges. @@ -77,8 +92,14 @@ Card `uniform-transfer-audit`, scope **refined** to the reservoir placement's ordinary-callee bill. Canonical main fetched 2026-10-23 at `cef4b52f2a59009865bf8eabde1be3f159063703`, priority revision 7. Source pins are in [SOURCES.json](SOURCES.json). This answers open question 1 -of pending #4938 and the reservoir remainder of open question 2 in #4377 -and #4650. +of pending #4938 together with #4942, and the reservoir remainder of open +question 2 in #4377 and #4650. + +**Overlap.** James Reed's CLAIM for #4942 (discussion #1166, comment +19136868) and this package's CLAIM (comment 19136883) crossed one minute +apart. #4942 covers the wrapper branch and states that the three-field +placement is not covered. This package therefore cites #4942 for the branch +and contributes the placement call count. ## Reproduce @@ -121,8 +142,10 @@ reservoir constructor, the disjoint-exchange geometry and the six-exchange invoice. unpaidmoon, PRs #4377 and #4650, for the evaluator bills and the open question 2 this continues. Nick Petalas, PR #4845, for the full-batch arena bill. -PR #4938 (JoyboyBrian, pending) for the layout binding and the question -answered here. +James Reed (jwr404), PR #4942 (pending), for the wrapper-branch threshold +and the `E`/`k` values at both layouts, recomputed here. PR #4938 +(JoyboyBrian, pending) for the layout binding and the question answered +here. Prepared by JoyboyBrian with substantial Anthropic Claude (Claude Code, Opus 5.5) assistance. Apache-2.0. No independent human review and no diff --git a/research/crt-reservoir-interchange-bill/TASK.json b/research/crt-reservoir-interchange-bill/TASK.json index 0853823c4d..34186df771 100644 --- a/research/crt-reservoir-interchange-bill/TASK.json +++ b/research/crt-reservoir-interchange-bill/TASK.json @@ -55,12 +55,12 @@ }, "scope_status": "refined", "actual_scope": "Write one #4174 Plan.placement (three reservoir sources to front u, front t, back b) as calls of BIT.md's ordinary interchange, the callee CRT.md section 3-4 bills at O(V H^{1-a}+V). Count placement and restoration calls, and evaluate BIT.md section 4's wrapper branch at the actual width H = r_max G, starting with p = 1310720, ell = 21 (H = 10752) and the #4174 production layout.", - "scope_change_reason": "The card asks for one quantified #4100 step at its actual caller. This refines it to the reservoir side left open by #4377/#4650 open question 2 and pending #4938 open question 1: the ordinary-callee bill of the #4174 placement. BIT.md's theorem is used as stated, not reproved.", + "scope_change_reason": "The card asks for one quantified #4100 step at its actual caller. This refines it to the reservoir side left open by #4377/#4650 open question 2 and pending #4938 open question 1: the ordinary-callee bill of the #4174 placement. BIT.md's theorem is used as stated, not reproved. The wrapper-branch threshold (parts iii-iv) was first delivered by James Reed's pending PR #4942, whose claim crossed this one; it is recomputed here and cited, not claimed as new. The new content is parts (i)-(ii), the six-call placement/restoration count and its 6x bill, plus the padding ranges (v) and the D-independent Remark 4.", "bottleneck_link": "Side result on the #4100 transfer obligations. It prices one inherited callee interface of the CRT route at its actual parameters. It does not change the selected exponent.", "budget_minutes": 90, "stop_rule": "Stop after the six-call decomposition, the conditional bill, the exact wrapper branch threshold, the elementary-range inequality and the padding ranges at the two layouts. Do not reprove BIT.md, price the rest of the section 4 gadget, or claim a new kappa.", "outcome": "completed", - "evidence": "PROOF.md proves (i)-(v). verify.py checks 12 exchange orders on dirty Placement fixtures, all 131072 minimal and 104864 production plans, the exact GL_64 order bounds and j(D) table, the wrapper branch at every E <= 311309, the radix lemma, the elementary inequality, the padding ranges and 13 rejection controls. It prints PASS_CRT_RESERVOIR_INTERCHANGE_BILL. Ten source mutations of sharp claims all fail.", + "evidence": "PROOF.md proves (i)-(ii) and (v), and recomputes #4942's (iii)-(iv). verify.py checks 12 exchange orders on dirty Placement fixtures, all 131072 minimal and 104864 production plans, the exact GL_64 order bounds and j(D) table, the wrapper branch at every E <= 311309, the radix lemma, the elementary inequality, the padding ranges and 13 rejection controls. It prints PASS_CRT_RESERVOIR_INTERCHANGE_BILL. Ten source mutations of sharp claims all fail.", "author": "JoyboyBrian", "ai_assistance": "Substantial assistance from Anthropic Claude (Claude Code, Opus 5.5)", "open_questions": [