Prove the separated Gaussian carve has Schur bandwidth at most 2W-1.

research/gaussian-carve-schur-bandwidth/README.md

@@ -0,0 +1,134 @@
+# Boundary-order bandwidth of the separated Gaussian carve
+
+**Scoped audit, no new κ.** One precision/conditioning step of the proposed
+#4100 construction holds at the retained dyadic carve. Selected κ stays
+**0.001672660197076918**.
+
+## Result
+
+Let a matrix have bandwidth `b` when it vanishes for `|i-j| > b`. Eliminate
+disjoint contiguous interiors, and write the Schur complement in survivor
+order (the order GAUSSIAN.md calls boundary order: original order with each
+eliminated gap closed).
+
+**Theorem.** If at least `b` survivors lie between successive interiors, and
+each eliminated block is invertible, that Schur complement has bandwidth at
+most `2b-1`. One middle interval already attains `2b-1`, and so does a pair
+of intervals separated by exactly `b` survivors. The constant cannot be
+replaced by `b`.
+
+**Application.** #4100's carve, as specified by the retained capped-interior
+loop, puts exactly `W` boundary vertices between successive interiors and
+reserves `W` vertices at each end of a phase cell. GAUSSIAN.md truncates at
+physical half-bandwidth `W`, so `b = W`, and calls the same separation
+"interior neighbors are separated by `W`". The Schur matrix in boundary order
+therefore has bandwidth at most `2W-1`. That is `O(W)`, which is the claim in
+GAUSSIAN.md, and it is the same cap PR #4285 proved for one middle interval.
+Separated interiors do not force a wider band. The written boundary costs
+`O(V d W^(τ-1) / B polylog(p))` and `O(V d W / B polylog(p))`, with
+`τ = 45/16`, stay valid: replacing `W` by `2W-1` multiplies a pure power
+`W^(29/16)` by less than 4.
+
+**The separation hypothesis is necessary.** For bandwidth 2, singleton
+interiors separated by only one survivor have Schur bandwidth equal to the
+interior count on every chain of length 1 through 8. From four interiors
+onward that exceeds `2b-1 = 3`, and the band keeps growing through the
+checked range. An entry at distance `b+2`, with nothing eliminated between
+its endpoints, also escapes the cap. GAUSSIAN.md's `O(W)` sentence is not
+claimed for that shorter gap.
+
+## Proof
+
+Number coordinates by integers. Interiors are `B_k = {L_k, ..., R_k}` with
+`R_k < L_{k+1}` and `S_k = L_{k+1} - R_k - 1 ≥ b`.
+
+The closest indices of `B_k` and `B_{k+1}` differ by `S_k + 1 ≥ b + 1 > b`,
+so the pivot block has no entry between distinct interiors. It is their
+direct sum, and the Schur update is the sum of the individual updates.
+
+A survivor meets `B_k` only from the original-index rim `[L_k - b, L_k)` or
+`(R_k, R_k + b]`. Because the neighbouring separator contains at least `b`
+survivors, that rim lies entirely in the separator and contains no other
+interior. Two survivors on the same rim are at most `b - 1` apart in both
+original and boundary order. A left-rim survivor `u` and a right-rim survivor
+`v` satisfy `v - u ≤ R_k - L_k + 2b`, and the only eliminated indices between
+them are the `R_k - L_k + 1` points of `B_k`. Closing that gap leaves
+boundary distance at most `2b - 1`.
+
+An original entry has `|u - v| ≤ b`. Eliminated indices between its endpoints
+only shorten boundary distance, so the entry stays within distance `b`.
+Entries with neither an original coupling nor a common rim are zero. The
+bandwidth is therefore at most `2b - 1`.
+
+A prefix pivot has an empty rim on one side, so it has no cross term and the
+bandwidth is at most `b`. The retained loop reserves `W` endpoints before the
+first interior, so every carved interior is two-sided and the sharp cap is
+`2W - 1`, not `W`.
+
+PR #4285's 7×7 witness (off-diagonal `-1/8`, eliminate `{2,3,4}`) attains
+bandwidth 3 with far entry `-1/432`. The two-interval host in the verifier,
+separator exactly `b = 2`, also attains bandwidth 3. Both are inside the
+support count above; neither is an exception to it.
+
+PR #4298 and PR #4299 certify one interior on one equal-weight path, of
+bandwidth 2 and 3, for a few lengths. They do not bound a second interior,
+and both say they do not measure the truncated Gaussian row. The counting
+argument above is what lets the retained loop delete every interior at once.
+
+## What was not proved
+
+This does not price inverse norms, Gaussian tails, halo rectangles, or a
+circular phase cell. PR #4286 already shows that a circular band can follow
+arc length; the linear theorem uses the retained period cuts and endpoint
+strips as boundary. No Strassen leading constant is recomputed, and no
+#4100 executable window is replayed. Finite samples are certificates for the
+sharp and failing hosts. The all-size support bound is the counting argument
+above, not an extrapolation from those hosts.
+
+The RHS batch "between `W` and `2W`" is a count of right-hand sides. It is
+wide enough to hold one row of a `2W-1` band. This audit does not decide
+whether some narrow solver instead builds triangular factors of width exactly
+`W`. GAUSSIAN.md states `O(W)`, not `≤ W`.
+
+## Reproduce
+
+CPython 3.12, standard library only, from the repository root:
+
+```sh
+python3 -B research/gaussian-carve-schur-bandwidth/verify.py
+python3 scripts/research_package.py --package research/gaussian-carve-schur-bandwidth
+```
+
+The verifier recomputes the #4285 witness, the separated-cap layouts for
+bandwidth 1, 2 and 3, the growing under-separated chain, an out-of-band
+failure control, and a singular-pivot rejection. It also checks the pinned
+GAUSSIAN.md and CAPPED-GAUGE-AUDIT.md sentences and `7^16 < 2^45`.
+
+## Open next questions
+
+1. Does any narrow boundary solve on this Schur complement use triangular
+   windows of width exactly `W`? That would miss the `2W-1` fill even though
+   the `O(W)` cost sentence survives. The first step is to bind one narrow
+   solve in the retained shallow-Toeplitz schedule to a concrete window width.
+   Blocker: GAUSSIAN.md does not name that width; it names `O(W)` and an RHS
+   batch of width at most `2W`.
+
+2. Does every #4100 phase cell retain a period cut through elimination? A
+   circular cell with no retained cut is the setting where PR #4286 lets
+   bandwidth follow arc length. The first step is one full-period cell in the
+   caller, with its cut marked boundary before the carve. Blocker: this
+   package audits the linear loop and does not replay the tensor caller.
+
+## Credit
+
+The carve sentence and the `O(W)` claim are Cinna Davis's #4100
+`GAUSSIAN.md`. The loop that retains the next `W` vertices as boundary is the
+capped-interior audit in `research/capped-phase-fusion/CAPPED-GAUGE-AUDIT.md`.
+The one-interval cap `2b-1`, the witness ratios, and the far entry `-1/432`
+are jwr's PR #4285; they are recomputed here and not imported. PR #4298 and
+PR #4299 are the one-interior boundary-order checks on equal-weight paths.
+PR #4283 and PR #4286 are the neighbouring bandwidth audits. PR #4311's
+coverage map is the checklist that still listed the carve comparison as open.
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0.
+No independent human or formal-kernel review is claimed.

research/gaussian-carve-schur-bandwidth/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "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"
+    },
+    {
+      "path": "research/capped-phase-fusion/CAPPED-GAUGE-AUDIT.md",
+      "usage": "input",
+      "git_blob": "a2d1c5ae923db7649627dbf419434e36267e57c6",
+      "sha256": "1030a34922709ab8d3434a4c57a4a58934ae268c237fb598cb415697da411c9f"
+    },
+    {
+      "path": "research/unconditional-batched-crt/GAUSSIAN.md",
+      "usage": "input",
+      "git_blob": "adfb28c93e6b06178c901caaac39ede41a9e541b",
+      "sha256": "2f63c91c58f2d1cf31294812c75970ea390c61866a8da7ed700d4316a033a242"
+    }
+  ]
+}

research/gaussian-carve-schur-bandwidth/TASK.json

@@ -0,0 +1,80 @@
+{
+  "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": "At the #4100 dyadic carve, physical half-bandwidth W and at least W retained coordinates between successive interiors, the Schur complement in boundary order has bandwidth at most 2W-1. This matches the one-interval cap and justifies the written O(W) claim. The constant is sharp. A separator of W-1 coordinates can make the bandwidth grow with the number of interiors.",
+  "scope_change_reason": "The card asks for one quantified #4100 implication at its caller. The chosen implication is the precision/conditioning bandwidth of the separated carve, not CRT repair, the free-algebra lift, or fixed-tape induction. Those remain open.",
+  "bottleneck_link": "The O(W) Schur band is what keeps the carved boundary cost inside the #4100 Gaussian allowance. The audit confirms that band at the sharp cap 2W-1. It does not change a supplier moment or the selected kappa.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop once the boundary-order cap is proved for separators of at least b survivors and the shorter-separator counterexample is certified. Do not reprice Strassen or audit another #4100 partition.",
+  "outcome": "completed",
+  "evidence": "Exact rational checks: the #4285 7x7 witness attains bandwidth 3 with far entry -1/432; separated layouts of bandwidth 1, 2 and 3 stay within 2b-1 and a two-interval host attains it; the bandwidth-2 chain with one survivor between singleton interiors has Schur bandwidth equal to the interior count for 1..8 interiors. Counting argument in README.md. Verifier prints PASS gaussian-carve-schur-bandwidth.",
+  "author": "unpaidmoon",
+  "ai_assistance": "Substantial Cursor Grok assistance.",
+  "open_questions": [
+    {
+      "question": "Does any narrow boundary solve on this Schur complement use triangular windows of width exactly W?",
+      "why_it_matters": "A window of width W misses the sharp 2W-1 fill. The O(W) cost sentence would still be true, but that solver would be the wrong band.",
+      "first_step": "Bind one narrow solve in the retained shallow-Toeplitz schedule to a concrete window width and compare it with 2W-1.",
+      "blocked_by": "GAUSSIAN.md states O(W) and an RHS batch of width at most 2W. It does not name an executable triangular-window width."
+    },
+    {
+      "question": "Does every #4100 phase cell retain a period cut through elimination?",
+      "why_it_matters": "A circular cell with no retained cut is the setting where Schur bandwidth can follow arc length instead of the linear cap 2W-1.",
+      "first_step": "Take one full-period cell in the caller and mark its period cut as boundary before the carve.",
+      "blocked_by": "This package audits the linear capped-interior loop and does not replay the tensor caller."
+    }
+  ]
+}

research/gaussian-carve-schur-bandwidth/VERIFY.json

@@ -0,0 +1,21 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/capped-phase-fusion/CAPPED-GAUGE-AUDIT.md",
+    "research/unconditional-batched-crt/GAUSSIAN.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Pinned carve sentences; one-interval witness including far entry -1/432 and both inverse norms 488/389; separated layouts stay within 2b-1 and one attains it; under-separated chain grows past the cap; out-of-band entry and singular pivot fail closed."
+    }
+  ]
+}