From 4bd1d57ebee0a6f2270cae117f3dff3a551f6667 Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Wed, 21 Oct 2026 23:52:59 +0700 Subject: [PATCH] =?UTF-8?q?Independently=20check=20#4373's=20carve=20Schur?= =?UTF-8?q?=20bandwidth:=20an=20exact=20formula=20for=20any=20eliminated?= =?UTF-8?q?=20set,=20exhaustive=20over=20196,512=20layouts=20(no=20new=20?= =?UTF-8?q?=CE=BA)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 5.5 --- .../carve-schur-bandwidth-census/README.md | 94 +++++++++ .../carve-schur-bandwidth-census/SOURCES.json | 18 ++ .../carve-schur-bandwidth-census/TASK.json | 74 +++++++ .../carve-schur-bandwidth-census/VERIFY.json | 18 ++ .../carve-schur-bandwidth-census/verify.py | 187 ++++++++++++++++++ 5 files changed, 391 insertions(+) create mode 100644 research/carve-schur-bandwidth-census/README.md create mode 100644 research/carve-schur-bandwidth-census/SOURCES.json create mode 100644 research/carve-schur-bandwidth-census/TASK.json create mode 100644 research/carve-schur-bandwidth-census/VERIFY.json create mode 100644 research/carve-schur-bandwidth-census/verify.py diff --git a/research/carve-schur-bandwidth-census/README.md b/research/carve-schur-bandwidth-census/README.md new file mode 100644 index 0000000000..525387652d --- /dev/null +++ b/research/carve-schur-bandwidth-census/README.md @@ -0,0 +1,94 @@ +# Exhaustive check of #4373's carve Schur bandwidth, with an exact formula + +**Claim type:** an exact structural lemma for every eliminated set, checked on every layout of +every path `n ≤ 15` for bandwidth `b ∈ {1, 2, 3}`. **No new κ.** It independently confirms +unpaidmoon's [#4373](https://github.com/CrocSwap/integer-mult-bounds/pull/4373), at head +`479a03d7967594e30427a8b2f9783cc10673a001`, and imports nothing from it. + +## Lemma: boundary-order bandwidth of any carve + +Take a bandwidth-`b` matrix on the path `0..n−1` with generic entries. Eliminate a set `E` +whose pivot blocks are invertible, and write the Schur complement on the survivors in +boundary order. Group `E` into components: consecutive eliminated indices at distance at most +`b` belong to the same component. Then + + bw(E) = max( max over components C of #{survivors in [min C − b, max C + b]} − 1 , + max over survivor pairs u < v with v − u ≤ b of their boundary distance ). + +**Proof.** By the fill-path lemma (Rose–Tarjan), survivors `u` and `v` couple in the Schur +complement exactly when they are adjacent, or are joined through eliminated vertices only. +They are joined in the second way exactly when both touch one component `C`. Inside a +component, consecutive indices are at most `b` apart. So the survivors touching `C` are +exactly those in `[min C − b, max C + b]`, and their boundary-order span is that count minus +one. A survivor pair with no eliminated index between them keeps its original distance. +Generic entries make every structurally possible fill nonzero. Particular entries can only +cancel fill, so in every case `bw(E)` is an upper bound. + +**Corollaries.** + +- **#4373's theorem.** With at least `b` survivors between consecutive interiors, each + interior run is its own component. Its rims lie in the separators, so it touches at most + `2b` survivors. Hence `bw ≤ 2b − 1`, with equality exactly when some interior has `b` + survivors on both sides (and trivially at `b = 1`). An interior at the end of the path gives + at most `b`, matching #4373's prefix remark. +- **Necessity.** If separators hold only `b − 1` survivors, components merge into chains. + - With `k` singleton interiors and `b` survivors at each end, a chain has + `bw = 2b − 1 + (k − 1)(b − 1)`, which is unbounded. + - #4373's own chain has `b = 2` and one survivor at each end. Its bandwidth equals `k`, as + stated. + +## Evidence + +`verify.py` computes the formula and an actual Schur complement, from random band entries over +the prime field `2^61 − 1`. For **196,512 layouts** (every nonempty proper eliminated subset of +every path `n = 1..15`, for each of `b = 1, 2, 3`) it checks: + +- the formula equals the Schur bandwidth; +- on the 84,491 layouts that satisfy #4373's separation hypothesis, the cap `2b − 1` holds; +- among those, the two-sided criterion decides exactly which layouts attain the cap. + +It also checks two controls: + +- the under-separated chains for `b = 2, 3` and `k = 1..8`, against the formula above, and + #4373's `b = 2` chain; +- #4285's 7×7 bandwidth-2 witness, recomputed in exact rationals: far entry `−1/432`, + bandwidth `3 = 2b − 1`, and both inverse norms `488/389`. + +The field computation witnesses generic fill. The upper bound for real Gaussian entries is the +lemma's structural direction. + +## Not covered + +- Inverse norms beyond the #4285 witness. +- Circular phase cells. The lemma is linear; #4286 covers the circular case. +- Window widths in #4100's narrow solver (#4373's open question 1). +- Whether real Gaussian entries produce every possible fill. Only the upper bound matters for + #4100. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/carve-schur-bandwidth-census --check-only +python3.12 -B scripts/research_package.py --package research/carve-schur-bandwidth-census +``` + +The verifier prints `PASS_CARVE_SCHUR_BANDWIDTH_CENSUS` in about 50 seconds, using only the +standard library. + +## Open next questions + +1. **Does the retained carve ever produce merged components?** + - *Why it matters:* the formula prices any layout. Where a separation shortfall occurs at + holes or cell cuts, it gives the exact width. + - *First step:* run the formula on #4100's carve layouts with holes and cuts marked. + - *Blocked by:* a concrete layout generator for the caller. + +## Credit + +- The theorem, its application to `GAUSSIAN.md` and the chain example are unpaidmoon's + (#4373). +- The one-interval cap and the 7×7 witness are jwr's (#4285). +- The carve and the `O(W)` claim are #4100's `GAUSSIAN.md`. + +Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. +Apache-2.0. diff --git a/research/carve-schur-bandwidth-census/SOURCES.json b/research/carve-schur-bandwidth-census/SOURCES.json new file mode 100644 index 0000000000..fcfba8aa31 --- /dev/null +++ b/research/carve-schur-bandwidth-census/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + } + ] +} diff --git a/research/carve-schur-bandwidth-census/TASK.json b/research/carve-schur-bandwidth-census/TASK.json new file mode 100644 index 0000000000..13dc18bf6e --- /dev/null +++ b/research/carve-schur-bandwidth-census/TASK.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "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": "Independently check #4373's separated-carve Schur bandwidth theorem: an exact boundary-order bandwidth formula for every eliminated set, checked exhaustively for n<=15 and b<=3.", + "scope_change_reason": "The card asks for one quantified #4100 precision/conditioning step; #4373 supplies one (the O(W) Schur bandwidth) with finite certificates on a few hosts and no independent check.", + "bottleneck_link": "GAUSSIAN.md's boundary costs use the O(W) bandwidth of the carved Schur matrix.", + "budget_minutes": 45, + "stop_rule": "Stop at the formula and the exhaustive census; do not audit solver windows or circular cells.", + "outcome": "completed", + "evidence": "verify.py: formula = generic Schur bandwidth on 196,512 layouts; 84,491 separated layouts obey 2b-1 with exact two-sided sharpness; chains grow as 2b-1+(k-1)(b-1); #4285 witness reproduced.", + "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 the retained #4100 carve ever produce merged components at holes or cuts?", + "why_it_matters": "The formula then prices the exact width.", + "first_step": "Run the formula on caller layouts with holes and cuts marked.", + "blocked_by": "A concrete layout generator for the caller." + } + ] +} diff --git a/research/carve-schur-bandwidth-census/VERIFY.json b/research/carve-schur-bandwidth-census/VERIFY.json new file mode 100644 index 0000000000..60b2406ebd --- /dev/null +++ b/research/carve-schur-bandwidth-census/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": 300, + "checks": "Exact bandwidth formula vs random-entry Schur complements over GF(2^61-1) on all 196,512 layouts (n<=15, b=1,2,3); #4373's separated cap 2b-1 and its two-sided sharpness; under-separated chain growth formula and #4373's b=2 chain; #4285 witness far entry -1/432, bandwidth 3, inverse norms 488/389." + } + ] +} diff --git a/research/carve-schur-bandwidth-census/verify.py b/research/carve-schur-bandwidth-census/verify.py new file mode 100644 index 0000000000..73beaa887c --- /dev/null +++ b/research/carve-schur-bandwidth-census/verify.py @@ -0,0 +1,187 @@ +#!/usr/bin/env python3 +"""Exhaustive independent check of #4373's separated-carve Schur bandwidth theorem. + +For a bandwidth-b path matrix on 0..n-1 and ANY eliminated set E, the generic Schur complement onto the +survivors, written in boundary order, has bandwidth + + bw(E) = max( max over components C of E in the band graph of #{survivors in [min C - b, max C + b]} - 1, + max over survivor pairs u < v with v - u <= b of their boundary-order distance ). + +(Fill-path lemma: a survivor pair fills iff both ends touch one eliminated component.) The verifier checks +this formula against an actual Schur complement with random entries over a 61-bit prime field, for every +subset E of every path n <= NMAX and b = 1, 2, 3. It then reads off #4373's claims: with at least b +survivors between consecutive interiors the bandwidth is at most 2b - 1, attained exactly when some +interior has b survivors on both sides; separators of b - 1 survivors grow without bound. +Separately written; imports nothing from #4373. +Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. +""" +from fractions import Fraction as Q +import json +import random +import sys + +PRIME = 2**61 - 1 +NMAX = 15 +rng = random.Random(4373) + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +def runs(elim): + """maximal runs of consecutive eliminated indices, as (L, R)""" + out, cur = [], None + for i in sorted(elim): + if cur and i == cur[1] + 1: + cur[1] = i + else: + cur = [i, i] + out.append(cur) + return [tuple(r) for r in out] + + +def formula(n, b, elim): + surv = [i for i in range(n) if i not in elim] + pos = {v: k for k, v in enumerate(surv)} + best = 0 + # components of elim in the band graph: consecutive eliminated indices at distance <= b + comps, cur = [], None + for i in sorted(elim): + if cur and i - cur[1] <= b: + cur[1] = i + else: + cur = [i, i] + comps.append(cur) + for lo, hi in comps: + rim = [v for v in surv if lo - b <= v <= hi + b] + if rim: + best = max(best, pos[rim[-1]] - pos[rim[0]]) + for u in surv: + for v in surv: + if u < v <= u + b: + best = max(best, pos[v] - pos[u]) + return best + + +def schur_bandwidth(n, b, elim): + """eliminate elim (in index order) from a random band matrix mod PRIME; boundary-order bandwidth""" + while True: + a = [[rng.randrange(1, PRIME) if abs(i - j) <= b else 0 for j in range(n)] for i in range(n)] + ok = True + for e in sorted(elim): + piv = a[e][e] + if piv == 0: + ok = False + break + inv = pow(piv, PRIME - 2, PRIME) + col = [a[i][e] for i in range(n)] + row = a[e] + for i in range(n): + if i != e and col[i]: + f = col[i] * inv % PRIME + ai = a[i] + for j in range(n): + if row[j]: + ai[j] = (ai[j] - f * row[j]) % PRIME + for i in range(n): + a[i][e] = a[e][i] = 0 + if ok: + break + surv = [i for i in range(n) if i not in elim] + best = 0 + for x, u in enumerate(surv): + for y, v in enumerate(surv): + if a[u][v]: + best = max(best, abs(x - y)) + return best + + +def separated(n, b, elim): + """at least b survivors between successive interiors""" + rs = runs(elim) + return all(rs[k + 1][0] - rs[k][1] - 1 >= b for k in range(len(rs) - 1)) + + +def two_sided(n, b, elim): + return any(L >= b and R <= n - 1 - b for L, R in runs(elim)) + + +def witness_4285(): + """7x7 bandwidth-2 host, unit diagonal, off-diagonal -1/8, eliminate {2,3,4}""" + n, b, elim = 7, 2, (2, 3, 4) + a = [[Q(1) if i == j else (Q(-1, 8) if abs(i - j) <= b else Q(0)) for j in range(n)] for i in range(n)] + for e in elim: + piv = a[e][e] + for i in range(n): + if i != e and a[i][e]: + f = a[i][e] / piv + a[i] = [x - f * y for x, y in zip(a[i], a[e])] + surv = [i for i in range(n) if i not in elim] + far = a[surv[0]][surv[-1]] + bw = max(abs(x - y) for x, u in enumerate(surv) for y, v in enumerate(surv) if a[u][v] != 0) + s = [[a[u][v] for v in surv] for u in surv] + k = len(s) + w = [row[:] + [Q(int(i == j)) for j in range(k)] for i, row in enumerate(s)] + for c in range(k): + w[c] = [x / w[c][c] for x in w[c]] + for r in range(k): + if r != c: + f = w[r][c] + w[r] = [x - f * y for x, y in zip(w[r], w[c])] + inv = [row[k:] for row in w] + inf = max(sum(abs(x) for x in row) for row in inv) + one = max(sum(abs(inv[i][j]) for i in range(k)) for j in range(k)) + return far, bw, inf, one + + +def main(): + total = cap_cases = sharp = 0 + for b in (1, 2, 3): + for n in range(1, NMAX + 1): + for mask in range(1, 2 ** n): + elim = {i for i in range(n) if mask >> i & 1} + if len(elim) == n: + continue + f = formula(n, b, elim) + s = schur_bandwidth(n, b, elim) + need(s == f, f"formula = generic Schur bandwidth at n={n}, b={b}, E={sorted(elim)}") + total += 1 + if separated(n, b, elim): + cap_cases += 1 + need(f <= 2 * b - 1, "#4373: separated carve has bandwidth <= 2b-1") + need((f == 2 * b - 1) == two_sided(n, b, elim) or b == 1 and f == 1, + "sharp exactly at a two-sided interior") + sharp += f == 2 * b - 1 + # necessity: singleton interiors separated by b-1 survivors on a long path + growth = {} + for b in (2, 3): + for k in range(1, 9): + n = b + k * b + b # b ends, k singletons spaced by b-1 survivors + elim = {b + j * b for j in range(k)} + f = formula(n, b, elim) + need(f == schur_bandwidth(n, b, elim), "chain: formula = Schur") + growth.setdefault(b, []).append(f) + need(growth[b][-1] > 2 * b - 1 and growth[b] == sorted(growth[b]), "under-separation grows") + need(growth[b] == [2 * b - 1 + (k - 1) * (b - 1) for k in range(1, 9)], "chain: bandwidth formula in k") + # #4373's own chain: b = 2, one survivor at each end and between singletons -> bandwidth = count + for k in range(1, 9): + elim = {1 + 2 * j for j in range(k)} + n = 2 * k + 1 + need(formula(n, 2, elim) == schur_bandwidth(n, 2, elim) == k, "#4373 chain: bandwidth = interior count") + far, bw, inf, one = witness_4285() + need(far == Q(-1, 432) and bw == 3, "#4285 witness: far entry -1/432, bandwidth 3 = 2b-1") + need(inf == one == Q(488, 389), "#4285 witness: both inverse norms 488/389") + print(json.dumps({ + "status": "PASS_CARVE_SCHUR_BANDWIDTH_CENSUS", + "layouts_checked": total, "paths": f"n = 1..{NMAX}", "bandwidths": [1, 2, 3], + "separated_layouts": cap_cases, "separated_attaining_2b_minus_1": sharp, + "under_separated_chain_bandwidths": growth, + "witness_4285": {"far_entry": str(far), "bandwidth": bw}, + "new_kappa_claimed": False, + }, indent=1)) + + +if __name__ == "__main__": + sys.exit(main())