diff --git a/research/crt-interchange-width-threshold/README.md b/research/crt-interchange-width-threshold/README.md new file mode 100644 index 0000000000..d39ab092e5 --- /dev/null +++ b/research/crt-interchange-width-threshold/README.md @@ -0,0 +1,133 @@ +# Ordinary interchange threshold at the reservoir width + +**Scoped exact computation with a written all-width argument. No new κ.** +The selected conditional exponent stays 60403/20000000. This does not +accept PR #4100. + +## Result + +BIT.md §4 runs the elementary digit-swap algorithm when `2k ≥ e` or the +body width is below 64. Here `e` is the q-ary field width, `q = 2^89 − 1`, +and `k` is the least integer with `q^k ≥ K(w)^{D(e)}`. Evaluated exactly, +this test gives: + +1. **Exact threshold.** The elementary branch runs exactly for q-ary widths + `e ≤ 311308`. Every width `e ≥ 311309` takes the recursive branch. + In binary, an `h`-bit field reaches the recursive branch exactly when + `h ≥ 27706412`. +2. **Every #4174 reservoir up to 2.77 · 10^9 bits is elementary.** Since + `r_max = floor(L/(100G))`, `H = r_max G ≤ L/100`. A recursive H-bit + interchange therefore needs `L ≥ 2770641200`. The production plan + `p = 9240576`, `ell = 24` has `L = 1540096`, which is 1,799 times too + short. Its `H = 15360` bits is 173 q-digits. The smallest layout with + `L ≤ p` from #4938 (`p = 1310720`, `ell = 21`) has `H = 10752`, which + is 121 q-digits. Both are elementary. +3. **What this means for #4938's question.** One ordinary H-bit interchange + does fit `O(V H^{1−a} + V)`, because BIT.md's statement is uniform and + its finitely many elementary widths are absorbed into the constant. On + every elementary width, `E^{a2} < 2^{19 a2} < 2^{0.033}`, so the absorption + costs at most that factor over the elementary constant. At the actual + #4174 width, however, the factor `H^{−a}` is not realized. The callee does + elementary swaps, so there is no width saving. + +## Argument + +Fix `w`. BIT.md takes `w = ceil(e^c)` with `c = 8667/5000000`, so +`w = 2` exactly for `2 ≤ e ≤ 2^{1/c}`, and `1/c > 576`. Width `e = 1` is +elementary trivially. + +*Stock digits.* Write `β = 269241600 N` with `N = |GL_64(F_q)|`. The +verifier checks `q^4096 < β < q^4097` exactly. At `w = 2`, +`K^D = q^{4096D} β^D`, so `k = 4096 D + j(D)`, where `j(D)` is the least +`j` with `q^j ≥ β^D`. Then `4096 D < j(D) ≤ 4097 D`, and `k ≤ 8193 D`. +The verifier computes `j(D)` exactly for `D ≤ 20`. In particular +`k = 155654` at `D = 19`, so `2k = 311308`. + +*Depth blocks.* The map `n ↦ 42 floor(n/64)` is nondecreasing, so `D` is +nondecreasing by induction. `D(e) = D` therefore holds exactly on the block +`[m_D, m_{D+1})`, with `m_1 = 64` and `m_{D+1} = 64 ceil(m_D/42)`. Since +`k` depends on `e` only through `D(e)` at fixed `w`, the elementary set in +each block is an initial segment, ending at `max(2k_D, k_D + 127)`. + +*Below the D = 20 block.* The verifier checks every width +`2 ≤ e < m_20` against the literal test. The result is elementary exactly +for `e ≤ 311308`. That boundary lies inside the `D = 19` block. + +*From D = 20 up to 2^576.* For each block start `m_D ≤ 2^576` with +`D ≥ 20`, the verifier checks `2 · 8193 D < m_D` and +`(m_D − 8193 D)/2 ≥ 64`. By the block property, each whole block is then +recursive. There are finitely many such blocks, and all of them are +checked. + +*Beyond 2^576 (`w ≥ 3`).* Put `x = log2 e ≥ 576`. Then +`w ≤ e^c + 1 ≤ 2^{cx+1}`. Each depth step multiplies by at most `21/32`, +so `D ≤ 1 + 1.65 x`. Also `k ≤ (4096 w + 1) D + D`. Together these give +`2k < 2^{17 + cx + log2 x}`, and at `x = 576` the exponent is below +`575 < x − 1`. The gap `x − cx − log2 x` increases for `x ≥ 2`, so +`2k < e/2` for all larger `e`. The body width `(e − k)/w ≥ e/2^{cx+2}` is +far above 64. This range lies far outside any physical width and is +included only so that the threshold statement covers all `e`. + +*Binary widths.* BIT.md embeds `2^h` into `q^E`, with `E` least such that +`q^E ≥ 2^h`. Then `E ≤ 311308` exactly when `2^h ≤ q^311308`. The bit +length of `q^311308` is 27706412, so the recursive branch starts at +`h = 27706412`. + +*Both stages.* The test depends only on `e`, `w` and the fixed stock, and +not on the preceding saving `a`. The `a = 0 → a1` and `a1 → a2` wrappers +therefore share this threshold. + +## Scope + +Card `uniform-transfer-audit`, scope **refined** to the callee's branch at +the reservoir width (see `TASK.json`). This package follows BIT.md §4 as +written: the stock is `K(w)^{D(e)}` on the original radix width, and the +body width is `n = floor((e − k)/w)`. + +The following are not covered: the constants `C` and `c_el` (BIT.md gives +neither), the three-field placement (#4174 proves it), the guard scan, the +sparse repair, and any statement about the complete CRT or multiplication +theorem. The threshold is a fact about the callee as written. A smaller +stock or a different wrapper test would move it. + +Base: canonical main `cef4b52f2a59009865bf8eabde1be3f159063703`, +priority revision 7, fetched 2026-10-23T03:05Z. `find_overlap.py`, the PR +search for "interchange" and the handoff thread found no open claim on this +threshold. That is a search result, not a novelty proof. Claim: +[#1166 comment](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19136868). + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -B research/crt-interchange-width-threshold/verify.py +python3.12 -B scripts/research_package.py --package research/crt-interchange-width-threshold +``` + +The direct command prints `PASS_CRT_INTERCHANGE_WIDTH_THRESHOLD` in about +20 seconds. Most of that time goes to the exact `β^D` comparisons. Changing +the q-ary boundary to 311309, the binary boundary to 27706411 or the +production q-width to 172 makes the verifier fail. + +## Open next questions + +1. **At what reservoir length does the composed CRT bill first beat the + elementary-callee bill?** Below `L = 2770641200` every reservoir exchange + is elementary. Any CRT-layer saving in that range has to come from some + other source. *First step:* write the per-layer cost as `c_el V H` + (elementary) and `C V H^{1−a2}` (recursive), then solve for the smallest + #4174 layout at a stated ratio `C/c_el`. *Blocked by:* BIT.md states + neither constant, so the answer is conditional on the stated ratio. + +## Credit + +Cinna Davis, PR #4100, for the CRT construction, BIT.md and its wrapper +test. Hiroki KUMAZAKI (@kumagi), PR #4174, for the constructor and the +production plan. JoyboyBrian, PR #4938, for the evaluator binding and the +open question. PR2195, PR2234, PR2753/2809, PR2899 and PR2915 for the +retained interchange assembly lineage credited in BIT.md. + +Prepared by James Reed with substantial Anthropic Claude (Claude Code) +assistance. Apache-2.0. No independent human review and no formal-kernel +acceptance are claimed. diff --git a/research/crt-interchange-width-threshold/SOURCES.json b/research/crt-interchange-width-threshold/SOURCES.json new file mode 100644 index 0000000000..a6bc4b4e6c --- /dev/null +++ b/research/crt-interchange-width-threshold/SOURCES.json @@ -0,0 +1,36 @@ +{ + "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/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" + }, + { + "path": "research/crt-reservoir-placement/allocator.py", + "usage": "input", + "git_blob": "4b3ad89652a28f7d142248d1b5747272e696493c", + "sha256": "b764195fc6291e3c8fa8297b1f4ceaefc119d5664d8ff348b49eac8a2e79c688" + } + ] +} diff --git a/research/crt-interchange-width-threshold/TASK.json b/research/crt-interchange-width-threshold/TASK.json new file mode 100644 index 0000000000..dae07bf6e1 --- /dev/null +++ b/research/crt-interchange-width-threshold/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": "refined", + "actual_scope": "Decide whether BIT.md section 4's ordinary interchange runs its recursive or elementary branch at the #4174 reservoir width H = r_max G, by evaluating the wrapper test 2k >= e (or body width below 64) exactly at every q-ary width.", + "scope_change_reason": "PR #4938 open question 1 asks whether one ordinary H-bit interchange fits O(V H^(1-a) + V) at the actual #4174 width. The callee's statement is uniform in width, so the remaining content is which branch the callee takes at that width. This package computes the exact branch threshold and compares it with H. It does not price the elementary algorithm's constant, the three-field placement, or any other CRT step.", + "bottleneck_link": "The CRT layer's saving a - 2(1-epsilon) assumes the interchange's h^(-a) gain. Below the computed width the callee realizes no gain. That holds at the production plan and at every #4174 layout with L below 100 times the threshold. The asymptotic statement is unchanged, and so is the selected frontier.", + "budget_minutes": 60, + "stop_rule": "Stop after the exact threshold, its all-width monotonicity argument and the comparison with H on the two cited #4174 layouts. Do not build an interchange, price constants or revisit placement.", + "outcome": "completed", + "evidence": "python3.12 -B scripts/research_package.py --package research/crt-interchange-width-threshold", + "author": "James Reed", + "ai_assistance": "Substantial assistance from Anthropic Claude (Claude Code, Opus 5.5).", + "open_questions": [ + { + "question": "Does the CRT layer's claimed saving survive with the interchange's actual threshold, i.e. at which reservoir length does the composed O(V p^(1-a) ell^2 polylog p) bill first improve on the elementary-callee bill, once the K = O(ell + log p) colors and O(ell log d) layers are counted?", + "why_it_matters": "Below L = 2,770,641,200 bits every reservoir interchange is elementary, so any CRT-layer saving below that size must come from elsewhere.", + "first_step": "Write the per-layer cost with an elementary callee as c_el V H and with a recursive callee as C V H^(1-a2), and find the smallest #4174 layout where the recursive form is smaller for a stated ratio C/c_el.", + "blocked_by": "The constants C and c_el are not stated in BIT.md; any answer is conditional on a stated ratio." + } + ] +} diff --git a/research/crt-interchange-width-threshold/VERIFY.json b/research/crt-interchange-width-threshold/VERIFY.json new file mode 100644 index 0000000000..ff88041cf7 --- /dev/null +++ b/research/crt-interchange-width-threshold/VERIFY.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/unconditional-batched-crt/BIT.md", + "research/unconditional-batched-crt/CRT.md", + "research/crt-reservoir-placement/allocator.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Exact BIT.md section 4 branch test at w=2: elementary exactly for q-ary widths E <= 311308 (exhaustive below the D=20 block, block induction to 2^576, written bound beyond). Binary threshold 27706412 bits. The #4174 production H=15360 (173 q-digits) and smallest L<=p H=10752 (121 q-digits) are elementary; a recursive call needs L >= 2770641200." + } + ] +} diff --git a/research/crt-interchange-width-threshold/verify.py b/research/crt-interchange-width-threshold/verify.py new file mode 100644 index 0000000000..c9dd4119f1 --- /dev/null +++ b/research/crt-interchange-width-threshold/verify.py @@ -0,0 +1,200 @@ +#!/usr/bin/env python3 +"""Width threshold of the ordinary interchange's recursive branch. + +BIT.md section 4 runs the elementary digit-swap algorithm whenever +2k >= e or the body width is below 64. This verifier computes that test +exactly, finds the q-ary and binary width thresholds, and compares them +with the #4174 reservoir width H = r_max G. No new kappa is claimed. +""" + +from __future__ import annotations + +import hashlib +import importlib.util +import json +import sys +from fractions import Fraction +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = ROOT / "research" / "crt-interchange-width-threshold" +BIT = ROOT / "research/unconditional-batched-crt/BIT.md" +CRT = ROOT / "research/unconditional-batched-crt/CRT.md" +ALLOCATOR = ROOT / "research/crt-reservoir-placement/allocator.py" + +Q = (1 << 89) - 1 +C = Fraction(8667, 5000000) +A2 = C * (1 - C * C) +LAST_ELEMENTARY = 311308 +BINARY_THRESHOLD = 27706412 + +BIT_PHRASES = ( + "q=2^89-1,", + "c=8667/5000000,", + "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), and retain that w at every descendant.", + "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", + "failures occur at only finitely many widths. Otherwise write e=k+nw+ell", + "Finally embed each 2^e binary field into q^E, E=ceil(log_q(2^e)); each", +) +CRT_PHRASES = ( + "G=64(ell+ceil(log2(p+2))), B=2^G, K=64G,", + "r_max=floor(L/(100G)), H=r_max G.", + "One color uses O(1) ordinary H-bit interchanges plus linear scans and paid", + "repair. It costs O(V H^(1-a)+V). With K colors and H<=L=O(p), one switch", +) + + +def need(condition: bool, message: str) -> None: + if not condition: + raise SystemExit("FAIL: " + message) + + +def pins_and_phrases() -> None: + sources = json.loads((PACKAGE / "SOURCES.json").read_text(encoding="utf-8")) + for row in sources["files"]: + if row["usage"] == "input": + digest = hashlib.sha256((ROOT / row["path"]).read_bytes()).hexdigest() + need(digest == row["sha256"], row["path"]) + bit = BIT.read_text(encoding="utf-8") + for phrase in BIT_PHRASES: + need(phrase in bit, "BIT.md phrase: " + phrase) + crt = CRT.read_text(encoding="utf-8") + for phrase in CRT_PHRASES: + need(phrase in crt, "CRT.md phrase: " + phrase) + selected = json.loads( + (ROOT / "certificates/selected-result.json").read_text(encoding="utf-8") + ) + need(selected["kappa"] == "60403/20000000", "selected kappa") + + +def depth(n: int) -> int: + count = 0 + while n >= 64: + n = 42 * (n // 64) + count += 1 + return count + + +def block_starts(limit: int) -> list[int]: + """m[D] is the least n with depth(n) = D, for every block starting below limit.""" + starts = [0, 64] + while starts[-1] < limit: + starts.append(64 * -(-starts[-1] // 42)) + return starts + + +def stock_digits(max_depth: int) -> list[int]: + """j[D] is the least j with q^j >= (269241600 N)^D, so k = 4096 D + j[D] at w=2.""" + group_order = 1 + for i in range(64): + group_order *= Q**64 - Q**i + base = 269241600 * group_order + need(Q**4096 < base < Q**4097, "269241600 N lies strictly between q^4096 and q^4097") + digits = [] + power = 1 + for d in range(max_depth + 1): + guess = 4096 * d + (31475 * d + 99999) // 100000 + while Q ** (guess - 1) >= power: + guess -= 1 + while Q**guess < power: + guess += 1 + need(Q ** (guess - 1) < power <= Q**guess, f"exact stock digits at D={d}") + digits.append(guess) + power *= base + for d in range(1, max_depth + 1): + need(0 <= digits[d] - digits[d - 1] - 4096 <= 1, f"stock increment at D={d}") + return digits + + +def elementary(width: int, digits: list[int]) -> bool: + """BIT.md section 4 test at w = 2, valid for 2 <= width <= 2^576.""" + k = 4096 * depth(width) + digits[depth(width)] + return 2 * k >= width or (width - k) // 2 < 64 + + +def threshold(digits: list[int]) -> None: + # w = ceil(E^c) = 2 exactly when 2 <= E <= 2^(1/c); 1/c > 576. + need(Fraction(1) / C > 576, "w = 2 on 2 <= E <= 2^576") + starts = block_starts(1 << 20) + for d in range(1, len(starts) - 1): + need(depth(starts[d]) == d and depth(starts[d] - 1) == d - 1, f"block {d} start") + need(starts[19] <= LAST_ELEMENTARY < starts[20], "the boundary lies in the D=19 block") + k19 = 4096 * 19 + digits[19] + need(k19 == 155654 and 2 * k19 == LAST_ELEMENTARY, "2 k = 311308 at D = 19") + # Exhaustive check below the boundary block's end, and the boundary itself. + for width in range(2, starts[20]): + need(elementary(width, digits) == (width <= LAST_ELEMENTARY), f"width {width}") + # Larger blocks with w = 2. Since 269241600 N < q^4097, j[D] <= 4097 D and k <= 8193 D. + starts = block_starts(1 << 577) + for d in range(20, len(starts)): + if starts[d] > 1 << 576: + break + bound = 8193 * d + need(2 * bound < starts[d] and (starts[d] - bound) // 2 >= 64, f"block {d}") + # The w >= 3 range E > 2^576: 2k < 2^(17 + c x + log2 x) < 2^(x-1) at x = 576. + need(17 + C * 576 + 10 < 575, "w >= 3 range") + + +def binary_threshold() -> None: + power = Q**LAST_ELEMENTARY + need(power.bit_length() == BINARY_THRESHOLD, "binary width threshold") + need(BINARY_THRESHOLD - 1 < 89 * LAST_ELEMENTARY, "consistent with log2 q < 89") + + +def q_width(bits: int) -> int: + width = 0 + power = 1 + while power < 1 << bits: + power *= Q + width += 1 + return width + + +def load_allocator(): + spec = importlib.util.spec_from_file_location("crt_reservoir_allocator", ALLOCATOR) + module = importlib.util.module_from_spec(spec) + sys.modules[spec.name] = module + spec.loader.exec_module(module) + return module + + +def layouts(allocator, digits: list[int]) -> None: + production = allocator.Layout(9240576, 24, (24, 23) * 32768) + need(production.L == 1540096 and production.r_max == 5, "production layout") + need(production.H == 15360 and q_width(production.H) == 173, "production H") + need(elementary(173, digits), "production interchange is elementary") + floor = allocator.Layout(1310720, 21, (20,) * 65536) + need(floor.L == 1310720 and floor.r_max == 4, "smallest L <= p layout") + need(floor.H == 10752 and q_width(floor.H) == 121, "smallest L <= p H") + need(elementary(121, digits), "smallest-layout interchange is elementary") + # r_max = floor(L/(100G)) gives H <= L/100, so a recursive call needs L >= 100 e*. + need(100 * production.H <= production.L and 100 * floor.H <= floor.L, "H <= L/100") + need(100 * BINARY_THRESHOLD == 2770641200, "length needed for a recursive call") + need(2770641200 // production.L == 1799, "ratio to the production length") + + +def absorption() -> None: + # E < 2^19 on every elementary width, so E^a2 < 2^(19 a2) < 2^0.033. + need(LAST_ELEMENTARY < 1 << 19, "elementary widths are below 2^19") + need(19 * A2 < Fraction(33, 1000), "19 a2 < 0.033") + + +def main() -> None: + pins_and_phrases() + digits = stock_digits(20) + threshold(digits) + binary_threshold() + layouts(load_allocator(), digits) + absorption() + print( + "PASS_CRT_INTERCHANGE_WIDTH_THRESHOLD " + f"last_elementary_q_width={LAST_ELEMENTARY} binary_threshold={BINARY_THRESHOLD} " + "production_q_width=173" + ) + + +if __name__ == "__main__": + main()