From 915b94b890cde927fba98e02db32ae2864f6bf05 Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 10:20:52 +0700 Subject: [PATCH] =?UTF-8?q?Independently=20recompute=20#4507's=20chronolog?= =?UTF-8?q?ical=20batch=20widths=20(p7=20rank=201000:=2017,504=20->=202,52?= =?UTF-8?q?4=20bits;=20175=20vs=20700;=20no=20new=20=CE=BA)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 5.5 --- research/batch-width-recount/README.md | 66 ++++++++ research/batch-width-recount/SOURCES.json | 18 +++ research/batch-width-recount/TASK.json | 100 ++++++++++++ research/batch-width-recount/VERIFY.json | 18 +++ research/batch-width-recount/verify.py | 189 ++++++++++++++++++++++ 5 files changed, 391 insertions(+) create mode 100644 research/batch-width-recount/README.md create mode 100644 research/batch-width-recount/SOURCES.json create mode 100644 research/batch-width-recount/TASK.json create mode 100644 research/batch-width-recount/VERIFY.json create mode 100644 research/batch-width-recount/verify.py diff --git a/research/batch-width-recount/README.md b/research/batch-width-recount/README.md new file mode 100644 index 0000000000..6d6cbe02c7 --- /dev/null +++ b/research/batch-width-recount/README.md @@ -0,0 +1,66 @@ +# Independent recomputation of #4507: chronological batch widths + +**Claim type:** an independent recomputation by separately written code. **No new κ.** It covers +mihir-s-05's [#4507](https://github.com/CrocSwap/integer-mult-bounds/pull/4507). That PR derives the least +common replication factor for #4436's direct mixed flow under a chronological batching policy. It reports +a raw-p7 rank-1,000 width of 2,524 bits, against 17,504 for #4436's nested construction, and a rank-12 +counterexample to pooling across cuts. + +## Method + +- **Sources and aggregate exits** come from my independent #4436 flow (as in + `research/pr4436-direct-flow-check`). +- **Per-cut batches** come from a new enumerator: + - target words are aggregated by product, `F_0(1) = 1`, `F_h(c) = Σ_k W_k F_{h−1}(c/k)`; + - at depth `d`, path multiplier `ρ`, present class `c` and paid rank `r`, the cut leaves + `q = Σ_k W_k F_{G−d−1}(c/k)` over `k` with `mρr(c/k) > n`, at rank `ρrc`; + - at depth `G`, every leaf class leaves one job per paid position; + - path multiplicities scale totals but never a per-cut batch. +- **Widths.** `B_e = 1` below `m`, and + + a_n = lcm over complements (n−s, S_s) and per-cut exits (e, q) of B_e / gcd(B_e, q), B_n = S·a_n. + +## Results + +All of #4507's numbers reproduce: + +| Check | Value | +| --- | --- | +| aggregate per-cut exits = flow exits | every rank checked | +| toy `{2:4,3:1} ← {1:6,2:2}` widths, ranks 0–12 | `1,1,1,5,5,25,140,140,700,625,875,4375,110600` | +| rank-12 counterexample | pooled multiplier **175**, chronological **700** (eight rank-8 leaf cuts of one job each) | +| fixture `{2:1,5:1} ← {1:2,4:1}`, rank 100 | 433 → 42 bits, strict at 95 of 96 ranks | +| fixture `{2:4,3:1} ← {1:6,2:2}`, rank 100 | 1,002 → 88 bits, strict at 97 of 98 ranks | +| raw p7, rank 1,000 | **17,504 → 2,524 bits**, factor in `[2^14980, 2^14981)`, strict at 879 of 880 ranks | + +Every new width divides the nested width. + +## Not covered + +- The native supplier and the physical contracts, which #4507 also keeps as hypotheses. +- Minimality beyond the stated policy and library. +- The normalized leaf cost. It is unchanged by construction, since the factor `a` cancels; this check + does not recompute it. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/batch-width-recount --check-only +python3.12 -B scripts/research_package.py --package research/batch-width-recount +``` + +The verifier prints `PASS_BATCH_WIDTH_RECOUNT` in about a second, using only the standard library. + +## Open next questions + +1. **Does choosing replication per path class, rather than one common `a_n`, shrink the width further?** + - *First step:* solve the per-class divisibility as a separate LCM per class and compare bit lengths + at rank 1,000. + +## Credit + +- The batching lemma, the counterexample and the question are mihir-s-05's (#4507). +- The flow is zxv's (#4436). + +Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. +Apache-2.0. diff --git a/research/batch-width-recount/SOURCES.json b/research/batch-width-recount/SOURCES.json new file mode 100644 index 0000000000..18b51b4e95 --- /dev/null +++ b/research/batch-width-recount/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40", + "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + } + ] +} diff --git a/research/batch-width-recount/TASK.json b/research/batch-width-recount/TASK.json new file mode 100644 index 0000000000..5331dae49b --- /dev/null +++ b/research/batch-width-recount/TASK.json @@ -0,0 +1,100 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 7, + "base_commit": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc", + "original_card": { + "id": "independent-moment", + "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/staged544-mixed-fourth-entry/README.md", + "research/staged-fourth-mixture-ceiling/README.md", + "research/r437-two-window-carrier/README.md" + ], + "methods": [ + "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.", + "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Calling an aggregate histogram or source archive an independently accepted physical supplier." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering", + "4088", + "4091", + "4067", + "staged544-mixed-fourth-entry", + "staged-fourth-mixture-ceiling", + "r437-two-window-carrier" + ], + "existing_checks": [ + { + "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.", + "evidence": "research/staged-fourth-mixture-ceiling/README.md", + "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.", + "status": "author-checked", + "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.", + "evidence": "research/r437-two-window-carrier/README.md", + "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.", + "status": "author-checked", + "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Independent recomputation of #4507's chronological batch widths.", + "scope_change_reason": "Independent coverage of a compiler-size follow-up named in the maintainers' review plan.", + "bottleneck_link": "Side result: compiler-size accounting for the direct-flow route.", + "budget_minutes": 30, + "stop_rule": "Stop at #4507's stated numbers.", + "outcome": "completed", + "evidence": "Toy widths, pooled 175 vs chronological 700, fixtures 433->42 and 1002->88, p7 17,504->2,524 bits (factor 14,981 bits), 879/880 strict ranks; all match.", + "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance", + "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance; no independent human review.", + "open_questions": [ + { + "question": "Does per-class replication shrink the width further?", + "why_it_matters": "A smaller explicit compiler.", + "first_step": "Separate LCM per path class at rank 1000.", + "blocked_by": "None." + } + ] +} diff --git a/research/batch-width-recount/VERIFY.json b/research/batch-width-recount/VERIFY.json new file mode 100644 index 0000000000..677feb2e32 --- /dev/null +++ b/research/batch-width-recount/VERIFY.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "#4507 recomputation: per-cut exits vs flow totals at every rank, toy widths and 175-vs-700 counterexample, fixture bit lengths, raw p7 rank-1000 bits 17,504 -> 2,524 and factor range, strict reductions, divisibility." + } + ] +} diff --git a/research/batch-width-recount/verify.py b/research/batch-width-recount/verify.py new file mode 100644 index 0000000000..880852e283 --- /dev/null +++ b/research/batch-width-recount/verify.py @@ -0,0 +1,189 @@ +#!/usr/bin/env python3 +"""Independent recomputation of #4507: least chronological batch widths for #4436's direct mixed flow. + +Separately written code: #4436's flow (as in research/pr4436-direct-flow-check) for sources and aggregate exits, and a +new per-cut enumerator. Target words are aggregated by product, F_0(1) = 1, F_h(c) = sum_k W_k F_(h-1)(c/k); at depth +d, path multiplier rho and present class c (m rho c <= n) a rank-r paid position leaves the per-cut batch +q = sum_k W_k F_(G-d-1)(c/k) over k with m rho r (c/k) > n (q = F_0 = 1 at depth G), at rank rho r c. Path +multiplicities scale totals but never a per-cut batch. Widths: B_e = 1 below m, and + a_n = lcm over complements (n - s, S_s) and per-cut exits (e, q) of B_e / gcd(B_e, q), B_n = S a_n. +Checks: aggregate per-cut exits equal the flow's exits at every rank; the toy {2:4,3:1} <- {1:6,2:2} widths through +rank 12 and #4507's counterexample (pooled multiplier 175, chronological 700, B_12 = 110600); the fixture bit lengths +433 -> 42 and 1,002 -> 88 at rank 100; raw p7 at rank 1,000: 17,504 nested bits -> 2,524 bits, factor in +[2^14980, 2^14981), strict reduction at 879 of 880 ranks; every new width divides the nested width. +Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. +""" +from math import gcd +import json +import sys + +from math import factorial +def multis(n_types, size): + if n_types == 0: + if size == 0: yield () + return + for x in range(size + 1): + for rest in multis(n_types - 1, size - x): yield (x,) + rest +def flow(N, W, P): + ks = sorted(W); m = ks[-1]; kmin = ks[0] + def c(a): + v = 1 + for k, x in zip(ks, a): v *= k ** x + return v + def u(a): + v = factorial(sum(a)) + for k, x in zip(ks, a): v = v // factorial(x) * W[k] ** x + return v + G = 0 + while kmin ** (G + 1) <= N // m: G += 1 + F = [{1: 1}] + for d in range(1, G + 1): + nxt = {} + for rho, cnt in F[d - 1].items(): + for r, pr in P.items(): + if m * rho * r <= N: nxt[rho * r] = nxt.get(rho * r, 0) + cnt * pr + F.append(nxt) + S, X, BX = {}, {}, {} + col = units = matched = 0 + add = lambda D, k, v: D.__setitem__(k, D.get(k, 0) + v) + present = lambda rho, a: m * rho * c(a) <= N + for d in range(G + 1): + for rho, cnt in F[d].items(): + for b in multis(len(ks), G - d): + if not present(rho, b): continue + units += cnt * u(b); col += cnt * u(b) * rho * c(b) + for r, pr in P.items(): + issued = cnt * pr * u(b); rank = r * rho * c(b) + if d == G: + add(X, rank, issued); continue + D = sum(W[k] * u(tuple(x - (i == j) for j, x in enumerate(b))) + for i, k in enumerate(ks) if b[i] > 0 and present(rho * r, tuple(x - (i == j) for j, x in enumerate(b)))) + matched += cnt * pr * D + if issued - cnt * pr * D: + add(X, rank, issued - cnt * pr * D); add(BX, rank, issued - cnt * pr * D) + for a in multis(len(ks), G): + if present(1, a): + for k in ks: add(S, k * c(a), W[k] * u(a)) + for d in range(1, G + 1): + for rho, cnt in F[d - 1].items(): + for r, pr in P.items(): + for a in multis(len(ks), G - d): + if not present(rho * r, a): continue + for i, k in enumerate(ks): + b = list(a); b[i] += 1 + if not present(rho, tuple(b)): + add(S, rho * r * c(tuple(b)), cnt * pr * u(a) * W[k]) + return dict(G=G, S=S, X=X, BX=BX, col=col, units=units, matched=matched) + + +def lcm(a, b): + return a // gcd(a, b) * b + + +def cuts(N, W, P): + """per-cut exit batches (e, q, copies) under the chronological policy, plus aggregate exits""" + ks = sorted(W); m = ks[-1]; kmin = ks[0] + G = 0 + while kmin ** (G + 1) <= N // m: + G += 1 + cap = N // m + Fh = [{1: 1}] + for h in range(1, G + 1): + nxt = {} + for c, v in Fh[-1].items(): + for k, w in W.items(): + if c * k <= cap: + nxt[c * k] = nxt.get(c * k, 0) + w * v + Fh.append(nxt) + paths = [{1: 1}] # depth -> rho -> multiplicity + for d in range(1, G + 1): + nxt = {} + for rho, mult in paths[-1].items(): + for r, pr in P.items(): + if m * rho * r <= N: + nxt[rho * r] = nxt.get(rho * r, 0) + mult * pr + paths.append(nxt) + out, agg = [], {} + for d in range(G + 1): + h = G - d + for rho, mult in paths[d].items(): + for c, units in Fh[h].items(): + if m * rho * c > N: + continue + for r, pr in P.items(): + if h == 0: + q = units # = 1: every paid job of the leaf class exits + else: + q = sum(w * Fh[h - 1].get(c // k, 0) for k, w in W.items() + if c % k == 0 and m * rho * r * (c // k) > N) + if q: + e = rho * r * c + out.append((e, q, mult * pr)) + agg[e] = agg.get(e, 0) + q * mult * pr + return G, out, agg + + +def widths(W, P, Nmax, check_every=0): + m = max(W) + B = [1] * m # base widths below m (B_0 = 1) + nested = [1] * m + for N in range(m, Nmax + 1): + R = flow(N, W, P) + G, cs, agg = cuts(N, W, P) + assert agg == {e: v for e, v in R['X'].items() if v}, (N, 'aggregate exits match the flow') + S = sum(R['S'].values()) + a = 1 + for s, cnt in R['S'].items(): + e = N - s + a = lcm(a, B[e] // gcd(B[e], cnt)) + for e, q, _ in cs: + a = lcm(a, B[e] // gcd(B[e], q)) + B.append(S * a) + nested.append(nested[-1] * S) + assert nested[-1] % B[-1] == 0, (N, 'new width divides nested width') + return B, nested + + + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +def main(): + toy_W, toy_P = {2: 4, 3: 1}, {1: 6, 2: 2} + B, nested = widths(toy_W, toy_P, 12) + need(B == [1, 1, 1, 5, 5, 25, 140, 140, 700, 625, 875, 4375, 110600], "toy widths through rank 12") + R = flow(12, toy_W, toy_P) + G, cs, agg = cuts(12, toy_W, toy_P) + need(R["S"] == {6: 60, 8: 64, 9: 6, 12: 28} and agg == {1: 216, 2: 216, 4: 72, 8: 8}, "toy sources and exits") + pooled = 1 + for s, cnt in R["S"].items(): + pooled = lcm(pooled, B[12 - s] // gcd(B[12 - s], cnt)) + for e, tot in agg.items(): + pooled = lcm(pooled, B[e] // gcd(B[e], tot)) + need(pooled == 175 and B[12] // sum(R["S"].values()) == 700, "pooled 175 versus chronological 700") + need(sorted({(e, q) for e, q, _ in cs if e == 8}) == [(8, 1)], "the rank-8 leaf cuts each hold one job") + fixtures = {} + for W, P, n, bits in (({2: 1, 5: 1}, {1: 2, 4: 1}, 100, (433, 42, 95, 96)), + ({2: 4, 3: 1}, {1: 6, 2: 2}, 100, (1002, 88, 97, 98))): + B, nested = widths(W, P, n) + m = max(W) + got = (nested[n].bit_length(), B[n].bit_length(), sum(1 for e in range(m, n + 1) if B[e] < nested[e]), n - m + 1) + need(got == bits, f"fixture {W} <- {P}: {got}") + fixtures[str(W)] = got + W = {5: 420, 6: 270, 7: 840, 8: 1395, 9: 3195, 25: 448, 41: 448, 57: 448, 121: 224} + P = {1: 37305, 2: 10695, 3: 3360, 4: 1530, 5: 300, 8: 1464, 16: 448, 32: 448, 48: 448} + B, nested = widths(W, P, 1000) + factor = nested[1000] // B[1000] + need(nested[1000].bit_length() == 17504 and B[1000].bit_length() == 2524, "p7 rank 1000 bit lengths") + need(2 ** 14980 <= factor < 2 ** 14981, "p7 reduction factor") + need(sum(1 for e in range(121, 1001) if B[e] < nested[e]) == 879, "strict reduction at 879 of 880 ranks") + print(json.dumps({"status": "PASS_BATCH_WIDTH_RECOUNT", "toy_B12": 110600, "pooled_vs_chronological": [175, 700], + "fixtures_bits": fixtures, "p7_bits": [17504, 2524], "p7_factor_bits": factor.bit_length(), + "new_kappa_claimed": False}, indent=1)) + + +if __name__ == "__main__": + sys.exit(main())