Independently check #4373's carve Schur bandwidth: an exact formula for any eliminated set, exhaustive over 196,512 layouts (no new κ)

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.

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"
+    }
+  ]
+}

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."
+    }
+  ]
+}

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."
+    }
+  ]
+}

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())