Prove exact optimal circular Schur bandwidth (no new κ)

research/cycle-schur-optimal-order/PROOF.md

@@ -0,0 +1,101 @@
+# Optimal ordering of a one-arc circular Schur complement
+
+Let n >= 3, 1 <= w <= floor(n/2), and let a nonempty proper contiguous arc
+of the n-cycle be eliminated. Write M >= 1 for the surviving count. Label
+the surviving path by 0,...,M-1 in its inherited cyclic orientation.
+Half-bandwidth in an order p is max |p(i)-p(j)| over nonzero off-diagonal
+entries, with value zero for a singleton.
+
+**Theorem.** For any matrix supported on the circular radius-w band, if
+the eliminated principal block is invertible, its Schur complement admits a
+simultaneous row/column order of half-bandwidth at most min(M-1,2w).
+For the full negative host H=I-E, where E has zero diagonal, strictly positive
+entries at every circular distance 1,...,w, zero entries outside the band,
+and every row sum is less than one, this is the exact minimum over all orders.
+Equal off-diagonal magnitudes are unnecessary.
+
+The new result is the optimal ordering and its matching lower bound. The
+negative-sign/no-cancellation argument is credited to James Reed / jwr404's
+[PR #4289](https://github.com/CrocSwap/integer-mult-bounds/pull/4289), following
+[#4286](https://github.com/CrocSwap/integer-mult-bounds/pull/4286).
+Those packages leave survivor reordering open. This theorem makes no claim
+about the physical price of the permutation or the Gaussian caller's order.
+
+## 1. Identify the survivor support graph
+
+Put B={0,...,min(w,M)-1} union {max(0,M-w),...,M-1}.
+The survivors touching the eliminated arc are exactly B. A path from a
+survivor to the arc first crosses one of the two surviving endpoints, so
+the minimum circular distance to the arc is min(i+1,M-i).
+
+For an arbitrary band-supported matrix, the Schur update can couple only
+pairs in B. An original coupling between i<j either has j-i <= w along the
+surviving path, or its shorter route crosses the eliminated arc. In the
+latter case both endpoints touch that arc and hence belong to B. Thus the
+Schur support is contained in the graph G_(M,w) whose edges are
+
+    i < j and [j-i <= w or {i,j} subset B].
+
+For the full negative host, the eliminated block is I-E_A. Its inverse is
+sum_(k>=0) E_A^k. All terms are nonnegative, and every entry is positive:
+the arc is connected by the strictly positive nearest-neighbor entries.
+Therefore each pair in B receives a strictly negative Schur update. Every
+original in-band edge is strictly negative and cannot cancel this update.
+Edges with j-i <= w are original edges. Hence this host's support is exactly
+G_(M,w). This uses the predecessor's sign argument as a premise and derives
+the explicit path-plus-end-clique graph needed for the new ordering theorem.
+
+## 2. A folded order attains the upper bound
+
+Use the vertex order
+
+    0, M-1, 1, M-2, 2, M-3, ...
+
+with the middle vertex written only once. If p(i) is its zero-based position,
+
+    p(i)=2i                   if i < ceil(M/2),
+    p(i)=2(M-1-i)+1           otherwise.
+
+Consecutive surviving-path vertices have position differences at most two,
+including the central pair. Summing these adjacent differences gives
+|p(i)-p(j)| <= 2|i-j|. Every path-power edge therefore spans at most 2w.
+
+If M >= 2w, B occupies exactly the first 2w positions of this order, so its
+clique spans at most 2w-1. If M < 2w, B is the entire graph and every edge
+spans at most M-1. These bounds prove min(M-1,2w) for all edges. A simultaneous
+permutation changes entries' locations only, so it preserves this support
+bound for arbitrary coefficients and any cancellations.
+
+## 3. No order improves the constant on the full negative host
+
+In any linear vertex order of half-bandwidth b, the first vertex has degree
+at most b. Thus b is at least the graph's minimum degree.
+
+If M <= 2w, B contains every vertex, so G_(M,w) is complete and its minimum
+degree is M-1.
+
+If M >= 2w+1, B consists of two disjoint w-vertex strips. A vertex outside B
+has exactly 2w path-power neighbors. A vertex in B has 2w-1 other clique
+vertices and at least one neighbor outside B: vertex w for the left strip,
+or vertex M-w-1 for the right strip. Its degree is therefore at least 2w.
+There is at least one vertex outside B, so the minimum degree is exactly 2w.
+The folded upper bound and this degree lower bound coincide.
+
+For example, M=9 and w=2 give exact minimum four, while the inherited linear
+survivor order has bandwidth eight. The same graph shows that the linear
+separated-carve constant 2w-1 cannot replace 2w in this circular problem.
+This is an optimal reordering result, not a disagreement with the
+predecessor's bandwidth measured in circular distance.
+
+## Scope
+
+The proof covers all sizes in the stated matrix class. Finite checks only
+corroborate the graph identification and ordering; they are not a proof of
+these quantifiers. An arbitrary invertible arc block gives the upper bound;
+full negative support and the row-sum condition give the sharp lower bound.
+Zero or signed couplings can have smaller minima. Multiple eliminated arcs
+can join different support components and are outside this theorem. Row/column
+routing costs, ownership, inverse norms, rounded arithmetic, tape layout,
+compiler/hosting, supplier admission and a new kappa are unclaimed. No
+independent human or formal proof-kernel review is claimed. No literature
+priority is claimed for folding a path or the minimum-degree bandwidth bound.

research/cycle-schur-optimal-order/README.md

@@ -0,0 +1,127 @@
+# Exact optimal ordering after a circular arc is eliminated
+
+**Scoped proof with finite corroboration.** For a full negative circular band
+of radius w, eliminate one nonempty proper arc and retain M vertices. The
+exact minimum Schur half-bandwidth over simultaneous row/column orders is
+
+    min(M-1, 2w).
+
+The order `0, M-1, 1, M-2, ...` attains it. In the resulting support graph,
+the minimum degree gives the matching lower bound. With M=9 and w=2, this
+changes the inherited linear survivor bandwidth from eight to four. No
+ordering reaches three. For arbitrary coefficients supported on the same
+circular band and any invertible arc pivot, the same order gives the upper
+bound; cancellations can reduce the optimum.
+
+This answers the survivor-reordering question left open by James Reed /
+jwr404's [PR #4289](https://github.com/CrocSwap/integer-mult-bounds/pull/4289).
+The new contribution is an optimal linear order and its sharp constant.
+The predecessor's sign/no-cancellation argument is a credited premise, not a
+validation deliverable. [PROOF.md](PROOF.md) gives the complete all-size
+argument and precise negative-host hypotheses. No predecessor executable is
+imported or replayed. No literature-priority claim is made for path folding
+or the elementary minimum-degree bandwidth bound.
+
+## Evidence and reproduction
+
+From the repository root, CPython 3.12, standard library only:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/cycle-schur-optimal-order
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/cycle-schur-optimal-order/verify.py
+```
+
+On another checkout, substitute its Python 3.12 interpreter. Both registered
+commands, warning-strict normal and optimized execution, emit
+`PASS_CYCLE_SCHUR_OPTIMAL_ORDER`. Normal verification writes no files. Each
+execution prints a generated receipt with SHA256 hashes of all six package
+files. `verify.py --write-receipt NEW_PATH` additionally writes it to a new
+external path and refuses overwrite. No hand-written receipt is committed.
+The direct verifier is self-contained and works without Git or repository
+inputs. Generic metadata/source-history checks require the pinned Git history.
+
+The bounded checks enumerate:
+
+- 4,656 graph/radius pairs through M=96, including 8,403,952 edge occurrences,
+  checking the folded order and exact minimum-degree floor.
+- All 362,879 vertex permutations for all 36 graph/radius pairs through M=8.
+  This separate direct evaluator uses no folded-order or degree-bound pruning.
+- 651 circular layouts through n=16, one representative for each radius and
+  eliminated-arc length. Literal graph vertex elimination independently checks
+  the new path-power-plus-end-clique support identification and folded order.
+- Nine invalid-input rejections and four semantic controls for the old order,
+  an incorrect `2w-1` cap, omitted clique fill, and saturation at M-1.
+
+These are finite corroboration of the new theorem. No numeric matrix census,
+predecessor reproduction, physical schedule, benchmark or full selected replay
+is claimed. The all-size claim rests on the written proof. The selected
+conditional kappa remains 0.00302015.
+
+## Scope and source closure
+
+The negative host is H=I-E with zero diagonal in E, strictly positive entries
+at every circular distance from one through w, zero entries elsewhere, and
+row sums less than one. This guarantees connected positive inverse fill and
+prevents cancellation. Arbitrary invertible arc pivots need only the stated
+support condition for the upper bound. Signed or missing couplings do not
+inherit the sharp lower bound.
+
+The original `uniform-transfer-audit` card is explicitly changed to this
+ordering theorem, following another contributor's open question. It is a local
+interface result, not an audit of #4100. Physical row and right-hand-side
+permutations, routing, restoration, multiple arcs, inverse norms, precision,
+tape access, compiler/hosting and complete supplier costs remain open. No
+supplier admission, new kappa or complete multiplication theorem is supplied.
+Independent human and formal proof-kernel review are unclaimed.
+
+Base canonical main is `624de9dc66858af0945e5f8a0942488d62280d43`, priority
+revision 7. [SOURCES.json](SOURCES.json) pins historical task/selected provenance
+and the exact credited predecessor notes. No external executable or data input
+is required by the new verifier. The selected-source metadata orientation
+passed; it was not the selected scientific cold replay.
+
+Entry overlap used live open PRs, this account's recent submissions, current
+handoffs, local question locks, distinctive all-main README searches and merged
+PR searches. The cached card scan reported sparse-note omissions. Arbitrary
+diffs and unpublished work remain outside coverage; no-match searches do not
+establish novelty. [The claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19134026)
+preceded the substantive work. Research stops at this first proved result.
+
+## Verification design
+
+Build the Lever led to a rerunnable ordering and exhaustive optimum checker.
+Prove It Works led to independent direct permutation evaluation and literal
+circular graph elimination. Power of Ten bounds graph size at 96 vertices,
+permutation enumeration at eight, and circular elimination at sixteen. Every
+loop has a bound from those constants; functions remain below 60 lines;
+rejection checks remain active under optimization. Python's managed allocation
+is a documented deviation from fixed allocation: one graph has at most 4,560
+edge tuples, the literal adjacency table has at most 256 booleans, and brute
+orders are streamed. Package source files are fixed local inputs. Python's
+allocator and standard-library internals are outside inspection. There is no
+recursion, dynamic code generation, shared mutable state or native dependency.
+Warning-strict Python and the repository metadata/publication checks are the
+available diagnostics; no separate linter is installed in the supplied venv.
+
+## Open next questions
+
+Can the folded order be realized in one actual circular Gaussian boundary
+solve within its complete paid routing allowance? First bind both permutation
+directions, all right-hand sides and eventual restoration in a literal caller.
+This matters because a smaller algebraic band does not pay for moving data.
+No physical conversion or complete caller is constructed here.
+
+Which multiple-arc elimination layouts retain an O(w) optimal linear bandwidth?
+First specify a separation rule and derive the survivor support. This matters
+because merged eliminated components can create larger cliques. The present
+one-arc theorem does not decide that case. Structured versions of both questions
+are in [TASK.json](TASK.json).
+
+## Credit
+
+This contribution is produced by Nick Petalas. James Reed / jwr404's #4289,
+following #4286, supplies the circular-arc sign/support argument and the explicit
+open reordering question. Cinna Davis's #4100 supplies the Gaussian boundary
+motivation. unpaidmoon's #4373 and Ryanson Jonathan's #4407 address linear
+separated carves and support fill; their `2w-1` constant has different
+hypotheses. Their source files and credit lines are unchanged. Apache-2.0.

research/cycle-schur-optimal-order/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "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/equal-weight-cycle-diameter/README.md",
+      "usage": "provenance",
+      "git_blob": "2f7c1c001caa12a26fcdafd0f060f9cbeb210502",
+      "sha256": "c41e951fa788783c522a2c223a850534b0a86ff04c60690409d1eb658f86a130"
+    },
+    {
+      "path": "research/gaussian-carve-schur-bandwidth/README.md",
+      "usage": "provenance",
+      "git_blob": "cebb6a30cc0859822dd256dee78f54ca97fa238d",
+      "sha256": "31b2930d6c140c526ff2fe0a68216b1ff17d22df9ef4a3c518079037e86b232a"
+    },
+    {
+      "path": "research/carve-schur-bandwidth-census/README.md",
+      "usage": "provenance",
+      "git_blob": "525387652dfb847f05b76d3e98aea653ee35749e",
+      "sha256": "e95963d7bcae7c052ddb16d086f6405b8aaee628930528d6799cc965d85b8dc9"
+    }
+  ]
+}

research/cycle-schur-optimal-order/TASK.json

@@ -0,0 +1,81 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "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": "changed",
+  "actual_scope": "Exact minimum linear-order Schur half-bandwidth after one nonempty proper circular arc: min(M-1,2w).",
+  "scope_change_reason": "Original all-size caller-audit card changed to an original graph/order theorem answering the survivor-reordering question in another contributor's PR4289. No predecessor replay or audit is the deliverable.",
+  "bottleneck_link": "A circular-distance fill can grow with arc length; an explicit simultaneous permutation restores a sharp O(w) linear band. Physical permutation cost and actual Gaussian caller integration remain unknown.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first proved optimal order and bounded exact corroboration; do not extend to multiple arcs or a physical implementation.",
+  "outcome": "completed",
+  "evidence": "PROOF.md and the source-hash-bound runtime receipt emitted by verify.py.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can the folded order be realized in one actual circular Gaussian boundary solve within its paid routing allowance?",
+      "why_it_matters": "An algebraic bandwidth improvement does not pay for rearranging the data.",
+      "first_step": "Choose one literal caller, bind both permutation directions and all right-hand sides, then price their complete movement and restoration.",
+      "blocked_by": "No physical order conversion or complete caller is supplied here."
+    },
+    {
+      "question": "Which multiple-arc elimination layouts retain an O(w) optimal linear bandwidth?",
+      "why_it_matters": "Merged eliminated components may create larger survivor cliques.",
+      "first_step": "Specify a separation rule and derive its exact survivor support before searching for an order.",
+      "blocked_by": "The present theorem has exactly one eliminated arc."
+    }
+  ],
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19134026"
+}

research/cycle-schur-optimal-order/VERIFY.json

@@ -0,0 +1,32 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 180,
+      "checks": "Exact folded orders and degree floors through M=96; every permutation through M=8; independent circular graph elimination through n=16; invalid-input and semantic controls; source-hash-bound receipt."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 180,
+      "checks": "Exact folded orders and degree floors through M=96; every permutation through M=8; independent circular graph elimination through n=16; invalid-input and semantic controls; source-hash-bound receipt."
+    }
+  ]
+}